
/* PNS.H -- Version 2.3 (July 2011)

   This is the main header file. It defines the data types used for Petri net
   representation as well as other data types used for the input specification
   and code generation. More information about the meaning of the data types
   for input specifications can be found in the file input2.sp. */

#ifndef PNS_H
#define PNS_H

#include<stdio.h>
#include<stdlib.h>
#include<stdarg.h> 
#include<string.h>
#include"general.h"
#include"matrix.h"


typedef struct cblock {
  char *text;
  char *file;
  int line; // the line of 'file' on which the text begins
} cblock;


typedef struct TransInfo {
  //char *name; /* the name of the transition useful for debugging purposes */
  int l; /* the observation label; l = 0 means no label is assigned. */
  unsigned uncontrollable:1; /* 0 if controllable */
  unsigned unobservable:1;   /* 0 if observable */
  unsigned live:1; /* 1 if transition should be made live */
} TransInfo; /* Default values set by tCheck() in pns.c */

/* Each transition has a TransInfo object. Lines of the specification file
   of the form 
     uncontrollable: t1 t4 
     live: t1 t6
     unobservable: t2 
   can be implemented by setting the corresponding bits of the TransInfo
   objects associated with the transitions. 
*/

typedef struct PlaceInfo {
  //char *name; /* the name of the place useful for debugging purposes */
  unsigned nondeterministic:1; /* 1 if the place is nondeterministic */
} PlaceInfo;


struct placelist {
  int place;
  struct placelist* next;
};

typedef struct arcs {
  int in_place; /* negative number means no input place */
  struct placelist *out_places;
  cblock condition; /* activation condition of the arc */
  struct arcs *next;
} arcs;

/* The structure arcs describes how a process should continue when a 
   transition is fired. Each object of this type represents one of the 
   specification file commands of the form 
     (place, transition, places).{condition} 
   Examples: 
   1) (p3, t, p2, p4).{i == 1} would correspond to
      in_place = 3; // assuming p3 has the row 3 of incidence matrix  
      condition = "i == 1";
      out_places->place = 2;
      out_places->next->place = 4;  out_places->next->next = 0;
   2) (p3, t)
      in_place = 3; condition = 0; out_places = 0;
      3) (t, p2, p4)
      in_place = -1; // negative number means no place
      out_places->place = 2;
      out_places->next->place = 4; out_places->next->next = 0;    
*/

typedef struct pns {
  /* Defines a Petri net structure and the initial marking. */
  /* Note: It is expected that all arrays are allocated dynamically. */

  int pnum; /* number of places */
  int tnum; /* number of transitions */

  matrix out;/*The output matrix D^-; places on rows, transitions on columns.*/

  matrix in; /*The input matrix D^+; places on rows, transitions on columns. */

  /* The places */

  /* There are pnum places: 0, 1, 2, ..., pnum-1. The place number i 
     corresponds to the rows i of the input and output matrices. */

  int* marking; /* The initial marking. For instance, marking[1] is the marking
		   of the place 1. */

  int* C; /* The capacities of the places. If C = 0, all places have infinite 
	     capacity. If C[i] = 0, the place i has infinite capacity. */

  char **place_name; /* Defines names for each of the places 0 ... pnum-1. This
			is useful for debugging purposes. For instance, 
			place_name[0] is the name of the place 0. */

  cblock *segment; /* Array containing segments of code for each place. For 
		      instance, segment[1] describes the segment of code 
                      associated with the place 1. */

  cblock *select; /* select[i] refers to the function used to select 
		     between transitions enabled by the place i. Refer to the 
		     code generation module for details. */

  PlaceInfo* p; /* If p = 0 assume default values for places. */

  /* The transitions */

  /* There are tnum transitions: 0, 1, 2, ..., tnum-1. The transition number i 
     corresponds to the columns i of the input and output matrices. */

  char **trans_name; /* Defines names for each transition. This
			is useful for debugging purposes. For instance, 
			trans_name[0] is the name of the transition 0. */

  TransInfo* t; /* If t = 0 assume default values for transitions */

  arcs** arc_list; /* Directs the implementation of the transition arcs
		      in software. Note that arc_list[i] is the list of 
		      arcs corresponding to the transition i. Currently 
		      used for plant PNs, not supervisor PNs. */

  void* data; /* provides a way to associate arbitrary data with a PN */

} pns;



#define new_label(x) --x;
/* Used to generate automatically labels. This kind of labels are negative.
   The parameter is the last label number and identifies the set of labels
   generated automatically: {x, x+1, ... , -2, -1}. */


inline int get_label(pns* pn, int t); 
/* Returns the label of t or zero if no label is defined */


inline int get_marking(pns* pn, int place);
/* Returns the (initial) marking of the place */


pns createpn(const char *str, ...);
/* Creates pns objects. This is the format:
   createpn("param1 param2 param3 ...", param1, param2, param3, ...)
   where these are the possible parameters. 
   IT IS ESSENTIAL THAT THE PARAMETERS HAVE THE CORRECT TYPE. 
   THE FIELDS OF THE OBJECT MAY NOT BE ALL ALLOCATED UNLESS ALL RELEVANT 
   INFORMATION IS GIVEN. 
   - pnum: int type expected. Represents the number of places. 
   - tnum: int type expected. Represents the number of transitions.
   - D:  int* type expected. Represents the incidence matrix. This option 
   may also be used for arrays declared with lines of the form 
   "int D[m][n];", such as "int D[2][3];".  
   - Dm: int* type expected. Represents the output matrix.
   - Dp: int* type expected. Represents the input matrix.
   - pD:  int** type expected. Represents the incidence matrix.
   - pDm: int** type expected. Represents the output matrix.
   - pDp: int** type expected. Represents the input matrix.
   - mD:  matrix type expected. Represents the incidence matrix.
   - mDm: matrix type expected. Represents the output matrix.
   - mDp: matrix type expected. Represents the input matrix.
 
   - arcs: int and arcs* types expected, in this order. The integer 
   argument identifies the transition. The arcs* argument is placed
   in the arcs_list element of the pns object. Therefore, do not 
   deallocate it! All the 'next' pointers in the arcs* argument must 
   be zero, unless some other element follows. 
   - C: int* type expected. The parameter is the capacity vector.
   - freelabel: int* type expected. Assigns distinct labels to unlabeled
   transitions. The parameter should be the address of an integer 
   variable. Labels are distinct if no other variable is used for
   free labeling, the variable is never modified except by 
   createpn/updatepn, and its initial value is <= 0.
   - label: int* type expected. Represents transition labels.
   - live: int type expected. The parameter identifies the transition 
   that should be live.
   - m0: int* type expected. The parameter is the initial marking vector.
   - nondeterministic: int type expected. The parameter identifies the
   place that should be marked as nondeterministic.
   - place_name: int and char*. That is, two arguments are expected in 
   this order. The integer identifies the place (0 ... pnum-1) and 
   the pointer to characters gives its name. Note that the string
   is copied. Thus, the memory used by the second argument will not be 
   deallocated by deallocating the memory used by the pn object.
   - segment: int, int, and char* types expected, in this order. See 
   comments for place_name. The second int is the line number. Note:
   the 'file' field of the cblock structure is not used. 
   - select: int, int, and char* types expected, in this order. See 
     comments for segment.
   - trans_name: int and char* types expected, in this order. See 
     comments for place_name.
   - Tuc: int* type expected. Tuc[i] = 0 if transition i is controllable.
                              Tuc[i] = 1 otherwise.
   - Tuo: int* type expected. Tuo[i] = 0 if transition i is observable.
                              Tuo[i] = 1 otherwise.
   - uncontrollable: int type expected. The parameter identifies the
     transition that should be marked as uncontrollable.
   - unobservable: int type expected. The parameter identifies the
     transition that should be marked as unobservable.

   Additional options can be found in the definition of the function.
*/

void updatepn(pns* pn, const char *str, ...);
/* Updates object created by createpn. It has the same options as createpn.
   However, changing the number of places or transitions is not allowed. */

pns getpn(matrix* Dm, matrix* Dp, int* Tuc, int* Tuo, int* m0, int* C);
/* SPNBOX function. 
   Used to create a pns object based on the output and input matrices, the 
   lists of uncontrollable and unobservable transitions, the initial marking,
   and the capacity of the places. Parameters of zero value 
   request the default initialization of the pns object. */

pns copypn(pns* pn); /* Creates a copy of *pn. */

void d2dd(const matrix* D, matrix* Dm, matrix* Dp);
/* SPNBOX function. 
   Determines the input and output matrices Dm and Dp of a pure PN based on
   the incidence matrix D. The function assumes that Dm and Dp are already
   allocated and have the right dimension. */ 

void deallocpn(pns *pn); 
/* frees the space used by the arrays inside the pns structure */

void displaypn(pns pn, FILE *f); 
/* Write pn information into a file. */

inline int nextmarking(pns *pn, int* m1, int t, int* m2);
/* Initializes m2 such that m1[t>m2. Returns 0 if t is not enabled. If t 
   is not enabled the value of m2 is undefined! */

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


/* The following structures are used in ComposePN in order to associate to
   each transition of the composed PN the list of transitions from which it 
   is obtained. */

struct tranlist {
  pns* pn;
  int t; /* the transition of pn */
  struct tranlist *next;
};

struct tarray {
  struct tranlist *T; /* array of n elements */
  int n; /* the number of elements in the array T */
  struct alloc mem; // struct alloc defined in general.h for memory management
};

#define alloc_tarray(p,m)						\
  if(!m) p = 0;								\
  else {								\
    p = tcalloc(1, sizeof(struct tarray));				\
    ((struct tarray*) (p))->n = m;					\
    ((struct tarray*) (p))->T = tcalloc(m, sizeof(struct tranlist));	\
    initalloc(&(((struct tarray*) (p))->mem), 50*sizeof(struct tranlist)); \
  }

void dealloc_tarray(struct tarray* p); /* in pns.c */
/* deallocates everything, including p itself */


// The following composition-information structure is used in order to
// determine the origin of a place or transition of a PN obtained by 
// parallel composition. 
struct cpinfo {     
  struct tarray *T; // Information about transition i at T->T[i]
  struct tarray *P; // Information about place i at P->T[i]
};


void dealloc_cpinfo(struct cpinfo* p); // in pns.c
/* deallocates everything, including p itself */



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

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

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

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

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

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


#define composepn(x,y) ComposePN(x,y,0,0,0);



#define MARKINGV 0 /* marking */
#define FIRINGV  1 /* firing vector */
#define PARIKHV  2 /* Parikh vector (firing count vector) */

#define __NAME_SYMBOL "$$$" 
/* When the specification is written, the name of the files generated by the 
   program may not be known. Moreover, build rules in the specification file 
   may apply to several different file names, for different families of 
   process instances may have different files. Thus, when build rules are 
   written in the specification, the text defined above should be used in the 
   place of a specific file name. The code generation module replaces this
   text with the actual file name WITHOUT ANY EXTENSION. */  


typedef struct variable { /* list of variables in an inequality */
  unsigned char type:2; /* type = MARKINGV, FIRINGV, or PARIKHV. Indicates whether the 
		      variable is part of the marking, firing, or Parikh vector.*/
  int coefficient; /* the coefficient of the variable in the inequality */
  pns* pn;   /* the address of the PN to which the variable belongs; the address
                should match the address of a process PN. */
  int index; /* index of place or transition in PN (row or column number in 
		the input and output matrices) */
  struct variable *next;
} variable;


typedef struct inequality { 
  /* Describes an inequality of the form a1*x1 + a2*x2 + ... <= b, where
     x1, x2, ... are variables and a1, a2, ... b are integers. */ 
  int free_term; /* the free term b */
  variable* variable_list; /* Describes the variables x1, x2, ... and their */
} inequality;              /* coefficients. */

typedef struct inequality2 { 
  /* Describes an inequality of the form a1*x1 + a2*x2 + ... <= b, where
     x1, x2, ... are variables and a1, a2, ... b are integers. */ 
  int free_term; /* the free term b */
  int lb, ub;	/* upper bound, lower bound */
  variable* variable_list; /* Describes the variables x1, x2, ... and their */
} inequality2;              /* coefficients. */

typedef struct expression { /* Describes logic expressions of inequalities. */
  int type:1; /* operation type; 0 indicates AND; 1 indicates OR */
  struct expression *left_expr, *right_expr; /* nonzero iff ineq is zero */
  struct inequality *left_ineq, *right_ineq; /* nonzero iff expr is zero */
} expression;

  /* Example: an expression ((A AND B) OR C ) OR (D AND E) is represented by
     the following tree. Note that A, B, C, D, E are inequalities. 

       ((A AND B) OR C ) OR (D AND E)
            /                  \
           /                    \
    ((A AND B) OR C )         (D AND E)
        /       \               /   \
       /         \             /     \
   (A AND B)      C           D       E
    /    \
   /      \
  A        B

  */

/* The following generalizes the previous data type so that we can have
   conjunctions and disjunctions of an arbitrary number of terms. 
   This creates a tree in which each node may have an arbitrary number 
   of successors. */

typedef struct expression2 {
  unsigned char type:1; /* operation type; 0 indicates AND; 1 indicates OR */
  unsigned char n:7; /* the number of successor nodes and leaves */
  struct expression2 **successor; // should be an array of n elements
  struct inequality2 **leaf; // should be an array of n elements
  /* For each i = 0 ... n-1, exactly ONE of leaf[i] and successor[i] is 
     nonzero. */
} expression2;


typedef struct constraint {
  expression *expr;
  struct constraint *next;
} constraint;


/* The following structure is used to represent commands of the form 
     sync pn1.t1 pn2.t2 
   in the specification file.*/

typedef struct syncc { /* Each element of the list mentions that the transition
                         t1 of pn1 is the same as t2 of pn2. */
  pns *pn1, *pn2;     
  int t1, t2;         /* t1 (t2) is the column number of the input & output 
			 matrices that corresponds to t1 (t2). */
  struct syncc *next;  
} syncc;

/* The concept of "process types" has been used with two meanings:
   (a) a process type defined in the low level language
   (b) the class of a group of processes that have exactly the same properties 
   (such as, they are synchronized the same way and are monitored the same 
   way by the supervisor).

   Accordind to the meaning (b), the following 'struct process' defines process
   types. In the future, these will be called process subtypes (to distinguish
   them from the (a) interpretation). 
 */

typedef struct process { 
  /* Represents an instance of a process or of a group of identical processes.
     NOTE: 
     1) Two different 'process' objects may not share the same pointer 
     parameters. For instance, the 'pn' field may not be the same for two 
     different 'process' objects, even if the two objects have the same process
     type. 
     2) Any pointer to 'pns' in the 'syncc' or 'variable' structure is equal to
     the address stored in the 'pn' field of the 'process' structure.
  */
  char* file; /* the name of the file in which the process is defined */
  char* name; /* name of process type */
  char* instance; /* name of process instance */
  pns* pn; /* underlying PN structure.*/
  char* build; /* the command that should be used to build the process */
  cblock include; /* user code to be included at the beginning of the source 
                    file of the process. */
  char* dfns; /* automatically generated definitions to be included at
		 the beginning of the source file of the process */
  cblock main; /* text to be included in the main function of the process */

  char thread:1; /* set to 1 if process should be implemented as a thread */
  char supervisor:1; /* set to 1 if the process is a supervisor component */

  /* The following are not used */

  int type:1; /* type = 1 indicates an external process */
  int start:1; /* start = 1 if the supervisor should start this process */

} process;


typedef struct specs {
  char* name; /* the name of the input specs file without extension */
  pns** pn_array; /* reserved for future use; array of PNs extracted from the 
		     input specs file */
  int pn_num; /* reserved for future use; number of PNs */
  syncc* synclist; /* list of synchronization constraints */
  constraint *constraint_list; /* list of algebraic constraints */
  process **process_array; /* each array element contains the address of one
			      process object */
  int process_num; /* the number of elements of the process array */

  cblock include; /* text to be included at the beginning of the 
		    supervisor file */
  cblock main; /* text to be included in the main function of the supervisor */

  char* sbuildparam; /* Indicates additional parameters that should be included
			in the command line building main executable file.  
			Used in WriteMakefile of supervisorCompiler.c */
  unsigned char signals:1; /* if implementation should use signals */
  unsigned char sleep:1; /* if false, the supervisor does not enter a "sleep"
			    state when there are no events */
  unsigned char singlechannel:1; /* if supervisor should read from a single 
				    pipe */
  unsigned char nomain:1; /* if 0, main function will be generated */
  unsigned char templ:1; /* if 1, custom templates are expected */
} specs;


void extractLHCB(specs* sp, pns* pn, matrix* L, matrix* H, matrix* C, int** B,\
		 char **scplaces);

/* Extracts a SC specification of the form Lm + Hq + Cv <= B from sp. Also
   initializes pn to the Petri net on which the specs should be enforced. 
   Furthermore, it writes the vector scplaces so that scplaces[i] is nonzero
   when the place i of pn belongs to a supervisor component. */


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


void printLHCB(pns* pn, matrix* L, matrix* H, matrix* C, int* B, int n, FILE* f);

/* Displays the constraint number n stored in the matrices L, H. C, B. The 
   first constraint has the number 0 (not 1). To display all constraints, 
   use n < 0. The pn parameter specifies the PN on which the constraints
   are defined. If one or more of L, H, or C is unavailable, enter 0. */

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

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

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

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



char* pn_check(pns* p); // in pns.c

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


char* process_check(process* pr); // in pns.c

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


pns PNComposition(process** process_array, int num, struct cpinfo **TR);
/* Composes the PNs in the array, finds *TR, and returns the composed PN. */

#define pn_composition(x,y) PNComposition(x,y,0);


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

/* This function is obsolete. See the newer version below.

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

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


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

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

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


void dealloc_specs(specs* sp);

void dealloc_process(process* p);

void dealloc_synclist(syncc* s);

void dealloc_constraint(constraint* c);

void dealloc_expression(expression* e);

void dealloc_variable(variable* v);

void dealloc_inequality(inequality* in);

void dealloc_cblock(cblock *p);

int inline is_verbose();


/* The following are used to define 'struct label_lst', which can be used to
   create a list indicating the transitions associated with each label. The
   function used to create such a list is get_label_list, declared below. */

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

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

struct label_lst {
  int l;
  struct label_lst* next;
  struct prlist* pr; // may not be zero
};

struct label_lst* get_label_list(struct process** pr, int n);
/* The result is a label list organized in increasing order of the labels */

void free_label_list(struct label_lst* p);

specs* ScanInput(char* specs_file); 
/* Scans the file and creates specs structure. In case of error the function
   should return zero. Defined in actions.c. */


// The following describes the transitions participating in an interprocess
// synchronization.

struct sync_element { 
  int prtype; // process subtype
  int n; // the number of elements of the following arrays
  union {
    int *p; // list of place numbers of prtype for an "o" entry of synclist
    int *t; // list of trans. numbers of prtype for an "s" entry of synclist
            // Note: sync can be fired if for all 'sync_element' objects in 
            // the list 's' at least one transition in 't' is enabled.
  };
  int *w; // weight of transition arc (state machines are assumed!)
  int disj;// for "s" entry only: if nonzero, indicates the number of the entry
  // of the "o" list (i.e. 1st, 2nd, 3rd, ...) that has transitions that are 
  // an alternative to the transitions in the 't' field.
  struct sync_element *next;
};

// The following describes a list of synchronizations
//
// Each element of synclist represents a synchronization. Each element contains
// two lists of sync_element items (s and o). To fire transitions according to 
// this synchronization, there must be an enabled transition in each of the 
// sync_element items of 's'. If such a combination is found, the transitions
// in the combination can be fired. In addition, one transition from each 
// sync_element item of the list o is fired, provided the sync_element
// has a process subtype that does not appear in the list s.  
// 
// LIMITATION: Consider the list s and the list o. Note that a process will
// not make a request to fire a transition from o. The supervisor is correct
// (specifically, the function IsPermissible() of the supervisor is correct) 
// if either of 1) OR 2) is satisfied:
//  1) Any two elements of the list s correspond to different process types.
//  2) Both (a) and (b) are satisfied:
//     (a) if two elements of the list s belong to the same process type and 
//         share a common transition, they must have identical content 
//         (i.e. identical lists of transitions). 
//     (b) Recall that when a process asks the supervisor for permission to
//         fire a transition, it sends a list of firable transitions. Then,  
//         the supervisor selects a transition to fire. Any two processes
//         of the same type either send the same list of transitions or 
//         send lists that do not have any common elements. In particular, 
//         this requirement is satisfied when the lists have only one element.  
// This limitation is imposed in order to simplify the algorithms of the 
// supervisor. The supervisor must perform simple operations, not searches
// of exponential complexity. If more complex synchronization patterns are
// needed, the complexity of the supervisor function IsPermissible should
// be considered. It might be better to leave the synclist format as it is 
// and express complex synchronization patterns by more than one synclist
// element. This may also require adding new plant transitions.  

struct synclist {
  struct sync_element* s; // s may not be zero!
                          // describes input arcs (constraints of t. firing)
  struct sync_element* o; // describes output arcs (what procs are started)
  struct synclist* next;  // link to next synchronization; it may be zero.
};


// The following structure describes transition data. It indicates whether a
// plant transition is controlled and/or observed by a supervisor. It could 
// be enhanced for decentralized control purposes.

typedef struct _TrData {
  char flags; // if (flags & 1) then controlled by DES supervisor
              // if (flags & 2) then observed by DES supervisor
              // if (flags & 4) then controlled for synchronizations
              // if (flags & 8) then observed for synchronizations

  // int s_id; // Id of supervisor in charge of this transition
} TrData;


TrData** get_TrData(pns *sr, process** prarray, int num, struct label_lst* llst);
/* sr: the pn of the supervisor
   prarray: the array of process subtypes
   num: the number of process subtypes (number of rows of prarray)
   Return value: an array x such that x[s][t] is the TrData object associated 
   with the transition t of the process subtype s.
   The function is defined in the 2010 supervisorCompiler.c. */

void free_TrData(TrData** p, int num);
/* num: the number of rows of p, that is, the number of process subtypes. 
   The function is defined in the 2010 supervisorCompiler.c. */

struct synclist* get_synclist(struct label_lst* lls, process** prarray);
/* Obtains one of the parameters required for code generation based on the 
   'lls' object and the array of process subtypes. Note that 'lls' must be 
   obtained with get_label_list(). */

void free_synclist(struct synclist* p);


int GenerateProgam(pns *supervisor, char* sname, process** prarray, int num); 
/* Used in the 2009 version of the software. UNDEFINED in the subsequent version.
   Generates the supervisor and the process source files. It also generates
   the makefile that should be used to build them. Note that sname is the 
   name of the supervisor program. Further, num is the number of processes. */


int CodeGenerator(pns *supervisor, specs* sp, process** prarray, int num,\
		  struct synclist* sl, TrData** TInf); 
/* This is the 2010 version of GenerateProgram. 
   The function is defined in the 2010 supervisorCompiler.c.

   'sbuildparam' gives a list of parameters (such as file names) that 
   should be included in the command line building the executable file of the
   supervisor. 'sbuildparam' is used in WriteMakefile of supervisorCompiler.c.
   Note that files generated by the code generation module are included 
   automatically, as appropriate. Only additional parameters or files should 
   be included in 'sbuildparam'. Use sbuildparam = 0 if there are no 
   additional parameters.*/


#endif 
