/****************************************************************************
supervisorCompiler.c -- Generates the c code for the supervisor.
This is the 2010 version. The 2010 version was written by M. V. Iordache.
Created: June 2010.
Last updated: July 2011.
****************************************************************************/

/* To do: deal with zero label transitions
   also with spr without trasitions */ 

#include<stdio.h>
#include<stdarg.h>
#include<time.h>
#include"pns.h"
#include"codegen.h"
#include"insert.h"

#define TEMPL "SupervisorTemplate.c"


struct _labels {
  int l; // label used for SC, not the action label
  char free; // if true, syn should be freed when the structure is. 
  struct synclist *syn;
  struct _labels *next;
};

char *inc_name; // the name of the spcommon.h include file, a global variable

extern char spcommon_h[], SupervisorTemplate_c[];

static int **plabels; // action labels are stored here for each process
static struct _labels *llist, *plref;//action labels have also the list defined
// llist is the base of the list and plref points to the nActRef element
// (see below)
static int nActLab, nActRef, nSync; // nactlab: total number of action labels; 
// nActRef: the first action label number that is not about interprocess 
// synchronization. 
// nSync: number of synchronization constraints involving more than one plant
// process.

static int MaxNo; // the maximum value of the field 'no' of 'struct ___action'.
// It is determined in 'writeActions'. MaxNo is used for the size of
// the array '___mask'.


// Subroutine of createLabels()

struct _labels* insertLabel(struct _labels **list, struct _labels *pl, \
			    struct synclist *syn, int l, char fr) {
  struct _labels* p;

  if(!pl) {
    *list = tcalloc(1, sizeof(**list));
    p = *list;
  }
  else {
    pl->next = tcalloc(1, sizeof(**list));
    p = pl->next;
  }
  p->syn = syn;
  p->l = l;
  p->free = fr;

  return p;
}


// The following is a subroutine of createLabels()

void _update_plabels(process **prs, int nprs, int lb, int action, int** pl) {
  int i, j, tnum;
  TransInfo *t;

  for(i = 0; i < nprs; i++) {
    t = prs[i]->pn->t;
    tnum = prs[i]->pn->tnum;
    for(j = 0; j < tnum; j++) {
      if(pl[i][j] < 0 && t[j].l == lb)
	pl[i][j] = action;
    }
  }
}


//////////////////////////////////////////////////////////////////////////
//  CREATELABELS
//////////////////////////////////////////////////////////////////////////

// The supervisor receives service requests from processes. Each service 
// request is associated with a specific action. This function assigns a number
// between 0 and n to each possible action. This number is called here label.
// Any message from a process to a supervisor will include the number denoting
// the action that is requested. 
// Possible actions are grouped as follows:
// 1) Synchronizations involving processes of different type and possibly
//    transitions of the supervisor.
// 2) Synchronizations involving processes of the same type and possibly 
//    transitions of the supervisor.
// 3) Synchronizations of a plant process with a supervisor transition.
// Case 2) corresponds to plant transitions that have an input weight greater
// than 1. 
// Case 2) considers only the situations not covered at 1). Case 3) considers 
// only the situations not covered at 1) and 2).
// Included at 3) are the actions associated with notification messages sent by
// processes when they fire transitions observed but not controlled by the 
// supervisor. In such cases all that the supervisor has to do is to update 
// its marking and to launch new processes, if any are associated with the 
// fired plant transition. 

void createLabels(pns *sup, process **prs, int nprs, struct synclist *sl, \
		  TrData** TrInfo) {
  int i, j, k, l, n, pnum, tnum, t, w;
  int nptran; // number of process transitions
  struct synclist *psl;
  struct _labels *pl, *pl2;
  struct sync_element *sel;
  matrix *dm;
  char flag;
  TransInfo* ti;

  plabels = tcalloc(nprs, sizeof(*plabels));

  // 1. Find the number of process transitions and allocate plabels

  for(i = 0, nptran = 0; i < nprs; i++) {
    n = prs[i]->pn->tnum;
    nptran += n;
    plabels[i] = tcalloc(n, sizeof(**plabels));
    for(j = 0; j < n; j++)
      plabels[i][j] = -1; // initialize the vector
  }

  // 2. Create new labels. n will denote the next available label

  n = 0; pl = 0; // pl must be initialized to zero because of insertLabel()

  // 2.1 Assign labels to transitions in the synchornization list sl. Each
  //     synchronization will have a distinct label.

  for(psl = sl; psl; psl = psl->next, n++) { // pl must be initialize 0
    if(!psl->s)
      merror(0, "NEWCODEGEN: Sync list elements must have nonzero 's' entry");
    pl = insertLabel(&llist, pl, psl, prs[psl->s->prtype]->pn->t[psl->s->t[0]].l, 0);
    for(sel = psl->s; sel; sel = sel->next) 
      for(j = 0; j < sel->n; j++) {
	plabels[sel->prtype][sel->t[j]] = n;
	if(psl->s->next)//if 2 or more entries, transition should be controlled
	  TrInfo[sel->prtype][sel->t[j]].flags |= 4; 
	else // if only one entry, transition should be observed
	  TrInfo[sel->prtype][sel->t[j]].flags |= 8;
      }
  }

  nSync = n;

  // 2.2 Take in account process transitions with weight greater than one

  for(i = 0; i < nprs; i++) {
    dm = &prs[i]->pn->out;
    pnum = prs[i]->pn->pnum; tnum = prs[i]->pn->tnum;
    for(j = 0; j < pnum; j++)
      for(k = 0; k < tnum; k++) { // check also if tran. not considered already
	w = GetMatrixEl(dm, j, k);
	if(w > 1) {
	  if(plabels[i][k] < 0) { 
	    psl = tcalloc(1, sizeof(*psl)); sel = tcalloc(1, sizeof(*sel)); 
	    sel->n = 1; sel->w = malloc(sizeof(*sel->w)); sel->w[0] = w; 
	    sel->prtype = i; sel->t = malloc(sizeof(*sel->t)); sel->t[0] = k; 
	    psl->s = sel;
	    pl = insertLabel(&llist, pl, psl, prs[i]->pn->t[k].l, 1);
	    plabels[i][k] = n;
	    n++;
	  }
	  TrInfo[i][k].flags |= 4; // transition should be controlled for sync.
	}
      }
  }

  // 2.3 Now, take in account supervisor labels

  nActRef = n; nActLab = n;
  if(!sup) return; // return if there are no supervisor labels

  for(i = 0, flag = 1; i < sup->tnum; i++) {
    l = sup->t[i].l;
    if(!l)
      continue; // internal transitions of the supervisor are not considered

    // 2.3.1 Check whether the supervisor label has been considered already
    //       in previous iterations of this "for loop".

    if(!flag) {
      for(pl2 = plref; pl2; pl2 = pl2->next) 
	if(l == pl2->l)
	  break;
      if(pl2) // if label considered in previous iterations
	continue;
    }

    // 2.3.2 Check whether there are plant transitions with this label that
    //       have not been considered already

    if(nActRef > 0) { // if any elements were added at 2.1 or 2.2
      for(j = 0; j < nprs; j++) {
	tnum = prs[j]->pn->tnum; ti = prs[j]->pn->t;
	for(k = 0; k < tnum; k++) 
	  if(ti[k].l == l)
	    if(plabels[j][k] < 0)
	      break; // the label should be considered here
	if(k < tnum)
	  break; // the label should be considered here
      }

      if(j >= nprs) // the label has been considered already
	continue;
    }

    // 2.3.3 If the label should be considered here, create element in llist

    pl = insertLabel(&llist, pl, 0, l, 0); 
    _update_plabels(prs, nprs, l, n, plabels);
    n++;

    if(flag) { // if first element
      flag = 0;
      plref = pl;
    }
  }
  nActLab = n;
}



void free_lstruct(struct _labels *x) {
  struct _labels *pl, *pl2;
  struct synclist *psl, *psl2;
  struct sync_element *sel, *sel2;

  for(pl = x; pl; pl = pl2) {
    if(pl->free) 
      for(psl = pl->syn; psl; psl = psl2) {
	for(sel = psl->s; sel; sel = sel2) {
	  sel2 = sel->next;
	  free(sel);
	}
	psl2 = psl->next;
	free(psl);
      }
    pl2 = pl->next;
    free(pl);
  }
}


int st_insert1D(char* s, int x, struct myinsert* ps) {
  // same as insert1D (below), except it takes one element at a time
  static int i = 0;
  int j;

  j = i;
  if(s) {
    i = 0;
    *ps = SInsert(" }", *ps);
  }
  else {
    if(i > 0)
      *ps = CInsert(',', *ps);
    else
      *ps = CInsert('{', *ps);
    *ps = FSInsert(*ps, " %d", x);
    i++;
    return i;
  }

  return j;
}


struct myinsert insert1D(int* x, int n, struct myinsert ins) {
  // if x = 1, 2, 3, ... it writes the string "{1, 2, 3, ...}" to ins.
  int i;
  struct myinsert in;

  in = CInsert('{', ins);
  if(n > 0) {
    for(i = 0; i < n - 1; i++)
      in = FSInsert(in, " %d,", x[i]);
    in = FSInsert(in, " %d }", x[n-1]);
  }
  else
    in = CInsert('}', in);
  return in;
}


struct myinsert insert2D(int** x, int nr, int nc, char* sep, \
			 struct myinsert ins) {
  // See insert1D; 
  int i;
  struct myinsert in;

  for(i = 0, in = ins; i < nr-1; i++) {
    in = insert1D(x[i], nc, in);
    in = SInsert(sep, in);
  }
  in = insert1D(x[i], nc, in);
  return in;
}


struct myinsert insertMatrix(matrix *m, char* sep, struct myinsert ins) {
  int **x;
  struct myinsert in;

  x = matrix2array(*m);
  in = insert2D(x, NumberOfRows(*m), NumberOfColumns(*m), sep, ins);
  free2Darray(x, NumberOfRows(*m));
  return in; 
}


struct myinsert cinsert2D(matrix* x, int *nel, struct myinsert ins) {
  // This function is for a compact representation of vectors with few nonzero
  // elements. 
  // The format is { ... {index, index, (nonzero) value at indices} ...}
  // The function writes to nel the number of elements written

  int i, j, nr, nc, e, flag;
  struct myinsert in;

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

  if(!nr || !nc)
    merror(0, "Unexpected zero value in cinsert2D");

  in = CInsert('{', ins);
  for(i = 0, flag = 0; i < nr; i++) 
    for(j = 0; j < nc; j++) {
      e = GetMatrixEl(x, i, j);
      if(e != 0) {
	if(flag)
	  in = SInsert(", ", in);
	in = FSInsert(in, "{%d, %d, %d}", i, j, e);
	flag++;
      }
    }
  if(!flag) {
    in = SInsert("{0, 0, 0}}", in);
    flag = 1;
  }
  else
    in = CInsert('}', in);

  *nel = flag;
  return in;
}


struct myinsert cinsert1D(int* x, int n, int *nel, struct myinsert ins) {
  // This function is for a compact representation of vectors with few nonzero
  // elements. If x = 0, 2, 0, ... it writes the string "{ {1, 2}, ...}". 
  // The format is { ... {index, (nonzero) value at index} ...}
  // The function writes to nel the number of elements written

  int i, flag;
  struct myinsert in;

  if(!n)
    merror(0, "Unexpected zero value in cinsert1D");

  in = CInsert('{', ins);
  for(i = 0, flag = 0; i < n; i++) {
    if(x[i] != 0) {
      if(flag)
	in = SInsert(", ", in);
      in = FSInsert(in, "{%d, %d}", i, x[i]);
      flag++;
    }
  }
  if(!flag) {
    in = SInsert("{0, 0}}", in);
    flag++;
  }
  else
    in = CInsert('}', in);

  *nel = flag;
  return in;
}


inline void write_sub(char* s, int j, int i, int x, struct myinsert* inp) {
  // This is a subroutine of writeActions for printing 1D arrays

  if(!j)
    *inp = FSInsert(*inp, "%s%d[] = {", s, i);
  else
    *inp = SInsert(", ", *inp); // separates between two elements of an array
  *inp = FSInsert(*inp, "%d", x);

}

void write_2D(char *s1, char *s2, struct sync_element* psr, char c,\
	      int i, struct myinsert* inp) {
  // This is a subroutine of writeActions for printing 2D arrays

  struct sync_element* ps;
  int k, j, *ip;
  char* name;

  if(!psr)
    return;

  // For instance, if s2 = 't' and i = 1, the code could define t1_0[]
  // and t1_1[] in the first block of code and then define
  // t1[] = {t1_0, t1_1} in the second block of code.

  *inp = FSInsert(*inp, "%s", s1);
  for(ps = psr, j = 0; ps; ps = ps->next, j++) {
    if(j)
      *inp = SInsert("}, ", *inp);
    *inp = FSInsert(*inp, "%s%d_", s2, i);
    switch(c) {
    case 't': ip = ps->t; break;
    case 'w': ip = ps->w; break;
    case 'p': ip = ps->p; break;
    default: merror(0, "NEWCODEGEN: write_2D() has no option '%c'", c);
    }
    for(k = 0; k < ps->n; k++)
      write_sub("", k, j, ip[k], inp);
  }

  *inp = FSInsert(*inp, "}, *%s%d[] = {", s2, i);
  for(ps = psr, j = 0; ps; ps = ps->next, j++) {
    if(j)
      *inp = SInsert(", ", *inp);
    *inp = FSInsert(*inp, "%s%d_%d", s2, i, j);
  }
}


struct myinsert writeActions(pns *sup, struct myinsert in) {
  // Writes the ___act[] array and related data.
  struct myinsert ins = in;
  int i, *npr, *ntr, *nor, j;
  struct _labels *pl; 
  struct sync_element *ps;
  char flag, first;

  npr = tcalloc(nActLab, sizeof(*npr));
  nor = tcalloc(nActLab, sizeof(*nor));
  ntr = tcalloc(nActLab, sizeof(*ntr));
 
  // 1)  Define integer arrays used to initialize the ___act array

  for(pl = llist, i = 0, flag = 1; pl; pl = pl->next, i++) {
    if(pl->syn) {
      ps = pl->syn->s;
      if(!ps)
	merror(0, "NEWCODEGEN: Unexpected zero element in synclist structure");
      for(j = 0; ps; ps = ps->next, j++) {
	if(flag) { // if this is the first array
	  flag = 0;
	  ins = SInsert("const int ", ins);
	}
	else if(!j)
	  ins = SInsert(", ", ins); // separates between two arrays
	write_sub("___type", j, i, ps->prtype, &ins);
      } // for end
      npr[i] = j;
      if(j) { // if some array was defined
	for(ps = pl->syn->s, j = 0; ps; ps = ps->next, j++) 
	  write_sub("}, ___nit", j, i, ps->n, &ins);
	for(ps = pl->syn->s, j = 0; ps; ps = ps->next, j++) 
	  write_sub("}, ___disj", j, i, ps->disj, &ins);
	write_2D("}, ", "___weight", pl->syn->s, 'w', i, &ins);
	write_2D("}, ", "___itr", pl->syn->s, 't', i, &ins);
	if(pl->syn->o) {
	  for(ps = pl->syn->o, j = 0; ps; ps = ps->next, j++)
	    write_sub("}, ___otype", j, i, ps->prtype, &ins);
	  for(ps = pl->syn->o, j = 0; ps; ps = ps->next, j++) 
	    write_sub("}, ___not", j, i, ps->n, &ins);
	  write_2D("}, ", "___oweight", pl->syn->o, 'w', i, &ins);
	  write_2D("}, ", "___oplace", pl->syn->o, 'p', i, &ins);
	  nor[i] = j;
	}
	ins = CInsert('}', ins);
      }
    } // end of if(pl->syn)

    // Next, consider the 't' entry of "struct ___action".
    // Find which supervisor transitions have the label pl->l
    if(sup) {
      for(j = 0, first = 1; j < sup->tnum; j++) {
	if(sup->t[j].l == pl->l) {
	  ntr[i]++; // ntr[i] initialized in tcalloc above
	  if(first) {
	    if(flag) {
	      flag = 0;
	      ins = SInsert("const int ", ins);
	    }
	    else
	      ins = SInsert(", ", ins); // separates between two arrays
	  }
	  write_sub("___trs", !first, i, j, &ins); // insert transition number
	  first = 0;
	}
      }
      if(!first) // if some array was defined
	ins = CInsert('}', ins);
    } // end of if(sup)
  }
  if(!flag) // if some line was written, terminate it with semicolon
    ins = SInsert(";\n\n", ins);

  // 2) Write the ___act array

  if(nActLab) {
    ins = FSInsert(ins, "#define ___ACTIONS %d\n", nActLab);
    ins = FSInsert(ins, "struct ___action ___act[%d] = { ", nActLab);
  }
  for(i = 0; i < nActLab; i++) {
    if(npr[i]) 
      ins = FSInsert(ins, "%d, ___type%d, ___nit%d, ___disj%d, ___itr%d, ___weight%d, ",\
		     npr[i], i, i, i, i, i); 
    else
      ins = SInsert("0, 0, 0, 0, 0, 0, ", ins);
    if(nor[i]) 
      ins = FSInsert(ins, "%d, ___otype%d, ___not%d, ___oweight%d, ___oplace%d, ",\
		     nor[i], i, i, i, i);
    else
      ins = SInsert("0, 0, 0, 0, 0, ", ins);
    if(ntr[i])
      ins = FSInsert(ins, "%d, ___trs%d", ntr[i], i);
    else
      ins =  SInsert("0, 0", ins);
    if(i == nActLab - 1)
      ins = SInsert("};\n\n", ins);
    else
      ins = SInsert(", ", ins); 
  }

  for(i = 0, MaxNo = 0; i < nActLab; i++)  // determines MaxNo
    if(nor[i] > MaxNo)
      MaxNo = nor[i];

  free(npr); free(ntr); free(nor);

  return ins;
}


struct myinsert writeSPN(pns *sup, struct myinsert in) {
  struct myinsert ins = in;
  int i, j, ni, no, w, pnum, tnum;
  int *iplace, *oplace, *iweight, *oweight, *nri, *nro;
  matrix *d;
  char first;

  first = !sup;
  if(sup)
    first = !(sup->tnum);
  if(first) {
    ins = SInsert("const struct ___PN ___trans[] = {};\n\n", ins);
    return ins;
  }

  pnum = sup->pnum; tnum = sup->tnum;
  iplace = tcalloc(pnum, sizeof(*iplace));
  oplace = tcalloc(pnum, sizeof(*oplace));
  iweight = tcalloc(pnum, sizeof(*iweight));
  oweight = tcalloc(pnum, sizeof(*oweight));
  nri = tcalloc(tnum, sizeof(*nri));
  nro = tcalloc(tnum, sizeof(*nro));

  for(i = 0, first = 1; i < tnum; i++) {
    for(j = 0, ni = 0, no = 0; j < pnum; j++) {
      w = GetMatrixEl(&sup->out, j, i); // sup->out --> output transitions
      if(w) {
	iplace[ni] = j; // j: input place to transition i (i output of j)
	iweight[ni] = w;
	ni++;
      }
      w = GetMatrixEl(&sup->in, j, i); // sup->in --> input transitions
      if(w) {
	oplace[no] = j;
	oweight[no] = w;
	no++;
      }
    }
    nri[i] = ni;
    nro[i] = no;
    if(ni || no) {
      if(first) { // if first array
	ins = SInsert("const int ", ins);
	first = 0;
      }
      else // include separator 
	ins = SInsert(", ", ins); // separator between arrays
    }
    if(ni) {
      ins = FSInsert(ins, "___ipl%d[] = ", i);
      ins = insert1D(iplace, ni, ins);
      ins = FSInsert(ins, ", ___iwt%d[] = ", i);
      ins = insert1D(iweight, ni, ins);
      if(no)
	ins = SInsert(", ", ins); // separator between arrays
    }
    if(no) {
      ins = FSInsert(ins, "___opl%d[] = ", i);
      ins = insert1D(oplace, no, ins);
      ins = FSInsert(ins, ", ___owt%d[] = ", i);
      ins = insert1D(oweight, no, ins);
    }
  }

  ins = SInsert(";\n\n", ins);
  ins = SInsert("const struct ___PN ___trans[] = {", ins);
  for(i = 0; i < tnum; i++) {
    if(nri[i])
      ins = FSInsert(ins, " %d, ___ipl%d, ___iwt%d,", nri[i], i, i);
    else
      ins = SInsert(" 0, 0, 0,", ins);
    if(nro[i])
      ins = FSInsert(ins, " %d, ___opl%d, ___owt%d", nro[i], i, i);
    else
      ins = SInsert(" 0, 0, 0", ins);
    if(i < tnum - 1)
      ins = CInsert(',', ins);
  }
  ins = SInsert("};\n\n", ins);

  free(iplace); free(iweight); free(oplace); free(oweight);
  free(nri); free(nro);
  return ins;
}


int* MaxOutpTranNum(process **prs, int nprs) {

  int* ip, i, j, p, t, pnum, tnum, mx;
  pns* pn;
  ip = calloc(nprs, sizeof(*ip));

  for(i = 0; i < nprs; i++) {
    mx = 0;
    pn = prs[i]->pn;
    tnum = pn->tnum;
    pnum = pn->pnum;
    for(p = 0; p < pnum; p++) {
      for(t = 0, j = 0; t < tnum; t++)
	if(GetMatrixEl(&pn->out, p, t))
	  j++;
      if(j > mx) mx = j; // mx = (j > mx)?j:mx;
    }
    ip[i] = mx;
  }

  return ip;
}

/*
  int MaxSrcTranNum(process **prs, int nprs) {
  // Finds the max number of source transitions belonging to the same process
  // that have the same label 

  // Suboptimal implementation

  int i, j, l, m, t, pnum, tnum, mx;
  pns* pn;


  for(i = 0, mx = 0; i < nprs; i++) {
  pn = prs[i]->pn;
  tnum = pn->tnum;
  pnum = pn->pnum;
  for(t = 0; t < tnum; t++) {
  if(!is_source(pn, t))
  continue;
  l = get_label(pn, t);
  for(j = t+1, m = 1; j < tnum; j++) {
  if(l != get_label(pn, j))
  continue;
  if(!is_source(pn, j))
  continue;
  m++;
  }
  if(m > mx) mx = m;
  }
  }
  return mx;
  } 
*/


struct myinsert supDefineBlock(pns *sup, process **prs, int nprs, specs* sp, \
			       TrData** TrInfo, struct synclist *sl) {
  struct myinsert ins;
  int i, j, n, p, t, *mk, *ip, first;

  llist = 0;
  createLabels(sup, prs, nprs, sl, TrInfo); // creates a table of action labels
  // and writes the synchronization entries of TrInfo.

  ins = InitInsert(512); 

  if(sup) {
    ins = FSInsert(ins, "#define ___pnum %d\n", sup->pnum);
    ins = FSInsert(ins, "#define ___tnum %d\n", sup->tnum);
    //ins = FSInsert(ins, "const int ___out[][%d] = { \\\n", sup->tnum);
    //ins = insertMatrix(&sup->out, ",\\\n", ins); // for full representation
    //ins = SInsert("\\\n};\n", ins);
    /*
      ins = SInsert("const int ___out[][3] = ", ins);
      ins = cinsert2D(&sup->out, &j, ins);
      ins = SInsert(";\n", ins);
      ins = FSInsert(ins, "#define n___out %d//Number of rows of ___out\n", j);
      ins = SInsert("const int ___in[][3] = ", ins);
      ins = cinsert2D(&sup->in, &j,  ins);
      ins = SInsert(";\n", ins);
      ins = FSInsert(ins, "#define n___in %d // Number of rows of ___in\n", j);
    */
    if(sup->pnum) {
      if(!sup->marking) { // initialize it to zero
	ip = calloc(sup->pnum, sizeof(*ip));
	updatepn(sup, "m0", ip);
	free(ip);
      }
      ins = SInsert("const int ___m0[][2] = ", ins);
      ins = cinsert1D(sup->marking, sup->pnum, &j, ins);
      ins = SInsert(";\n", ins);
      ins = FSInsert(ins,"#define n___m0 %d // Number of rows of ___m0\n\n",j);
    }
    else {
      ins = SInsert("const int ___m0[][2] = {};\n", ins);
      ins = FSInsert(ins, "#define n___m0 0 // Number of rows of ___m0\n\n");
    }
  } // end of if(sup)
  else {
    ins = SInsert("#define ___pnum 0\n", ins);
    ins = SInsert("#define ___tnum 0\n", ins);
    ins = SInsert("const int ___m0[][2] = {};\n", ins);
    ins = FSInsert(ins, "#define n___m0 0 // Number of rows of ___m0\n\n");
  }
  /*  ins = SInsert("const int ___labels[] = { ", ins);
      if(!sup->t)
      merror(0, "The supervisor should be labeled!");
      for(i = 0; i < -1+sup->tnum; i++) 
      ins = FSInsert(ins, "%d, ", sup->t[i]);
      ins = FSInsert(ins, "%d };\n", sup->t[i]); */

  // Write the initial marking for each process type in the format
  // (type, place, nonzerovalue)

  ins = SInsert("const int ___pm0[][3] = {", ins);
  for(t = 0, n = 0, first = 1; t < nprs; t++) {
    mk = prs[t]->pn->marking;
    if(!mk)
      continue; 
    for(p = 0; p < prs[t]->pn->pnum; p++) {
      if(mk[p]) {
	n++;
	if(first) {
	  ins = FSInsert(ins, " { %d, %d, %d }", t, p, mk[p]);
	  first = 0;
	}
	else
	  ins = FSInsert(ins, ", { %d, %d, %d }", t, p, mk[p]);
      }
    }
  }
  ins = SInsert(" };\n", ins);
  ins = FSInsert(ins, "#define n___pm0 %d // Number of rows of ___pm0\n\n", n);
  if(!n)
    merror(0, "NEWCODEGEN: All plant PNs have zero initial marking!"); 


  // Writes the PN structure as an array
  ins = writeSPN(sup, ins);

  // Define the array of action labels
  ins = writeActions(sup, ins);

  // Find the number of supervisor transitions with zero label

  if(sup) {
    if(!sup->t)
      n = 0;
    else {
      ip = calloc(sup->tnum, sizeof(*ip));
      for(i = 0, n = 0; i < sup->tnum; i++)
	if(!sup->t[i].l) {
	  ip[n] = i;
	  n++;
	}
      if(n) {
	ins = FSInsert(ins, "#define ZERO_LABEL_TRANS %d\n", n);
	ins = SInsert("const int ___zltrans[ZERO_LABEL_TRANS] = ", ins);
	ins = insert1D(ip, n, ins);
	ins = SInsert(";\n\n", ins);
      }
      free(ip);
    }
  }

  // Define the array of process-type addresses

  if(!nprs)
    merror(0, "NEWCODEGEN: At least one process type should be defined");
  ins = FSInsert(ins, "#define n___prtypes %d // Number of process types\n",\
		 nprs);
  ins = SInsert("struct proc* ___wtlist[n___prtypes] = {", ins);
  for(i = 0; i < nprs-1; i++) 
    ins = SInsert(" 0,", ins);
  ins = SInsert(" 0};\n", ins);

  ins = SInsert("struct proc* ___wtlistLast[n___prtypes] = {", ins);
  for(i = 0; i < nprs-1; i++) 
    ins = SInsert(" 0,", ins);
  ins = SInsert(" 0};\n", ins);

  free_lstruct(llist);

  // Include define directives for threads and processes

  for(i = 0; i < nprs; i++)
    if(prs[i]->thread) {
      ins = SInsert("#define ___THREADS\n\n", ins);
      break;
    }
  for(i = 0; i < nprs; i++)
    if( ! prs[i]->thread) {
      ins = SInsert("#define ___PROCESSES\n\n", ins);
      break;
    }

  // Define the array of process-type names (names of executable files)
  // The name is given only for processes; the entries of threads are zero.

  ins = SInsert("const char* ___pname[] = {", ins);
  for(i = 0; i < nprs; i++) {
    if(prs[i]->name)
      if(strlen(prs[i]->name)) {
	if( ! prs[i]->thread )
	  ins = FSInsert(ins, " \"./%s.exe\"", prs[i]->name);
	else
	  ins = SInsert(" 0", ins);
	if(i == nprs - 1)
	  ins = SInsert(" };\n\n", ins);
	else
	  ins = CInsert(',', ins);
	continue;
      }
    merror(0, "NEWCODEGEN: Process type %d has no name!", i);
  }

  // Define the array of start-function addresses for threads; processes
  // have zero entries. 

  for(i = 0; i < nprs; i++) { // Declare the start functions first
    if( prs[i]->thread )
      ins = FSInsert(ins, "void* ___start_%s(void* v);\n", prs[i]->name);
  }

  ins = SInsert("\nvoid *(*___start_fn[]) (void *) = {", ins);
  for(i = 0; i < nprs; i++) {
    if( prs[i]->thread )
      ins = FSInsert(ins, " &___start_%s", prs[i]->name);
    else
      ins = SInsert(" 0", ins);
    if(i == nprs - 1)
      ins = SInsert(" };\n\n", ins);
    else
      ins = CInsert(',', ins);
  }

  // Find the max number of output transitions for each proc. type 

  ip = MaxOutpTranNum(prs, nprs);
  ins = SInsert("const int ___maxOutpTranNum[] = ", ins);
  ins = insert1D(ip, nprs, ins);
  ins = SInsert(";\n\n", ins);
  free(ip);
  
  if(MaxNo) { // determined by "writeActions" as the max value of the 'no' field
    ins = FSInsert(ins,"#define ___MASK %d\n", MaxNo);
    ins = SInsert("char ___mask[___MASK]; // Masked transitions are not fired\n\n",ins);
  }

  // Implement the settings of sp

  if(!(sp->nomain))
    ins = SInsert("#define ___MAIN_FUNCTION\n", ins);
  if(sp->signals)
    ins = SInsert("#define ___SIGNALS\n", ins);
  if(sp->singlechannel)
    ins = SInsert("#define SINGLE_READ_CHANNEL\n", ins);
  if(sp->sleep)
    ins = SInsert("#define ___SLEEP 2\n", ins);
  ins = SInsert("\n", ins);

  return ins;
}


void  WriteMakefile(FILE* f, char *mf, char* sn, process** prs, int n, \
		    const char* buildparam) {
  time_t currentTime;
  int i, *thr, nt, np;
  char* incl = "spcommon.h";

  if(inc_name)
    incl = inc_name;

  thr = calloc(n, sizeof(*thr));

  // Identify the threads; find nt, their number; find np, the number of 
  // processes (not threads) with user defined build commands.  

  for(i = 0, nt = 0, np = 0; i < n; i++) {
    if(prs[i]->thread) {
      thr[i] = 1;
      nt++;
    }
    else
      if(prs[i]->build)
	np++;
  }

  time(&currentTime); 
  fprintf(f, "# This is %s automatically generated on %s\n", mf,\
	  asctime(localtime(&currentTime)));
#ifndef ___USE_PTHREAD_LIB
  fprintf(f, "COMPILER=gcc -g\n\n");
#else
  fprintf(f, "COMPILER=gcc -g -pthread\n\n");
#endif

  // The rule for the supervisor program.
  // This rule is executed always, even if no changes are made.
  // This is in order to account for user defined makefiles, which
  // are executed also in this rule.

  fprintf(f, "# The following rule includes user defined build commands\n\n");

  fprintf(f, "all: %s.c %s", sn, incl);
  for(i = 0; i < n; i++) {
    if(prs[i]->build)
      fprintf(f, " %s.c", prs[i]->name);
    else {
      if(thr[i])
        fprintf(f, " %s.o", prs[i]->name);
      else
        fprintf(f, " %s.exe", prs[i]->name);
    }
  }
  for(i = 0; i < n; i++)
    if(prs[i]->build)
      fprintf(f, "\n\t%s", prs[i]->build);
#ifdef ___USE_PTHREAD_LIB
  fprintf(f, "\n\t$(COMPILER) -o %s.exe %s.c", sn, sn);
  // in this case -pthread option included in $(COMPILER)
#else
  fprintf(f, "\n\t$(COMPILER) -lpthread -o %s.exe %s.c", sn, sn);
#endif
  for(i = 0; i < n; i++) 
    if(thr[i])
      fprintf(f, " %s.o", prs[i]->name);
  if(buildparam)
      fprintf(f, " %s", buildparam);
  if(np) {
    fprintf(f, "\n\t# Checking whether user defined build commands have created the required");
    fprintf(f, "\n\t# files ...");
    for(i = 0; i < n; i++)
      if(!thr[i] && prs[i]->build)
	fprintf(f, "\n\twhich ./%s.exe", prs[i]->name);
    fprintf(f, "\n\t# All required files were found.");
  }

  // Here are the command lines for the remaining files

  fprintf(f, "\n\n# Default build commands follow");

  for(i = 0; i < n; i++) {
    if(prs[i]->build)
      continue; // This is taken in account in the supervisor rule

    // Generating default rules for the files that do not have user specified
    // build commands.

    if(thr[i]) {  
      fprintf(f, "\n\n%s.o: %s.c %s", prs[i]->name, prs[i]->name, incl);
      fprintf(f, "\n\t$(COMPILER) -c %s.c", prs[i]->name, prs[i]->name);
    }
    else {
      fprintf(f, "\n\n%s.exe: %s.c %s", prs[i]->name, prs[i]->name, incl);
#ifdef ___USE_PTHREAD_LIB
      fprintf(f, "\n\t$(COMPILER) -o %s.exe %s.c", prs[i]->name, prs[i]->name);
      // In this case -pthread option included in $(COMPILER)
#else
      fprintf(f, "\n\t$(COMPILER) -lpthread -o %s.exe %s.c", prs[i]->name, prs[i]->name);
#endif
    }
  }

  fprintf(f, "\n");
  free(thr);
}

void compileSupervisor(specs* sp, pns *supervisor, process **procTypes, \
		       int nbrTypes, TrData** TrInfo, struct synclist* sl) {

  FILE *supFile;
  char *fileName, *sname, *buildparam; 
  struct myinsert incl, pre;
  time_t currentTime;
  cblock bl;
  struct input in;

  inc_name = 0;
  sname = sp->name;
  buildparam = sp->sbuildparam;

  if(sp->templ) {
    in.file = searchTemplate(TEMPL); in.buf = 0;
    rewind(in.file);
  }
  else {
    in.file = 0; in.buf = SupervisorTemplate_c;
    // write spcommon.h
    asprintf(&inc_name, "%s__spcommon.h", sname);
    supFile = fopen(inc_name, "w"); 
    if(!supFile) 
      merror(0, "NEWCODEGEN: Unable to write %s", inc_name);
    time(&currentTime);
    fprintf(supFile, "// Automatically generated on %s\n\n", asctime(localtime(&currentTime)));
    fputs(spcommon_h, supFile);
    fclose(supFile);
  }
  fileName = GetFileName(sname, "c");
  supFile = fopen(fileName, "w");    
  if(!supFile) 
    merror(0, "NEWCODEGEN: Error creating supervisor file %s", fileName);
  else if(DBG3)
    printf("Created supervisor file %s\n", fileName);

  // Write header of file

  pre = InitInsert(128); 
  time(&currentTime); 
                
  pre = FSInsert(pre, "\
// This is %s generated from template %s.\n\
// %s\n\n", fileName, TEMPL, asctime(localtime(&currentTime)));
  pre = FSInsert(pre, "#define ___NAME \"%s\"\n", sname);

  incl = supDefineBlock(supervisor, procTypes, nbrTypes, sp, TrInfo, sl);

  // Write output file

  bl.text = GetInsertBuf(&incl); bl.file = 0;
  FillTemplate(in, supFile, fileName, inc_name, GetInsertBuf(&pre), bl, \
	       sp->include, sp->main);

  free(fileName); free(GetInsertBuf(&incl)); free(GetInsertBuf(&pre));
  fclose(supFile);

  if(sp->templ)
    fclose(in.file);

  // Write Makefile

  fileName = GetFileName(sname, "mak");
  supFile = fopen(fileName, "w");    
  if(!supFile) 
    merror(0, "NEWCODEGEN: Error creating makefile %s", supFile);
  else if(DBG3)
    printf("Created makefile %s\n", fileName);

  WriteMakefile(supFile, fileName, sname, procTypes, nbrTypes, buildparam);

  free(fileName); fclose(supFile);
}


/***************************************************************************
 GET_TRDATA
****************************************************************************/

TrData** get_TrData(pns *sr, process** prarray, int num, struct label_lst* llst) {
  // sr: pn of supervisor
  // num: number of process subtypes and also the number of rows of the result

  TrData** p, temp;
  int i, j, l, t, t1;
  char *scanned; //flag array indicating which transitions have been examined  
  char control, observe; //flags
  struct label_lst *pl;
  struct prlist *pr;
  struct ilist *pi;

  // Initialize p

  p = tcalloc(num, sizeof(*p));
  for(i = 0; i < num; i++)
    p[i] = tcalloc(prarray[i]->pn->tnum, sizeof(**p));

  if(!sr) return p; // if supervisor PN is empty
  if(!sr->t) return p; // if supervisor is unlabeled

  // Check all supervisor labels

  scanned = tcalloc(sr->tnum, sizeof(*scanned));
  for(t = 0; t < sr->tnum; t++) {
    if(scanned[t])
      continue;
    l = sr->t[t].l; // the current label
    if(!l)
      continue;

    // Determine what kind of control/observation is needed for this label

    for(t1 = t, control = 0, observe = 0; t1 < sr->tnum; t1++) {
      if(l != sr->t[t1].l)
	continue;
      scanned[t1] = 1;
      control |= !is_source(sr, t1); // suboptimal approach to find 'control'
      for(j = 0; j < sr->pnum; j++) {
	if(GetMatrixEl(&sr->out, j, t1) != GetMatrixEl(&sr->in, j, t1)) {
	  observe = 1;
	  break;
	}
      }
      if(control && observe)
	break;
    }

    // Write TrData for plant transitions having this label

    temp.flags = control + (observe<<1); // what will be written to TrData
    for(pl = llst; pl; pl = pl->next) {
      if(l > pl->l)
	continue;
      if(l < pl->l)
	break; // the label l is not in the list

      // lines below reached if l == pl->l

      for(pr = pl->pr; pr; pr = pr->next) { // for each process having the label
	for(pi = pr->itlist, j = pr->pr; pi; pi = pi->next)
	  p[j][pi->t] = temp;
	for(pi = pr->otlist; pi; pi = pi->next)
	  p[j][pi->t] = temp;
      }
      break;
    }
  }

  free(scanned);
  return p;
}


void free_TrData(TrData** p, int num) {
  // num: the number of rows of p, that is, the number of process subtypes.

  int i;
  for(i = 0; i < num; i++) 
    free(p[i]);
  free(p);
}


int CodeGenerator(pns *supervisor, specs* sp, process** prarray, int num,\
		  struct synclist* sl, TrData** TInf) {

  process* pr;
  int i, j, k, m;
  char *s;
  struct myinsert ins;

  if(!sp) {
    merror(0,"NEWCODEGEN: Empty specification object!"); 
    return 1;
  }

  // 2. Preprocess the array of prarray

  // 2.1. Update 'name' to correspond to the file name that will be
  // generated. 

  for(i = 0; i < num; i++) {
    pr = prarray[i];
    if(!pr->name)
      merror(0, "NEWCODEGEN: Process subtype %d has no name!", i);
    if(pr->instance) {
      asprintf(&s, "%s__%s", pr->name, pr->instance);
      free(pr->name);
      pr->name = s;
    }
  }

  // 2.2 Check that there are no repeated names

  for(i = 0; i < num; i++) {
    pr = prarray[i];
    for(j = i+1; j < num; j++)
      if(!strcmp(pr->name, prarray[j]->name))
	merror(0, \
	       "NEWCODEGEN: Process subtypes %d and %d have the same name, namely '%s'",\
	       i, j, pr->name);
  }

  // 2.3 Substitute __NAME_SYMBOL (defined in pns.h) with 'name' in 'build'

  for(i = 0, m = strlen(__NAME_SYMBOL); i < num; i++) {
    if(!prarray[i]->build)
      continue;
    s = prarray[i]->build;
    k = strlen(s);
    if(!k)
      continue;
    ins = InitInsert(64);
    for(j = 0; j < k; j++) {
      if(strncmp(s+j, __NAME_SYMBOL, m)) 
	ins = CInsert(s[j], ins);
      else {
	ins = SInsert(prarray[i]->name, ins);
	j += m-1; // -1 because of subsequent j++ in for loop
      }
    }
    free(s);
    prarray[i]->build = GetInsertBuf(&ins);
  }

  // 3. Generate the code. 

   compileSupervisor(sp, supervisor, prarray, num, TInf, sl);
   compileProcessArray(sp, prarray, num, TInf, plabels); 
   // plabels is generated by compileSupervisor

  // Free data

  for(i = 0; i < num; i++)
    free(plabels[i]);
  free(plabels);

  if(inc_name) // initialized in compileSupervisor
    free(inc_name);

  return 0;
}
