// TO DO:
// - The program does not give an error when in format2.hl 
//   the line "p1.p1.select { p1_select(___TR); ..." is replaced with
//   "p1.p1.select { p1_select(___TR); // ___TR: defined in context of call }" 
// - To check that var strings are deallocated
// - The program does not check if C blocks are defined twice for the same
//   place.

#include"read.h"

static unsigned int errors; // indicates the number of errors

unsigned char first_pass; 

static struct pa_proc *first_pr; // first process in process chain

static variable *first_var; 
// first variable in the inequality variable chain that is presently considered

static constraint *last_cnstr; // last constraint added to the specification

static struct pa_proc *last_pr; // last process in process chain

extern int parseline; // defined in read.lex

static int pr_num; // the number of process variables

static inequality *pres_ineq; // the inequality that is presently built

static struct pa_proc *pres_pr; 
// the process that is presently under consideration

static variable *pres_var; 
// the inequality variable that is presently considered

static int pres_var_coef; // inequality variable coefficient

static enum var_type pres_vartype; 
// stores present specification variable type

static specs* sp; // the specification object that is built

static char* spec_name;

static struct dict variables; // stores variable names




////////////////////////////////////////////////////////////////////////////
// ADD_ARC
////////////////////////////////////////////////////////////////////////////

void add_arc(struct rvalue *s1, struct rvalue *s2, struct rvalue *s3, \
	     struct rvalue *condition) {
// Processes the instructions that add arcs. 
// In the first pass it checks for errors. 
// In the second pass it creates an "arcs" object and adds it to the pn of the
// current process.

  char flag = 0; // error flag (currently not used)
  struct dictree* y;
  struct pa_var* v;
  arcs *a;
  int t;
  char* s;

  if(!pres_pr) {
    report_error(s1->line, "the arc definition \"(%s, %s ...\"  is not within a process block", s1->p, s2->p);
    return;
  }

  if(first_pass) { // check whether variables are defined
    if(s3 && s2) { // then the format is (place, transition, place)

      if(registered_place(s1->p) < 0) {
	report_error(s1->line, "the place \"%s\" in the arc definition \"(%s, %s ...\" has not been defined", s1->p, s1->p, s2->p);
	flag = 1;
      }

      if(registered_transition(s2->p) < 0) {
	report_error(s2->line, "the transition \"%s\" in the arc definition \"(%s, %s ...\" has not been defined", s2->p, s1->p, s2->p);
	flag = 1;
      }

      if(registered_place(s3->p) < 0) {
	report_error(s3->line, "the place \"%s\" in the arc definition \"(%s, %s ...\" has not been defined", s3->p, s1->p, s2->p);
	flag = 1;
      }

    }

    else if(!s2) { // then the format is "state to state"

      // The lines below are useful if a line 's1 to s2' should generate an
      // error if s1 and s2 have not been predefined. 

      /*
      if(registered_place(s1->p) < 0) {
	report_error(s1->line, "the state \"%s\" in the definition \"%s to %s\" has not been defined", s1->p, s1->p, s3->p);
	flag = 1;
      }
 
     if(registered_transition(s3->p) < 0) {
	report_error(s3->line, "the state \"%s\" in the definition \"%s to %s\" has not been defined", s3->p, s1->p, s3->p);
	flag = 1;
      }

     if(flag)
       return;
      */

      // Include variables in list of variables (unless already defined).

      add_var_sub(s1->p, s1->line, PLACE, 0);
      add_var_sub(s3->p, s3->line, PLACE, 0);

      // Add default transition name to the set of variables

      s = default_tname(s1->p, s3->p);
      add_var_sub(s, s1->line, TRANS, 1);
      free(s);
    }

    else { // then the format is (place, transition) or (transition, place)

      y = dic_lookup(s1->p, pres_pr->var.root);
      if(!y) {
	report_error(s1->line, "the variable \"%s\" in the arc definition \"(%s, %s)\" has not been defined", s1->p, s1->p, s2->p);
	flag = 1;
      }
      else {
	v = (struct pa_var*) (y->data);
	if(v->type == PLACE) {
	  if(registered_transition(s2->p) < 0) {
	    report_error(s2->line, "the transition \"%s\" in the arc definition \"(%s, %s)\" has not been defined", s2->p, s1->p, s2->p);
	    flag = 1;
	  }
	}
	else if(v->type == TRANS) {
	  if(registered_place(s2->p) < 0) {
	    report_error(s2->line, "the place \"%s\" in the arc definition \"(%s, %s)\" has not been defined", s2->p, s1->p, s2->p);
	    flag = 1;
	  }
	}
	else {
	    report_error(s1->line, "the variable \"%s\" in the arc definition \"(%s, %s)\" is neither a place nor a transition", s1->p, s1->p, s2->p);
	    flag = 1;
	}
      }
    }
    if(s1)
      free(s1->p);
    if(s2)
      free(s2->p);
    if(s3)
      free(s3->p);
    return;
  }

  // Insert the arc into the pn 

  if(!first_pass) {
    a = tcalloc(1, sizeof(*a));
    if(condition) {
      a->condition.text = condition->p;
      a->condition.line = condition->line;
    }
    if(s3 && s2) { // then the format is (place, transition, place)
      a->in_place = registered_place(s1->p);
      a->out_places = tcalloc(1, sizeof(*(a->out_places)));
      a->out_places->place = registered_place(s3->p);
      t = registered_transition(s2->p);
    }
    else if(!s2) { // then the format is "state to state"
      a->in_place = registered_place(s1->p);
      a->out_places = tcalloc(1, sizeof(*(a->out_places)));
      a->out_places->place = registered_place(s3->p);
      s = default_tname(s1->p, s3->p);
      t = registered_transition(s);
      free(s);
    }
    else { // then the format is (place, transition) or (transition, place)
      y = dic_lookup(s1->p, pres_pr->var.root);
      v = (struct pa_var*) (y->data);
      if(v->type == PLACE) { // case (place, transition)
	a->in_place = registered_place(s1->p);
	t = registered_transition(s2->p);
      }
      else { // case (transition, place)
	t = registered_transition(s1->p);
	a->in_place = -1;
	a->out_places = tcalloc(1, sizeof(*(a->out_places)));
	a->out_places->place = registered_place(s2->p);
      }
    }
    if(t < 0)
      merror(0, "Internal error in ADD_ARC function of parser: t = %d", t);
    updatepn(sp->process_array[pres_pr->id]->pn, "arcs", t, a);
    if(s1)
      free(s1->p);
    if(s2)
      free(s2->p);
    if(s3)
      free(s3->p);
  }
}


////////////////////////////////////////////////////////////////////////////
// ADD_C_BLOCK
////////////////////////////////////////////////////////////////////////////

void add_c_block(struct rvalue proc, struct rvalue place, \
		 struct rvalue block, char type) {
// If type = 'i', associates to 'place' of the process 'proc' the embedded 
// instructions of 'block'.
// If type = 's', associates to 'place' of the process 'proc' the select
// function call of 'block'.)

  struct pa_var* v;
  int p;
  struct pa_proc* pr;

  v = is_process(proc.p, proc.line);

  if(!v)
    return;

  if(v->pr->supervisor) {
    report_error(proc.line, "'%s' was defined as a supervisor component. A supervisor component does not support code for its places.", proc.p);
    return;
  }
  pr = pres_pr;
  pres_pr = v->pr;
  p = registered_place(place.p);
  pres_pr = pr;
  if(p < 0)  {
    report_error(place.line, "Undefined place '%s'", place.p);
    return;
  }

  if(first_pass)
    return;

  // second pass instructions follow

  if(type == 'i')
    updatepn(sp->process_array[v->pr->id]->pn, "segment", p, block.line, block.p);
  if(type == 's')
    updatepn(sp->process_array[v->pr->id]->pn, "select", p, block.line, block.p);
}


////////////////////////////////////////////////////////////////////////////
// ADD_INEQ
////////////////////////////////////////////////////////////////////////////

void add_ineq(struct rvalue in1, struct rvalue in2, int type) {
// Adds a constraint of the form 'in1' [ = | <= | < ] 'in2'.
// It has no effect in the first pass.

  int line;
  inequality *i1, *i2;
  variable *var, *nvar;
  constraint *c, *c2;

  if(first_pass)
    return;

  line = (in1.line > in2.line) ? in2.line : in1.line;

  if(!type) {
    report_error(line, "Equality constraints are not supported");
    return;
  }

  i1 = (inequality*) (in1.v);
  i2 = (inequality*) (in2.v);

  if(type > 1)  // If this is a strict inequality
    i1->free_term = -1 - i1->free_term + i2->free_term;
  else
    i1->free_term = - i1->free_term + i2->free_term;

  for(var = i2->variable_list; var; var = nvar) {
    nvar = var->next;
    set_ineq_sub(i1, var, 1); // may deallocate var
  }
  free(i2);

  if(!i1->variable_list) {
    report_error(line, "The constraint has no variables or the variables cancel each other");
    return;
  }

  // add inequality to specification

  c = tcalloc(1, sizeof(*c));
  c->expr = tcalloc(1, sizeof(*(c->expr)));
  c->expr->left_ineq = i1;
  if(sp->constraint_list) // if so, then last_cnstr has a valid value
    last_cnstr->next = c;
  else // if c is the first constraint
    sp->constraint_list = c;
  last_cnstr = c;
}

////////////////////////////////////////////////////////////////////////////
// ADD_INEQ_VAR
////////////////////////////////////////////////////////////////////////////

struct rvalue add_ineq_var(struct rvalue *pr, struct rvalue *v2,\
			   struct rvalue *v3) {
// Creates an object for an inequality variable during the second pass.
// It checks variable names during the first pass.

  struct dictree* y;
  struct pa_var* v;
  struct pa_proc* p;
  unsigned char type;
  int place = -1, trans = -1; 
  struct rvalue res;
  variable *pv;

  memset(&res, 0, sizeof(res));

  // Check whether the process variable was defined

  y = dic_lookup(pr->p, variables.root);
  if(!y) {
    report_error(pr->line, "Undefined process '%s'", pr->p);
    return res;
  }
  v = (struct pa_var*) y->data;
  if(v->type != PROC) {
    report_error(pr->line, "'%s' was not defined as a process (see line %d)", pr->p, v->line);
    return res;
  }

  // Check whether the place or transition variable was defined

  p = pres_pr;
  pres_pr = v->pr;
  if(v3) { // then the variable is in v3
    place = registered_place(v3->p);
    if(place < 0)
      trans = registered_transition(v3->p);
  }
  else { // then the variable is in v2
    place = registered_place(v2->p);
    if(place < 0)
      trans = registered_transition(v2->p);
  }
  pres_pr = p;

  if(place < 0 && trans < 0)  {
    if(v3) 
      report_error(v3->line, "in '%s.%s.%s': '%s' is neither a place nor a transition of the process '%s'", pr->p, v2->p, v3->p, v3->p, pr->p);
    else 
      report_error(v2->line, "in '%s.%s': '%s' is neither a place nor a transition of the process '%s'", pr->p, v2->p, v2->p, pr->p);
    return res;
  }

  type = MARKINGV; // set the default variable type

  // Check the second parameter when the format proc.option.var is used

  if(v3) {
    if(trans > 0)
      type = FIRINGV;

    // check the type of v2

    if(!strcmp(v2->p, "v")) 
      type = PARIKHV;
    else if(!strcmp(v2->p, "q")) 
      type = FIRINGV;
    else if(!strcmp(v2->p, "m")) 
      type = MARKINGV;
    else {
      report_error(v2->line, "the '%s' option in '%s.%s.%s' is not supported", v2->p, pr->p, v2->p, v3->p);
      return res;
    }

    // check settings

    if(trans < 0 && type != MARKINGV) {
      report_error(v3->line, "in '%s.%s.%s': '%s' must be a transition of the process '%s'", pr->p, v2->p, v3->p, v3->p, pr->p);
      return res;
    }

    if(place < 0 && type == MARKINGV) {
      report_error(v3->line, "in '%s.%s.%s': '%s' must be a place of the process '%s'", pr->p, v2->p, v3->p, v3->p, pr->p);
      return res;
    }
  }  // end of if(v3)

  if(first_pass) 
    return;

  // the following lines reached only in the second pass

  pv = tcalloc(1, sizeof(*pv));
  pv->type = type;
  pv->pn = sp->process_array[v->pr->id]->pn;
  pv->index = (place < 0) ? trans : place;
  res.v = pv;
  res.line = pr->line;
  res.lastline = (v3 != 0) ? v3->lastline : v2->lastline;
  return res;
}



////////////////////////////////////////////////////////////////////////////
// ADD_VAR
////////////////////////////////////////////////////////////////////////////


struct pa_var* add_var_sub(char *name, int line, enum var_type type, char f) {
  struct dictree *y;
  struct pa_var *v;
  int r;

  if(!first_pass)
    return 0; // nothing to do

  r = dic_insert(name, strlen(name), DFLT_NODE_TYPE, 0, &y, &(pres_pr->var));
  if(!r) {
    if(f)
      report_error(line, "the variable \"%s\" has been defined already on line %d.", name, ((struct pa_var*)(y->data))->line);
    return 0;
  }
  v = szalloc(&(pres_pr->var.mem), sizeof(struct pa_var));
  v->type = type;
  v->line = line;
  if(type == TRANS) {
    v->id = pres_pr->tnum;
    pres_pr->tnum++;
  }
  else if(type == PLACE) {
    v->id = pres_pr->pnum;
    pres_pr->pnum++;
  }
  y->data = v;
  return v;
}


struct pa_var* add_var(struct rvalue s) {
  struct dictree *y;
  struct pa_var *v;
  int r;

  if(!first_pass)
    return 0; // nothing to do
  if(!pres_pr) {
    report_error(s.line, "the variable \"%s\" is not defined in a process context", s.p);
    return 0;
  }
  if(pres_vartype == NONE) {
    report_error(s.line, "cannot determine the type of the variable \"%s\"", s.p);
    return 0;
  }

  v = add_var_sub(s.p, s.line, pres_vartype, 1);
  free(s.p);
  return v;
}


////////////////////////////////////////////////////////////////////////////
// ADD_VARIABLE
////////////////////////////////////////////////////////////////////////////


struct pa_var* add_var2(struct pa_proc *pr, char *name, int line, \
			enum var_type type, char fl, struct pa_var** dfn, \
			struct pa_var* ref) {
// Subroutine of add_variable and copy_process. 
// This function is meant for the first pass.
// It adds a variable to the process pr, if pr is nonzero. Otherwise, the
// variable is added to the default process. Otherwise, if there is no
// default process, the variable is added to the list of global variables.
// If 'ref' != 0 then, the variable is added with
// the id given by 'ref'. (This is useful when copying a process to another.) 
// If the variable is already defined and defn != 0, then *defn is set to the
// entry of the variable. The return value is 0 if there is an error, or the
// entry added to the variable list. An attempt to add an already defined 
// variable is an error. 
// Errors are reported if 'fl' is nonzero. 'line' denotes the line on which
// the variable 'name' is defined. Error checking includes whether variables
// are defined in the proper context (such as transitions and places in the
// context of a process).

  struct dictree *y;
  struct pa_var *v;
  struct pa_proc *proc;
  struct dict *d;
  int r;
 
  if(dfn)
    *dfn = 0; // initialize dfn

  if(!first_pass)
    return 0; // nothing to do

  proc = pr;
  if(!pr)
    proc = pres_pr;

  if(proc) {
    if(type == PROC) {
      if(fl)
	report_error(line, "the process \"%s\" is defined in the context of process \"%s\". Nested process definitions are not supported.", name, proc->name);
      return 0; 
    }
    d = &(proc->var);
  }
  else {
    if(type == TRANS || type == PLACE) {
      if(fl)
	report_error(line, "the variable \"%s\" is not defined within a process block. Place and transition declarations must be made inside of a process block.", name);
      return 0; 
    }
    d = &variables;
  }

  r = dic_insert(name, strlen(name), DFLT_NODE_TYPE, 0, &y, d);
  if(!r) {
    if(fl)
      report_error(line, "the variable \"%s\" has been defined already on line %d.", name, ((struct pa_var*)(y->data))->line);
    if(dfn)
      *dfn = (struct pa_var*)(y->data);
    return 0;
  }
  v = szalloc(&(d->mem), sizeof(struct pa_var));
  v->type = type;
  v->line = line;
  if(type == TRANS) {
    if(ref)
      v->id = ref->id;
    else {
      v->id = proc->tnum;
      proc->tnum++;
    }
  }
  else if(type == PLACE) {
    if(ref)
      v->id = ref->id;
    else {
      v->id = proc->pnum;
      proc->pnum++;
    }
  }
  y->data = v;
  return v;
}


inline struct pa_var* add_variable(struct pa_proc *pr, char *name, int line, \
			    enum var_type type, char fl, struct pa_var** dfn) {
  return add_var2(pr, name, line, type, fl, dfn, 0);
}

////////////////////////////////////////////////////////////////////////////
// COMMIT_CONSTRAINT
////////////////////////////////////////////////////////////////////////////

void commit_constraint() {
  if(first_pass)
    return;
  pres_ineq = 0;
  pres_var = 0;
  first_var = 0;
}



////////////////////////////////////////////////////////////////////////////
// COMMIT_PROCESS
////////////////////////////////////////////////////////////////////////////

struct pa_proc* define_process(int type, struct rvalue s) {
  // Subroutine of commit_process and copy_process

  struct dictree *y;
  struct pa_proc *p;
  struct pa_var *v;
  process *pr;

  int r;

  if(pres_pr) {
      report_error(s.line, "\"%s\" is defined within the definition of \"%s\". Nested process definitions are not supported.", s.p, pres_pr->name);
      return 0;
  }

  r = dic_insert(s.p, strlen(s.p), DFLT_NODE_TYPE, 0, &y, &variables);

  if(first_pass) {
    if(!r) {
      report_error(s.line, "the process \"%s\" has been defined already on line %d.", s.p, ((struct pa_var*)(y->data))->line);
      return 0;
    }
    // Allocate and add new process

    p = szalloc(&(variables.mem), sizeof(struct pa_proc));
    v = smalloc(&(variables.mem), sizeof(struct pa_var));
    v->type = PROC;
    v->pr = p;
    v->line = s.line;
    y->data = v;
    if(last_pr)
      last_pr->next = p;
    last_pr = p;
    if(!first_pr)
      first_pr = p;
    p->id = pr_num;
    p->name = s.p; // s.p already allocated in read.lex
    p->thread = (type == 1);
    p->supervisor = (type == 2);
    init_dict(p->var);
    pr_num++; // increment the number of processes
  }
  else {
    p = ((struct pa_var*) (y->data))->pr;
    pr = tcalloc(1, sizeof(*pr));
    pr->pn = tcalloc(1, sizeof(*(pr->pn)));
    asprintf(&(pr->file), "%s", spec_name);
    asprintf(&(pr->name), "%s", sp->name);
    asprintf(&(pr->instance), "%s", p->name);
    pr->thread = (type == 1);
    pr->supervisor = (type == 2);
    sp->process_array[p->id] = pr;
  }
  return p;
}



void commit_process(int type, struct rvalue s) {
  struct pa_proc *p;
  process *pr;

  p = define_process(type, s);

  if(!p)
    return;

  pres_pr = p;

  if(!first_pass) {
    pr = sp->process_array[p->id];
    *(pr->pn) = createpn("pnum tnum", p->pnum, p->tnum);
  }
}


char* default_tname(char *p1, char *p2) {
// Creates a transition name for unnamed transitions based on the names of 
// of the states it connects.
  char* s;

  asprintf(&s, "%s__to__%s", p1, p2);

  return s;
}


////////////////////////////////////////////////////////////////////////////
// COPY_PROCESS
////////////////////////////////////////////////////////////////////////////

void copy_process(int type, struct rvalue src, struct rvalue dst) {
// 'src' describes the source (an already defined process) and 'dst' the
// new process of type 'type' to which 'src' should be copied. 
// If 'type' < 0, 'dst' will have the same type as 'src'. The function
// copies the PN structure (2nd pass), the variables (excepting certain  
// internal variables) (1st pass), and the specification fields (2nd pass). 
// It does not copy or update constraints affecting 'src'. 

  struct pa_var *vsrc, *v, *v2;
  struct pa_proc *psrc, *p;
  process *pr, *prs;
  char *str;
  struct dictree *y;

  vsrc = is_process(src.p, src.line); // checks also for errors

  if(!vsrc)
    return;

  psrc = vsrc->pr;
  if(type < 0) // then use the type of src
    type = (psrc->thread != 0) + 2*(psrc->supervisor != 0);

  p = define_process(type, dst); // checks also for errors

  if(!p)
    return;

  if(first_pass) { // initialize fields of p not initialized by define_process
    // copy pnum and tnum
    p->pnum = psrc->pnum; p->tnum = psrc->tnum; 
    // copy variables
    str = tmalloc(psrc->var.maxlen*sizeof(*str));
    str[0] = 0;
    next_entry(0,0); // reset next_entry()
    while(1) {
      y = next_entry(str, &(psrc->var));
      if(!y)
	break;
      v = (struct pa_var*) y->data;
      if(!strcmp("___init", str)) continue;
      if(!strcmp("___build", str)) continue;
      if(!strcmp("___include", str)) continue;
      if(!strcmp("___main", str)) continue;
      add_var2(p, str, v->line, v->type, 0, &v2, v);
    }
    free(str);
  }

  if(!first_pass) { // copy psrc data to specification
    pr = sp->process_array[p->id];
    *(pr->pn) = copypn(sp->process_array[psrc->id]->pn); // copy the pn
    updatepn(pr->pn, "m0", 0); // reset the marking
    prs = sp->process_array[psrc->id];
    if(prs->build && pr->thread == prs->thread && \
       pr->supervisor == prs->supervisor)
      asprintf(&(pr->build), "%s", prs->build);
    if(prs->include.text) {
      asprintf(&(pr->include.text), "%s", prs->include.text);
      if(prs->include.file)
	asprintf(&(pr->include.file), "%s", prs->include.file);
      pr->include.line = prs->include.line;
    }
    if(prs->main.text) {
      asprintf(&(pr->main.text), "%s", prs->main.text);
      if(prs->main.file)
	asprintf(&(pr->main.file), "%s", prs->main.file);
      pr->main.line = prs->main.line;
    }
    if(prs->file)
      asprintf(&(pr->file), "%s", prs->file);
  }
}


////////////////////////////////////////////////////////////////////////////
// FREE_RVLCHAIN
////////////////////////////////////////////////////////////////////////////

void free_rvlchain(struct qalloc *p) {

  struct rvl_chain *y;
  int i;

  while(1) {
    y = (struct rvl_chain*) next_in_line(p);
    if(!y) break;
    if(y->alloc)
      free(y->rvl.p);
  }

  qfree(p);
}



////////////////////////////////////////////////////////////////////////////
// INCLUDE_ADDITIONAL_VARIABLES
////////////////////////////////////////////////////////////////////////////

static void include_additional_variables() {
// Must be called ONLY after the 'include' field of the proc array and the
// PN data have been written to the array.
//
// Enhances the include blocks of the process array with additional
// constants/variables which may be useful for developing the user code.

  int i, j;
  process **ar, *pr;
  struct pa_proc *psrc;
  char *str;
  struct dictree *y;
  struct pa_var *v;
  struct myinsert ins;

  if(!sp) return;
  ar = sp->process_array;
  if(!ar) return;

  for(i = 0; i < sp->process_num; i++) {
    pr = ar[i];
    if(!pr) continue;
    if(!pr->pn || !pr->instance) continue;

    // Add transition names if select functions have been defined

    if(pr->pn->select && pr->pn->tnum >= 1) {
      y = dic_lookup(pr->instance, variables.root);
      if(!y) continue;
      v = (struct pa_var*) y->data;
      if(v->type != PROC) continue; 
      psrc = v->pr;
      str = tmalloc(psrc->var.maxlen*sizeof(*str));
      str[0] = 0;
      ins = InitInsert(512);
      ins = SInsert("enum ___tr_names {", ins);
      next_entry(0,0); // reset next_entry()
      while(1) {
         y = next_entry(str, &(psrc->var));
	 if(!y)
	   break;
	 v = (struct pa_var*) y->data;
	 if(v->type != TRANS)
	   continue;
	 ins = FSInsert(ins, " ___%s = %d,", str, v->id);
      }
      ins = SInsert("};\n", ins);
      pr->dfns = GetInsertBuf(&ins);
      free(str);
    } // end of if(pr->pn->select)
  }
}



////////////////////////////////////////////////////////////////////////////
// INIT_PVAR
////////////////////////////////////////////////////////////////////////////

void init_pvar(struct rvalue proc, struct rvalue list) {
// Does error checking during the first pass.
// Initializes the marking vector of the process variable during the second
// pass.

  struct pa_var *pvar, *v2;
  struct pa_proc *pv;
  struct rvl_chain *r;
  int place, *marking;

  pvar = is_process(proc.p, proc.line); // also reports errors
  if(!pvar) {
    free_rvlchain((struct qalloc*) (list.v));
    free((struct qalloc*) (list.v));
    return;
  }
  pv = pvar->pr;
  if(first_pass) { //IMPORTANT! Renaming "___init" affects copy_process()
    add_variable(pv, "___init", proc.line, INTG, 0, &v2);
    if(v2) {
      report_error(proc.line, "\"%s\" was also initialized on line %d", pv->name, v2->line);
      free_rvlchain((struct qalloc*) (list.v));
      free((struct qalloc*) (list.v));
      return;
    }
  }
  else // i.e. if(!first_pass)
    marking = tcalloc(pv->pnum, sizeof(*marking));
    
  while(1) { // Check the variables in list
    // Take first the VAR element
    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v));
    if(!r)
      break;
    place = is_var(pv, r->rvl, PLACE);
    free(r->rvl.p);
    // Next take the INTEGER element 
    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v));
    if(!first_pass) 
      marking[place] = r->rvl.i;
  }

  if(!first_pass) {
    updatepn(sp->process_array[pv->id]->pn, "m0", marking);
    free(marking);
  }

  qfree((struct qalloc*) (list.v));
  free((struct qalloc*) (list.v));
}



////////////////////////////////////////////////////////////////////////////
// INSERT_COMMAND
////////////////////////////////////////////////////////////////////////////

void insert_command(struct rvalue *proc, struct rvalue type, \
		    struct rvalue block) {
// Inserts in the specification object one of the following (as selected
// by 'type'): a build, include, or main command.
// During the first pass it checks for errors.

  struct pa_var *v, *v2;
  struct pa_proc* pv = 0;
  char *varname, *command, **cwhere;
  cblock *where = 0;
  process *pr = 0;

  if(proc) {
    v = is_process(proc->p, proc->line); 
    if(!v)
      return;
    pv = v->pr;
    if(!first_pass)
      pr = sp->process_array[pv->id];
  }

  // IMPORTANT! Changes to variable names affect copy_process()

  switch(type.i) {
  case 0: 
    varname = "___build";
    command = "build";
    if(pr)
      cwhere = &(pr->build);
    else 
      cwhere = &(sp->sbuildparam);
    break;
  case 1:
    varname = "___include";
    command = "include";
    if(pr)
      where = &(pr->include);
    else
      where = &(sp->include);
    break;
  case 2:
    varname = "___main";
    command = "main";
    if(pr)
      where = &(pr->main);
    else
      where = &(sp->main);
    break;
  default:
    return; // this is an error
  }

  if(first_pass) {
    add_variable(pv, varname, type.line, INTG, 0, &v2);
    if(v2) 
      report_error(type.line, "the %s command has been written already on line %d", command, v2->line);
    return;
  }

  // lines reached only in the second pass
  if(where) {
    cwhere = &(where->text);
    where->line = block.line;
    asprintf(&(where->file), "%s", spec_name);
  }
  if(*cwhere)
    free(*cwhere);
  *cwhere = block.p;
}

////////////////////////////////////////////////////////////////////////////
// IS_PROCESS
////////////////////////////////////////////////////////////////////////////

struct pa_var* is_process(char* name, int line) {
  struct dictree* y;
  struct pa_var* v;

  y = dic_lookup(name, variables.root);
  if(!y) {
    report_error(line, "Undefined process '%s'", name);
    return 0;
  }
  v = (struct pa_var*) y->data;
  if(v->type != PROC) {
    report_error(line, "'%s' was not defined as a process (see line %d)", name, v->line);
    return 0;
  }
  return v;
}



////////////////////////////////////////////////////////////////////////////
// IS_VAR
////////////////////////////////////////////////////////////////////////////


int is_var(struct pa_proc *pr, struct rvalue name, enum var_type type) {
  // Checks whether 'name' is a variable of the type 'type' of the process 'pr'.
  // Returns its id. Otherwise, if it is not defined, it returns -1 and reports
  // an error. If pr == 0, pres_pr is used instead of pr.

  struct dictree* y;
  struct pa_var* v;

  if(!pr) {
    if(!pres_pr) {
      report_error(name.line, "the variable \"%s\" does not appear in the context of a process", name.p);
      return -1;
    }
    pr = pres_pr;
  }

  y = dic_lookup(name.p, pr->var.root);
  if(!y) {
    report_error(name.line, "\"%s\" is not a variable of the process \"%s\"", name.p, pr->name);
    return -1;
  }

  v = (struct pa_var*) (y->data);
  if(v->type == type)
    return v->id;

  switch(type) {
  case PLACE:
    report_error(name.line, "\"%s\", as defined on line %d, is not a place of the process \"%s\"", name.p, v->line, pr->name);
    break;
  case TRANS:
    report_error(name.line, "\"%s\", as defined on line %d, is not a transition of the process \"%s\"", name.p, v->line, pr->name);
    break;
  default:
    report_error(name.line, "the type of \"%s\" on line %d is inconsistent with the type expected on this line", name.p, v->line);
  }
  return -1;

}


////////////////////////////////////////////////////////////////////////////
// LIVE_TRANS
////////////////////////////////////////////////////////////////////////////

void live_trans(struct rvalue type, struct rvalue list) {
  // Does error checking during the first pass.
  // Updates transition attributes during the second pass.

  struct pa_var *pvar;
  struct pa_proc *pv;
  struct rvl_chain *r;
  int trans;
  char *text;

  switch(type.i) {
  case 0: text = "live"; break;
  case 1: text = "uncontrollable"; break;
  case 2: text = "unobservable"; break;
  }

  while(1) { // Check the variables in list

    // Take first the VAR element (the process)

    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v));
    if(!r)
      break;
    pvar = is_process(r->rvl.p, r->rvl.line); // also reports errors
    if(!pvar) {
      free_rvlchain((struct qalloc*) (list.v));
      free((struct qalloc*) (list.v));
      return;
    }
    pv = pvar->pr;
    free(r->rvl.p);

    // Next take the second VAR element (the transition)

    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v)); 
    trans = is_var(pv, r->rvl, TRANS); // takes care of errors
    free(r->rvl.p);
    if(!first_pass) // second pass not reached if there are errors
      updatepn(sp->process_array[pv->id]->pn, text, trans);
  }

  qfree((struct qalloc*) (list.v));
  free((struct qalloc*) (list.v));
}


////////////////////////////////////////////////////////////////////////////
// RELEASE_PROCESS
////////////////////////////////////////////////////////////////////////////

void release_process() {
  pres_pr = 0;
}


////////////////////////////////////////////////////////////////////////////
// REGISTERED_VAR
////////////////////////////////////////////////////////////////////////////

int registered_var(char* name, enum var_type type) {
  // If the variable is found (in the context of the current process) with the 
  // correct type, the function returns its id. Otherwise, it returns -1. 
 
  struct dictree* y;
  struct pa_var* v;

  if(!pres_pr)
    return -1;

  y = dic_lookup(name, pres_pr->var.root);
  if(!y) 
    return -1;

  v = (struct pa_var*) (y->data);
  if(v->type == type)
    return v->id;
  return -1;
}


////////////////////////////////////////////////////////////////////////////
// REPORT_ERROR
////////////////////////////////////////////////////////////////////////////

#define MAX_ERRORS 10

void report_error(int line, char* str, ...) {
  va_list param;

  errors++;
  if(errors > MAX_ERRORS)
    return;
  if(line == 0)
    fprintf(stderr, "%s: error on line %d or above: ", spec_name, parseline);
  else if(line > 0)
    fprintf(stderr, "%s: error on line %d: ", spec_name, line);
  else
    fprintf(stderr, "%s: error: ", spec_name);
  va_start(param, str);
  vfprintf(stderr, str, param);
  va_end(param);
  fprintf(stderr, "\n");
}


////////////////////////////////////////////////////////////////////////////
// RVALUE_LIST
////////////////////////////////////////////////////////////////////////////


struct rvalue rvalue_list(struct rvalue* v, struct rvalue var, \
			  struct rvalue intg, char alloc) {
  // The function updates (or creates if v = 0) a chain of struct rvalue objects.
  // Thus, it adds 'var' and 'intg' to the begining of the chain in v->v. 
  // It returns the updated v. 

  struct rvalue res;
  struct qalloc *q;
  struct rvl_chain *p;

  if(!v) {
    q = tcalloc(1, sizeof(*q));
    initqalloc(q, 10, sizeof(*p)); 
  }
  else 
    q = (struct qalloc*) v->v;

  p = (struct rvl_chain*) place_in_line(q);
  p->rvl = var;
  p->n = 1;
  p->alloc = 1; // since it is a variable
  p = (struct rvl_chain*) place_in_line(q);
  p->rvl = intg;
  p->n = 0;
  p->alloc = alloc; 

  res.v = q;
  return res;
}


////////////////////////////////////////////////////////////////////////////
// SET_COEF
////////////////////////////////////////////////////////////////////////////

struct rvalue set_coef(int coef, struct rvalue var, int line, int lastline) {
  // Returns an updated 'var' containing the coefficient information.
  // The function has almost no effect in the first pass.

  var.line = line;
  var.lastline = lastline;
  if(first_pass)
    return var;
  ((variable*)(var.v))->coefficient = coef;
  return var;
}


////////////////////////////////////////////////////////////////////////////
// SET_FREE_TERM
////////////////////////////////////////////////////////////////////////////

struct rvalue set_free_term(struct rvalue term) {
  // The function initializes the v field of the result with a pointer to a 
  // 'variable' object in which the pn field is 0 (to indicate the free term).
  // The function has almost no effect in the first pass.

  struct rvalue var;
  variable *pv;

  var.line = term.line;
  var.lastline = term.lastline;
  if(first_pass)
    return var;
  pv = tcalloc(1, sizeof(*pv));
  pv->coefficient = term.i;
  var.v = pv;
  return var;
}


////////////////////////////////////////////////////////////////////////////
// SET_INEQ
////////////////////////////////////////////////////////////////////////////

struct rvalue set_ineq(struct rvalue *list, int sign, struct rvalue *term) {
  // The function returns an updated version of (*list) that includes (*term).
  // It also does the proper initializations when 'list' = 0 and when 
  // 'list' = 'term' = 0. 
  // Note that the v field of the result contains an 'inequality' object.
  // The function has almost no effect in the first pass.

  struct rvalue res;
  inequality *pin;

  if(list) { // then it must be that term != 0
    res = *list;
    if(res.line < 0)
      res.line = term->line;
    if(res.lastline < 0)
      res.lastline = term->lastline;
  }
  else {
    memset(&res, 0, sizeof(res));
    if(term) {
      res.line = term->line;
      res.lastline = term->lastline;
    }
    else {
      res.line = -1;
      res.lastline = -1;
    }
  }

  if(first_pass)  
    return res;

  // the following lines are for the second pass 

  if(!list)
    pin = tcalloc(1, sizeof(*pin));
  else
    pin = (inequality*) list->v;
  res.v = pin;
  if(!term) 
    return res;
  set_ineq_sub(pin, (variable*) (term->v), sign); // may deallocate term->v
  return res;
}

////////////////////////////////////////////////////////////////////////////
// SET_INEQ_SUB
////////////////////////////////////////////////////////////////////////////

void set_ineq_sub(inequality* pin, variable* var, int sign) {
  // This is a subroutine of set_ineq of more general interest. It inserts
  // the variable 'var' in the inequality 'pin' with the sign 
  // indicated by 'sign'.

  variable* pv, *prev_pr;

  if(sign) // change sign of coefficient
    var->coefficient = - var->coefficient;
  if(!var->pn) { // Then this is a free-term
    pin->free_term += var->coefficient;
    free(var);
  }
  else { // insert term in inequality
    if(!pin->variable_list)  // if the list is empty
      pin->variable_list = var;
    else { // if the list is not empty, 
      // check whether variable already in list and update list
      for(pv = pin->variable_list; ; pv = pv->next) {
	if(var->type == pv->type && var->pn == pv->pn && \
	   var->index == pv->index) { // if variable already in list
	  pv->coefficient += var->coefficient;
	  free(var);
	  if(!pv->coefficient) { // remove variable if it has null coefficient
	    if(pv == pin->variable_list) 
	      pin->variable_list = pv->next;
	    else 
	      prev_pr->next = pv->next;
	    free(pv);
	  }
	  break; // finished updating the list
	} // end of if variable already in list
	// line reached if variable not found yet in the list
	if(!pv->next) { // if this is the last list element
	  // then insert variable, since it was not found in the list
	  var->next = 0;
	  pv->next = var;
	  break; // finished updating the list
	}
	prev_pr = pv;
      } // end of for loop
    } // end of if variable list is not empty
  } // end of insert term in inequality
}


////////////////////////////////////////////////////////////////////////////
// SCAN_INPUT
////////////////////////////////////////////////////////////////////////////

void specs_check(specs* s) {
  // This is used in ScanInput to check whether the specification is valid.
  // It ensures that all required fields are initialized or else it returns
  // an error.

  char *str;

  int i;

  if(!s) {
    report_error(-1, "the specification appears to be empty");
    return;
  }

  if(!s->name) {
    report_error(-1, "the specification name could not be determined");
    return;
  }

  if(s->process_num <= 0 || !s->process_array) {
    report_error(-1, "at least one process or thread must be defined");
    return;
  }

  for(i = 0; i < s->process_num; i++) {
    if(!s->process_array[i]) {
      report_error(-1, "insufficient information about the process or thread %d", i);
      return;
    }
  }

  for(i = 0; i < s->process_num; i++) 
    if(!s->process_array[i]->supervisor)
      break;

  if(i >= s->process_num)  // if all processes are supervisor components
    report_error(-1, "at least one process or thread must be defined");
  // no need to return; next checks may proceed

  for(i = 0; i < s->process_num; i++) {
    str = process_check(s->process_array[i]);
    if(str) {
      report(-1, "Process %d: ", i, str);
      free(str);
    }
  }
}


specs* ScanInput(char* specs_file) {
  FILE* f;
  struct pa_proc* p;
  int i;
  struct myinsert ins;
  char c;

  f = fopen(specs_file,"r");
  if(!f) {
    fprintf(stderr, "\nThe file %s could not be opened!\n", specs_file);
    return 0;
  }

  spec_name = specs_file;
  for(i = strlen(spec_name)-1; i >= 0; i--) // remove path from spec_name
    if(spec_name[i] == '/')
      break;
  if(i >= 0)
    spec_name = spec_name + i + 1;

  // Initializations

  init_dict(variables);

  errors = 0;
  first_pr = 0;
  first_pass = 1;
  first_var = 0;
  parseline = 1; // in read.lex
  pr_num = 0;
  pres_ineq = 0;
  pres_pr = 0;
  pres_var = 0;
  pres_vartype = NONE;

  // Write file content in a buffer

  ins = InitInsert(4096);
  while(fread(&c, 1, 1, f)) 
    ins = CInsert(c, ins);
  ins = CInsert('\n', ins); // add newline in case file does not end with one
  // this simplifies the lexer, since it is not necessary to worry about 
  // commands terminated with EOF

  // First Scan

  parse_buffer(GetInsertBuf(&ins));
  // rewind(f); parse_file(f); 

  if(!errors) {

    // Process data

    sp = tcalloc(1, sizeof(*sp));
    sp->name = tmalloc(sizeof(char)*(1+strlen(specs_file)));
    strcpy(sp->name, specs_file);
    // Remove extension from file name
    for(i = strlen(sp->name); i > 0; i--)// i > 0, in case name begins with '.'
      if(sp->name[i] == '.') {
	sp->name[i] = 0;
	break;
      }
    // filter special characters (the spec name can appear in function
    // and variable names of the generated C files) 
    for(i = 0; sp->name[i]; i++) 
      if(!isalnum(sp->name[i])) 
	sp->name[i] = '_';
    sp->process_num = pr_num;
    sp->process_array = tcalloc(pr_num, sizeof(*(sp->process_array)));

    // Second Scan

    first_pass = 0;
    parseline = 1; // in read.lex

    parse_buffer(GetInsertBuf(&ins));
    // rewind(f); parse_file(f); 

    if(!errors)
      specs_check(sp); // reports errors if the specs object is incomplete

    if(errors)
      dealloc_specs(sp);
    else
      include_additional_variables();
  }

  for(p = first_pr; p; p = p->next) 
    free_dict(p->var); 
  
  free_dict(variables);
  free(GetInsertBuf(&ins));

  if(errors)
    return 0;

  return sp;
}



void set_vartype(enum var_type v) {
  pres_vartype = v;
}



////////////////////////////////////////////////////////////////////////////
// SYNC_TRANS
////////////////////////////////////////////////////////////////////////////


void sync_trans(struct rvalue list, struct rvalue *alist) {
// Deals with synchronization constraints.
// Verifies data during the first pass.
// Updates specification object during the second pass. 

  syncc *ps;
  struct pa_var *pvar;
  struct pa_proc *pv;
  struct rvl_chain *r;
  int t[2], id[2], i, line, trans;
  char j;

  for(i = 0, j = 0; ; i++) { // Check the variables in list

    // Take first the VAR element (the process)

    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v));
    if(!r)
      break;
    line = r->rvl.line;
    pvar = is_process(r->rvl.p, line); // also reports errors
    if(!pvar) {
      free_rvlchain((struct qalloc*) (list.v));
      free((struct qalloc*) (list.v));
      return;
    }
    pv = pvar->pr;
    free(r->rvl.p);

    // Next take the second VAR element (the transition)

    r = (struct rvl_chain*) next_in_line((struct qalloc*) (list.v)); 
    trans = is_var(pv, r->rvl, TRANS); // takes care of errors
    free(r->rvl.p);
    if(!first_pass) { // second pass not reached if there are errors
      t[j] = trans;
      id[j] = pv->id;
      j = !j; // j takes 0 or 1 values
      if(i >= 1) { // if at least two transitions have been considered
	ps = tcalloc(1, sizeof(*ps));
	ps->pn1 = sp->process_array[id[0]]->pn;
	ps->pn2 = sp->process_array[id[1]]->pn;
	ps->t1 = t[0];
	ps->t2 = t[1];
	ps->next = sp->synclist;
	sp->synclist = ps;
      }
    }
  }

  if(i <= 1) 
    report_error(line, "at least two transitions should be given in a synchronization instruction");

  qfree((struct qalloc*) (list.v));
  free((struct qalloc*) (list.v));
}
