/********************************************************************/
/* SLAP -- Static Livelock Analyzer for CSP Processes, version 0.1. */
/********************************************************************/

/*********************************************************************
 Copyright 2003, Joel Ouaknine (hereinafter AUTHOR). All rights
 reserved. By using this software the USER indicates that he or she
 has read, understood and will comply with the following:

 --- AUTHOR hereby grants USER nonexclusive permission to use, copy
 and/or modify this software for internal, noncommercial, research
 purposes only. Any distribution, including commercial sale or
 license, of this software, copies of the software, its associated
 documentation and/or modifications of either is strictly prohibited
 without the prior consent of AUTHOR. Title to copyright to this
 software and its associated documentation shall at all times remain
 with AUTHOR. Appropriate copyright notice shall be placed on all
 software copies, and a complete copy of this notice shall be
 included in all copies of the associated documentation.

 --- This software and any associated documentation is provided "as is"

 AUTHOR MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED,
 INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR
 PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR ASSOCIATED
 DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, TRADEMARKS
 OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.

 AUTHOR shall not be liable under any circumstances for any direct,
 indirect, special, incidental, or consequential damages with respect
 to any claim by USER or any third party on account of or arising from
 the use, or inability to use, this software or its associated
 documentation, even if AUTHOR has been advised of the possibility of
 those damages.
*********************************************************************/

/******************************************************************
 Please send any bug reports/comments/suggestions to 
 joelo@andrew.cmu.edu .
 Thanks, and enjoy!
******************************************************************/


#include <stdio.h>
#include <string.h>
#include <ctype.h>
#include <stdlib.h>
#include <assert.h>

#define MAXWORD 1000
#define BUFSIZE 1000

struct wordlist {   /* implements a bag of strings      */
  char *wordp;
  int number;       /* The number of instances of wordp */
  struct wordlist *next;
};

struct wordnode {   /* implements an ordered set */
  char *wordp;
  int  booleanvar;  /* gives a bool. var. # for each event from 1 to ... */
  struct wordnode *left;
  struct wordnode *right;
};

struct setnode {    /* implements an ordered set of named sets */ 
  char *name;
  struct wordnode *set;
  struct setnode *left;
  struct setnode *right;
};

struct relnode {    /* implements an ordered set of named sets */
  char *name;
  struct wordnode *rel;
  struct relnode *left;
  struct relnode *right;
};

struct setlist {              /* a list of sets of events, represented */
  int *set;                   /* by their boolean variable numbers */   
  struct setlist *next;       /* set[0] gives no. of elements */
};                            /* The set is ordered in increasing order */

struct varguardsnode {  /* basis of X-guards of P, for fixed P and various */
  char *varname;        /* X, ordered by X */
  struct setlist *guards;
  struct varguardsnode *left;
  struct varguardsnode *right;
};                       

struct nonexmatnode { /* set of N_X(P), for fixed P and various X, */
  char  *varname;         /* ordered by X */
  int * *nonexmatrix; 
  struct nonexmatnode *left;
  struct nonexmatnode *right;
};

struct staticinfo {   /* Information to perform the livelock analysis */
  int   *set;         /* For parallel and hiding */
  int * *renamingmatrix; /* renaming... */
  struct nonexmatnode *nonextree; /* Every process */
  struct setlist      *tickguards;  /* Every process */
  struct varguardsnode *varguardstree; /* Every process */
};

struct procnode {   /* a process node */
  char tag[7];      /*  STOP, SKIP, |~|, [], ->, ;, \, [|{}|], |||, [[<-]]
                        var, mu, proc */  
  char *name;
  struct wordnode *setrelarg;
  struct procnode *procarg1;
  struct procnode *procarg2;

  struct staticinfo data;   
};

struct vectornode {  /* implements an unordered list of named processes */
  char *name;
  struct procnode *process;
  struct vectornode *next;
};

/************** GLOBAL VARIABLES *****************************/

FILE *inputfile;

char inputfilename[100];

int inputfilebuf[BUFSIZE];  /* Buffer for ungetting characters 
			       type int to be able to store EOF */
int inputfilebufpos;

int lineno;                 /* The current line no. in the input */

                 /* all options are off by default */
int muoption;    /* if on, process input uses mu operator */
int terseoption; /* just get the answer, "livelock-free" or 
		    "potential livelock" */

int bekicoption; /* prints out the bekicification of the process; 
		    no effect under -terse */

                 /* There is also -help...*/

int alphabetsize;  /* The size of the alphabet at the end */

struct wordnode   *alphabet; /* To store all events */ 
struct setnode    *sets;     /* All named sets */
struct relnode    *renrels;  /* All named renaming relations */
struct wordnode   *defined;  /* Binary tree node; the tree is a set of words */
struct wordlist   *procnametobedefined; /* Process named not yet declared */
struct vectornode *vector;   /* The list of all processes */

/*************************************************************/

void readcommandline(int argc, char *argv[])
{ 
  int i;

  muoption = terseoption = bekicoption = 0;
  strcpy(inputfilename,"");

  if (argc < 2) {      
    printf("Syntax: slap [options] inputfile\n");
    printf("where available options are -terse, -mu, -bekic.\n\n"); 
    exit(0);
  }

  for (i = 1; i < argc; i++) {
    if (strcmp(argv[i],"-mu") == 0)
      muoption = 1;
    else if (strcmp(argv[i],"-terse") == 0)
      terseoption = 1;
    else if (strcmp(argv[i],"-bekic") == 0)
       bekicoption = 1;  
    else if (argv[i][0] == '-') {  /* -help or unknown option */
      printf("Syntax: slap [options] inputfile\n");
      printf("where available options are -terse, -mu, -bekic.\n\n"); 
      exit(0);
    }
    else {
      if ((inputfile = fopen(argv[i],"r")) == NULL) {
	printf("Error: can't open %s\n",argv[i]);
	exit(1);
      }
      strcpy(inputfilename,argv[i]);
    }
  }
  if (strcmp(inputfilename,"") == 0) {
    printf("Syntax: slap [options] inputfile\n");
    printf("where available options are -terse, -mu, -bekic.\n\n"); 
    exit(0);
  }
  
  if (bekicoption && muoption) {
    printf("Error: cannot use bekic option with mu option\n");
    exit(1);
  }

  if (bekicoption && terseoption) {
    printf("Error: cannot use bekic option with terse option\n");
    exit(1);
  }
}

/*************************************************************/

/* getch gets the next inputfile character, first checking the file buffer */

int getch(void)
{
  int c;

  if (inputfilebufpos == 0)
    c = getc(inputfile);
  else
    c = inputfilebuf[--inputfilebufpos];
  if (c == '\n')
    lineno++;
  return(c);
}

/*************************************************************/

void ungetch(int c)
{
  if (inputfilebufpos >= BUFSIZE) {
    printf("Line %d: error: input file buffer full\n",lineno);
    exit(1);
  }
  else {
    if (c == '\n')
      lineno--;
    inputfilebuf[inputfilebufpos++] = c;
  }
}
    
/*************************************************************/

void ungetword(char *wordp)
{
  int i;

  ungetch(' ');
  for (i = (strlen(wordp)-1); i >= 0; i--)
    ungetch(wordp[i]);
}
  
/*************************************************************/

/* identchar: determines if c is an identifier character */

int identchar(int c)
{
  return (isalnum(c) ||   /* alphanumeric? */
	  (c == '_') ||
	  (c == '.') ||
	  (c == '\''));   /* Note: this is a "prime" (as in P') */
}

/*************************************************************/

int isreserved(char wordbuf[])
{
  return ((strcmp(wordbuf,"channel") == 0) ||
	  (strcmp(wordbuf,"STOP") == 0) ||
	  (strcmp(wordbuf,"SKIP") == 0) ||
	  (strcmp(wordbuf,"mu") == 0) ||
	  (strcmp(wordbuf,"SIGMA") == 0) ||
	  (strcmp(wordbuf,"divcheck") == 0));
}

/*************************************************************/

/* declaration: */
struct wordnode *addwordnode(struct wordnode *root, char *wordp); 

int initialize_defined(void)  /* Initializes defined with reserved words */
{
  defined = NULL;
  defined = addwordnode(defined,"channel");
  defined = addwordnode(defined,"STOP");
  defined = addwordnode(defined,"SKIP");
  defined = addwordnode(defined,"mu");
  defined = addwordnode(defined,"SIGMA");
  defined = addwordnode(defined,"divcheck");

  return(0);
}

/*************************************************************/

/* getnext(wordbuf) returns in wordbuf the next identifier, reserved word
or the first non-(space, tab), non-identifier character.
The return value is always the first character of wordbuf; this
is especially usful for EOF.
*/

int getnext(char wordbuf[])
{
  int i, c,d;

  while (((c = getch()) == ' ') || (c == '\t'))
    ;

  if (c == '-') {
    if ((d = getch()) == '-') /* we have just read "--" */
      while (((c = getch()) != EOF) && (c != '\n')) 
	;
    else
      ungetch(d);
  }

  if (c == EOF) 
    return(EOF);
  
  if (!identchar(c)) {
    wordbuf[0] = c;
    wordbuf[1] = '\0';
    return(c);
  }

  for(i = 0; identchar(c); i++) {
    wordbuf[i] = c;
    c = getch();
  }

  wordbuf[i] = '\0';
  ungetch(c);
  return(wordbuf[0]);
}

/*************************************************************/

/* getnextnnl(wordbuf) returns in wordbuf the next identifier, 
reserved word or the first non-(space, tab, newline), non-identifier 
character. The return value is always the first character of wordbuf; 
this is especially usful for EOF.
*/

int getnextnnl(char wordbuf[])
{
  int c;

  while ((c = getnext(wordbuf)) == '\n')
    ;
  return (c);
}

/*************************************************************/

int getnewline(void)
{
  int c;
  char wordbuf[MAXWORD];
  
  if ((c = getnext(wordbuf)) == EOF) 
    ungetch(c);
  else if (c != '\n') {
    printf("Line %d: syntax error: newline expected instead of\
 \'%c\'\n",lineno,c);
    exit(1);
  }

  return(c);
}

/*************************************************************/

char *wordalloc(char *wordp)
{
  char *newwordp;

  newwordp = (char *) malloc(strlen(wordp)+1);
  return(strcpy(newwordp,wordp));
}

/*************************************************************/

struct wordnode *wordnodealloc(char *wordp)
{ 
  struct wordnode *wordnodep;

  wordnodep = (struct wordnode *) malloc(sizeof(struct wordnode));
  wordnodep->wordp = wordalloc(wordp);
  wordnodep->left = wordnodep->right = NULL;
  
  return(wordnodep);
} 

/*************************************************************/

struct setnode *setnodealloc(char *name, struct wordnode *set)
{
  struct setnode *setnodep;

  setnodep = (struct setnode *) malloc(sizeof(struct setnode));
  setnodep->name = wordalloc(name);
  setnodep->set = set;
  setnodep->left = setnodep->right = NULL;

  return(setnodep);
} 

/*************************************************************/

struct relnode *relnodealloc(char *name, struct wordnode *rel)
{
  struct relnode *relnodep;

  relnodep = (struct relnode *) malloc(sizeof(struct relnode));
  relnodep->name = wordalloc(name);
  relnodep->rel = rel;
  relnodep->left = relnodep->right = NULL;

  return(relnodep);
} 

/*************************************************************/

struct procnode *procnodealloc(char tag[], 
			       char *name,
			       struct wordnode *setrelarg,
			       struct procnode *procarg1,
			       struct procnode *procarg2)
{
  struct procnode *procnodep;

  procnodep = (struct procnode *) malloc(sizeof(struct procnode)); 
  strcpy(procnodep->tag,tag);
  procnodep->name = wordalloc(name);
  procnodep->setrelarg = setrelarg;
  procnodep->procarg1 = procarg1;
  procnodep->procarg2 = procarg2;

  procnodep->data.set = NULL;
  procnodep->data.renamingmatrix = NULL;
  procnodep->data.nonextree = NULL;
  procnodep->data.tickguards = NULL;
  procnodep->data.varguardstree = NULL;

  return(procnodep);
} 

/*************************************************************/

struct nonexmatnode *nonexmatnodealloc(char *varname,
				       int * *nonexmatrix)
{
  struct nonexmatnode *temp;
  
  temp = (struct nonexmatnode *) malloc(sizeof(struct nonexmatnode));
  temp->varname = wordalloc(varname);
  temp->nonexmatrix = nonexmatrix;
  temp->left = NULL;
  temp->right = NULL;
  return(temp);
}

/*************************************************************/

struct varguardsnode *varguardsnodealloc(char *varname,
					 struct setlist *basis)
{
  struct varguardsnode *temp;
  
  temp = (struct varguardsnode *) malloc(sizeof(struct varguardsnode));
  temp->varname = wordalloc(varname);
  temp->guards = basis;
  temp->left = NULL;
  temp->right = NULL;
  return(temp);
}

/*************************************************************/

struct procnode *duplicate(struct procnode *process)
{
  if (process == NULL)
    return(NULL);

  return(procnodealloc(process->tag,
		       process->name,
		       process->setrelarg,
		       duplicate(process->procarg1),
		       duplicate(process->procarg2)));
}

/*************************************************************/

struct wordlist *addwordlist(struct wordlist *root, char *wordp)
{

  if (root == NULL) {
    root = (struct wordlist *) malloc(sizeof(struct wordlist));
    root->wordp = wordalloc(wordp);
    root->number = 1;
    root->next = NULL;
  }
  else if (strcmp(root->wordp,wordp) == 0) {
    (root->number)++; 
  }
  else { 
    root->next = addwordlist(root->next,wordp);
  }

  return(root);
}

/*************************************************************/

/* deletewordlist removes from wordlist one instance of wordp;  */
/* If wordp does not belong to *root somewhere, nothing happens */

struct wordlist *deletewordlist(struct wordlist *root, char *wordp)
{
  struct wordlist *wordlistp;
  
  if (root == NULL)
    return(root);
  
  if (strcmp(root->wordp,wordp) == 0) {
    if (root->number == 1) {
      wordlistp = root->next;
      free(root->wordp);    /* ONLY BECAUSE NEW SPACE WAS ALLOCATED */
      free(root);
      return(wordlistp);
    }
    else {
      (root->number)--;
      return(root);
    }
  }
      
  root->next = deletewordlist(root->next,wordp);
  return(root);
}

/*************************************************************/

struct wordnode *addwordnode(struct wordnode *root, char *wordp)
{
  int cond;

  if (root == NULL)
    root = wordnodealloc(wordp);
  else if ((cond = strcmp(wordp, root->wordp)) < 0)
    root->left = addwordnode(root->left, wordp);
  else if (cond > 0)
    root->right = addwordnode(root->right, wordp);
  return(root);
}

/*************************************************************/

struct setnode *addsetnode(struct setnode *root, char *name, 
			   struct wordnode *set)
{
  int cond;

  if (root == NULL)
    root = setnodealloc(name,set);
  else if ((cond = strcmp(name, root->name)) < 0)
    root->left = addsetnode(root->left, name, set);
  else if (cond > 0)
    root->right = addsetnode(root->right, name, set);

  return(root);
}

/*************************************************************/

struct relnode *addrelnode(struct relnode *root, char *name, 
			   struct wordnode *rel)
{
  int cond;

  if (root == NULL)
    root = relnodealloc(name,rel);
  else if ((cond = strcmp(name, root->name)) < 0)
    root->left = addrelnode(root->left, name, rel);
  else if (cond > 0)
    root->right = addrelnode(root->right, name, rel);
 
  return(root);
}

/*************************************************************/

struct vectornode *addvectornode(struct vectornode *root, char *name, 
				 struct procnode *process)
{
  struct vectornode *temp;

  temp = (struct vectornode *) malloc(sizeof(struct vectornode));
  temp->name = wordalloc(name);
  temp->process = process;
  temp->next = root;
  return(temp);
} 

/*************************************************************/

/* deletevectornode removes the process named "name" from vector   */
/* If "name" does not belong to vector, an internal error occurs   */

struct vectornode *deletevectornode(struct vectornode *root, char *name)
{
  struct vectornode *temp;
  
  if (root == NULL) {
    printf("Internal error: process %s not found in vector\n",name);
    exit(1);
  }

  if (strcmp(root->name,name) == 0) {
    temp = root->next;
    free(root->name);  /* ONLY BECAUSE NEW SPACE WAS ALLOCATED */
    free(root); /* Note that we do not free root->process. 
		   because of cross-reference, never delete this. */
    return(temp);
  }
  else {
    root->next = deletevectornode(root->next,name);
    return(root);
  }
}

/*************************************************************/

struct nonexmatnode *addnonexmatnode(struct nonexmatnode *root, 
				       char *varname,
				       int * *nonexmatrix)
{
  int cond;

  if (root == NULL)
    root = nonexmatnodealloc(varname,nonexmatrix);
  else if ((cond = strcmp(varname, root->varname)) < 0)
    root->left = addnonexmatnode(root->left,varname,nonexmatrix);
  else if (cond > 0)
    root->right = addnonexmatnode(root->right,varname,nonexmatrix);
  return(root);
}

/*************************************************************/

struct varguardsnode *addvarguardsnode(struct varguardsnode *root,
				       char *varname,
				       struct setlist *basis)
{
  int cond;

  if (root == NULL)
    root = varguardsnodealloc(varname,basis);
  else if ((cond = strcmp(varname,root->varname)) < 0)
    root->left = addvarguardsnode(root->left,varname,basis);
  else if (cond > 0)
    root->right = addvarguardsnode(root->right,varname,basis);
  return(root);
}

/*************************************************************/

/* wordnodepointerint(booleanvar,root) returns a pointer to the node
   in root whose booleanvar is booleanvar. This is used to print
   sets corresponding to satisfying assignments. 
*/

struct wordnode *wordnodepointerint(int booleanvar, struct wordnode *root)
{

  if (root == NULL) 
    return(NULL);
  if (root->booleanvar == booleanvar)
    return(root);
  else if (booleanvar < root->booleanvar) 
    return(wordnodepointerint(booleanvar,root->left));
  else 
    return(wordnodepointerint(booleanvar,root->right));
}

/*************************************************************/

/* wordnodepointer(wordp,root) returns a pointer to the node in root
   (initially alphabet) whose name is wordp, and NULL if there is no
   such node.
*/

struct wordnode *wordnodepointer(char* wordp, struct wordnode *root)
{
  int cond;

  if (root == NULL)
    return(NULL);
  else if ((cond = strcmp(wordp, root->wordp)) == 0)
    return(root);
  else if (cond < 0) 
    return(wordnodepointer(wordp,root->left));
  else 
    return(wordnodepointer(wordp,root->right));
}

/*************************************************************/

/* setnodepointer(name,root) returns a pointer to the node whose
   name is name, and NULL if there is no such node. 
*/

struct setnode *setnodepointer(char* name, struct setnode *root)
{
  int cond;

  if (root == NULL)
    return(NULL);
  else if ((cond = strcmp(name,root->name)) == 0)
    return(root);
  else if (cond < 0) 
    return(setnodepointer(name,root->left));
  else 
    return(setnodepointer(name,root->right));
}

/*************************************************************/

/* relnodepointer(name,root) returns a pointer to the node whose
   name is name, and NULL if there is no such node. 
*/

struct relnode *relnodepointer(char* name, struct relnode *root)
{
  int cond;

  if (root == NULL)
    return(NULL);
  else if ((cond = strcmp(name,root->name)) == 0)
    return(root);
  else if (cond < 0) 
    return(relnodepointer(name,root->left));
  else 
    return(relnodepointer(name,root->right));
}

/*************************************************************/

/* wordlistpointer(wordp,root) returns a pointer to the node whose
   name is name, and NULL if there is no such node. 
*/

struct wordlist *wordlistpointer(char* wordp, struct wordlist *root)
{

  if (root == NULL)
    return(NULL);
  else if (strcmp(wordp, root->wordp) == 0) {
    return(root);
  }
  else
    return(wordlistpointer(wordp,root->next));
}

/*************************************************************/

/* processpointer(name,root) returns a pointer to the node whose
   name is name, and NULL if there is no such node. 
*/

struct vectornode *processpointer(char *name, struct vectornode *root)
{
  if (root == NULL)
    return(NULL);
  else if (strcmp(name, root->name) == 0)
    return(root);
  else
    return(processpointer(name,root->next));
}

/*************************************************************/

/* nonexmatnodepointer(varname,root) returns a pointer to the node in
   root whose name is varname, and NULL if there is no such node.
*/

struct nonexmatnode *nonexmatnodepointer(char* varname, 
					 struct nonexmatnode *root)
{
  int cond;

  if (root == NULL)
    return(NULL);
  else if ((cond = strcmp(varname,root->varname)) == 0)
    return(root);
  else if (cond < 0) 
    return(nonexmatnodepointer(varname,root->left));
  else 
    return(nonexmatnodepointer(varname,root->right));
}

/*************************************************************/

/* varguardsnodepointer(varname,root) returns a pointer to the node in
   root whose name is varname, and NULL if there is no such node.
*/

struct varguardsnode *varguardsnodepointer(char* varname, 
					   struct varguardsnode *root)
{
  int cond;

  if (root == NULL)
    return(NULL);
  else if ((cond = strcmp(varname,root->varname)) == 0)
    return(root);
  else if (cond < 0) 
    return(varguardsnodepointer(varname,root->left));
  else 
    return(varguardsnodepointer(varname,root->right));
}

/*************************************************************/

void printwordlist(struct wordlist *root)
{
  if (root != NULL) {
    printwordlist(root->next);
    printf("%s\n",root->wordp);
  } 
}

/*************************************************************/

/* Prints a tree of events                                                */
/* If it's *not* the first element, we print ",x", otherwise we print "x" */
/* We return 0 if we've printed something, 1 otherwise                    */

int printwordnodetree(struct wordnode *root, int first)
{
  if (root != NULL) {
    first = printwordnodetree(root->left,first);
    printf("%s%s",first? "":",",root->wordp); 
                    /* Now first is and will stay 0 */
    first = printwordnodetree(root->right,0);
  }
  return(first);
}

/*************************************************************/

void printsetnodetree(struct setnode *root)
{
  if (root != NULL) {
    printsetnodetree(root->left);
    printf("%s = {",root->name);
    printwordnodetree(root->set,1); 
    printf("}\n");
    printsetnodetree(root->right);
  }
}

/*************************************************************/

void printsetlist(struct setlist *basis)
{
  int i;

  while (basis != NULL) {
    printf("{");
    for (i = 1; i < basis->set[0]; i++)
      printf("%s,",(wordnodepointerint(basis->set[i],alphabet))->wordp);
    if (basis->set[0] > 0)
      printf("%s",(wordnodepointerint(basis->set[basis->set[0]],alphabet))
	     ->wordp);
    printf("}\n");
    basis = basis->next;
  }
}

/*************************************************************/

void printrelnodetree(struct relnode *root)
{
  if (root != NULL) {
    printrelnodetree(root->left);
    printf("%s = [",root->name);
    printwordnodetree(root->rel,1);
    printf("]\n");
    printrelnodetree(root->right);
  }
}

/*************************************************************/

int atomic(struct procnode *process)
{
  return((strcmp(process->tag,"STOP") == 0) ||
	 (strcmp(process->tag,"SKIP") == 0) ||
	 (strcmp(process->tag,"proc") == 0) ||
	 (strcmp(process->tag,"var") == 0)  ||
	 (strcmp(process->tag,"\\") == 0) ||
	 (strcmp(process->tag,"[[<-]]") == 0));
}

/*************************************************************/

void printprocess(struct procnode *root)
{

  if (root != NULL) {
    if (strcmp(root->tag,"STOP") == 0) {
      printf("STOP");
      return;
    }
    if (strcmp(root->tag,"SKIP") == 0) {
      printf("SKIP");
      return;
    }
    if (strcmp(root->tag,"var") == 0) {
      printf("%s",root->name);
      return;
    }
    if (strcmp(root->tag,"mu") == 0) {
      printf("mu %s * ",root->name);
      printprocess(root->procarg1);
      return;
    }
    if (strcmp(root->tag,"proc") == 0) {
      printf("%s",root->name);
      return;
    }
    if (strcmp(root->tag,"\\") == 0) { 
      /* check if empty unnamed set */
      if ((strcmp(root->name,"{") == 0) && (root->setrelarg == NULL)) {
	printprocess(root->procarg1);
	return;
      }
      /* we have either a non-empty unnamed set or a named set */
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      if (strcmp(root->name,"{") == 0) {
	printf("\\{");
	printwordnodetree(root->setrelarg,1);
	printf("}");
      }
      else
	printf("\\%s",root->name);
      return;
    }
    if (strcmp(root->tag,"[[<-]]") == 0) {
      /* check if empty unnamed renaming relation */
      if ((strcmp(root->name,"[") == 0) && (root->setrelarg == NULL)) {
	printprocess(root->procarg1);
	return;
      }
      /* we have either a non-empty unnamed ren. rel. or a named ren. rel. */
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");

      if (strcmp(root->name,"[") == 0) {
	printf("[[");
	printwordnodetree(root->setrelarg,1);
	printf("]]");
	return;
      }
      else
	printf("[%s]",root->name);
      return;
    }
    if (strcmp(root->tag,"|~|") == 0) {
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      printf(" |~| ");
      if (!atomic(root->procarg2)) 
	printf("(");
      printprocess(root->procarg2);
      if (!atomic(root->procarg2)) 
	printf(")");
      return;
    }
    if (strcmp(root->tag,"[]") == 0) {
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      printf(" [] ");
      if (!atomic(root->procarg2)) 
	printf("(");
      printprocess(root->procarg2);
      if (!atomic(root->procarg2)) 
	printf(")");
      return;
    }
    if (strcmp(root->tag,";") == 0) {
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      printf(" ; ");
      if (!atomic(root->procarg2)) 
	printf("(");
      printprocess(root->procarg2);
      if (!atomic(root->procarg2)) 
	printf(")");
      return;
    }
    if (strcmp(root->tag,"|||") == 0) {
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      printf(" ||| ");
      if (!atomic(root->procarg2)) 
	printf("(");
      printprocess(root->procarg2);
      if (!atomic(root->procarg2)) 
	printf(")");
      return;
    }
    if (strcmp(root->tag,"[|{}|]") == 0) {
      if (!atomic(root->procarg1)) 
	printf("(");
      printprocess(root->procarg1);
      if (!atomic(root->procarg1)) 
	printf(")");
      if (strcmp(root->name,"{") == 0) {
	printf(" [|{");
	printwordnodetree(root->setrelarg,1);
	printf("}|] ");
      }
      else
	printf(" [|%s|] ",root->name);
      if (!atomic(root->procarg2)) 
	printf("(");
      printprocess(root->procarg2);
      if (!atomic(root->procarg2)) 
	printf(")");
      return;
    }
    if (strcmp(root->tag,"->") == 0) {
      printf("%s -> ",root->name);
      if ((!atomic(root->procarg1)) && 
	  (strcmp(root->procarg1->tag,"->") != 0)) 
	printf("(");
      printprocess(root->procarg1);
      if ((!atomic(root->procarg1)) && 
	  (strcmp(root->procarg1->tag,"->") != 0)) 
	printf(")");
      return;
    }

    printf("Internal error: unknown tag: %s",root->tag);
    exit(1);
  }
}

/*************************************************************/

void printvectorlist(struct vectornode *root)
{
  if (root != NULL) {
    printvectorlist(root->next);
    printf("%s = ",root->name);
    printprocess(root->process);
    printf("\n");
  }
}

/*************************************************************/

int getchannels() 
{
  char wordbuf[MAXWORD];
  int c;

  if (!identchar(getnext(wordbuf))) {
    printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	   lineno,wordbuf[0]);
    exit(1);
  }
  
  if (isreserved(wordbuf)) {
    printf("Line %d: syntax error: %s is a reserved word\n",
	   lineno,wordbuf);
    exit(1);
  }

  if (wordnodepointer(wordbuf,defined) != NULL) {
    printf("Line %d: error: %s already defined\n",lineno,wordbuf);
    exit(1);
  }

  alphabet = addwordnode(alphabet,wordbuf); 
  defined = addwordnode(defined,wordbuf);

  while (((c = getnext(wordbuf)) != EOF) && (c != '\n')) {
    if (c != ',') {
      printf("Line %d: syntax error: \',\' expected instead of %s\n",
	     lineno,wordbuf);
     exit(1);
    } 
   
    if (!identchar(getnext(wordbuf))) {
      printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	     lineno,wordbuf[0]);
      exit(1);
    }
    
    if (isreserved(wordbuf)) {
      printf("Line %d: syntax error: %s is a reserved word\n",
	     lineno,wordbuf);
      exit(1);
    }

    if (wordnodepointer(wordbuf,defined) != NULL) {
      printf("Line %d: error: %s already defined\n",lineno,wordbuf);
      exit(1);
    }
    
    alphabet = addwordnode(alphabet,wordbuf); 
    defined = addwordnode(defined,wordbuf);

  } 

  ungetch(c);

  return(0);
}  
    
/*************************************************************/

struct wordnode *getset() 
{
  struct wordnode *setp;
  char wordbuf[MAXWORD];
  int c;

  setp = NULL;

  if ((c = getnextnnl(wordbuf)) == '}')
    return(NULL);  /* the empty set */
  
  if (!identchar(c)) {
    printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	   lineno,wordbuf[0]);
    exit(1);
  }
   
  if (wordnodepointer(wordbuf,alphabet) == NULL) {
    printf("Line %d: unknown event: %s\n",lineno,wordbuf);
    exit(1);
  }
  
  setp = addwordnode(setp,wordbuf);

  while (((c = getnextnnl(wordbuf)) != EOF) && (c != '}')) {
    if (c != ',') {
      printf("Line %d: syntax error: \'}\' or \',\' expected instead of %s\n",
	     lineno,wordbuf);
      exit(1);
    } 
    
    if (!identchar(getnextnnl(wordbuf))) {
      printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	     lineno,wordbuf[0]);
      exit(1);
    }
    
    if (wordnodepointer(wordbuf,alphabet) == NULL) {
      printf("Line %d: unknown event: %s\n",
	     lineno,wordbuf);
      exit(1);
    }
     
    setp = addwordnode(setp,wordbuf);
  } 
  
  if (c == EOF) {
    printf("Line %d: syntax error: \'}\' expected instead of EOF\n",
	   lineno);
    exit(1);
  }

  return(setp);
}

/*************************************************************/

struct wordnode *getrel() 
{
  struct wordnode *relp;
  char wordbuf[MAXWORD], wordbuf1[MAXWORD], tempwordbuf[MAXWORD];
  int c;

  relp = NULL;

  if ((c = getnextnnl(wordbuf)) == ']')
    return(NULL);  /* the empty renaming relation */
   
  if (!identchar(c)) {
    printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	   lineno,wordbuf[0]);
    exit(1);
  }
  
  if (wordnodepointer(wordbuf,alphabet) == NULL) {
    printf("Line %d: unknown event: %s\n",
	   lineno,wordbuf);
    exit(1);
  }
  
  /* We have now sucessfully read the target event of the first
     renaming clause */

  if ((c = getnextnnl(tempwordbuf)) != '<') {
    printf("Line %d: syntax error: \'<-\' expected instead of \'%c\'\n",
	   lineno,wordbuf[0]);
    exit(1);
  }
  
  if ((c = getch()) != '-') {
    printf("Line %d: syntax error: \'<-\' expected instead of \'<%c\'\n",
	   lineno,c); 
    exit(1);
  } 

  /* We have now read "<-" */
  
  if (!identchar(getnextnnl(wordbuf1))) {  /* note that <-- Bla, as in
					      comment, would be a
					      syntax error, leaving
					      "<" hanging. However,
					      <--- Bla would work,
					      parsing as <- -- Bla */
    printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	   lineno,wordbuf1[0]);
    exit(1);
  }
  
  if (wordnodepointer(wordbuf1,alphabet) == NULL) {
    printf("Line %d: unknown event: %s\n",
	   lineno,wordbuf1);
    exit(1);
  }
  
  relp = addwordnode(relp,strcat(strcat(wordbuf,"<-"),wordbuf1));
    
  while (((c = getnextnnl(wordbuf)) != EOF) && (c != ']')) {
    if (c != ',') {
      printf("Line %d: syntax error: \']\' or \',\' expected instead of %s\n",
	     lineno,wordbuf);
      exit(1);
    } 
    
    if (!identchar(getnextnnl(wordbuf))) {
      printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	     lineno,wordbuf[0]);
      exit(1);
    }
    
    if (wordnodepointer(wordbuf,alphabet) == NULL) {
      printf("Line %d: unknown event: %s\n",
	     lineno,wordbuf);
      exit(1);
    }
    
    /* We have now sucessfully read the target event of the current
       renaming clause */
    
    if ((c = getnextnnl(tempwordbuf)) != '<') {
      printf("Line %d: syntax error: \'<-\' expected instead of \'%c\'\n",
	     lineno,wordbuf[0]);
      exit(1);
    }
    
    if ((c = getch()) != '-') {
      printf("Line %d: syntax error: \'<-\' expected instead of \'<%c\'\n",
	     lineno,c); 
      exit(1);
    } 
    
    /* We have now read "<-" */
    
    if (!identchar(getnextnnl(wordbuf1))) {
      printf("Line %d: syntax error: event expected instead of \'%c\'\n",
	     lineno,wordbuf1[0]);
      exit(1);
    }
    
    if (wordnodepointer(wordbuf1,alphabet) == NULL) {
      printf("Line %d: unknown event: %s\n",
	     lineno,wordbuf1);
      exit(1);
    }
    
    relp = addwordnode(relp,strcat(strcat(wordbuf,"<-"),wordbuf1));
  
  }  

  if (c == EOF) {
    printf("Line %d: syntax error: \']\' expected instead of EOF\n",
	   lineno);
    exit(1);
  } 
  
  return(relp);
}

/*************************************************************/

/* endprocess() detects whether the end of process input has
   been reached. That occurs either when
   * the next word is EOF or channel or divcheck
   * the second next word is "="
   Note that if the _next_ word is "=" then either we have a
   syntax error or we missed the end earlier (shouldn't happen!)
   endprocess() pushes all words back onto the stack. It has no 
   error behavior of its own. It merely corresponds to checking for
   the defunct "#".
   Note also that it is important to know whether at least one newline
   has been read, and if so to push it back on the stack if needed.
*/

int endprocess()
{
  char wordbuf1[MAXWORD], wordbuf2[MAXWORD];
  int newlinecond1,newlinecond2,c;

  if ((c = getnext(wordbuf1)) == '\n') {
    newlinecond1 = 1;
    c = getnextnnl(wordbuf1);
  }
  else
    newlinecond1 = 0;

  if (c == EOF) {
    ungetch(EOF);
    if (newlinecond1)
      ungetch('\n');
    return(1);
  }
 
  if ((strcmp(wordbuf1,"channel") == 0) ||
      (strcmp(wordbuf1,"divcheck") == 0)) {
    ungetword(wordbuf1);
    if (newlinecond1)
      ungetch('\n'); 
    return(1);
  }
  
  if ((c = getnext(wordbuf2)) == '\n') {
    newlinecond2 = 1;
    c = getnextnnl(wordbuf2);
  }
  else
    newlinecond2 = 0;
  
  if (c == EOF) {
    ungetch(EOF);
    if (newlinecond2)
      ungetch('\n');
    if (identchar(wordbuf1[0]))
      ungetword(wordbuf1);
    else
      ungetch(wordbuf1[0]);
    if (newlinecond1)
      ungetch('\n'); 
    return(0);
  }

  if (strcmp(wordbuf2,"=") == 0) {
    ungetch('=');
    if (newlinecond2)
      ungetch('\n');
    if (identchar(wordbuf1[0]))
      ungetword(wordbuf1);
    else
      ungetch(wordbuf1[0]); 
    if (newlinecond1)
      ungetch('\n'); 
    return(1);
  }

  if (identchar(wordbuf2[0]))
    ungetword(wordbuf2);
  else
    ungetch(wordbuf2[0]);
  if (newlinecond2)
    ungetch('\n');
  if (identchar(wordbuf1[0]))
    ungetword(wordbuf1);
  else
    ungetch(wordbuf1[0]); 
  if (newlinecond1)
    ungetch('\n'); 
  return(0);
}
    
/*************************************************************/

/**** PROCESSBLURB

recall that
struct procnode {
  char tag[7];
  char *name;
  struct wordnode *setrelarg;
  struct procnode *procarg1;
  struct procnode *procarg2;
};

tag is one of:
 STOP     -- no arguments                  
 SKIP     -- no arguments
 |~|      -- procarg1, procarg2             prec: 6, left-assoc
 []       -- procarg1, procarg2             prec: 6, left-assoc
 ->       -- wordarg, procarg1              prec: 8
 ;        -- procarg1, procarg2             prec: 8, left-assoc
 \        -- procarg1, setarg               prec: 10
 [|{}|]   -- procarg1, procarg2, setarg     prec: 4, left-assoc
 |||      -- procarg1, procarg2             prec: 4, left-assoc
 [[<-]]   -- procarg1, relarg               prec: 10
 var      -- wordarg
 mu       -- wordarg, procarg1              prec: 2
 proc     -- wordarg

****/

/*** getterm returns a pointer to a process term.  It receives as
     argument a "precedence" integer. It keeps reading and
     constructing a process until either a ")" or an operator
     with operator-precedence <= precedence argument is encountered,
     or the end of process input is detected.
     The latter occurs when: 
     * the next word is EOF or channel or divcheck 
     * the second next word is "=".
     
     boundvars is a pointer to the set of variables currently under
     the scope of a mu operator, so that they're not confused with
     process names defined separately.

***/

struct procnode *getterm(int precedence,struct wordlist *boundvars)

{
  int c,d,e;
  char wordbuf[MAXWORD], wordbuf1[MAXWORD], wordbuf2[MAXWORD];
  struct procnode *term1, *term2;
  struct wordnode *setrel;
  struct setnode *setp;
  struct relnode *relp;
  struct vectornode *processp;

  if (getnextnnl(wordbuf) == EOF) {
    printf("Line %d: syntax error: process term expected\n",lineno);
    exit(1);
  }

  if (wordbuf[0] == '(') {
    term1 = getterm(0,boundvars);
    if ((c = getnextnnl(wordbuf1)) != ')') {
      printf("Line %d: syntax error: \')\' expected instead of \'%c\'\n",
	     lineno,c);
      exit(1);
    } /* we have read the term1 argument */
  } /* ELSE ... read first term argument */
  else if (!identchar(wordbuf[0])) {
    printf("Line %d: syntax error: %s\n",lineno,wordbuf);
    exit(1);
  }
  else if (strcmp(wordbuf,"mu") == 0) {  /* if we have a mu */
    if (!muoption) {
      printf("Line %d: syntax error: -mu option off\n",lineno);
      exit(1);
    }
    if (!identchar(c = getnextnnl(wordbuf1))) {
      printf("Line %d: syntax error: variable expected instead of \'%c\'\n",
	     lineno,c);
      exit(1);
    }
    if (wordnodepointer(wordbuf1,defined) != NULL) {
      printf("Line %d: syntax error: variable expected instead of %s%s\n",
	     lineno,
	     (processpointer(wordbuf1,vector) != NULL)? "process " : "",
	     wordbuf1);
      exit(1);
    }
    if (wordlistpointer(wordbuf1,procnametobedefined) != NULL) {
      printf("Line %d: syntax error: variable expected instead of\
 process %s\n",lineno,wordbuf1);
      exit(1);
    } 

    /**** WE now allow mu X * mu X * STOP, etc. (nested binding) *****/
    
    /* begin treatment of mu */

    boundvars = addwordlist(boundvars,wordbuf1);
    if ((c = getnextnnl(wordbuf2)) != '*') {
      printf("Line %d: syntax error: \'*\' expected instead of \'%c\'\n",
	     lineno,c);
      exit(1); 
    } 
    term1 = getterm(0,boundvars);
    /* Note also that since we called getterm with precedence 0
       (because of mu), there is nothing further to read, so we return. */
    boundvars = deletewordlist(boundvars,wordbuf1);
    return(procnodealloc("mu",wordbuf1,NULL,term1,NULL));
  } /* end treatment of mu */

  else { /* We have an identifier. It could be STOP, SKIP,
	    an (old or new) process name / variable,
	    or an event followed by -> */
    if (wordnodepointer(wordbuf,alphabet) != NULL) {  /* an event */
      if (getnextnnl(wordbuf1) != '-') {
	printf("Line %d: syntax error: \'->\' expected instead of \'%c\'\n",
	       lineno,wordbuf1[0]);
	exit(1); 
      } 
      if ((c = getch()) != '>') {
	printf("Line %d: syntax error: \'->\' expected instead of \'-%c\'\n",
	       lineno,c);
	exit(1); 
      } 
      /* We have read '->' */
      term2 = getterm(8,boundvars); /* temp */
      term1 = procnodealloc("->",wordbuf,NULL,term2,NULL);
    } 
    /* See now whether we have STOP, SKIP, a process name / variable */
    else {
      if (strcmp(wordbuf,"STOP") == 0) 
	term1 = procnodealloc("STOP",wordbuf,NULL,NULL,NULL);
      else if (strcmp(wordbuf,"SKIP") == 0)
	term1 = procnodealloc("SKIP",wordbuf,NULL,NULL,NULL);
      else { /* is it a process name / variable? */
	if (muoption) {
	  if (wordlistpointer(wordbuf,boundvars) != NULL)
	    term1 = procnodealloc("var",wordbuf,NULL,NULL,NULL);
	  else if ((processp = processpointer(wordbuf,vector)) != NULL) 
	    term1 = duplicate(processp->process);
	  else {
	    if (getnextnnl(wordbuf1) == '-')
	      if (getnextnnl(wordbuf1) == '>') {
		printf("Line %d: syntax error: %s appears to be an undefined\
 event\n",lineno,wordbuf);
		exit(1);
	      }
	    printf("Line %d: error: process %s undefined with -mu option on\n",
		   lineno,wordbuf);
	    exit(1);
	  }
	}
	else { /* muoption is off */
	  if (wordnodepointer(wordbuf,defined) != NULL) {
	    if (processpointer(wordbuf,vector) == NULL) {
	      printf("Line %d: syntax error: %s is not a process\n",
		     lineno,wordbuf);
	      exit(1);
	    } 
	  }
	  else if (wordlistpointer(wordbuf,procnametobedefined) == NULL) 
	    procnametobedefined = addwordlist(procnametobedefined,wordbuf);
	  term1 = procnodealloc("proc",wordbuf,NULL,NULL,NULL);
	}
      }
    }
  }
  /* We now have term1. Proceed with the rest. */

  while (1 == 1) { 
    if (endprocess())
      return(term1);

    if ((c = getnextnnl(wordbuf)) == EOF) {
      printf("Line %d: syntax error: unexpected EOF\n",lineno);
      exit(1);
    }

    if (c == ')') {
      ungetch(c);
      return(term1);
    }

    if (c == '\\') {   /* the backslash character, i.e., hiding
			it beats all precedences, so no checks */
      if (getnextnnl(wordbuf1) == EOF) {
	printf("Line %d: syntax error: set expected\n",lineno);
	exit(1);
      }
      if (wordbuf1[0] == '{') 
	setrel = getset();
      else if (strcmp(wordbuf1,"SIGMA") == 0)
	setrel = alphabet;
      else if ((setp = setnodepointer(wordbuf1,sets)) == NULL) {
	printf("Line %d: unknown set: %s\n",lineno,wordbuf1);
	exit(1);
      }
      else
	setrel = setp->set;
      /* Now setrel is a pointer to the hiding set
	 and wordbuf1 contains "{" or the name of the set */
      term1 = procnodealloc("\\",wordbuf1,setrel,term1,NULL);
      /* we've now augmented term1 appropriately.
	 Note: we're keeping the name of the set, of "{" if unnamed */
      continue;
    }

    if (c == ';') { /* sequential composition */
      if (8 <= precedence) { /* ; does not bind tightly enough */ 
	ungetch(c);
	return(term1);
      }	
      else { /* ; binds tighter than precedence */
	term2 = getterm(8,boundvars); /* term2 is temp */
	term1 = procnodealloc(";","",NULL,term1,term2);
	/* term1 has been augmented */
	continue;
      }
    }
    
    if (c == '[') { /* choice of [], [[, [|, [ R */
      if ((d = getch()) == ']') { /* We have external choice */
	if (6 <= precedence) { /* [] does not bind tightly enough */ 
	  ungetch(d);
	  ungetch(c); /* wordbuf was just c since it was '[' */
	  return(term1);
	}	
	else { /* [] binds tighter than precedence */ 
	  term2 = getterm(6,boundvars); /* term2 is temp */
	  term1 = procnodealloc("[]","",NULL,term1,term2);
	  /* term1 has been augmented */
	  continue;
	}
      }
      else if (d == '[') { /* we have an unnamed renaming relation */
	setrel = getrel();
	/* Now getrel is a pointer to the renaming relation.
	   we just need to read off "]]".
	   HOWEVER, since getrel() has already read off one ']',
	   we just need to read off the second one.
	   no need to check precedence. */
	if (getnextnnl(wordbuf2) != ']') {
	  printf("Line %d: syntax error: \']]\' expected instead of \'%c\'\n",
		 lineno,wordbuf2[0]);
	  exit(1);
	}
	term1 = procnodealloc("[[<-]]","[",setrel,term1,NULL);
	/* we've now augmented term1 appropriately. */
	/* Note: we're keeping "[" as the "name" of the (unnamed) 
	   renaming relation. */ 
	continue;
      }
      else if (d == '|') { /* we have a synchronized parallel */
	if (4 <= precedence) { /* [|{}|] does not bind tightly enough */ 
	  ungetch(d);
	  ungetch(c);
	  return(term1);
	}	
	else { /* [|{}|] binds tighter than precedence */ 
	  if (getnextnnl(wordbuf1) == EOF) {
	    printf("Line %d: syntax error: set expected\n",lineno);
	    exit(1);
	  }
	  if (wordbuf1[0] == '{')  /* set is unnamed */
	    setrel = getset();
	  else if (strcmp(wordbuf1,"SIGMA") == 0)  /* set is SIGMA */
	    setrel = alphabet;
	  else if ((setp = setnodepointer(wordbuf1,sets)) == NULL) {
	    printf("Line %d: unknown set: %s\n",
		   lineno,wordbuf1);
	    exit(1);
	  }
	  else 
	    setrel = setp->set;
	  /* Now setrel is a pointer to the synchronizing set
	     and wordbuf1 is either "{" or the name of the set.
	     We first read "|]" off. */
	  if (getnextnnl(wordbuf2) != '|') {
	    printf("Line %d: syntax error: \'|]\' expected instead of\
 \'%c\'\n",lineno,wordbuf2[0]);
	    exit(1);
	  }
	  if ((c = getch()) != ']') {
	    printf("Line %d: syntax error: \'|]\' expected instead of\
 \'%c\'\n",lineno,c);
	    exit(1);
	  }
	  term2 = getterm(4,boundvars); /* term2 is temp */
	  term1 = procnodealloc("[|{}|]",wordbuf1,setrel,term1,term2);
	  /* we've now augmented term1 appropriately. 
	     We keep "{" or the name of the set, if named */
	  continue;
	}
      }
      else /* We did not read ],[, or | in d -- undo and read normally */
	ungetch(d);
     
      /* We are still in the case c == '[' */

      if (!identchar(getnextnnl(wordbuf1))) {
	printf("Line %d: syntax error: \']\', \'[\', \'|\', or\
 a renaming relation expected instead of %c\n",lineno,wordbuf1[0]);
	exit(1);
      }
      /* Now wordbuf1 holds an identifier -- presumably a renaming rel. */
      if ((relp = relnodepointer(wordbuf1,renrels)) == NULL) {
	printf("Line %d: unknown renaming relation: %s\n",lineno,wordbuf1);
	exit(1);
      }
      else 
	setrel = relp->rel;
      /* Now setrel is a pointer to the renaming relation set.
	 we need to read off ']' */
      if (getnextnnl(wordbuf2) != ']') {
	printf("Line %d: syntax error: \']\' expected instead of \'%c\'\n",
	       lineno,wordbuf2[0]);
	exit(1);
      }
      term1 = procnodealloc("[[<-]]",wordbuf1,setrel,term1,NULL);
      /* term1 has been augmented. 
         we keep its name */
      continue;
      /* this ends the case of c == '[' */
    }
    
    if (c == '|') { /* choice of ||| and |~| */ 
      if ((d = getch()) == '|') { /* We have interleaving */
	if ((e = getch()) != '|') {
	  printf("Line %d: syntax error: \'|||\' expected instead of %c\n",
		 lineno,e);
	  exit(1);
	}
	/* We have proper interleaving */
	if (4 <= precedence) { /* ||| does not bind tightly enough */ 
	  ungetch(e);
	  ungetch(d);
	  ungetch(c);
	  return(term1);
	}	
	term2 = getterm(4,boundvars); /* term2 is temp */
	term1 = procnodealloc("|||","",NULL,term1,term2);
	/* we've now augmented term1 appropriately. */
	continue;
      }
      else if (d == '~') { /* We have internal choice */
	if ((e = getch()) != '|') {
	  printf("Line %d: syntax error: \'|~|\' expected instead of %c\n",
		 lineno,e);
	  exit(1);
	}
	if (6 <= precedence) { /* |~| does not bind tightly enough */ 
	  ungetch(e);
	  ungetch(d);
	  ungetch(c);
	  return(term1);
	}
	term2 = getterm(6,boundvars); /* term2 is temp */
	term1 = procnodealloc("|~|","",NULL,term1,term2);
	/* we've now augmented term1 appropriately. */
	continue;
      }
    }

    /* No other choice for 'c' */

    if ((c == '-') && ((d = getch()) == '>')) {
      printf("Line %d: syntax error: %s appears to be an undefined event\n",
	     lineno,term1->name);
      exit(1);
    }

    printf("Line %d: syntax error: end of process or \')\' or\
 operator expected instead of %c\n",lineno,c);
    exit(1);
  }
}

/*************************************************************/

/*** See PROCESSBLURB above ***/

struct procnode *getprocess() 
{
  struct procnode *process;

  process = getterm(0,NULL);  /* precedence 0, read as far as possible
				 no bound variables */

  if (!endprocess()) {
    printf("Line %d: syntax error: end of process expected\n",
	   lineno);
    exit(1);
  }

  return(process);
}

/*************************************************************/

/* procappearsin(procname,process) decides if the process name procname
   *appears in process. It is only used with muoption off. Note
   that there are no binding considerations.

   return(1) means name was found free, return(0) means no.
*/

int procappearsin(char *procname, struct procnode *process)

{
  if (process == NULL)
    return(0);
  
  if (strcmp(process->name,procname) == 0) {
    if (strcmp(process->tag,"proc") != 0) {
      printf("Internal error: tag should be proc instead of %s\n",
	     process->tag);
      exit(1);
    }     
    return(1);
  }

  return(procappearsin(procname,process->procarg1) ||
	 procappearsin(procname,process->procarg2));
}

/*************************************************************/

/* returns 1 if varname appears freely in process, 0 otherwise */

int isfreein(char *varname, struct procnode *process)
{ 
  if (process == NULL)
    return(0);

  if (strcmp(process->name,varname) == 0) {
    if (strcmp(process->tag,"var") == 0)
      return(1);
    else if (strcmp(process->tag,"mu") == 0)
      return(0);
    else {
      printf("Internal error: tag for %s should be mu or var instead of %s\n",
	     varname,process->tag);
      exit(1);
    }  
  }
  
  return(isfreein(varname,process->procarg1) || 
	 isfreein(varname,process->procarg2));
}      

/*************************************************************/

/* Removes from process every "mu X" node for which the process argument
   does not have X as a free variable. */

struct procnode *trimfree(struct procnode *process)
{
  struct procnode *temp;

  if (process == NULL)
    return(NULL);

  if (strcmp(process->tag,"mu") == 0) {
    if (isfreein(process->name,process->procarg1)) {
      process->procarg1 = trimfree(process->procarg1);
      return(process);
    }
    else {
      temp = trimfree(process->procarg1);
      free(process); /* don't free the variable name, may be used elsewhere */
      return(temp);
    }
  }

  process->procarg1 = trimfree(process->procarg1);
  process->procarg2 = trimfree(process->procarg2);
  return(process);
}

/*************************************************************/

/* substitute(process,procname,replacementprocess) replaces by (a freshly
   mallocked new copy of) replacementprocess every occurrence of the
   process name procname in process. There are no binding
   considerations. Note that replacementprocess is unaltered and no
   new pointer points to it.
*/

struct procnode *substitute(struct procnode *process,
			    char *procname,
			    struct procnode *replacementprocess)
{
  if (process == NULL)
    return(NULL);

  if (strcmp(process->name,procname) == 0) {
    if (strcmp(process->tag,"proc") != 0) {
      printf("Internal error: tag should be proc instead of %s\n",
	     process->tag);
      exit(1);
    }     
    if ((process->procarg1 != NULL) || (process->procarg2 != NULL)) {
      printf("Internal error: proc node has non-NULL process argument(s)\n");
      exit(1);
    }
    free(process); /* in the calling procedure, process gets assigned 
		      the return value... */
    return(duplicate(replacementprocess));
  } 

  process->procarg1 = substitute(process->procarg1,
				 procname,
				 replacementprocess);
  process->procarg2 = substitute(process->procarg2,
				 procname,
				 replacementprocess);
  return(process);
}

/*************************************************************/

/* vartag(root) replaces all "proc" tags by "var" tags. This is
   called from bekic()
*/

void vartag(struct procnode *root)
{
  if (root != NULL) {
    if (strcmp(root->tag,"proc") == 0)
      strcpy(root->tag,"var");
    
    vartag(root->procarg1);
    vartag(root->procarg2);
  }
}

/*************************************************************/

/* bekic() bekicifies by removing processes from vector one at a time.
   It is only called if muoption is off. */

struct procnode *bekic(struct procnode *process)
{
  struct procnode *newprocess, *tempprocess; 
  char tempprocessname[MAXWORD];
  struct vectornode *vectortemp;

  /* First we grab the process we will Bekicify in newprocess */

  if (strcmp(process->tag,"proc") == 0) { /* If it's just a name */
    newprocess = (processpointer(process->name,vector)->process);
    if (newprocess == NULL) { 
      printf("Internal error: process %s not found in vector\n",
	     process->name);
      exit(1);
    }
    vector = deletevectornode(vector,process->name);
  }
  else
    newprocess = process;
 
  /* Now we bekicify vector + newprocess */

  while (vector != NULL) {
    tempprocess = vector->process; 
    strcpy(tempprocessname,vector->name);
    vector = deletevectornode(vector,vector->name);

    /* First we check if tempprocessname is free in tempprocess */

    if (procappearsin(tempprocessname,tempprocess))
      tempprocess = procnodealloc("mu",tempprocessname,NULL,tempprocess,NULL);

    /* Now we replace every free (but they're all free!) occurrence of
       tempprocessname in vector by tempprocess */

    vectortemp = vector;
    while (vectortemp != NULL) {
      vectortemp->process = substitute(vectortemp->process,
				       tempprocessname,
				       tempprocess);
      vectortemp = vectortemp->next;
    }
    newprocess = substitute(newprocess,tempprocessname,tempprocess);
  }

  /* One last mu-ification */

  if (strcmp(process->tag,"proc") == 0)
    if (procappearsin(process->name,newprocess))
      newprocess = procnodealloc("mu",process->name,NULL,newprocess,NULL);

  /* finally, we replace all "proc" tags by "var" tags in newprocess */

  vartag(newprocess);
      
  return(newprocess);
}

/*************************************************************/

/* assigns boolean variable (integers) from start (originally 1)
   onwards to the elements in root (originally alphabet), preserving
   the order. Returns the total number of elements, plus start.
*/

int assignboolvars(int start, struct wordnode *root)

{
  if (root == NULL)
    return(start);
  start = assignboolvars(start,root->left);
  root->booleanvar = start++;
  start = assignboolvars(start,root->right);
  return(start);
}

/*************************************************************/
/*************************************************************/

/* The non-expansive "matrices" are represented as an array of int *.
   This array contains alphabetsize+1 elements, basically one for each
   of the elements in alphabet (we ignore the index 0). If the matrix
   is NULL it means the relevant variable is not free in the
   process. Each line contains a pointer to an array of ints. The
   0-indexed integer of element i holds the number of elements that i
   renames to. If the pointer is NULL this indicates that the element
   maps to "FALSE". Each array is sorted in increasing order.
*/

/*************************************************************/
/*************************************************************/

/* mergewordlist merges list1 and list2 together. The wordcount always
   remains at 1. list1 and list2 are affected. */

struct wordlist *mergewordlist(struct wordlist *list1,
			       struct wordlist *list2)
{
  struct wordlist *temp;
  
  while (list2 != NULL)
    if (wordlistpointer(list2->wordp,list1) == NULL) {
      temp = list2->next;
      list2->next = list1;
      list1 = list2;
      list2 = temp;
    }
    else {
      temp = list2->next;
      free(list2->wordp);    /* ONLY BECAUSE NEW SPACE WAS ALLOCATED */
      free(list2);
      list2 = temp;
    }
    
  return(list1);
}

/*************************************************************/

void freematrix(int * *matrix)
{
  int i;
  for (i = 1; i <= alphabetsize; i++)
    free(matrix[i]);
  free(matrix);
}

/*************************************************************/

/* Frees everything in nonextree. */

void zapnonextree(struct nonexmatnode *nonextree)
{
  if (nonextree == NULL) 
    return;
  zapnonextree(nonextree->left);
  zapnonextree(nonextree->right);
  free(nonextree->varname);
  freematrix(nonextree->nonexmatrix);
  free(nonextree);
}

/*************************************************************/

/* Frees everything in nonextree, except the entry with varname. */

void zapbut(struct nonexmatnode *nonextree, char *varname)
{
  if (nonextree == NULL) 
    return;
  zapbut(nonextree->left,varname);
  zapbut(nonextree->right,varname);
  if (strcmp(nonextree->varname,varname) == 0) {
    nonextree->left = NULL;
    nonextree->right = NULL;
  }
  else {
    free(nonextree->varname);
    freematrix(nonextree->nonexmatrix);
    free(nonextree);
  }
}

/*************************************************************/

/* Frees everything in nonextree, except the entry with varname;
   Return a pointer to the entry with varname. */

struct nonexmatnode *zapnonextreebut(struct nonexmatnode *nonextree,
				     char *varname)
{
  struct nonexmatnode *pointer;

  pointer = nonexmatnodepointer(varname,nonextree);
  zapbut(nonextree,varname);
  return(pointer);
}

/*************************************************************/

/* Frees the tree structure, not the bases. */

void zapvarguardstree(struct varguardsnode *varguardstree)
{
  if (varguardstree == NULL) 
    return;
  zapvarguardstree(varguardstree->left);
  zapvarguardstree(varguardstree->right);
  free(varguardstree->varname);
  free(varguardstree);
}

/*************************************************************/

int * *duplicatematrix(int * *matrix)
{
  int * *newmatrix;
  int *matrix_i,*newmatrix_i;
  int i,j;

  if (matrix == NULL)
    return(NULL);

  newmatrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 1; i <= alphabetsize; i++) {
    matrix_i = matrix[i];
    if (matrix_i == NULL) {
      newmatrix[i] = NULL;
      continue;
    }
    newmatrix[i] = (int *) calloc(matrix_i[0]+1,sizeof(int));
    newmatrix_i = newmatrix[i];
    for (j = 0; j<= matrix_i[0]; j++)
      newmatrix_i[j] = matrix_i[j];
  }

  return(newmatrix);
}

/*************************************************************/

struct setlist *duplicatebasis(struct setlist *basis)
{
  struct setlist *newbasis,*temp;
  int i;

  newbasis = NULL;

  while (basis != NULL) {
    temp = newbasis;
    newbasis = (struct setlist *) malloc(sizeof(struct setlist));
    newbasis->set = (int *) calloc((basis->set[0])+1,sizeof(int));
    for (i = 0; i <= basis->set[0]; i++)
      newbasis->set[i] = basis->set[i];
    newbasis->next = temp;
    basis = basis->next;
  }
  
  return(newbasis);
}

/*************************************************************/

/* Merges array1 and array2 (assumed to be sorted) into a new array.
   If either is NULL, we return NULL */

int *arraymerge(int *array1, int *array2)
{
  int *array,*temp;
  int index,index1,index2,c1,c2;

  if ((array1 == NULL) || (array2 == NULL))
    return(NULL);

  array = (int *) calloc(array1[0] + array2[0] + 1,sizeof(int));
  /* possibly an overapproximation, for now */

  index1 = index2 = index = 1;

  while ((index1 <= array1[0]) && (index2 <= array2[0])) 
    if ((c1 = array1[index1]) < (c2 = array2[index2])) {
      array[index++] = c1;
      index1++;
    }
    else if (c1 > c2) {
      array[index++] = c2;
      index2++;
    }
    else {
      array[index++] = c1;
      index1++;
      index2++;
    }
 
  if (index1 > array1[0])
    while (index2 <= array2[0])
      array[index++] = array2[index2++];
  else
    while (index1 <= array1[0])
      array[index++] = array1[index1++];

  array[0] = index-1;

  if (array[0] < array1[0] + array2[0]) { /* correct the overapproximation */
    temp = (int *) calloc(array[0]+1,sizeof(int));
    for (index = 0; index <= array[0]; index++)
      temp[index] = array[index];
    free(array);
    array = temp;
  }
  return(array);  
}

/*************************************************************/

/* Merges matrix1 and matrix2, and returns a brand new matrix. */

int * *buildmerge(int * *matrix1,int * *matrix2)
{
  int * *matrix;
  int i;

  if (matrix1 == NULL)
    return(duplicatematrix(matrix2));
  
  if (matrix2 == NULL)
    return(duplicatematrix(matrix1));
  
  matrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 0; i <= alphabetsize; i++) 
    matrix[i] = arraymerge(matrix1[i],matrix2[i]);

  return(matrix);
}

/*************************************************************/

/* Hides the sorted array set from matrix. matrix is affected. 
   We return matrix. */

int * *hidesetmatrix(int * *matrix, int *set)
{
  int i;

  if (matrix == NULL) {
    printf("Internal error: hiding set from NULL nonexpansive matrix\n");
    exit(1);
  }

  for (i = 1; i <= set[0]; i++) {
    free(matrix[set[i]]);
    matrix[set[i]] = NULL;
  }
  return(matrix);
}
  
/*************************************************************/

/* Fills out, for every event (number), the line of event (numbers) 
   it renames to in matrix. For every domain event added, we
   increase the event's line's 0-th entry by 1. Note that the events
   being renamed to actually end up sorted. */

void updaterenamingmatrix(int * *matrix, struct wordnode *root)
{
  int *matrix_event1;
  int i, event1, event2;
  char wordbuf[MAXWORD];

  if (root != NULL) {
    if (root->left != NULL)
      updaterenamingmatrix(matrix,root->left); /* deal with left branch */
    for (i = 0; (root->wordp)[i] != '<';i++)  /* copy first event in wordbuf */
      wordbuf[i] = (root->wordp)[i];
    wordbuf[i] = '\0';
    i++; i++;   /* root->wordp + i now points right after <-, = second event */
    
    event1 = (wordnodepointer(wordbuf,alphabet))->booleanvar;
    event2 = (wordnodepointer((root->wordp) + i,alphabet))->booleanvar;

    matrix_event1 = matrix[event1];
    
    matrix_event1[0]++;

    matrix_event1[matrix_event1[0]] = event2;

    if (root->right != NULL)
      updaterenamingmatrix(matrix,root->right); /* deal with right branch */
  }    
}

/*************************************************************/

/* Transform a renaming relation into a matrix.  */

int * *buildrenamingmatrix(struct wordnode *setrel)
{ 
  int * *matrix;
  int *matrix_i,*array;
  int i,j;

  matrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 1; i <= alphabetsize; i++)
    matrix[i] = (int *) calloc(alphabetsize+1,sizeof(int));

  updaterenamingmatrix(matrix,setrel);

  for (i = 1; i <= alphabetsize; i++) {
    matrix_i = matrix[i];
    if (matrix_i[0] == 0) {
      matrix_i[0] = 1;
      matrix_i[1] = i;  /* i renames to i */
    }
    array = (int *) calloc(matrix_i[0]+1,sizeof(int));
    for (j = 0; j <= matrix_i[0]; j++)
      array[j] = matrix_i[j];
    free(matrix_i);
    matrix[i] = array;
  }

  return(matrix);
}

/*************************************************************/

void swap(int array[], int i, int j)
{
  int temp;

  temp = array[i];
  array[i] = array[j];
  array[j] = temp;
}

/*************************************************************/

void quicksort(int array[],int left,int right)
{
  int i,last;

  if (left >= right)
    return;

  swap(array,left,(left+right)/2);
  last = left;
  for (i = left+1; i <= right; i++)
    if (array[i] < array[left])
      swap(array,++last,i);
  swap(array,left,last);
  quicksort(array,left,last-1);
  quicksort(array,last+1,right);
}

/*************************************************************/

/* Eliminates repeated elements from array array. array[0] has the
   initial number of elements. */

void elimredun(int array[])
{
  int i,index,noelem;
  noelem = array[0];

  index = 1;
  for (i = 2; i <= noelem; i++)
    if(array[i] == array[index])
      array[0]--;
    else
      array[++index] = array[i];
}

/*************************************************************/

/* Applies renamingmatrix to line, and returns the result in a new 
   sorted array. */

int *apply(int * *renamingmatrix,int *line)
{
  int *array,*matrixline,*renamingmatrix_ev;
  int j,k,size;

  if (line == NULL)
    return(NULL);

  size = 0;
  for (j = 1; j <= line[0]; j++)
    size += renamingmatrix[line[j]][0];  /* overapproximation...*/

  array = (int *) calloc(size+1,sizeof(int));

  for (j = 1; j <= line[0]; j++) {
    renamingmatrix_ev = renamingmatrix[line[j]];
    for (k = 1; k <= renamingmatrix_ev[0]; k++)
      array[++(array[0])] = renamingmatrix_ev[k];
  }
  quicksort(array,1,array[0]);
  elimredun(array);
  matrixline = (int *) calloc(array[0]+1,sizeof(int));
  for (j = 0; j <= array[0]; j++)
    matrixline[j] = array[j];
  free(array);
  
  return(matrixline);
}

/*************************************************************/

/* Builds a new matrix corresponding to the application of 
   renamingmatrix to matrix1. */

int * *buildrenamed(int * *matrix1,int * *renamingmatrix)
{
  int * *matrix;
  int i;

  if (matrix1 == NULL)
    return(NULL);

  matrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 1; i <= alphabetsize; i++) 
    matrix[i] = apply(renamingmatrix,matrix1[i]);

  return(matrix);
}

/*************************************************************/

int * *buildidentity()
{
  int * *matrix;
  int *matrix_i;
  int i;

  matrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 1; i <= alphabetsize; i++) {
    matrix[i] = (int *) calloc(2,sizeof(int));
    matrix_i = matrix[i];
    matrix_i[0] = 1;
    matrix_i[1] = i;
  }
  return(matrix);
}

/*************************************************************/

/* return 1 if c is in unsorted array, where array[0] gives no. of elements */

int isin(int c, int *array)
{
  int i;

  for (i = 1; i <= array[0]; i++)
    if (c == array[i])
      return(1);
  return(0);
}

/*************************************************************/

/* Saturates line with matrix1, viewed as a renaming relation. line
   remains untouched, we return a new sorted array. We assume 
   matrix is not NULL. */

int *makesaturate(int * *matrix, int *line)
{
  int *array,*matrix_horiz,*newline;
  int j,c,index;

  if (line == NULL)
    return(NULL);

  array = (int *) calloc(alphabetsize+1,sizeof(int));

  for (j = 0; j <= line[0]; j++)
    array[j] = line[j];

  index = 1;
  while (index <= array[0]) {
    matrix_horiz = matrix[array[index]];
    if (matrix_horiz == NULL) {
      free(array);
      return(NULL);
    }
    for (j = 1; j <= matrix_horiz[0]; j++)
      if (!isin((c = matrix_horiz[j]),array))
	array[++(array[0])] = c;
    index++;
  }
  
  newline = (int *) calloc(array[0]+1,sizeof(int));
  for (j = 0; j <= array[0]; j++) 
    newline[j] = array[j];

  free(array);

  quicksort(newline,1,newline[0]);
  return(newline);
}

/*************************************************************/

/* Creates a brand new matrix corresponding to 
   matrix1 ; matrix2^*. We assume that this function is never called
   with either matrix1 or matrix2 NULL. */

int * *buildsaturate(int * *matrix1, int * *matrix2)
{
  int * *matrix;
  int i;

  matrix = (int * *) calloc(alphabetsize+1,sizeof(int *));

  for (i = 1; i <= alphabetsize; i++) 
    matrix[i] = makesaturate(matrix2,matrix1[i]);

  return(matrix);
}
      
/*************************************************************/

void freebasis(struct setlist *basis)
{
  struct setlist *temp;

  while (basis != NULL) {
    temp = basis->next;
    free(basis->set); 
    free(basis);
    basis = temp;
  }
}

/*************************************************************/

/* returns 1 if elem belongs to set. set is an array of ints of set[0] 
   elements sorted in increasing order. */

int belongsto(int elem,int *set)
{
  int lower,upper,index;

  lower = 1;
  upper = set[0];

  while (lower <= upper) {
    index = (upper+lower)/2;
    if (elem < set[index])
      upper = index-1;
    else if (elem > set[index])
      lower = index+1;
    else
      return(1);
  }
  return(0);
}

/*************************************************************/

/* returns 1 if if set1 subset of set2. Recall set1[0] and set2[0]
   contain the respective number of elements. Also, the sets are
   sorted from smallest to largest. */

int subsetof(int *set1,int *set2)
{
  int i;

  if ((set1 == NULL) || (set2 == NULL)) {
    printf("Internal error: NULL set(s) in subsetof()\n");
    exit(1);
  }
  
  for (i = 1; i <= set1[0]; i++)
    if (!belongsto(set1[i],set2))
      return(0);

  return(1);
}

/*************************************************************/

/* returns 1 if if set1 intersects set2. Recall set1[0] and set2[0]
   contain the respective number of elements. Also, the sets are
   sorted from smallest to largest. */

int intersects(int *set1,int *set2)
{
  int i;

  if ((set1 == NULL) || (set2 == NULL)) {
    printf("Internal error: NULL set(s) in intersects()\n");
    exit(1);
  }
  
  for (i = 1; i <= set1[0]; i++)
    if (belongsto(set1[i],set2))
      return(1);

  return(0);
}

/*************************************************************/

/* Integrates set into basis (root). We assume set is sorted and basis
   is minimal.  Note that either the basis may already subsume set, or
   set may subsume other sets in basis. In the latter, we eliminate
   from basis all those sets that are above (i.e., contain) set. If
   set is found to be subsumed by some set in basis, we return
   basis and free set. If set is NULL, we just return basis. */

struct setlist *integrate(int *set,struct setlist *root)
{
  struct setlist *temp;

  if (set == NULL)
    return(root);

  if (root == NULL) {
    root = (struct setlist *) malloc(sizeof(struct setlist));
    root->set = set;
    root->next = NULL;
    return(root);
  }

  if (subsetof(root->set,set)) {
    free(set);
    return(root);
  }

  if (subsetof(set,root->set)) {
    temp = root->next;
    free(root->set);
    free(root);
    return(integrate(set,temp));
  }
  
  root->next = integrate(set,root->next);
  return(root);
}

/*************************************************************/

struct setlist *createemptysetbasis()
{
  struct setlist *basis;
  
  basis = (struct setlist *) malloc(sizeof(struct setlist));
  basis->set = (int *) calloc(1,sizeof(int)); /* initialized to 0 */
  basis->next = NULL;
  return(basis);
}

/*************************************************************/

int *makesingleton(char *event)
{
  int *singleton;

  singleton = (int *) calloc(2,sizeof(int));
  singleton[0] = 1;
  singleton[1] = (wordnodepointer(event,alphabet))->booleanvar;
  return(singleton);
}

/*************************************************************/

/* Returns a basis corresponding to the intersection of basis1 and basis2.
   basis1 and basis2 are untouched. */

struct setlist *createproduct(struct setlist *basis1,
			      struct setlist *basis2)
{
  struct setlist *basis,*setindex1,*setindex2;
  int *array;

  if ((basis1 == NULL) || (basis2 == NULL))
    return(NULL);

  basis = NULL;

  setindex2 = basis2;

  while(setindex2 != NULL) {
    setindex1 = basis1;
    while (setindex1 != NULL) {
      array = arraymerge(setindex1->set,setindex2->set);
      basis = integrate(array,basis);
      setindex1 = setindex1->next;
    }
    setindex2 = setindex2->next;
  }

  return(basis);
}

/*************************************************************/

/* Returns a basis corresponding to the union of basis1 and basis2. 
   Both are assumed non-NULL. basis1 and basis2 are modified/destroyed
   in the process. */

struct setlist *addbases(struct setlist *basis1,
			 struct setlist *basis2)
{
  struct setlist *largebasis,*smallbasis,*temp;
  int size1,size2;
  
  if (basis1 == NULL)
    return(basis2);
  
  if (basis2 == NULL)
    return(basis1);

  size1 = 0;
  temp = basis1;
  while (temp != NULL) {
    size1++;
    temp = temp->next;
  }
  
  size2 = 0;
  temp = basis2;
  while (temp != NULL) {
    size2++;  
    temp = temp->next;
  }

  if (size1 > size2) {
    largebasis = basis1;
    smallbasis = basis2;
  }
  else {
    largebasis = basis2;
    smallbasis = basis1;
  }
    
  temp = smallbasis;
  while (temp != NULL) {
    largebasis = integrate(temp->set,largebasis);
    temp = temp->next;
  }

  while (smallbasis != NULL) { /* This rather than freebasis(): */
    temp = smallbasis->next;   /* Keep the sets! */
    free(smallbasis);
    smallbasis = temp;
  }

  return(largebasis);
}

/*************************************************************/

/* counts the number of elements in a set. */

int setsize(struct wordnode *root)
{
  if (root == NULL)
    return(0);
  return(setsize(root->left) + setsize(root->right) + 1);
}

/*************************************************************/

/* recursively flattens root into array; we return the last
   occupied position in array everytime.
*/

int *updatesetarray(int *array,struct wordnode *root)
{
  if (root != NULL) {
    array = updatesetarray(array,root->left);
    *(++array) = (wordnodepointer(root->wordp,alphabet))->booleanvar;
    array = updatesetarray(array,root->right);
  }
  return(array);
}

/*************************************************************/

/* Converts set into a sorted array. */

int *makeset(struct wordnode *set)
{
  int *array;
  int size;

  array = (int *) calloc((size = setsize(set))+1, sizeof(int));
  updatesetarray(array,set);
  array[0] = size;
  return(array);
}

/*************************************************************/

/* Hides set from basis (root). basis is affected. We return basis. 
   We assume set is sorted. */

struct setlist *hidesetbasis(struct setlist *root,
			     int *set)
{
  struct setlist *temp;

  if (root == NULL)
    return(root);

  if (intersects(root->set,set)) {
    temp = root->next;
    free(root->set);
    free(root);
    return(hidesetbasis(temp,set));
  }

  root->next = hidesetbasis(root->next,set);
  return(root);
}

/*************************************************************/

/* Excises set from basisset and returns the result in a new array. */

int *makeexcision(int *basisset, int *set)
{
  int *newbasisset,*temp;
  int i,c;

  newbasisset = (int *) calloc(basisset[0]+1,sizeof(int));

  for (i = 1; i <= basisset[0]; i++)
    if (!belongsto((c = basisset[i]),set))
      newbasisset[++(newbasisset[0])] = c;
    
  temp = (int *) calloc(newbasisset[0]+1,sizeof(int));
  
  for (i = 0; i <= newbasisset[0]; i++)
    temp[i] = newbasisset[i];
    
  free(newbasisset);
  return(temp);
}
    
/*************************************************************/

/* For each set S in basis, we excise set from S, and form a brand
   new basis. basis remains untouched. */

struct setlist *createexciseset(struct setlist *basis, int *set)
{
  struct setlist *temp;

  temp = NULL;

  while (basis != NULL) {
    temp = integrate(makeexcision(basis->set,set),temp);
    basis = basis->next;
  }
  
  return(temp);
}

/*************************************************************/

/* Applies renamingmatrix to all entries in basis, and returns a brand
   new basis. basis is untouched. */

struct setlist *renamebasis(struct setlist *basis, int * *renamingmatrix)
{
  struct setlist *temp;

  temp = NULL;

  while (basis != NULL) {
    temp = integrate(apply(renamingmatrix,basis->set),temp);
    basis = basis->next;
  }
  
  return(temp);
}

/*************************************************************/

/* Applies matrix repeatedly to all entries in basis, and returns a brand
   new basis. basis is untouched. We assume matrix is not NULL. */ 

struct setlist *saturatebasis(struct setlist *basis, int * *matrix)
{
  struct setlist *temp;

  temp = NULL;

  while (basis != NULL) {
    temp = integrate(makesaturate(matrix,basis->set),temp);
    basis = basis->next;
  }
  return(temp);
}

/*************************************************************/

/* Returns a basis for the set of fair sets of processes. If there are
   no such sets, returns NULL. */

struct setlist *createfair(struct procnode *process)
{
  int * *renamingmatrix;
  int * *nonexpansivematrix;
  struct setlist *basis1,*basis2,*basis3,*basis4,*basis5,*basis6;
  int *set;

  if (process == NULL) {
    printf("Internal error: evaluating fair sets of NULL process\n");
    exit(1);
  }
  
  if ((strcmp(process->tag,"STOP") == 0) ||
      (strcmp(process->tag,"SKIP") == 0))
    return(createemptysetbasis());

  if (strcmp(process->tag,"->") == 0)
    return(createfair(process->procarg1));

  if ((strcmp(process->tag,"[]") == 0) ||
      (strcmp(process->tag,"|~|") == 0) ||
      (strcmp(process->tag,"|||") == 0) ||
      (strcmp(process->tag,";") == 0)) {
    basis1 = createfair(process->procarg1);
    basis2 = createfair(process->procarg2);
    basis3 = createproduct(basis1,basis2);
    freebasis(basis1);
    freebasis(basis2);
    return(basis3);
  }

  if (strcmp(process->tag,"[|{}|]") == 0) {
    set = process->data.set;
    basis1 = createfair(process->procarg1);
    basis2 = createfair(process->procarg2);
    basis3 = createexciseset(basis1,set);
    basis4 = createexciseset(basis2,set);
    free(set);
    basis5 = createproduct(basis1,basis4);
    freebasis(basis1); 
    freebasis(basis4);
    basis6 = createproduct(basis2,basis3);
    freebasis(basis2);
    freebasis(basis3);
    return(addbases(basis5,basis6));
  }

  if (strcmp(process->tag,"\\") == 0) {
    basis1 = createfair(process->procarg1);
    set = process->data.set;
    basis1 = hidesetbasis(basis1,set);
    free(set);
    return(basis1);
  }

  if (strcmp(process->tag,"[[<-]]") == 0) {
    basis1 = createfair(process->procarg1);  
    renamingmatrix = process->data.renamingmatrix;
    basis2 = renamebasis(basis1,renamingmatrix); 
    freematrix(renamingmatrix);
    freebasis(basis1);
    return(basis2);
  }

  if (strcmp(process->tag,"var") == 0)
    return(createemptysetbasis());

  if (strcmp(process->tag,"mu") == 0) {
    basis1 = process->procarg1->data.varguardstree->guards;
    basis2 = createfair(process->procarg1);
    basis3 = createproduct(basis1,basis2);
    freebasis(basis1);
    freebasis(basis2);
    nonexpansivematrix = process->procarg1->data.nonextree->nonexmatrix;
    basis4 = saturatebasis(basis3,nonexpansivematrix);
    freebasis(basis3);
    freematrix(nonexpansivematrix);
    return(basis4);
  }

  printf("Internal error: tag %s should not have occurred\n",process->tag);
  exit(1);
  
  return(NULL);  /* bogus return to avoid warning */
}

/*************************************************************/

/* We recursively descend into process and, from the bottom up, fill
   out the guards part of the field "data". We then clean up (free)
   all tick guards and all var guards except the X guards of nodes
   whose immediate parent is of the form mu X * ....  
   We always return the list of free variables of process. */

struct wordlist *assignguardsinfo(struct procnode *process)
{
  struct varguardsnode *pointer1,*pointer2;
  struct wordlist *list1,*list2,*list,*temp;
  int * *renamingmatrix;
  struct setlist *basis1,*basis2,*basis3,*basis4,*basis5,*basis6,*basis7;
  int *set;

  if (process == NULL) {
    printf("Internal error: assigning guards to NULL process\n");
    exit(1);
  }

  if (strcmp(process->tag,"STOP") == 0) { 
    process->data.tickguards = createemptysetbasis();
    /* No varguards since there are no free variables. */
    return(NULL);
  }
  
  if (strcmp(process->tag,"SKIP") == 0)
    return(NULL);

  if (strcmp(process->tag,"->") == 0) {
    list = assignguardsinfo(process->procarg1);

    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    set = makesingleton(process->name); 
    process->data.tickguards = integrate(set,basis1);
    
    /* now varguards */
    temp = list;
    while (temp != NULL) {
      basis1 = (varguardsnodepointer(temp->wordp,
				     process->procarg1->data.varguardstree))
	->guards;
      set = makesingleton(process->name);
      basis2 = integrate(set,basis1);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis2);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    return(list);
  }
  
  if ((strcmp(process->tag,"[]") == 0) ||
      (strcmp(process->tag,"|~|") == 0)) {
    list1 = assignguardsinfo(process->procarg1);
    list2 = assignguardsinfo(process->procarg2);
    list = mergewordlist(list1,list2);

    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    basis2 = process->procarg2->data.tickguards;
    basis3 = createproduct(basis1,basis2);
    freebasis(basis1);
    freebasis(basis2);
    process->data.tickguards = basis3;

    /* now varguards */
    temp = list;
    while (temp != NULL) {
      pointer1 = varguardsnodepointer(temp->wordp,
				      process->procarg1->data.varguardstree);
      pointer2 = varguardsnodepointer(temp->wordp,
				      process->procarg2->data.varguardstree);
      basis1 = (pointer1 == NULL)? createemptysetbasis() : pointer1->guards;
      basis2 = (pointer2 == NULL)? createemptysetbasis() : pointer2->guards;
      basis3 = createproduct(basis1,basis2);
      freebasis(basis1);
      freebasis(basis2);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis3);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    zapvarguardstree(process->procarg2->data.varguardstree);
    return(list);
  }

  if ((strcmp(process->tag,"[|{}|]") == 0) ||
      (strcmp(process->tag,"|||") == 0)) {
    list1 = assignguardsinfo(process->procarg1);
    list2 = assignguardsinfo(process->procarg2);
    list = mergewordlist(list1,list2);
    
    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    basis2 = process->procarg2->data.tickguards;
    process->data.tickguards = addbases(basis1,basis2);

    /* now varguards */
    temp = list;
    while (temp != NULL) {
      pointer1 = varguardsnodepointer(temp->wordp,
				      process->procarg1->data.varguardstree);
      pointer2 = varguardsnodepointer(temp->wordp,
				      process->procarg2->data.varguardstree);
      basis1 = (pointer1 == NULL)? createemptysetbasis() : pointer1->guards;
      basis2 = (pointer2 == NULL)? createemptysetbasis() : pointer2->guards;
      basis3 = createproduct(basis1,basis2);
      freebasis(basis1);
      freebasis(basis2);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis3);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    zapvarguardstree(process->procarg2->data.varguardstree);   
    return(list);
  }
    
  if (strcmp(process->tag,";") == 0) {
    list1 = assignguardsinfo(process->procarg1);
    list2 = assignguardsinfo(process->procarg2);
    list = mergewordlist(list1,list2);
    
    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    basis2 = process->procarg2->data.tickguards;
    basis3 = duplicatebasis(basis1);  
    process->data.tickguards = addbases(basis1,basis2);

    /* now varguards */
    temp = list;
    while (temp != NULL) {
      pointer1 = varguardsnodepointer(temp->wordp,
				      process->procarg1->data.varguardstree);
      pointer2 = varguardsnodepointer(temp->wordp,
				      process->procarg2->data.varguardstree);
      basis4 = (pointer1 == NULL)? createemptysetbasis() : pointer1->guards;
      basis5 = (pointer2 == NULL)? createemptysetbasis() : pointer2->guards;
      basis6 = addbases(basis3,basis5);
      basis7 = createproduct(basis4,basis6);
      freebasis(basis4);
      freebasis(basis6);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis7);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    zapvarguardstree(process->procarg2->data.varguardstree);
    return(list);
  }
    
  if (strcmp(process->tag,"\\") == 0) {
    list = assignguardsinfo(process->procarg1);
    set = process->data.set;

    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    process->data.tickguards = hidesetbasis(basis1,set);
    
    /* now varguards */
    temp = list;
    while (temp != NULL) {
      basis1 = (varguardsnodepointer(temp->wordp,
				     process->procarg1->data.varguardstree))
	->guards;
      basis2 = hidesetbasis(basis1,set);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis2);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    return(list);
  }

  if (strcmp(process->tag,"[[<-]]") == 0) {
    list = assignguardsinfo(process->procarg1);
    renamingmatrix = process->data.renamingmatrix;

    /* first tickguards */
    basis1 = process->procarg1->data.tickguards;
    process->data.tickguards = renamebasis(basis1,renamingmatrix);
    freebasis(basis1);
   
    /* now varguards */
    temp = list;
    while (temp != NULL) {
      basis1 = (varguardsnodepointer(temp->wordp,
				     process->procarg1->data.varguardstree))
	->guards;
      basis2 = renamebasis(basis1,renamingmatrix);
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis2);
      freebasis(basis1);
      temp = temp->next;
    }
    zapvarguardstree(process->procarg1->data.varguardstree);
    return(list);
  }

  if (strcmp(process->tag,"var") == 0) {
    /* tickguards is NULL, so is varguards, but we must make a note */
    process->data.varguardstree = 
      addvarguardsnode(NULL,
		       process->name,
		       NULL);
    return(addwordlist(NULL,process->name));
  }

  if (strcmp(process->tag,"mu") == 0) {
    list = assignguardsinfo(process->procarg1);
    list = deletewordlist(list,process->name);
    temp = list;

    /* first tickguards */
    process->data.tickguards = process->procarg1->data.tickguards;

    /* now varguards */
    while (temp != NULL) {
      basis1 = (varguardsnodepointer(temp->wordp,
				     process->procarg1->data.varguardstree))
	->guards;
      process->data.varguardstree = 
	addvarguardsnode(process->data.varguardstree,
			 temp->wordp,
			 basis1);
      temp = temp->next;
    }
    basis1 = (varguardsnodepointer(process->name,
				  process->procarg1->data.varguardstree))
      ->guards;
    zapvarguardstree(process->procarg1->data.varguardstree);
    process->procarg1->data.varguardstree = 
      addvarguardsnode(NULL,
		       process->name,
		       basis1);
    return(list);
  }

  printf("Internal error: tag %s should not have occurred\n",process->tag);
  exit(1);
  
  return(NULL);  /* bogus return to avoid warning */
}

/*************************************************************/

/* We recursively descend into process and, from the bottom up, fill
   out the field "data" (except for guards). When the node is a hiding
   or synchronized parallel, we store the set as an array of ints in
   data.set; otherwise data.set remains NULL. For a renaming node, we
   store the renaming relation in matrix form in data.renamingmatrix,
   otherwise leave it NULL. We always return the list of free
   variables of process. For each process node, for each free
   variable, we store the corresponding nonexpansive matrix within
   data.nonexmat. We then clean up (free) all nonexpansive matrices
   except N_X(P) for nodes P whose immediate parent is of the form mu
   X * (P). */

struct wordlist *assignstaticinfo(struct procnode *process)
{
  struct nonexmatnode *pointer1,*pointer2;
  int * *matrix1;
  int * *matrix2;
  int * *matrix3;
  struct wordlist *list1,*list2,*list,*temp;

  if (process == NULL) {
    printf("Internal error: assigning staticinfo to NULL process\n");
    exit(1);
  }

  if ((strcmp(process->tag,"STOP") == 0) ||
      (strcmp(process->tag,"SKIP") == 0))
    return(NULL); /* All static data remain NULL */

  if (strcmp(process->tag,"->") == 0) { /* NO NEW ALLOCATION */
    list = assignstaticinfo(process->procarg1);
    process->data.nonextree = process->procarg1->data.nonextree;
    return(list);
  }

  if ((strcmp(process->tag,"|~|") == 0) ||
      (strcmp(process->tag,"[]") == 0) ||
      (strcmp(process->tag,";") == 0)||
      (strcmp(process->tag,"[|{}|]") == 0) ||
      (strcmp(process->tag,"|||") == 0)) {
    if (strcmp(process->tag,"[|{}|]") == 0)
      process->data.set = makeset(process->setrelarg);
    list1 = assignstaticinfo(process->procarg1);
    list2 = assignstaticinfo(process->procarg2);
    list = mergewordlist(list1,list2);

    temp = list;
    while (temp != NULL) {
      pointer1 = nonexmatnodepointer(temp->wordp,
				     process->procarg1->data.nonextree);
      pointer2 = nonexmatnodepointer(temp->wordp,
				     process->procarg2->data.nonextree);
      matrix1 = (pointer1 == NULL)? NULL : pointer1->nonexmatrix;
      matrix2 = (pointer2 == NULL)? NULL : pointer2->nonexmatrix;

      matrix3 = buildmerge(matrix1,matrix2);
      process->data.nonextree = addnonexmatnode(process->data.nonextree,
						temp->wordp,
						matrix3);
      temp = temp->next;
    }
    zapnonextree(process->procarg1->data.nonextree);
    zapnonextree(process->procarg2->data.nonextree);
    return(list);
  }

  if (strcmp(process->tag,"\\") == 0) {
    list = assignstaticinfo(process->procarg1);
    temp = list;
    process->data.set = makeset(process->setrelarg);

    while (temp != NULL) {
      matrix1 =  
	(nonexmatnodepointer(temp->wordp,
			     process->procarg1->data.nonextree))->nonexmatrix;

      matrix2 = hidesetmatrix(matrix1,process->data.set);
      process->data.nonextree = addnonexmatnode(process->data.nonextree,
						temp->wordp,
						matrix2);
      temp = temp->next;
    }
    return(list);
  }

  if (strcmp(process->tag,"[[<-]]") == 0) {
    list = assignstaticinfo(process->procarg1);
    temp = list;
    process->data.renamingmatrix = buildrenamingmatrix(process->setrelarg);

    while (temp != NULL) {
      matrix1 =  
	(nonexmatnodepointer(temp->wordp,
			     process->procarg1->data.nonextree))->nonexmatrix;
      
      matrix2 = buildrenamed(matrix1,process->data.renamingmatrix);
      process->data.nonextree = addnonexmatnode(process->data.nonextree,
						temp->wordp,
						matrix2);
      temp = temp->next;
    }
    zapnonextree(process->procarg1->data.nonextree);
    return(list); 
  }

  if (strcmp(process->tag,"var") == 0) {
    process->data.nonextree = addnonexmatnode(NULL,
					      process->name,
					      buildidentity());
    return(addwordlist(NULL,process->name));
  }
  
  if (strcmp(process->tag,"mu") == 0) {
    list = assignstaticinfo(process->procarg1);
    list = deletewordlist(list,process->name);
    temp = list;
    
    while (temp != NULL) {
      matrix1 = 
	(nonexmatnodepointer(temp->wordp,
			     process->procarg1->data.nonextree))->nonexmatrix;
      matrix2 = 
	(nonexmatnodepointer(process->name,
			     process->procarg1->data.nonextree))->nonexmatrix;
      matrix3 = buildsaturate(matrix1,matrix2);
      process->data.nonextree = addnonexmatnode(process->data.nonextree,
						temp->wordp,
						matrix3);
      temp = temp->next;
    }
    process->procarg1->data.nonextree = 
      zapnonextreebut(process->procarg1->data.nonextree,
		      process->name);
    return(list); 
  }

  printf("Internal error: tag %s should not have occurred\n",process->tag);
  exit(1);

  return(NULL);  /* bogus return to avoid warning */
}

/*************************************************************/

/* dumps the data on the screen */

void dump()
{
  printf("SIGMA = {");
  printwordnodetree(alphabet,1);
  printf("}\n\n");

  if (sets != NULL) {
    printf("SETS:\n-----\n");
    printsetnodetree(sets);
    printf("\n");
  }

  if (renrels != NULL) {
    printf("RELATIONS:\n----------\n");
    printrelnodetree(renrels);
    printf("\n");
  }

  if (vector != NULL) {
    printf("PROCESSES:\n----------\n");
    printvectorlist(vector);
    printf("\n");
  }
}

/*************************************************************/

void divcheck(struct procnode *process) 
{ 
  struct setlist *fairsets;

  if (procnametobedefined != NULL) {
    printf("Line %d: error: the following processes are undefined:\n",
	   lineno);
    printwordlist(procnametobedefined);
    exit(1);
  }

  if (!terseoption) {
    dump();
    printf("divcheck ");     
    printprocess(process);
    printf("\n\n");
  }

  if (!muoption) { /* Need to Bekicify *process */ 
    process = trimfree(bekic(process));
    if (bekicoption) {
      printf("which becomes...\n\n");
      printprocess(process);
      printf("\n\n");
    }
  }
  else
    process = trimfree(process);

  /* Now we have a pure mu process in "process" */

  alphabetsize = assignboolvars(1,alphabet) - 1;

  assignstaticinfo(process);
  assignguardsinfo(process);

  fairsets = createfair(process); 

  if (fairsets == NULL)
    printf("POTENTIAL LIVELOCK\n\n");
  else {
    printf("LIVELOCK-FREE\n\n");
    if (!terseoption) {
      printf("FAIR SETS BASIS:\n----------------\n");
      printsetlist(fairsets);
      printf("\n");
    } 
    freebasis(fairsets);
  }
}

/*************************************************************/

int main(int argc, char *argv[])

{
  char wordbuf[MAXWORD], wordbuf1[MAXWORD], wordbuf2[MAXWORD];
  struct procnode *process;
  int c;
 
  printf("\nThis is SLAP, version 0.1 (beta release)\n\n");
 
  readcommandline(argc,argv);

  lineno = 1;

  alphabet  = NULL;
  sets      = NULL;
  renrels   = NULL;
  procnametobedefined = NULL;
  vector    = NULL;

  initialize_defined();

  while (getnextnnl(wordbuf) != EOF) {
    if (!identchar(wordbuf[0])) {
      printf("Line %d: syntax error: %s\n",lineno,wordbuf);
      exit(1);
    }
    
    if (strcmp(wordbuf,"channel") == 0) {
      getchannels();
      getnewline();
      continue;
    }
    
    if (strcmp(wordbuf,"divcheck") == 0) {
      process = getprocess();
      if (getnextnnl(wordbuf1) != EOF) {
	printf("Line %d: syntax error: EOF expected after\
 divcheck command, instead of %s\n",lineno,wordbuf1);
	exit(1);
      }
      fclose(inputfile); 
      divcheck(process);
      return(0);
    }

    if ((c = getnext(wordbuf1)) != '=') {
      printf("Line %d: syntax error: \'=\' expected instead of\
 \'%c\'\n",lineno,c);
      exit(1);
    }

    /* Now c is '=' */

    if (wordnodepointer(wordbuf,defined) != NULL) {
      printf("Line %d: error: %s already defined\n",lineno,wordbuf);
      exit(1);
    }

    if (getnextnnl(wordbuf2) == EOF) {
     printf("Line %d: syntax error: EOF after \'=\'\n",lineno);
      exit(1);
    } 

    if (wordbuf2[0] == '{') { 
      sets = addsetnode(sets,wordbuf,getset());
      getnewline();
    }
    else if (wordbuf2[0] == '[') {
      renrels = addrelnode(renrels,wordbuf,getrel());
      getnewline();
    }
    else {
      ungetword(wordbuf2);
      if (wordlistpointer(wordbuf,procnametobedefined) == NULL) 
	procnametobedefined = addwordlist(procnametobedefined,wordbuf);
      /* above is useful when mu option is on, to prevent P = mu P * ... */
      vector = addvectornode(vector,wordbuf,getprocess());
      procnametobedefined = deletewordlist(procnametobedefined,wordbuf);
      /* note that procnametobedefined never contains more than one
	 instance of a process name, so deletewordlist really removes the
         process name. */
      getnewline();
    }
    defined = addwordnode(defined,wordbuf);
  }
  
  printf("Line %d: error: no divcheck command in file\n",lineno);
  exit(1);
}


