/****************************************************************************
PNS.C
Written in 2008-2011 by M. V. Iordache. 
****************************************************************************/

#include"pns.h"
#include"matrixmath.h"
#include"insert.h"

void d2dd(const matrix* D, matrix* Dm, matrix* Dp) {
  int i, j, nr, nc;
  mtype x;

  nr = NumberOfRows(*D);
  nc = NumberOfColumns(*D);

  if(!D || !Dm || !Dp) {
    merror(0, "D2DD: one of the parameters has zero address.");
    return; 
  }

  if(nc <= 0 || nr <= 0) {
    merror(0, "D2DD: Wrong dimensions of D: %d x %d", D->nr, D->nc);
    return;
  }

  if((nr != NumberOfRows(*Dm)) || (nc != NumberOfColumns(*Dm)) ||	\
     (nr != NumberOfRows(*Dp)) || (nc != NumberOfColumns(*Dp))) {
    merror(0, "D2DD: One or more parameters have wrong dimensions");
    return;
  }
  for(i = 0; i < nr; i++)
    for(j = 0; j < nc; j++) {
      x = GetMatrixEl(D, i, j);
      if(x < 0)
	SetMatrixEl(Dm, i, j, -x);
      else if(x > 0)
	SetMatrixEl(Dp, i, j, x); 
    }
}


pns getpn(matrix* Dm, matrix* Dp, int* Tuc, int* Tuo, int* m0, int* C) {

  matrix mDm, mDp;
  pns pn;

  if(!Dm && !Dp) {
    merror(0, "GETPN: Both Dm and Dn are zero."); return pn;
  }
 
  if(!Dp) { /* In SPNBOX it is possible to call getpn(D) */
    d2dd(Dm, &mDm, &mDp);
    pn = createpn("mDm mDp Tuc Tuo m0 C", mDm, mDp, Tuc, Tuo, m0, C);
    DeallocateMatrix(&mDm);
    DeallocateMatrix(&mDp);
  }
  else 
    return createpn("mDm mDp Tuc Tuo m0 C", Dm, Dp, Tuc, Tuo, m0, C);

  return pn;
}

void _updatepn(pns* pn, const char *str, va_list param);


pns createpn(const char *str, ...) {
  pns pn;
  va_list param;
  char* s;
  char opt[] = "zero "; /* to set first the pn to zero */

  s = tmalloc((1+strlen(str)+strlen(opt))*sizeof(char));
  strcpy(s, opt);
  strcat(s, str);

  /* Do the initializations */

  va_start(param, str);
  _updatepn(&pn, s, param);
  va_end(param);

  free(s);

  return pn;
}


void updatepn(pns* pn, const char *str, ...) {
  va_list param;

  va_start(param, str);
  _updatepn(pn, str, param);
  va_end(param);
}


/* Subroutines of _updatepn */

void inline allocate_matrices(pns* pn) {
  if(!(pn->pnum) || !(pn->tnum))
    return;
  if(pn->in.nr !=pn->pnum || pn->in.nc !=pn->tnum)/*if not already allocated*/
    AllocateMatrixType(3, &(pn->in), pn->pnum, pn->tnum);
  if(pn->out.nr != pn->pnum || pn->out.nc != pn->tnum)
    AllocateMatrixType(3, &(pn->out), pn->pnum, pn->tnum);
}

void ptNumCheck(pns *pn, int m, int n) {
  if(m < 0) 
    merror(0, "_UPDATEPN: Request for %d places!", m);
  if(n < 0)
    merror(0, "_UPDATEPN: Request for %d places!", n);
  if(!pn->pnum && !pn->tnum) {  /* If the pn has not been yet initialized */
    pn->pnum = m;
    pn->tnum = n;
    allocate_matrices(pn);
  }
  else {
    if (pn->pnum != m)
      merror(0, "_UPDATEPN: Request to change from %d to %d the number of places", pn->pnum, m); 
    if (pn->tnum != n)
      merror(0, "_UPDATEPN: Request to change from %d to %d the number of transitions", pn->tnum, n); 
  }
}


void pCheck(pns *pn, char* s) {
  int i,j;
  char *p;
  if(!pn->pnum) {
    merror(0,"SETPN: Parameter '%s' requires at least one place",s); 
    return;
  }
  if(!pn->p) { /* Allocate t if not already allocated */
    pn->p = tmalloc(sizeof(PlaceInfo)*pn->pnum);
    for(i = 0; i < pn->pnum; i++) {
      p = (char*)&(pn->p[i]);
      for(j = 0; j <= sizeof(PlaceInfo)-sizeof(char); j++) 
	*(p+j) = 0; 
    }
  }
}


void tCheck(pns *pn, char* s) {
  int i,j;
  char *p;
  if(!pn->tnum) {
    merror(0,"SETPN: Parameter '%s' requires at least one transition",s); 
    return;
  }
  if(!pn->t) { /* Allocate t if not already allocated */
    pn->t = tmalloc(sizeof(TransInfo)*pn->tnum);
    for(i = 0; i < pn->tnum; i++) {
      p = (char*)&(pn->t[i]);
      for(j = 0; j <= sizeof(TransInfo)-sizeof(char); j++) 
	*(p+j) = 0; 
    }
  }
}

void dealloc_arcs(arcs *pa) {
  arcs *p, *p2;
  struct placelist *pl, *pl2;

  if(!pa)
    return;
  for(p = pa; p; ) {
    dealloc_cblock(&(p->condition));
    for(pl = p->out_places; pl; ) {
      pl2 = pl;
      pl = pl->next;
      free(pl2);
    }
    p2 = p;
    p = p->next;
    free(p2);
  }
}

void inclArcs(pns* pn, int t, arcs* p_arc) {
  arcs* pa, *p, *padst;
  struct placelist* pl;
  int i;

  if(!p_arc) { /* Remove all transition arcs of t */
    if(pn->arc_list)
      if(pn->arc_list[t]) {
	dealloc_arcs(pn->arc_list[t]);
	pn->arc_list[t] = 0;
      }
    MakeZeroColumn(&(pn->out), t);
    MakeZeroColumn(&(pn->in), t);
    return;
  } 
  if(!pn->arc_list)
    pn->arc_list = tcalloc(pn->tnum, sizeof(pn->arc_list[0]));

  /* Next, place arcs in arc_list and update the input & output matrices. */

  /* The following loop places the arcs in increasing order of the in_place field. */

  for(pa = p_arc; pa; ) { 
    if(!pn->arc_list[t]) { 
      pn->arc_list[t] = pa;
      pa = pa->next;
      pn->arc_list[t]->next = 0;
      continue;
    }
    if(pa->in_place <= pn->arc_list[t]->in_place) { /* insert at the beginning */
      p = pn->arc_list[t]; 
      pn->arc_list[t] = pa;
      pa = pa->next;
      pn->arc_list[t]->next = p;
      continue;
    }
    for(padst = pn->arc_list[t]; padst; padst = padst->next) {
      if(padst->next)
	if(pa->in_place > padst->next->in_place)
	  continue;
      p = padst->next; /* the line is reached if padst->next == 0 or 
			  pa->in_place <= padst->next->in_place */
      padst->next = pa;
      pa = pa->next;
      padst->next->next = p;
      break;
    }
  }

  /* Update the input and output matrices */

  MakeZeroColumn(&(pn->out), t);
  MakeZeroColumn(&(pn->in), t);
  for(pa = pn->arc_list[t]; pa; pa = pa->next) {
    if(pa->in_place >= 0) { /* write to the output matrix */
      i = 1 + GetMatrixEl(&(pn->out), pa->in_place, t);
      SetMatrixEl(&(pn->out), pa->in_place, t, i);
    }
    for(pl = pa->out_places; pl; pl = pl->next) { /* write to the input matrix */
      i = 1 + GetMatrixEl(&(pn->in), pl->place, t);
      SetMatrixEl(&(pn->in), pl->place, t, i);
    }
  }
}


void inclString(char*** pstr, int index, char* p, int num) {
  if(!num || index >= num || index < 0)
    merror(0, "SETPN: Attempt to describe undefined places or transitions");
  if(!*pstr)
    *pstr = tcalloc(num, sizeof(**pstr));
  if((*pstr)[index]) {
    free((*pstr)[index]);
    (*pstr)[index] = 0;
  }
  if(!p)
    p = "";
  if(!strlen(p))
    return;
  (*pstr)[index] = tcalloc(strlen(p)+1, sizeof(*p));
  strcpy((*pstr)[index], p);
}


void inclCblock(cblock** pstr, int index, int line, char* p, int num) {
  if(!num || index >= num || index < 0)
    merror(0, "SETPN: Attempt to describe undefined places or transitions");
  if(!*pstr)
    *pstr = tcalloc(num, sizeof(**pstr));
  if((*pstr)[index].text) {
    free((*pstr)[index].text);
    (*pstr)[index].text = 0;
  }
  (*pstr)[index].line = line;
  if(!p)
    p = "";
  if(!strlen(p))
    return;
  (*pstr)[index].text = tcalloc(strlen(p)+1, sizeof(*p));
  strcpy((*pstr)[index].text, p);
}


void _updatepn(pns* pn, const char *str, va_list param) {
  arcs* p_arc;
  char *sdest, *p;
  int i, j, count, m, n, **ar, *ip, m0, n0;
  matrix d, dm, dp;

  m0 = pn->pnum;
  n0 = pn->tnum;

  if(!pn || !str)  {
    merror(0, "SETPN: First two parameters must be nonzero.");
    return; 
  }

  sdest = tmalloc(sizeof(char)*(strlen(str)+1));

  for(count = 0; str[count]; count++) {
    if(str[count] == ' ' || str[count] == '\t') 
      continue;

    if(sscanf(str+count, "%s", sdest) < 0) {
      merror(0, "SETPN could not scan this input: \"%s\".", str); return; }

    /* Advance count to the next field */
    count++;
    for(; str[count] != ' ' && str[count] != '\t' && str[count]; count++);
    count--; 

    if(!strcmp(sdest,"arcs") || !strcmp(sdest,"arc")) {
      i = va_arg(param, int);
      p_arc = va_arg(param, arcs*);
      inclArcs(pn, i, p_arc);
    }
    else if(!strcmp(sdest,"D") || !strcmp(sdest,"pD")) {
      if(!pn->pnum || !pn->tnum) {
	merror(0,"SETPN: The D parameter applies to PNs with at least one place and one transition!"); return;
      }
      if(!strcmp(sdest,"pD")) {
	ar = va_arg(param, int**);
	if(!ar) {	
	  merror(0,"SETPN: The option pD = 0 is not implemented"); return;
	}
	d = array2matrix(ar, pn->pnum, pn->tnum);
      }
      else { /* the case "D" */
	ip = va_arg(param, int*);
	if(!ip) {	
	  merror(0,"SETPN: The option D = 0 is not implemented"); return;
	}
	d = vector2matrix(ip, pn->pnum, pn->tnum);
      }
      d2dd(&d, &(pn->out), &(pn->in));
      DeallocateMatrix(&d);
    }
    else if(!strcmp(sdest,"Dm")|| !strcmp(sdest,"O")|| !strcmp(sdest,"pDm")) {
      if(!pn->pnum || !pn->tnum) {
	merror(0,"SETPN: The Dm parameter applies to PNs with at least one place and one transition!"); return;
      }
      if(!strcmp(sdest,"pDm")) {
	ar = va_arg(param, int**);
	if(!ar) {	
	  merror(0,"SETPN: The option pDm = 0 is not implemented"); return;
	}
	dm = array2matrix(ar, pn->pnum, pn->tnum);
      }
      else {
	ip = va_arg(param, int*);
	if(!ip) {	
	  merror(0,"SETPN: The option Dm = 0 is not implemented"); return;
	}
	dm = vector2matrix(ip, pn->pnum, pn->tnum);
      }
      CopyMatrix(&dm, &(pn->out));
      DeallocateMatrix(&dm);
    }
    else if(!strcmp(sdest,"Dp")|| !strcmp(sdest,"I")|| !strcmp(sdest,"pDp")) {
      if(!pn->pnum || !pn->tnum) {
	merror(0,"SETPN: The Dp parameter applies to PNs with at least one place and one transition!"); return;
      }
      if(!strcmp(sdest,"pDp")) {
	ar = va_arg(param, int**);
	if(!ar) {	
	  merror(0,"SETPN: The option pDp = 0 is not implemented"); return;
	}
	dp = array2matrix(ar, pn->pnum, pn->tnum);
      }
      else {
	ip = va_arg(param, int*);
	if(!ip) {	
	  merror(0,"SETPN: The option Dp = 0 is not implemented"); return;
	}
	dp = vector2matrix(ip, pn->pnum, pn->tnum);
      }
      CopyMatrix(&dp, &(pn->in));
      DeallocateMatrix(&dp);
    }
    else if(!strcmp(sdest,"mD")) {
      d = va_arg(param, matrix);
      m = NumberOfRows(d);
      n = NumberOfColumns(d);
      ptNumCheck(pn, m, n); /*If uninitialized, pnum and tnum become m and n.*/
            /* If m and n are nonzero, pn->in,out are allocated if necessary.*/
      d2dd(&d, &(pn->out), &(pn->in));
    }
    else if(!strcmp(sdest,"mDm")) {
      d = va_arg(param, matrix);
      m = NumberOfRows(d);
      n = NumberOfColumns(d);
      ptNumCheck(pn, m, n); /*If uninitialized, pnum and tnum become m  and n*/
      CopyMatrix(&d, &(pn->out));
    }
    else if(!strcmp(sdest,"mDp")) {
      d = va_arg(param, matrix);
      m = NumberOfRows(d);
      n = NumberOfColumns(d);
      ptNumCheck(pn, m, n); /*If uninitialized, pnum and tnum become m  and n*/
      CopyMatrix(&d, &(pn->in)); 
    }
    else if(!strcmp(sdest,"C")) {
      ip = va_arg(param, int*);
      if(!ip) {
	if(pn->C)
	  free(pn->C);
	pn->C = 0;
      } 
      else {
	if(!pn->pnum) {
	  merror(0,"SETPN: Parameter 'C' requires at least one place");
	  return;
	}
	if(!pn->C)  /* Allocate C */
	  pn->C = tmalloc(sizeof(int)*pn->pnum);
	for(i = 0; i < pn->pnum; i++)
	  pn->C[i] = ip[i];
      }
    }
    else if(!strcmp(sdest,"m0")) {
      ip = va_arg(param, int*);
      if(!ip) {
	if(pn->marking)
	  free(pn->marking);
	pn->marking = 0;
      } 
      else {
	if(!pn->pnum) {
	  merror(0,"SETPN: Parameter 'm0' requires at least one place");
	  return;
	}
	if(!pn->marking)  /* Allocate marking */
	  pn->marking = tmalloc(sizeof(int)*pn->pnum);
	for(i = 0; i < pn->pnum; i++)
	  pn->marking[i] = ip[i];
      }
    }
    else if(!strcmp(sdest,"label") || !strcmp(sdest,"labels")) {
      ip = va_arg(param, int*);
      tCheck(pn, sdest); /* also allocates pn->t, if necessary */
      if(ip)
	for (i = 0; i < pn->tnum; i++)
	  pn->t[i].l = ip[i];
    }
    else if(!strcmp(sdest,"freelabel")) {
      ip = va_arg(param, int*);
      tCheck(pn, sdest); /* also allocates pn->t, if necessary */
      if(ip)
	for (i = 0; i < pn->tnum; i++)
	  if(!pn->t[i].l) /* do not change existing labels */
	    pn->t[i].l = --*ip;
    }
    else if(!strcmp(sdest,"Tuc")) {
      ip = va_arg(param, int*);
      tCheck(pn, "Tuc"); /* also allocates pn->t, if necessary */
      if(ip)
	for (i = 0; i < pn->tnum; i++)
	  pn->t[i].uncontrollable = ip[i];
    }
    else if(!strcmp(sdest,"Tuo")) {
      ip = va_arg(param, int*);
      tCheck(pn, "Tuo"); /* also allocates pn->t, if necessary */
      if(ip)
	for (i = 0; i < pn->tnum; i++)
	  pn->t[i].unobservable = ip[i];
    }
    else if(!strcmp(sdest,"live")) {
      i = va_arg(param, int);
      tCheck(pn, "live"); /* also allocates pn->t, if necessary */
      pn->t[i].live = 1;
    }
    else if(!strcmp(sdest,"nondeterministic")) {
      i = va_arg(param, int);
      pCheck(pn, "nondeterministic"); /* also allocates pn->t, if necessary */
      pn->p[i].nondeterministic = 1;
    }
    else if(!strcmp(sdest,"uncontrollable")) {
      i = va_arg(param, int);
      tCheck(pn, "uncontrollable"); /* also allocates pn->t, if necessary */
      pn->t[i].uncontrollable = 1;
    }
    else if(!strcmp(sdest,"unobservable")) {
      i = va_arg(param, int);
      tCheck(pn, "unobservable"); /* also allocates pn->t, if necessary */
      pn->t[i].unobservable = 1;
    }
    else if(!strcmp(sdest, "place_name")) {
      i = va_arg(param, int);
      p = va_arg(param, char*);
      inclString(&(pn->place_name), i, p, pn->pnum);
    }
    else if(!strcmp(sdest, "segment")) {
      i = va_arg(param, int);
      j = va_arg(param, int);
      p = va_arg(param, char*);
      inclCblock(&(pn->segment), i, j, p, pn->pnum);
    }    
    else if(!strcmp(sdest, "select")) {
      i = va_arg(param, int);
      j = va_arg(param, int);
      p = va_arg(param, char*);
      inclCblock(&(pn->select), i, j, p, pn->pnum);
    }    
    else if(!strcmp(sdest, "trans_name")||!strcmp(sdest, "transition_name")){
      i = va_arg(param, int);
      p = va_arg(param, char*);
      inclString(&(pn->trans_name), i, p, pn->tnum);
    }
    else if(!strcmp(sdest,"pnum")) {
      m = va_arg(param, int);
      if( (m0 || n0) && pn->pnum != m) { 
        merror(0,"SETPN: Attempt to change the number of places from %d to %d",pn->pnum,m); 
        return; }
      else {
	pn->pnum = m;
	allocate_matrices(pn);/* the input and output matrices, if necessary */
      }
    }
    else if(!strcmp(sdest,"tnum")) {
      m = va_arg(param, int);
      if( (m0 || n0) && pn->tnum != m) { 
        merror(0,"SETPN: Attempt to change the number of transitions from %d to %d",pn->tnum,m); 
        return; }
      else {
	pn->tnum = m;
	allocate_matrices(pn);/* the input and output matrices, if necessary */
      }
    }
    else if(!strcmp(sdest,"zero")) {  /* initialize pn to zero */
      /* for( i = 0, p = (char*)pn; i <= sizeof(pns)-sizeof(char); i++) 
       *(p+i) = 0; */
      memset(pn, 0, sizeof(pns));
      m0 = pn->pnum;
      n0 = pn->tnum;
    }
    else { /* ERROR */
      merror(0, "_UPDATEPN: The option \"%s\" is unimplemented", sdest);
      return;
    }
  }
  free(sdest);

  return;
}



inline pns _copytrans(pns dst, pns *src) {
  /* This is a subroutine of copypn and composepn for copying transitions
     and arcs from src to dst. */

  int i;
  arcs *pa; const arcs *pb;
  struct placelist *pd; const struct placelist *ps;

  if(src->t) {
    dst.t = tcalloc(src->tnum, sizeof(src->t[0]));
    memcpy(dst.t, src->t, (src->tnum)*sizeof(src->t[0]));
  }
  if(src->arc_list) { /* copy the list of arcs */
    dst.arc_list = tcalloc(dst.tnum, sizeof(*(dst.arc_list)));
    for(i = 0; i < src->tnum; i++) {
      if(src->arc_list[i]) {
	dst.arc_list[i] = tmalloc(sizeof(*(dst.arc_list[0])));
	for(pa = dst.arc_list[i], pb = src->arc_list[i]; pa; pa = pa->next) {
	  *pa = *pb;
	  pa->condition = pb->condition;
	  if(pb->condition.text) {
	    pa->condition.text = tmalloc(sizeof(char)*(strlen(pb->condition.text) + 1));
	    strcpy(pa->condition.text, pb->condition.text);
	  }
	  pa->condition.file = 0; // the file field is currently not used
	  if(pb->out_places) { /* copy out_places */
	    pa->out_places = tmalloc(sizeof(*(pa->out_places)));
	    for(pd = pa->out_places, ps = pb->out_places; pd; pd = pd->next) {
	      *pd = *ps;
	      ps = ps->next;
	      if(ps) /* else, pd->next is already 0 (because of *pd = *ps) */
		pd->next = tmalloc(sizeof(*pd));
	    }
	  }
	  pb = pb->next;
	  if(pb)
	    pa->next = tmalloc(sizeof(*pa)); /* else, pa->next already 0 */
	}
      }
    }
  }

  return dst;
}


pns copypn(pns *src) {
  pns dst;
  int i;

  dst = createpn("pnum tnum mDm mDp", src->pnum, src->tnum, src->out, src->in);
  if(src->marking)  updatepn(&dst, "m0", src->marking);
  if(src->C)        updatepn(&dst, "C", src->C);
  if(src->place_name) 
    for(i = 0; i < src->pnum; i++)
      if(src->place_name[i])
	updatepn(&dst, "place_name", i, src->place_name[i]);
  if(src->segment)
    for(i = 0; i < src->pnum; i++)
      if(src->segment[i].text)
	updatepn(&dst,"segment",i, src->segment[i].line, src->segment[i].text);
  if(src->select)
    for(i = 0; i < src->pnum; i++)
      if(src->select[i].text)
	updatepn(&dst, "select", i, src->select[i].line, src->select[i].text);
  if(src->trans_name)
    for(i = 0; i < src->tnum; i++)
      if(src->trans_name[i])
	updatepn(&dst, "trans_name", i, src->trans_name[i]);
  if(src->p) {
    dst.p = tcalloc(dst.pnum, sizeof(src->p[0]));
    for(i = 0; i < src->pnum; i++)
      dst.p[i] = src->p[i];
  }
  return _copytrans(dst, src);
}



void deallocpn(pns *pn) {
  int i, pnum, tnum;
  pnum = pn->pnum;
  tnum = pn->tnum;
  struct placelist *p, *q;

  if(pnum) {
    if(pn->marking)
      free(pn->marking);
    if(pn->C)
      free(pn->C);
    if(pn->p)
      free(pn->p);
    if(pn->place_name) {
      for(i = 0; i < pnum; i++)
	if(pn->place_name[i])
	  free(pn->place_name[i]);
      free(pn->place_name);
    }
    if(pn->segment) {
      for(i = 0; i < pnum; i++)
	dealloc_cblock((pn->segment)+i);
      free(pn->segment);
    }
    if(pn->select) {
      for(i = 0; i < pnum; i++)
	dealloc_cblock((pn->select)+i);
      free(pn->select);
    }
  }

  if(tnum) {
    if(pn->t)
      free(pn->t);
    if(pn->trans_name) {
      for(i = 0; i < tnum; i++)
	if(pn->trans_name[i])
	  free(pn->trans_name[i]);
      free(pn->trans_name);
    }
    if(pn->arc_list) {
      for(i = 0; i < tnum; i++)
	dealloc_arcs(pn->arc_list[i]);
      free(pn->arc_list);
    }
  }

  if(pn->in.type)
    DeallocateMatrix(&(pn->in));
  if(pn->out.type)
    DeallocateMatrix(&(pn->out));

  memset(pn, 0, sizeof(*pn)); 
  // Avoids segmentation fault if deallocpn is called again with the same parameter.

}


void dealloc_cblock(cblock *p) {
  if(p->text)
    free(p->text);
  if(p->file)
    free(p->file);
}


void dealloc_specs(specs* sp) {
  int i;
  if(sp->name)
    free(sp->name);
  if(sp->pn_num && sp->pn_array) {
    for(i = 0; i < sp->pn_num; i++) 
      deallocpn(sp->pn_array[i]);
    free(sp->pn_array);
  }
  if(sp->synclist)
    dealloc_synclist(sp->synclist);
  if(sp->constraint_list)
    dealloc_constraint(sp->constraint_list);
  if(sp->process_num && sp->process_array) {
    for(i = 0; i < sp->process_num; i++)
      dealloc_process(sp->process_array[i]);
    free(sp->process_array);
  }
  dealloc_cblock(&(sp->include));
  dealloc_cblock(&(sp->main));
  if(sp->sbuildparam)
    free(sp->sbuildparam);
}


void dealloc_synclist(syncc* s) {
  syncc *s1, *s2;

  for(s1 = s; s1; ) {
    s2 = s1->next;
    free(s1);
    s1 = s2;
  }
}

void dealloc_process(process* p) {
  if(p->file)
    free(p->file);
  if(p->name)
    free(p->name);
  if(p->instance)
    free(p->instance);
  if(p->build)
    free(p->build);
  dealloc_cblock(&(p->include));
  dealloc_cblock(&(p->main));
  if(p->dfns)
    free(p->dfns);
  if(p->pn) {
    deallocpn(p->pn);
    free(p->pn);
  }
}


void dealloc_constraint(constraint* c) {
  constraint *c1, *c2;

  for(c1 = c; c1; ) {
    c2 = c1->next;
    dealloc_expression(c1->expr);
    free(c1);
    c1 = c2;
  }
}

void dealloc_variable(variable* v) {
  variable *v1, *v2;

  for(v1 = v; v1; ) {
    v2 = v1->next;
    free(v1);
    v1 = v2;
  }
}

void dealloc_expression(expression* e) {

  if(e->left_expr)
    dealloc_expression(e->left_expr);
  if(e->right_expr)
    dealloc_expression(e->right_expr);
  if(e->left_ineq)
    dealloc_inequality(e->left_ineq);
  if(e->right_ineq)
    dealloc_inequality(e->right_ineq);
  free(e);
}

void dealloc_inequality(inequality* in) {
  if(in->variable_list)
    dealloc_variable(in->variable_list);
  free(in);
}


void dealloc_tarray(struct tarray* p) {
  if(p) { 
    sfree(&(p->mem));
    if(p->T) 
      free(p->T); 
    free(p); 
  } 
}


void dealloc_cpinfo(struct cpinfo* p) {
  if(p) {
    if(p->T)
      dealloc_tarray(p->T);
    if(p->P)
      dealloc_tarray(p->P);
    free(p);
  }
}


/***************************************************************************
 COMPOSEPN
****************************************************************************/


void inline insert_tranlist_sub(struct tranlist* where, pns* pn, int t,	\
				struct alloc* mem) {
  // subroutine of ComposePN; inserts a tranlist element in the chain such that
  // the pn fields in the chain are sorted in increasing order.

  struct tranlist *p, *q;

  if(!where->pn) { // this indicates an empty chain
    where->pn = pn;
    where->t = t;
    return;
  }

  p = smalloc(mem, sizeof(*p));

  if(pn < where->pn) { // if this must be the first chain element
    p->pn = where->pn;
    p->t = where->t;
    p->next = where->next;
    where->next = p;
    where->pn = pn;
    where->t = t;
    return;
  }
  p->pn = pn;
  p->t = t;
  for(q = where; q->next; q = q->next) {
    if(q->next->pn >= p->pn) { // insert p in chain
      p->next = q->next;
      q->next = p;
      return;
    }
  }
  q->next = p; // line reached if p must be at the end of the chain
  p->next = 0; // smalloc does not initialize memory to 0 when it allocates p
}


void inline insert_tranlist(struct tranlist* where, struct tranlist* what, \
			    struct alloc* mem) {
  // subroutine of ComposePN; inserts a tranlist element in the chain such that
  // the pn fields in the chain are sorted in increasing order.

  insert_tranlist_sub(where, what->pn, what->t, mem);
}


void update_TR(int i, int i1, int i2, struct tarray *T1, struct tarray *T2, \
	       struct tarray *TR) {
  // This is a subroutine of ComposePN. Copies T1[i1] and T2[i2] to TR[i].
  //
  // Relies on TR->T having its elements initialized to zero (satisfied when
  // TR->T is allocated with (t)calloc. 

  struct tranlist *p;

  if(T1)
    if(T1->T) 
      for(p = (T1->T)+i1; p; p = p->next) 
	insert_tranlist((TR->T)+i, p, &(TR->mem));

  if(T2)
    if(T2->T) 
      for(p = (T2->T)+i2; p; p = p->next) 
	insert_tranlist((TR->T)+i, p, &(TR->mem));
}


void set_TR(pns* pn, struct cpinfo* I, struct cpinfo **IR) {
  // This is a subroutine of ComposePN and PNComposition. 
  // It is used to initialize IR based on pn and I.
  int nt, i;
  struct tranlist *TL, *p;
  struct tarray **TR, **PR, *T = 0, *P = 0;

  if(!IR)
    return;

  *IR = tcalloc(1, sizeof(**IR));
  TR = &((*IR)->T); PR = &((*IR)->P);
  if(I) {
    T = I->T; P = I->P;
  }

  *TR = tcalloc(1, sizeof(**TR)); *PR = tcalloc(1, sizeof(**PR));
  initalloc(&((*TR)->mem), 50*sizeof(*(*TR)->T)); 
  //initalloc(&((*PR)->mem), 50*sizeof(*(*PR)->T)); // this is not used
  TL = 0;
  if(!T) {
    nt = pn->tnum;
    if(nt) TL = tcalloc(nt, sizeof(*(*TR)->T));
    for(i = 0; i < nt; i++) {
      TL[i].pn = pn;
      TL[i].t = i;
    }
  }
  else { // This is the case T != 0
    nt = T->n;
    if(nt) TL = tcalloc(nt, sizeof(*(*TR)->T));
    for(i = 0; i < nt; i++) {
      TL[i].pn = T->T[i].pn;
      TL[i].t = T->T[i].t;
      for(p = T->T[i].next; p; p = p->next) 
	insert_tranlist(TL+i, p, &((*TR)->mem));
    } 
  }
  (*TR)->n = nt;
  (*TR)->T = TL;

  TL = 0;
  if(!P) {
    nt = pn->pnum;
    if(nt) TL = tcalloc(nt, sizeof(*(*PR)->T));
    for(i = 0; i < nt; i++) {
      TL[i].pn = pn;
      TL[i].t = i;
    }
  }
  else { // This is the case P != 0
    nt = T->n;
    if(nt) TL = tcalloc(nt, sizeof(*(*TR)->T));
    for(i = 0; i < nt; i++) {
      TL[i].pn = T->T[i].pn;
      TL[i].t = T->T[i].t;
    } 
  }
  (*PR)->n = nt;
  (*PR)->T = TL;
}


pns ComposePN(pns* pn1, pns* pn2, struct cpinfo* T1, struct cpinfo* T2,\
	      struct cpinfo **TR) {

/* Returns the parallel composition of pn1 and pn2.
   
   The remaining parameters are ignored when TR = 0. 

   The role of T1, T2, and TR is as follows. If TR != 0, then *TR is 
   initialized with a data object showing the origin of each 
   place and transition in terms of the PNs that are composed. Since
   pn1 and pn2 may themselves be compositions of other PNs, *TR
   is determined based on T1 and T2, which are data objects providing
   information about the origin of the places and transitions of pn1
   and pn2. If T1 = 0 and/or T2 = 0, default values for T1 and/or T2 
   are found and used to determine *TR. The meaning of the TR data
   is as follows:

   - TR->P->T[i] indicates the origin of the place i (the PN from which
     it comes and its index in that PN).

   - TR->T->T[i] indicates the transitions that were composed in order 
     to form the transition i of the composed PN. Note that TR->T->T[i] 
     is a chain in which each element describes one of the transitions
     that were composed. The description consists of the PN to which 
     the transition belongs and its index in that PN.

   T1 (T2) should be zero if pn1 (pn2) is not the result of previous 
   PN compositions. Otherwise, T1 and T2 may be set to the *TR of the 
   previous PN compositions. The function PNComposition provides an 
   example showing how to obtain TR when more than two PNs are composed. 
 */


  /* Algorithm of pn composition:
     - Create the vector "lcount". For all t of pn1 lcount(t) indicates how
       many times the label of t appears in pn2. For all t of pn2 lcount(t)
       is 1 if the label of t appears in pn1. Otherwise it is 0. 
     - Determine the size of the composed pn based on lcount;
     - Compose the pns based on lcount.
     The program does not assume nonempty sets of places and transitions. 
  */

  int *lcount, np, np1, np2, nt, nt1, nt2, i, j, k, z, label;
  char free_T1, free_T2;
  pns pn;
  struct tranlist *TL;

  if(!pn1 && !pn2) {
    memset(&pn, 0, sizeof(pn));
    if(TR) *TR = 0;
    return pn;
  }
  if(!pn1)  { set_TR(pn2, T2, TR); return copypn(pn2);}
  if(!pn2)  { set_TR(pn1, T1, TR); return copypn(pn1);}

  nt1 = pn1->tnum; /* determine the number of transitions */
  nt2 = pn2->tnum;  

  if(nt1+nt2)
    lcount = tcalloc(nt1+nt2, sizeof(*lcount)); 
    /* This also initializes the elements of lcount to zero. */

  /* The default value of lcount does not have to be changed when one of the
     two pns is not labeled. Otherwise, lcount is calculated as shown next. */

  if((pn1->t) && (pn2->t))  /* if labels assigned to both pns */
    for(i = 0; i < nt1 ; i++) 
      if(pn1->t[i].l)  /* zero label means no label, so lcount[i] stays 0 */
	for(j = 0; j < nt2; j++) 
	  if(pn1->t[i].l == pn2->t[j].l) {
	    lcount[i]++;
	    lcount[nt1+j] = 1;
	  }

  /* The following determines the size of the composed pn. */

  for(nt = 0, i = 0; i < nt1; i++) {
    if(lcount[i])
      nt += lcount[i];
    else
      nt++;
  }
  for(; i < nt1+nt2; i++) 
    if(!lcount[i])
      nt++;

  /* It is assumed here that the places of the two pns are distinct */
 
  np = pn1->pnum + pn2->pnum;
  np1 = pn1->pnum; np2 = pn2->pnum;

  /* Create the composed pn */

  pn = createpn("pnum tnum", np, nt);
  if(TR)  { // if TR is to be used, then allocate *TR
    *TR = tcalloc(1, sizeof(**TR));
    alloc_tarray((*TR)->T, nt);
    alloc_tarray((*TR)->P, nt);
  }

  /* Initialize the capacity and marking entries */

  if(pn1->C || pn2->C) {
    pn.C = tcalloc(np, sizeof(*(pn.C)));
    if(pn1->C)  for(i = 0; i < np1; pn.C[i] = pn1->C[i++]);
    if(pn2->C)  for(i = 0; i < np2; pn.C[i+np1] = pn2->C[i++]);
  }

  if(pn1->marking || pn2->marking) {
    pn.marking = tcalloc(np, sizeof(*(pn.marking)));
    if(pn1->marking) for(i = 0; i < np1; pn.marking[i] = pn1->marking[i++]);
    if(pn2->marking) for(i = 0; i < np2; pn.marking[i+np1]= pn2->marking[i++]);
  }

  /* Next we deal with the case when pn1 or pn2 does not have transitions */

  if(!nt1 || !nt2) {
    if(!nt1)  /* if pn1 does not have transitions */
      pn = _copytrans(pn, pn2); // copies transitions and trans arcs to pn
    else /* if pn2 does not have transitions */
      pn = _copytrans(pn, pn1);
    // Copy also input/output matrix elements
    for(j = 0; j < nt1; j++) 
      if(np1) {
	Copy2ZeroColumn(&(pn1->in),j,&(pn.in),j,0);
	Copy2ZeroColumn(&(pn1->out),j,&(pn.out),j,0);
      }
    for(j = 0; j < nt2; j++) 
      if(np2) {
	Copy2ZeroColumn(&(pn2->in),j,&(pn.in),j,np1);
	Copy2ZeroColumn(&(pn2->out),j,&(pn.out),j,np1);
      }
    if(TR) {
      if(nt1) set_TR(pn1, T1, TR); 
      if(nt2) set_TR(pn2, T2, TR);
    }
    return pn;
  }

  /* The remaining part of the code is for the case nt1 and nt2 nonzero;
     np1 and np2 are allowed to be zero. */

  free_T1 = !T1; free_T2 = !T2; // indicate whether T1 and T2 should be freed.
  if(free_T1) set_TR(pn1, 0, &T1); // determine T1
  if(free_T2) set_TR(pn2, 0, &T2); // determine T2 

  /* The incidence matrix of the composed pn has the form
        T1' T2'
     P1 XX  XX 
     P2 XX  XX

     where P1 is the set of places of pn1, P2 the set of places of pn2, T1' is 
     the set of transitions that either do not have a label of pn2 or 
     are obtained by composing transitions of pn1 and pn2, and T2' is the set 
     of transitions of pn2 that do not have a label of pn1. */

  /* (*TR)->P is found next */

  if(TR) {
    TL = 0;
    (*TR)->P = tcalloc(1, sizeof(*(*TR)->P));
    (*TR)->P->n = np; // the number of places of the composed PN
    if(np) TL = tcalloc(np, sizeof(*TL));
    for(i = 0; i < np1; i++) {
      TL[i].pn = T1->P->T[i].pn;
      TL[i].t  = T1->P->T[i].t;
    }
    for(i = 0 ; i < np2; i++) {
      TL[i + np1].pn = T2->P->T[i].pn;
      TL[i + np1].t  = T2->P->T[i].t;
    }
    (*TR)->P->T = TL;
  }

  /* Next the transitions of pn1 are considered */

  for(i = 0, z = 0; i < nt1; i++) { // lcount[i] != 0 only if both pns labeled
    if(lcount[i]) { /* pn2 has lcount[i] transitions with the same label */
      label = pn1->t[i].l;
      for(j = 0, k = 0; k < lcount[i]; j++) {
	if(label == pn2->t[j].l) { /*compose transitions with the same label*/
	  /* copy the column i of the input/output matrix of pn1 to the column 
	     z of the input/output matrix of pn */
	  if(np1) {
	    Copy2ZeroColumn(&(pn1->in),i,&(pn.in),z,0);
	    Copy2ZeroColumn(&(pn1->out),i,&(pn.out),z,0);
	  } 
	  /* now copy the column j of the input/output matrix of pn2; there is
             an offset of value pn1->pnum since the places of pn2 appear in pn 
             beginning with the position pn1->pnum. */
	  if(np2) {
	    Copy2ZeroColumn(&(pn2->in),j,&(pn.in),z,np1);
	    Copy2ZeroColumn(&(pn2->out),j,&(pn.out),z,np1); 
	  }
	  /* now copy the label and any other transition information */
	  if(!pn.t) /* allocate pn.t if not already allocated */
	    pn.t = tcalloc(pn.tnum,sizeof(pn.t[0]));/*elements initial. to 0*/
	  memcpy((pn.t)+z, (pn1->t)+i, sizeof(pn.t[0]));
	  pn.t[z].uncontrollable = pn1->t[i].uncontrollable | \
                                   pn2->t[j].uncontrollable;
	  pn.t[z].unobservable=pn1->t[i].unobservable | pn2->t[j].unobservable;
	  pn.t[z].live = pn1->t[i].live | pn2->t[j].live;
	  if(TR) update_TR(z, i, j, T1->T, T2->T, (*TR)->T);
	  z++; /* z: number of next empty column in the matrices of pn */
	  k++;
	}
      }
    }
    else { /* pn2 has no transitions with the same label */
      if(np1) {
        Copy2ZeroColumn(&(pn1->in),i,&(pn.in),z,0);
        Copy2ZeroColumn(&(pn1->out),i,&(pn.out),z,0); 
      }
      if(pn1->t) { /* copy also the transition information if any */
	if(!pn.t) /* allocate pn.t if not already allocated */
	  pn.t = tcalloc(pn.tnum,sizeof(pn.t[0]));/*elements initialized to 0*/
	memcpy((pn.t)+z, (pn1->t)+i, sizeof(pn.t[0]));
      }
      if(TR) update_TR(z, i, 0, T1->T, 0, (*TR)->T);
      z++;       
    }
  }

  /* Next the transitions of pn2 are considered. Only the transitions that
     do not have labels in pn1 remain to be considered. */

  for(j = 0; j < nt2; j++) 
    if(!lcount[j+nt1]) {
      if(np2) {
        Copy2ZeroColumn(&(pn2->in),j,&(pn.in),z,np1);
        Copy2ZeroColumn(&(pn2->out),j,&(pn.out),z,np1);
      } 
      if(pn2->t) { /* copy also the transition information if any */
	if(!pn.t) /* allocate pn.t if not already allocated */
	  pn.t = tcalloc(pn.tnum,sizeof(pn.t[0]));/*elements initialized to 0*/
	memcpy((pn.t)+z, (pn2->t)+j, sizeof(pn.t[0]));
      }
      if(TR) update_TR(z, 0, j, 0, T2->T, (*TR)->T);
      z++; 
    }
  
  free(lcount);
  if(free_T1) dealloc_cpinfo(T1);
  if(free_T2) dealloc_cpinfo(T2);

  return pn;
}



pns PNComposition(process** process_array, int num, struct cpinfo **TR) {
  /* Composes the PNs in the process array and returns the result. */
  pns pn, pn1, *apn;
  int i;
  struct cpinfo *T;

  if(num <= 0 || !process_array) {
    memset(&pn, 0, sizeof(pn)); // return null pn
    if(TR) *TR = 0;
    return pn;
  }
  else if(num == 1) {
    pn = copypn(process_array[0]->pn);
    if(TR) set_TR(process_array[0]->pn, 0, TR);
    return pn;
  }

  apn = process_array[0]->pn;
  for(i = 1, T = 0; i < num; i++) {
    if(i > 1) {
      pn1 = pn; // save intermediary result for subsequent deallocation
      apn = &pn1;
      if(TR) 
	T = *TR;
    }
    pn = ComposePN(apn, process_array[i]->pn, T, 0, TR);
    if(i > 1)
      deallocpn(&pn1); // free intermediary result
    if(T)
      dealloc_cpinfo(T);
  }

  return pn;
}



int isfreelabeled(pns *rpn) {
  int i, j, label;

  if(rpn->t)
    for(i = 0; i < rpn->tnum; i++) {
      label = rpn->t[i].l;
      for(j = i+1; j < rpn->tnum; j++) 
	if(label == rpn->t[j].l)
	  return 0;
    }
  return 1;
}


inline int nextmarking(pns *pn, int* m1, int t, int* m2) {
  /* If m1[t, then m2 is initialized such that m1[t>m2 and 1 is returned. 
     Otherwise, 0 is returned. */
  int pnum, i, j;
  matrix *out, *in;
  MatrElem *inx, *outx;

  pnum = pn->pnum;
  out = &(pn->out);
  in = &(pn->in);

  if(in->type != 3 || out->type != 3 || in->trans || out->trans) {
    merror(0, "NEXTMARKING: Operation unimplemented"); 
    return 0;
  } /* (Transponsed input/output matrices are not accepted.) */

  inx = in->column[t];
  outx = out->column[t];

  for(i = 0; i < pnum; i++) {
    m2[i] = m1[i];
    if(outx) 
      if(i == outx->row) {
	j = m2[i] - outx->value;
	if(j < 0)
	  return 0;  /* the transition is not enabled */
	m2[i] = j;
	outx = outx->next[mDOWN];
	if(outx->row <= i) /* because the list is organized as a chain */
	  outx = 0;
      }
    
    if(inx) 
      if(i == inx->row) {
	m2[i] += inx->value;
	inx = inx->next[mDOWN];
	if(inx->row <= i) /* because the list is organized as a chain */
	  inx = 0;
      }
  }
  return 1;
}


/***************************************************************************
 DISPLAYPN
****************************************************************************/

void prlist(FILE* f, char* str, int *pj, int i, int num, int indent) {
  /* subroutine of displaypn; i = 0 ... num-1 is the number of the current
     element, str the string to be displayed at the current element, and
     indent is the number of blank spaces that are to be added at the 
     beginning of a new line. pj is an internal variable that contains the 
     current position on the row of text. */

  int k;

  if(i <= num - 2 && num > 2) /* formats the list element */
    strcat(str, ", ");
  else if(i == 0 && num == 2)
    strcat(str, " ");
  if(i == num - 2)
    strcat(str, "and ");
  if(i == num - 1)
    strcat(str, ".");

  if ( *pj + strlen(str) >= 80 ) { /* makes sure it fits on a row */
    fprintf(f, "\n");
    for(k = 0; k < indent; k++) 
      fprintf(f, " ");
    *pj = indent;
  }

  fprintf(f, "%s", str);
  *pj = *pj + strlen(str);
}

void displaypn(pns pn, FILE *f) {
  int i, j, k, l, uc, uo, u, v, z;
  mtype w;
  char str[80];
  MatrElem *p;

  if(!f)
    f = stderr;
  fprintf(f, "\nThe PN has %d places and %d transitions.", pn.pnum, pn.tnum);
  fprintf(f, "\n\n");
  uc = 0; uo = 0;
  if(pn.t) {
    for(i = 0; i < pn.tnum; i++) {
      uc += pn.t[i].uncontrollable;
      uo += pn.t[i].unobservable;
    }
  }

  /* Print the uncontrollable transitions */

  if(!uc) 
    fprintf(f, "No uncontrollable transition is defined.");
  else if(uc == 1) {
    fprintf(f, "One uncontrollable transition: ");
    for(i = 0; i < pn.tnum; i++)
      if(pn.t[i].uncontrollable)
	break;
    fprintf(f, "t%d.", i);
  }
  else {
    j = fprintf(f, "%d uncontrollable transitions: ", uc);
    for(i = 0, k = 0; i < pn.tnum && k < uc; i++) {
      if(pn.t[i].uncontrollable) {
	sprintf(str, "t%d", i);
        prlist(f, str, &j, k, uc, 4); /* indentation = 4 */
	k++;
      }
    }
  }
  fprintf(f, "\n\n");

  /* Print the unobservable transitions */

  if(!uo) 
    fprintf(f, "No unobservable transition is defined.");
  else if(uo == 1) {
    fprintf(f, "One unobservable transition: ");
    for(i = 0; i < pn.tnum; i++)
      if(pn.t[i].unobservable)
	break;
    fprintf(f, "t%d.", i);
  }
  else {
    j = fprintf(f, "%d unobservable transitions: ", uo);
    for(i = 0, k = 0; i < pn.tnum && k < uo; i++) {
      if(pn.t[i].unobservable) {
	sprintf(str, "t%d", i);
        prlist(f, str, &j, k, uo, 4); /* indentation = 4 */
	k++;
      }
    }
  }
  fprintf(f, "\n\n");

  /* Print label information */

  if(!(pn.t))
    fprintf(f, "No labels have been assigned.");
  else {
    if(isfreelabeled(&pn)) 
      fprintf(f, "All labels are distinct.");
    else
      fprintf(f, "There are transitions with the same label.");
    j = sprintf(str, "Transitions (labels in parantheses): ");
    fprintf(f, "\n\n%s", str);
    for(i = 0; i < pn.tnum; i++) {
      sprintf(str, "t%d (%d)", i, pn.t[i].l);
      prlist(f, str, &j, i, pn.tnum, 4); /* indentation = 4 */
    }
  }
  fprintf(f, "\n\n");

  /* Print the marking */

  j = sprintf(str, "Initial Marking (tokens in parantheses): ");
  fputs(str, f);
  if(!pn.marking)
    fprintf(f, "not specified.");
  else {
    for(i = 0, u = 0; i < pn.pnum; i++)  /* find number of marked places */
      if(pn.marking[i])
	u++;
    for(i = 0, k = 0; k < u; i++) 
      if(pn.marking[i]) {
	sprintf(str, "p%d (%d)", i, (int)pn.marking[i]);
	prlist(f, str, &j, k, u, 4); /* indentation = 4 */
	k++;
    }
    if(!k) fprintf(f, "zero.");
  }
  fprintf(f, "\n\n");

  /* Print the arcs */

  fprintf(f, "Transition arcs (weight in parantheses):\n");
  for(i = 0; i < pn.pnum; i++) {
    for(j = 0, v = 0, u = 0; j < pn.tnum; j++) { /* count arcs */
      v += (GetMatrixEl(&(pn.in), i, j) != 0); /* number of input trans. */
      u += (GetMatrixEl(&(pn.out), i, j) != 0); /* number of output trans. */
    }

    z = sprintf(str, "   *p%d: ", i); /* display input arcs of p_i */
    fputs(str, f);
    if(!v)
      fprintf(f, "no input transitions.");
    for(j = 0, k = 0; k < v; j++) {
      w = GetMatrixEl(&(pn.in), i, j); /* find the weight */
      if(w) {
	if(w > 1)
	  sprintf(str, "t%d (%d)", j, w);
	else
	  sprintf(str, "t%d", j);
        prlist(f, str, &z, k, v, 8); /* indentation = 8 */
	k++;
      }
    }

    fprintf(f, "\n");
    z = sprintf(str, "   p%d*: ", i); /* display output arcs of p_i */
    fputs(str, f);
    if(!u)
      fprintf(f, "no output transitions.");
    for(j = 0, k = 0; k < u; j++) {
      w = GetMatrixEl(&(pn.out), i, j); /* find the weight */
      if(w) {
	if(w > 1)
	  sprintf(str, "t%d (%d)", j, w);
	else
	  sprintf(str, "t%d", j);
        prlist(f, str, &z, k, u, 8); /* indentation = 8 */
	k++;
      }
    }

    fprintf(f, "\n");
  }

  /* Print conditions on arcs */

  arcs *a;
  struct placelist *op;
  if(pn.arc_list) 
    for(i = 0; i < pn.tnum; i++) 
      for(a = pn.arc_list[i]; a; a = a->next) 
	if(a->condition.text) {
	  fprintf(f, "\n(");
	  if(a->in_place >= 0)
	    fprintf(f, "p%d, ", a->in_place);
	  fprintf(f, "t%d", i);
	  for(op = a->out_places; op; op = op->next)
	    fprintf(f, ", p%d", op->place);
	  fprintf(f, ").{%s}", a->condition.text);
	}
  fprintf(f, "\n");
}


/***************************************************************************
 EXTRACTLHCB
****************************************************************************/

/* The implementation assumes that no disjunctive constraints are present. */

struct _extractLCHB {
  int i;
  struct tarray* p;
};


struct _extractLCHB find_var_index(variable* var, pns* pn, specs* sp) {
  int i, k;
  int lab;
  struct _extractLCHB u;

  if(var->type == MARKINGV) {
    if(var->index >= var->pn->pnum)
      merror(0, "EXTRACTLHCB: index %d >= place number (%d)", var->index, var->pn->pnum);
    for(i = 0, k = 0; i < sp->process_num; i++) {
      if(var->pn == sp->process_array[i]->pn) {
        u.i = var->index + k;
	return u;
      }
      k += sp->process_array[i]->pn->pnum;
    }
    merror(0, "EXTRACTLHCB: Marking variable does not match specified PNs");
  }
  else {
    if(!var->pn->t)
      merror(0, "EXTRACTLHCB expects labeled Petri nets");
    if(var->index >= var->pn->tnum)
      merror(0, "EXTRACTLHCB: index %d >= tran. number (%d)", var->index, var->pn->tnum);
    u.p = var->pn->data;
    u.i = var->index;
    /* lab = var->pn->t[var->index].l;
       for(i = 0; i < pn->tnum; i++)
       if(pn->t[i].l == lab) // Assumes free-labeled PN
       return i;
       merror(0, "EXTRACTLHCB: Variable does not match specified PNs"); */
  }
  return u;
}

void extractLHCB(specs* sp, pns* pn, matrix* L, matrix* H, matrix* C, int** B,\
		 char **scplaces) {
  int i, j;
  constraint *c;
  pns pn1, *apn, *vpn;
  int cnum; /* constraint number */
  variable* var;
  inequality* in;
  struct cpinfo *IR;
  struct tarray *TR, *PR;
  struct tranlist *p;
  void **data;
  struct _extractLCHB u;

  /* Find the composed PN */

  *pn = PNComposition(sp->process_array, sp->process_num, &IR);

  if(!IR)
    merror(0, "EXTRACTLHCB: PN composition failed to extract required data");
  TR = IR->T; PR = IR->P;
  if(!TR || !PR)
    merror(0, "EXTRACTLHCB: PN composition failed to extract required data");

  // Determine scplaces

  *scplaces = 0;
  if(pn->pnum) {
    *scplaces = tcalloc(pn->pnum, sizeof(**scplaces));
    if(PR->T)
      for(i = 0; i < pn->pnum && i < PR->n; i++) {
	vpn = PR->T[i].pn;
	if(vpn) {
	  for(j = 0; j < sp->process_num; j++)
	    if(sp->process_array[j]->pn == vpn) {
	      (*scplaces)[i] = (sp->process_array[j]->supervisor != 0);
	      break;
	    }
	}
      }
  }

  // Extract from TR transition information

  // First, allocate memory for 'data' for each PN component.
  data = tcalloc(sp->process_num, sizeof(*data));
  for(i = 0; i < sp->process_num; i++) { /* save 'data' content of each pn */
    data[i] = sp->process_array[i]->pn->data;
    alloc_tarray(sp->process_array[i]->pn->data, sp->process_array[i]->pn->tnum);
  }
  // Finally, write in 'data' for each transition of each PN component the
  // transition(s) of the composed PN to which it belongs.
  for(i = 0; i < TR->n; i++) { // i: current transition of the composed PN
    for(p = (TR->T)+i; p; p = p->next)
      if(p->pn)
	insert_tranlist_sub(((struct tarray*) p->pn->data)->T + p->t, \
			    pn, i, &((struct tarray*) p->pn->data)->mem);
    /* 2nd par of insert_... must be nonzero; value not essential */
  }


  /* May be deleted after testing pn_composition above
  if(sp->process_num == 1)
    *pn = copypn(sp->process_array[0]->pn);
  else {
    apn = sp->process_array[0]->pn;
    for(i = 1; i < sp->process_num; i++) {
      if(i > 1) {
	pn1 = *pn; // save intermediary result for future deallocation
	apn = &pn1;
      }
      *pn = composepn(apn, sp->process_array[i]->pn);
      if(i > 1)
        deallocpn(&pn1); // dealloc intermediary result
    }
  }
  */

  /* Find cnum, the number of constraints */
  for(c = sp->constraint_list, cnum = 0; c; c = c->next, cnum++);

  /* Allocate L, H, C, B */

  AllocateMatrixType(3, L, cnum, pn->pnum);
  AllocateMatrixType(3, H, cnum, pn->tnum);
  AllocateMatrixType(3, C, cnum, pn->tnum);
  if(!cnum)
    *B = 0;
  else
    *B = tcalloc(cnum, sizeof(**B));

  /* Initialize L, H, C, B */

  for(c = sp->constraint_list, i = 0; c; i++, c = c->next) {
    /* it is assumed that there are no disjunctive constraints */
    in = 0; 
    if(c->expr->left_ineq)
      in = c->expr->left_ineq;
    if(c->expr->right_ineq)
      in = c->expr->right_ineq;
    if(!in)
      merror(0, "EXTRACTLCHB: Unexpected expression format");
    (*B)[i] = in->free_term;
    for(var = in->variable_list; var; var = var->next) {
      u = find_var_index(var, pn, sp);
      if(var->type == MARKINGV) /* L(i, u.i) = L(i, u.i) + var->coefficient */
	SetMatrixEl(L, i, u.i, var->coefficient + GetMatrixEl(L, i, u.i));
      else {
	/* A loop is needed in order to account for ALL transitions of the 
	   composed pn corresponding to the transition var->index */
	for(p = (u.p)->T+(u.i); p; p = p->next) {
	  if(!(p->pn)) break;
	  j = p->t;
	  if(var->type == FIRINGV)
	    SetMatrixEl(H, i, j, var->coefficient + GetMatrixEl(H, i, j));
	  if(var->type == PARIKHV)
	    SetMatrixEl(C, i, j, var->coefficient + GetMatrixEl(C, i, j));
	}
      }
    }
  }

  for(i = 0; i < sp->process_num; i++) {/* restore data content of each pn */
    dealloc_tarray(sp->process_array[i]->pn->data);
    sp->process_array[i]->pn->data = data[i];
  }
  free(data);
  dealloc_cpinfo(IR);

}



/***************************************************************************
 EXTRACT_H
****************************************************************************/

matrix* extract_H(matrix* Dm, matrix* Dp, int n) {
// Determines the H matrix of a specification based on the closed-loop
// output/input matrices Dm/Dp and the number of constraints n.
// The function allocates both the return value and its content.

  matrix* H = 0;
  int i, t, m, nt, d_m, d_p;

  if(!Dm || !Dp || n <= 0) return 0;

  m = NumberOfRows(*Dm); nt = NumberOfColumns(*Dm);
  if(n > m || nt != NumberOfColumns(*Dp) || m != NumberOfRows(*Dp)) 
    return 0;

  H = tcalloc(1, sizeof(*H));
  AllocateMatrix(H, n, nt);

  for(i = m - n; i < m; i++) 
    for(t = 0; t < nt; t++) {
      d_m = GetMatrixEl(Dm, i, t);
      d_p = GetMatrixEl(Dp, i, t);
      if(d_m && d_p)
	SetMatrixEl(H, i - m + n, t, d_m);
    }

  return H;
}


/***************************************************************************
 PRINTLHCB
****************************************************************************/

void printLHCB(pns* pn, matrix* L, matrix* H, matrix* C, int* B, int row, FILE* f) {
  int i, j, nr, nc, x, flag, isnamed;
  matrix *mat;
  char *prefix, **name, c;

  if(L)
    nr = NumberOfRows(*L);
  else if(H)
    nr = NumberOfRows(*H);
  else if(C)
    nr = NumberOfRows(*C);
  else {
    merror(0, "PRINTLHCB: At least one of L, H, or C should be given");
    return;
  }

  if(row < 0) {
    if(nr <= 0)
      fprintf(f, "\nThere are no constraints\n");
    else if(nr == 1)
      fprintf(f, "\nThere is one constraint:\n");
    else 
      fprintf(f, "\nThere are %d constraints:\n", nr); 
    for(i = 0; i < nr; i++) 
      printLHCB(pn, L, H, C, B, i, f); 
    return;
  }

  if(row >= nr) {
    merror(0, "PRINTLHCB: Index %d exceeds number of constraints (%d)", row, nr);
    return;
  }

  flag = 1;
  for(j = 0; j < 3; j++) {

    if(j == 0) {
      fprintf(f, "\n(%d)  ", row+1);
      mat = L;
      prefix = "";
      c = 'p';
      name = pn->place_name;
    }
    else if(j == 1) {
      mat = H;
      prefix = "q.";
      c = 't';
      name = pn->trans_name;
    }
    else {
      mat = C;
      prefix = "v.";
      c = 't';
      name = pn->trans_name;
    }

    if(!mat)
      continue;

    nc = NumberOfColumns(*mat);

    for(i = 0; i < nc; i++) {
      x = GetMatrixEl(mat, row, i);
      if(x) {
	if (x == 1 && !flag) // flag = 1 indicates the first element
	  fprintf(f, "+ ");
	else if(x == -1)
	  fprintf(f, "- ");
	else if( x > 0 && x != 1)
	  fprintf(f, "+ %d*", x);
	else if( x < 0)
	  fprintf(f, "- %d*", -x);

	flag = 0;

	isnamed = 0;
	if(name)
	  if(name[i])
	    isnamed = name[i][0]; // nonzero if nonempty string
	if(isnamed)  
	  fprintf(f, "%s%s ", prefix, name[i]);
	else
	  fprintf(f, "%s%c%d ", prefix, c, i); 
      }
    }
  }
  if(flag)
    fprintf(f, "0 ");
  fprintf(f, "<= %d\n", B[row]);
}

/***************************************************************************
 TestLCB
****************************************************************************/

int TestLCB(matrix* L, int* m, matrix* C, int* v, int type, int* B) {

/* 'type' should be GREATER, LESS, EQUAL, GREATER_OR_EQUAL, or LESS_OR_EQUAL
   (which are defined in matrix.h).

   The function calculates L*m + C*v and compares the result to B.
   If all elements of the result satisfy the 'type' constraint when compared
   to B, then the function returns 1. Otherwise, it returns zero. 

   Unused entries may be set to zero. For instance, TestLCB(L,m,0,0,LESS,B,n)
   checks whether L*m < B. */ 

  int i, a, n;
  char zL, zC;

  zL = !L || !m;
  zC = !C || !v;

  if(!zL) zL = zL || ! NumberOfRows(*L) || ! NumberOfColumns(*L);
  if(!zC) zC = zC || ! NumberOfRows(*C) || ! NumberOfColumns(*C);

  if(!B || (zL && zC)) 
    return zL && zC && !B;

  if(!zL)
    n = NumberOfRows(*L);
  else
    n = NumberOfRows(*C);

  for(i = 0; i < n; i++) {
    a = 0;
    if(!zL)
      a = MultiplyVector(L, (matrix*) m, i, -1, 0);
    if(!zC)
      a += MultiplyVector(C, (matrix*) v, i, -1, 0);
    if(!TestCondition(a, type, B[i]))
      return 0;
  }
  return 1;
}


/***************************************************************************
 GETSUPERVISOR2
****************************************************************************/

pns* getSupervisor(pns* pn, matrix* Dcm, matrix* Dcp, int* ms0) {

/* Extracts the PN representing the supervisor from the plant PN (pn), the 
   closed-loop input (Dcp) and output (Dcm) matrices and from the initial 
   marking of the closed-loop (ms0). 

   This function assumes that the set of transitions of the closed-loop is 
   the same as the set of transitions of the plant. Two cases in which
   this is true are the following: 
   - free-labeled closed-loop PN. 
   - the supervisor implements Lm + Hq + Cv \leq b via SBPI. (Since SBPI does 
   not add new transitions). 
*/

  pns *apnsv;
  int tnum, i, j, k, l, t, pcn, tcn, flag, *labels;

  if(!pn->t)
    merror(0, "GETSUPERVISOR: Expects a labeled PN");

  /* Find tnum -- the number of supervisor transitions */

  pcn = NumberOfRows(*Dcm);
  tcn = NumberOfColumns(*Dcp);

  if(pcn <= pn->pnum)
    return 0; // Return, since the supervisor PN is empty

  for(j = 0, tnum = 0; j < tcn; j++) 
    for(i = pn->pnum; i < pcn; i++)
      if ( GetMatrixEl(Dcm, i, j) || GetMatrixEl(Dcp, i, j) ) {
        tnum++;
	break;
      }

  /* Initialize supervisor PN */

  apnsv = tcalloc(1, sizeof(*apnsv));
  *apnsv = createpn("pnum tnum", pcn - pn->pnum, tnum); 

  if(ms0)
    updatepn(apnsv, "m0", ms0+pn->pnum);

  apnsv->t = tmalloc(tnum*sizeof(*(apnsv->t)));
  if(pn->trans_name)
    apnsv->trans_name = tmalloc(tnum*sizeof(*(pn->trans_name)));

  for(j = 0, flag = 0, t = 0; j < tcn; j++, flag = 0) {
    for(i = pn->pnum; i < pcn; i++) {
      k = GetMatrixEl(Dcm, i, j);
      l = GetMatrixEl(Dcp, i, j);
      if( k || l ) { /* write data for place i and transition t */
	flag = 1;
	SetMatrixEl(&(apnsv->out), i - pn->pnum, t, k);
	SetMatrixEl(&(apnsv->in) , i - pn->pnum, t, l);
      }
    }
    if(flag) {
      apnsv->t[t] = pn->t[j];
      if(pn->trans_name)
	if(pn->trans_name[j]) {
	  apnsv->trans_name[t] = tmalloc((1+strlen(pn->trans_name[j]))*sizeof(char));
	  strcpy(apnsv->trans_name[t], pn->trans_name[j]);
	}
      t++;
    }
  }

  return apnsv;
}


int _is_connected(int t, matrix* Dcm, matrix* Dcp, int pnum, int* plpos, int spnum) {
/* Subroutine of getSupervisor2. Checks whether the transition t of the CL  
   is connected to the supervisor places. 

   The return value has the bit 0 set if the only supervisor places to 
   which t is connected belong to supervisor components. However, the bit 
   1 is set if t is connected to places associated with inequalities (the 
   places of index p >= pnum, as opposed to the places of the supervisor 
   components). 

   ASSUMES places are written in plpos in increasing order.
*/

  int i, p, fl = 0;

  for(i = spnum - 1; i >= 0; i--) { // check first inequality places
    p = plpos[i];
    fl = GetMatrixEl(Dcm, p, t);
    if(!fl)
      fl = GetMatrixEl(Dcp, p, t);
    if(fl) {
      if(p >= pnum)
	return 2; // connected to inequality places
      return 1; // connected only to places of supervisor components
    }
  }
  return 0; // t is not connected to the supervisor
}



int _compare_scn(int a, int b, matrix *Dcm, matrix *Dcp, int pnum, int *plpos, int spnum, char* inadm, int label) {

/* This is a subroutine of getSupervisor2.

   Returns a nonzero value if the transitions 'a' and 'b' are not connected
   the same way to the supervisor places. The function can detect whether an
   inequality is inadmissible with respect to the labeling function of the
   PN: if the control place associated with inequality i is not connected the
   same way to 'a' and 'b', the the inequality i is (structurally) 
   inadmissible. If inequality i is inadmissible inadm[i] is set to 'label',
   where 'label' is the label of 'a' and 'b'. 

   IMPORTANT: The function assumes that the inequality constraint places 
   appear last in 'plpos'.

   Algorithm: Are 'a' and 'b' connected the same way to the places of the
   supervisor components? If no, return 1. If yes, check admissibility. If 
   admissible, return 0. If inadmissible, return 2 and mark the label(s)
   causing inadmissibility in 'inadm'.
   
*/

  int i, p, fl = 0; // fl = 1 indicates inadmissible constraint 

  for(i = 0; i < spnum; i++) { // start with sup.-component places
    p = plpos[i];
    if(GetMatrixEl(Dcm, p, a) != GetMatrixEl(Dcm, p, b)) {
      if(p >= pnum) { 
	inadm[p-pnum] = label;
	fl = 2;
      }
      else 
	return 1; // no need to check other places
    }
    if(GetMatrixEl(Dcp, p, a) != GetMatrixEl(Dcp, p, b)) {
      if(p >= pnum) {
	inadm[p-pnum] = label;
	fl = 2;
      }
      else
	return 1;
    }
  }

  return fl;
}

void  _insert_zero_labels(matrix* Dcm, matrix* Dcp, int pnum, int* labels, int stnum, int* pos, char* splaces) {

  int i, p, t;

  for(t = 0; t < stnum; t++) {
    i = pos[t];
    for(p = 0; p < pnum; p++) {
      if(splaces[p]) // if place belongs to supervisor
	continue; // check only connections to the plant
      if(GetMatrixEl(Dcp, p, i))
	break; // exit, the transition is connected to the plant
      if(GetMatrixEl(Dcm, p, i))
	break; // exit, the transition is connected to the plant
    }
    if(p == pnum) // if the transition is not connected to the plant
      labels[t] = 0; // reset the label of t
  }
}


pns* getSupervisor2(pns* pn, matrix* Dcm, matrix* Dcp, int* ms0, char* spl) {

/* Extracts the PN representing the supervisor from the plant PN (pn), the 
   closed-loop input (Dcp) and output (Dcm) matrices, from the initial 
   marking of the closed-loop (ms0), and from a vector indicating the
   supervisor component places (if any) of 'pn' (spl). Note that the 
   number of elements of 'spl' must equal pn->pnum.   

   This function assumes constraints that are admissible with respect to
   the PN labeling (which represents the synchronization constraints). It
   does check for structural admissibility and reports errors in the form
   of a warning. The function also sets to zero the label of any supervisor
   component transition that is not synchronized with the plant. (In the
   supervisor program an enabled zero label transition is fired without
   waiting for the plant to generate an event having this label.) 
*/

  pns *apnsv;
  int pcn, tcn, spnum, stnum, i, j, k, l, t, pc, tc;
  int *labels, *pos, *plpos, *m0;
  char *inadm = 0; // to store indices of inadmissible constraints
  char flag, *splaces; // splaces extends spl to the size of Dcm/Dcp
  struct myinsert ins;

  if(!pn) return 0;

  if(!pn->t)
    merror(0, "GETSUPERVISOR2: Expects a labeled PN");

  // Determine spnum, the number of places of the supervisor

  pcn = NumberOfRows(*Dcm); // the number of places of the closed-loop
  tcn = NumberOfColumns(*Dcm); // the number of transitions of the CL
  if(!pcn || !tcn)
    return 0; // nothing to if the CL has no places or no transitions
  if(pcn < pn->pnum)
    return 0; // this would be an error

  spnum = pcn - pn->pnum;
  if(spl)
    for(i = 0; i < pn->pnum; i++)
      spnum += (spl[i] != 0);

  if(!spnum)
    return 0; // nothing to do if there are no supervisor places

  // Allocations

  labels = tmalloc(tcn*sizeof(*labels));
  plpos = tmalloc(spnum*sizeof(*plpos));
  m0 = tmalloc(spnum*sizeof(*m0));
  pos = tmalloc(tcn*sizeof(*pos));
  if(pcn > pn->pnum)
    inadm = tcalloc(pcn - pn->pnum, sizeof(*inadm)); 
  // tcalloc initializes inadm with zero elements
  splaces = tcalloc(pcn, sizeof(*splaces));

  // Find plpos, where plpos[i] indicates the place of the CL
  // that corresponds to the place i of the supervisor.

  for(i = 0, j = 0; i < pcn; i++) { // the loop calculates also splaces
    if(i < pn->pnum) {
      if(spl)
        splaces[i] = (spl[i] != 0);
    }
    else
      splaces[i] = 1; // it is an inequality constraint place
    if(splaces[i]) {
      plpos[j] = i;
      j++;
    }
  }

  // Next, the input/output matrices of the supervisor are built
  // label[i] will denote the label of transition i of supervisor
  // pos[i] will indicate the transition of the closed-loop to which
  // the transition i of the supervisor corresponds.

  // Determine first which transitions should be added to the supervisor

  for(i = 0, stnum = 0; i < tcn; i++) {

    // Check whether the transition i is connected to the supervisor places

    if(_is_connected(i, Dcm, Dcp, pn->pnum, plpos, spnum)) {

      // Next, check that the transition i is not connected to the supervisor
      // the same way as a previously added transition with the same label.  

      l = pn->t[i].l;
      for(j = 0, k = 1; k && j < stnum; j++) 
	if(labels[j] == l) {
	  k = k && _compare_scn(i, pos[j], Dcm, Dcp, pn->pnum, plpos, spnum, inadm, l);
	}

      // Add the transition to the supervisor if it is not identical with 
      // some previously added transition.
      
      if(k) { 
	pos[stnum] = i; labels[stnum] = l;
	stnum++;
      }

    } // end of if(_is_connected...)
  } // end of for(i = 0 ... )


  // Write zero in 'labels' for transitions that are not synchronized with 
  // the plant

  _insert_zero_labels(Dcm, Dcp, pn->pnum, labels, stnum, pos, splaces);


  // Construct the supervisor

  apnsv = tcalloc(1, sizeof(*apnsv));
  *apnsv = createpn("pnum tnum", spnum, stnum); 

  if(ms0) { // add the initial marking
    for(i = 0; i < spnum; i++)
      m0[i] = ms0[plpos[i]];
    updatepn(apnsv, "m0", m0);
  }

  apnsv->t = tmalloc(stnum*sizeof(*(apnsv->t)));
  if(pn->trans_name)
    apnsv->trans_name = tmalloc(stnum*sizeof(*(pn->trans_name)));

  for(t = 0; t < stnum; t++) {
    tc = pos[t]; // tc: the corresponding closed-loop transition
    for(i = 0; i < spnum; i++) {
      pc = plpos[i]; // pc: the corresponding closed-loop place
      k = GetMatrixEl(Dcm, pc, tc);
      j = GetMatrixEl(Dcp, pc, tc);
      if( k || j ) { // write data for place i and transition t 
	flag = 1;
	SetMatrixEl(&(apnsv->out), i, t, k);
	SetMatrixEl(&(apnsv->in) , i, t, j);
      }
    }
    if(flag) {
      apnsv->t[t] = pn->t[tc];
      apnsv->t[t].l = labels[t];
      if(pn->trans_name)
	if(pn->trans_name[tc]) {
	  apnsv->trans_name[t] = tmalloc((1+strlen(pn->trans_name[tc]))*sizeof(char));
	  strcpy(apnsv->trans_name[t], pn->trans_name[tc]);
	}
    }
  }


  // Report errors

  for(i = 0, flag = 0; i < pcn - pn->pnum; i++)
    flag += (inadm[i] != 0);

  if(flag) {
    ins = InitInsert(512);
    if(flag > 1)
      ins = SInsert("The following constraints appear to be inadmissible with respect to the\nsynchronization requirements:\n", ins);
    for(i = 0; i < pcn - pn->pnum; i++) {
      if(inadm[i]) {
	if(flag == 1) 
	  ins = FSInsert(ins, "Constraint %d appears to be inadmissible with respect to the label %d\n", i+1, inadm[i]);
	else 
	  ins = FSInsert(ins, " - Constraint %d with respect to label %d\n", i+1, inadm[i]);
      }
    } // end of for
    ins = SInsert("All constraints have been considered, including the liveness enforcement \nconstraints, if any. Note that the supervisor is not able to implement \naccurately inadmissible constraints.", ins);
    merror(1, GetInsertBuf(&ins));
    free(GetInsertBuf(&ins));
  } // end of if(flag)


  free(labels); free(plpos); free(m0); free(pos); free(splaces);
  if(inadm) free(inadm);

  return apnsv;
}


/***************************************************************************
GET_LABEL_LIST
****************************************************************************/

/* // Here are the definitions from pns.h

struct ilist {
int t;
struct ilist* next;
};


struct prlist {
int pr; // process subtype number
struct ilist* otlist; // source transition list
struct ilist* itlist; // non-source transition list
struct prlist* next;
};

struct label_lst {
int l;
struct label_lst* next;
struct prlist* pr;
};
*/

struct label_lst* place_in_label_lst(int label, struct label_lst** ares) {
  // Returns the address of the list element of label 'label' from the list *ares
  // If the element is not present, it creates it and updates *ares.

  struct label_lst* res, *pres, *p;

  if(!*ares) {
    res = tcalloc(1, sizeof(*res));
    res->l = label;
    *ares = res;
    return res;
  }
  for(res = *ares, pres = 0; res; res = res->next) {
    if(res->l == label)
      return res;
    if(res->l > label) 
      break;
    pres = res;
  }
  if(!pres) {
    res = tcalloc(1, sizeof(*res));
    res->l = label;
    res->next = *ares;
    *ares = res;
    return res;
  }
  p = tcalloc(1, sizeof(*res));
  p->l = label;
  p->next = res;
  pres->next = p;

  return p;
}

struct prlist* place_in_process_lst(int label, struct prlist** ares) {
  // Returns the address of the list element of id 'label' from the list *ares
  // If the element is not present, it creates it and updates *ares.

  struct prlist* res, *pres, *p;

  if(!*ares) {
    res = tcalloc(1, sizeof(*res));
    res->pr = label;
    *ares = res;
    return res;
  }
  for(res = *ares, pres = 0; res; res = res->next) {
    if(res->pr == label)
      return res;
    if(res->pr > label) 
      break;
    pres = res;
  }
  if(!pres) {
    res = tcalloc(1, sizeof(*res));
    res->pr = label;
    res->next = *ares;
    *ares = res;
    return res;
  }
  p = tcalloc(1, sizeof(*res));
  p->pr = label;
  p->next = res;
  pres->next = p;

  return p;
}

int is_source(pns* apn, int t) {
  // Returns nonzero when t is a source transition of apn

  int i;

  for(i = 0; i < apn->pnum; i++)
    if(GetMatrixEl(&(apn->out), i, t))
      return 0;
  return 1;
}

void insert_in_ilst(int t, struct ilist **root) {
  struct ilist* p;

  p = tcalloc(1, sizeof(*p));
  p->t = t;
  if(!*root)
    *root = p;
  else {
    p->next = *root;
    *root = p;
  }
}


struct label_lst* get_label_list(struct process** pr, int n) {
  // n: the size of the array pr
  // Ignores labels of value 0!

  struct label_lst* res = 0, *pllst;
  struct pns *apn;
  struct prlist *prlst;
  int i, j;

  for(i = 0; i < n; i++) {
    apn = pr[i]->pn;
    if(!apn->t) // if labels are not defined
      continue;
    for(j = 0; j < apn->tnum; j++) {
      if(!apn->t[j].l)
	continue; // ignore labels of value 0!
      pllst = place_in_label_lst(apn->t[j].l, &res);
      prlst = place_in_process_lst(i, &(pllst->pr)); // proc #i placed in list
      if(is_source(apn, j)) 
	insert_in_ilst(j, &(prlst->otlist));
      else
	insert_in_ilst(j, &(prlst->itlist));
    }
  }
  return res;
}


inline void add_to_synclist(struct synclist** acurrent, struct synclist** aroot) {
  if(!*aroot) {
    *aroot = tcalloc(1, sizeof(**aroot));
    *acurrent = *aroot;
  } 
  else {
    (*acurrent)->next = tcalloc(1, sizeof(**aroot));
    *acurrent = (*acurrent)->next;
  }
}

inline void add_sync_el(struct sync_element **crnt, struct sync_element **root,\
			struct prlist* pr, int n, process** prarray, char fn) {
  // 'fn': may be 's' or 'o', indicating the corresponding chain of synclist.
  // n: number of 'struct ilist' elements of the 's' or 'o' chain.

  struct sync_element *cr;
  struct ilist *lst, *p;
  int* data, *w, i, j, k, t;
  pns *pn;

  if(!*root) {
    *root = tcalloc(1, sizeof(**root));
    *crnt = *root;
  } 
  else {
    (*crnt)->next = tcalloc(1, sizeof(**root));
    *crnt = (*crnt)->next;
  }

  cr = *crnt;
  data = tcalloc(n, sizeof(*data));
  w = tcalloc(n, sizeof(*w));
  if(fn == 'o') {
    for(p = pr->otlist, i = 0; p; p = p->next, i++) {
      t = p->t;
      pn = prarray[pr->pr]->pn;
      for(j = 0; j < pn->pnum; j++) { // find output place of t
	k = GetMatrixEl(&(pn->in), j, t); 
	if(k) break; // j = t* and k = w(t, j)
      }
      if(!k)
	merror(0, "GET_SYNCLIST: No output place!");
      w[i] = k;
      data[i] = j;
    }
    cr->p = data;
  }
  else {
    for(p = pr->itlist, i = 0; p; p = p->next, i++) {
      data[i] = p->t;
      pn = prarray[pr->pr]->pn;
      for(j = 0; j < pn->pnum; j++) {
	k = GetMatrixEl(&(pn->out), j, data[i]);
	if(k) break;
      }
      if(!k)
	merror(0, "GET_SYNCLIST: No input place!");
      w[i] = k;
    }
    cr->t = data;
  }

  cr->prtype = pr->pr;
  cr->n = n;
  cr->w = w;
}

struct synclist* get_synclist(struct label_lst* lls, process** prarray) {
  struct synclist *current, *p2, *root;
  struct sync_element *se, *oe;
  struct label_lst *pl;
  struct prlist *pr;
  struct ilist *pi;
  int oidx, no, ni;

  for(pl = lls, root = 0; pl; pl = pl->next) {
    if(!pl->pr->next) // continue, since at least two process subtypes
      continue;       // are part of a synchronization

    add_to_synclist(&current, &root); // create new synchronization structure
    // 'current' will become a pointer to the new structure
    for(pr = pl->pr, oidx = 0; pr; pr = pr->next) {
      for(pi = pr->otlist, no = 0; pi; pi = pi->next, no++);
      for(pi = pr->itlist, ni = 0; pi; pi = pi->next, ni++);

      if(no) {
	oidx++;
	add_sync_el(&oe, &(current->o), pr, no, prarray, 'o');
      }
      if(ni) 
	add_sync_el(&se, &(current->s), pr, ni, prarray, 's');
      if(ni & no)
	se->disj = oidx;
    }
  }
  return root;
}


void free_sync_el(struct sync_element* p, char c) {
  struct sync_element* pa, *pb;
  if(!p)
    return;
  for(pa = p; pa; pa = pb) {
    pb = pa->next;
    if(c == 's')
      if(pa->n && pa->t)
	free(pa->t);
    if(c == 'o')
      if(pa->n && pa->p)
	free(pa->p);
    if(pa->n && pa->w)
      free(pa->w);
  }
}


void free_synclist(struct synclist* p) {
  struct synclist* pa, *pb;
  if(!p)
    return;
  for(pa = p; pa; pa = pb) {
    pb = pa->next;
    free_sync_el(pa->s, 's');
    free_sync_el(pa->o, 'o');
    free(pa);
  }
}

void free_ilist(struct ilist *p) {
  struct ilist* pa, *pb;
  if(!p)
    return;
  for(pa = p; pa; pa = pb) {
    pb = pa->next;
    free(pa);
  }
}

void free_prlist(struct prlist* p) {
  struct prlist* pa, *pb;
  if(!p)
    return;
  for(pa = p; pa; pa = pb) {
    free_ilist(pa->otlist);
    free_ilist(pa->itlist);
    pb = pa->next;
    free(pa);
  }
}

void free_label_list(struct label_lst* p) {
  struct label_lst* pa, *pb;
  if(!p)
    return;
  for(pa = p; pa; pa = pb) {
    free_prlist(pa->pr);
    pb = pa->next;
    free(pa);
  }
}



//=========================================================================

inline int get_label(pns* pn, int t) {
  if(!pn->t) return 0;
  return pn->t[t].l;
}

inline int get_marking(pns* pn, int place) {
/* Returns the (initial) marking of the place */
  if(!pn->marking) return 0;
  return pn->marking[place];
}

//=========================================================================

char* process_check(process* pr)  {

/* Checks the process object and returns zero if no errors are found. 
   If an error is found, it returns a string describing the error. The 
   string should be freed with free(). */

  struct myinsert ins;
  char *type, error = 0, *str;

  if(!pr) return 0;

  if(pr->supervisor)
    type = "supervisor component";
  else if(pr->thread)
    type = "thread";
  else
    type = "process";

  ins = InitInsert(128);

  if(!pr->name) {
    ins = FSInsert(ins, "\nThe name of the %s could not be determined.", type);
    error++;
  }

  if(!pr->instance) {
    ins = FSInsert(ins, "\nThe name of the %s instance could not be determined.", type);
    error++;
  }

  if(!pr->pn) {
    if(pr->instance)
      ins = FSInsert(ins, "\nThe DES structure of %s is unknown.", pr->instance);
    else
      ins = FSInsert(ins, "\nThe DES structure of the %s is unknown.", type);
    error++;
  }

  if(pr->pn) {
    str = pn_check(pr->pn);
    if(str) {
      if(pr->instance)
	ins = FSInsert(ins, "\nThe DES structure of %s has errors: %s", pr->instance, str);
      else
	ins = FSInsert(ins, "\nThe DES structure of the %s has errors: %s", type, str);
      error++;
      free(str);
    }
  }

  if(error)
    return GetInsertBuf(&ins);

  if(GetInsertBuf(&ins))
    free(GetInsertBuf(&ins)); 
  return 0; 
}



char* pn_check(pns* p) {

/* Checks the pn object and returns zero if no errors are found. 
   If an error is found, it returns a string describing the error. The 
   string should be freed with free(). */

// The function does not check for all possible errors. Other tests could
// be implemented if necessary.

  struct myinsert ins;
  char *type, error = 0, *str;

  if(!p) return 0;

  ins = InitInsert(128);

  if(!p->pnum && !p->tnum) {
    ins = SInsert("\nThe DES structure is empty: there are no places and no transitions.", ins);
    error++;
  }

  if(error)
    return GetInsertBuf(&ins);

  if(GetInsertBuf(&ins))
    free(GetInsertBuf(&ins)); 
  return 0; 
}


int TestConstraint();


/* Things to do:
   - composepn ignores the text fields of the pns. 
   - composepn assumes that the places in the two pns are distinct.
   - It would be helpful to read from a file PNs rather than use createpn. The
     format in which displaypn shows the data could be used. 
   - improve the is_source() function to take advantage of the matrix data struct.
*/
