/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 *******************************************************************
 *  $Log$
 *******************************************************************/

/*******************************************************************
 *
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *  Juan Carlos Berrocal Colmenarejo
 *
 *  3 Sept 1991
 *
 *  Basic Management of LOTOS attributes
 *  
 *  Definition of LOTOS attributes and functions to manage them.
 *  The attributes defined are:
 *
 *     GLA   -> Gate List Attribute.
 *     GSA   -> Gate Set Attribute.
 *     PA    -> Predicate Attribute.
 *     ELA   -> Expr List Attribute. 
 *     OLA   -> Offer List Attribute.
 *     RFLA  -> Relab Func List Attribute.
 *     VALA  -> Var Assign List Attribute.
 *     GDLA  -> Gate Declaration List Attribute
 *     ITCLA -> Interleaved Continuation list Attribute
 *     SSLA  -> Specification Source Line Attribute
 *     STA   -> Synchronization Tree Attribute
 *
 *  Common prefixes for all attribute value functions are the following
 *  ( X stand for any structure name (GL,GS,...) and
 *    V for a value stored in X ) :
 *
 *     InitX     : initialize the usage of structures X.
 *     NewX      : create a not initialized structure X.
 *     FreeX     : free the whole data structure X.
 *     DispX     : dispose only the structure node, and not its contents.
 *     CopyX     : copy a structure X.
 *     GetX      : make a copy of a structure X and free the old structure.
 *     ShareX    : increment the copy field of a structure if it is shareable
 *                 and the copy fields of all its shareable values.
 *     UnshareX  : decrement the copy field of a structure if it is shareable
 *                 and the copy fields of all its shareable values.
 *     MakeX     : create an structure X and initialize it.
 *     PrintX    : print X in a suitable LOTOS format.
 *     SPrintX   : return a string containing attr value X printed in.
 *     DrawX     : draw a structure X in a non LOTOS format.
 *     Is_P_X    : evaluate a predicate P on an structure X.
 *     EqualX    : equality of X structures.
 *     JunctionX : clever union of structures.
 *     Get_V_X   : take out a value from a structure and leave the place of
 *                 the structure which contained it to NULL.
 *     Put_V_X   : put a value into an structure. ( it should be NULL ).
 *     Look_V_X  : look at a value V of an structure X. 
 *     StatX     : statistics on the global usage of this structure nodes.
 *     StatisticX: report node usage of an structure of type X.
 *
 *  And when the structure is a list of structures :
 *
 *     CreateX   : create an empty list.
 *     JoinX     : concatenation of lists of structures.
 *     InsertX   : insertion at the head of a list of structures.
 *     AddX      : insertion at the tail of a list of structures.
 *
 *  COMPILATION FLAGS:
 *      
 *  TYPE DEFINITIONS:
 *     GateListTyp      : Gate List (DescriptorTyp list).
 *     GateSetTyp       : Gate Set.
 *     GateMaskTyp      : Gate mask i.e. Gate set of a single gate.
 *     PredicateTyp,
 *     PredNodeTyp      : Premises in selection predicates and guards.
 *     ExprListTyp      : List of expressions (ExprTyp).
 *     OfferTyp,
 *     POfferTyp        : Offer in a gate or exit statement.
 *     OfferListTyp     : Offer list.
 *     RelabFuncTyp,
 *     PRelabFuncTyp    : A single gate Relabel Function.
 *     RelabFuncListTyp : Relabel Function list.
 *     VarAssignTyp,
 *     PVarAssignTyp    : A single Variable Assignment.
 *     VarAssignListTyp : Variable Assignment list         
 *     GateDecTyp,
 *     PGateDecTyp      : A single Gate Declaration
 *     GateDecListTyp   : Gate Declaration list
 *     LabelTyp         : Iexpansion's Labels
 *     ITContTyp,
 *     PITContTyp       : Iexpansion's IT single Continuation
 *     ITContListTyp    : Iexpansion's IT Continuation list   
 *     SyncTreeTyp      : Debugger synchronization trees
 *  
 *  FUNCTION DEFINITIONS:
 *
 *     -----------  LOTOS ATTRIBUTES  FUNCTIONS ----------- 
 *
 *     FreeGL                       : free a gate list
 *     CopyGL                       : copy a gate list
 *     DrawGL                       : draw a gate list
 *     AddGL                        : add a gate to a gate list
 *     InsertGL                     : insert a gate into a list
 *     InGL                         : gate in a gate list
 *     JoinGL                       : concatenation of gate lists
 *     JunctionGL                   : union of gate lists as sets
 *     GateList_to_GateSet          : transform a gate list into a gate set
 *     GateSet_to_GateList          : transform a gate set into a gate list
 *     PrintGL                      : print a gate list
 *     SPrintGL                     : sprint a gate list
 *     EqualGL                      : say whether two gate list are equal
 *     InitGS                       : init the gate set module
 *     NewGS                        : create an empty gate set
 *     FreeGS                       : free a gate set
 *     CopyGS                       : copy a gate se
 *     GateInGS                     : say if a gate belongs to a gate set
 *     JunctionGS                   : union of gate sets
 *     IntersGS                     : intersection of two gate sets
 *     DiffGS                       : difference of gate sets
 *     EqualGS                      : say whether two gate sets are equal
 *     IsEmptyGS                    : say whether a gate set is empty
 *     IsFullGS                     : say whether a gate set is full
 *     SubSetGS                       : say whether a gate set is included
 *                                    in another
 *     ClearGS                      : clear up a gate set  
 *     FullGS                       : return a gate set filled up to a given
 *                                    gate descriptor
 *     AddGS                        : add a gate to a gate set 
 *     RemoveGS                     : remove a gate from a gate set
 *     DrawGS                       : draw a gate set
 *     PrintGS                      : print a gate set
 *     SPrintGS                     : sprint a gate set
 *     StatGS                       : statistics on gate sets
 *     Descr_to_Mask                : return the gate mask of a descriptor
 *     Mask_to_Descr                : return the descriptor of a gate mask
 *     InitPred                     : init the module of predicates
 *     StatPred                     : statistics on predicates
 *     NewPred                      : create a predicate
 *     AddPremisePred               : add another premise to a predicate
 *     PrintPred                    : print a predicate
 *     SPrintPred                   : sprint a predicate
 *     LookRwPred                   : look at the rewritten value of the
 *                                    current node of a predicate
 *     LookOrPred                   : look at the original value of the
 *                                    current node of a predicate   
 *     FreePred                     : free a predicate
 *     CopyPred                     : copy a predicate
 *     UnsharePred                  : unshare a predicate
 *     SharePred                    : share a predicate
 *     VarsInPred                   : variables used in a predicate
 *     MakeAndPred                  : make a predicate as AND of two predicates
 *     RemoveEqualExprPred          : remove from a predicate the duplicated
 *                                    premises
*     StatisticEL                  : statistics of an expression list
 *     CreateEL                     : create an expression list
 *     PrintEL                      : print an expression list
 *     SPrintEL                     : sprint an expression list
 *     PrintVL                      : print a variable list
 *     SPrintVL                     : sprint a variable list
 *     FreeEL                       : free an expression list
 *     CopyEL                       : copy an expression list
 *     UnshareEL                    : unshare an expression list
 *     DrawEL                       : draw an expression list
 *     InEL                         : say whether an expression e is in an
 *                                    expression list el
 *     InsertEL                     : insert an expression in an expression
 *                                    list
 *     IntersEL                     : intersection of two expression lists
 *     JoinEL                       : join expression lists
 *     AddEL                        : add an expression to an expression list
 *     VarsOfEL                     : variable names used in an expression list
 *     LookVarsInExpr               : list of pointers to the variables in
 *                                    an expression
 *     EqualEL                      : say whether two expression lists are
 *                                    equal
 *     InitOffer                    : init the module of offers
 *     StatOffer                    : statistics on offer nodes
 *     StatisticOL                  : statistics of an offer list
 *     NewOffer                     : get memory for a new offer.
 *     DispOffer                    : frees memory used by an offer cell.
 *     FreeOffer                    : free an offer
 *     CopyOffer                    : copy an offer
 *     LookExprOffer                : look at the expression of an offer
 *     GetExprOffer                 : get the expression of an offer
 *     PutExprOffer                 : put the expression into an offer
 *     LookKindOffer                : return the kind of offer 
 *     PutKindOffer                 : put the kind of offer
 *     MakeOffer                    : make an offer
 *     CreateOL                     : create an offer list
 *     FreeOL                       : free an offer list 
 *     LengthOL                     : offer list length
 *     CopyOL                       : copy an offer list
 *     UnshareOL                    : unshare an offer list
 *     JoinOL                       : join two offer lists
 *     PrintOL                      : print an offer list
 *     SPrintOL                     : sprint an offer list
 *     PrintExitOL                  : print an offer list of an exit
 *     SPrintExitOL                 : sprint an offer list of an exit
 *     MvNextOffer                  : move to the next offer
 *     AddOL                        : add an offer to an offer list.
 *     InsertOL                     : insert an offer into an offer list.
 *     IsThereQuestionOL            : say whether there is a ?v:s offer in an
 *                                    offer list
 *     IsThereExclamationOL         : say whether there is a !e offer in an
 *                                    offer list
 *     VarsDefinedInOL              : list of variables defined in an offer
 *                                    list
 *     LookForVarOL                 : look for the offer where a variable is
 *                                    being defined
 *     Convert_to_AdmirationOL      : transform all ? v:s offers into !e offers
 *     InitRF                       : init the relabel function module
 *     StatRF                       : statistics on relabel functions
 *     NewRF                        : create a new RF
 *     FreeRF                       : free a RF
 *     CopyRF                       : copy a RF
 *     MakeRF                       : make a RF
 *     CreateRFL                    : create a relabel function list
 *     FreeRFL                      : free a relabel function list
 *     LengthRFL                    : length of a relabel function list
 *     CopyRFL                      : copy a relabel function list
 *     JoinRFL                      : join two relabel function lists
 *     JunctionRFL                  : collapse two relabel function lists
 *     PrintRFL                     : print a relabel function list
 *     SPrintRFL                    : sprint a relabel function list
 *     AddRF                        : add a relabel function to a RFL
 *     AddRFL                       : add-check a relabel function to a RFL
 *     ActualRFL                    : actual gate of a formal gate, after RFL
 *     FormalRFL                    : n-th formal gate of an actual gate,
 *                                    before RFL
 *     LookForGateRF                : formal gate in the current RF 
 *     LookActGateRF                  : actual gate in the current RF 
 *     RangeRFL                     : formal gate set of a RFL 
 *     ImageRFL                     : actual gate set of a RFL 
 *     InvRFL                       : inverse gate relabel function list
 *     ApplyRFL                     : apply an RFL to a gate set
 *     ApplyGL_RFL                  : apply an RFL to a gate list
 *     InvApplyRFL                  : apply the inverse of RFL to a gate set
 *     Mk_GLs_RFL                   : make an RFL from two gate lists
 *     EqualRFL                     : say whether two RFLs are equal
 *     DeleteNodeRFL                : delete the current RF node
 *     RFL_to_GDL                   : equivalent gate declaration list of
 *                                    an RFL
 *     SimplifyRFL                  : simplify an RFL
 *     InitVA                       : init the var assign module
 *     StatVA                       : statistics on VA nodes
 *     StatisticVAL                 : statistics of a var assign list
 *     MakeVA                       : make a variable assignment
 *     FreeVA                       : free a VA
 *     CopyVA                       : copy a VA
 *     DrawVA                       : draw a VA
 *     CreateVAL                    : create a variable assign list (VAL)
 *     FreeVAL                      : free a VAL
 *     CopyVAL                      : copy a VAL
 *     UnshareVAL                   : unshare a VAL
 *     PrintVAL                     : print a VAL
 *     SPrintVAL                    : sprint a VAL
 *     DrawVAL                      : draw a var assign list
 *     JoinVAL                      : apply a VAL to another
 *     InsertVAL                    : insert a VA into a VAL
 *     AddVAL                       : add a VA to a VAL
 *     ActExprVAL                   : actual expression of a variable
 *     Mk_VLEL_VAL                  : make a var assign list from an
 *                                    expression list and a variable list.
 *     LookVarVAL                   : look at the formal var in the current
 *                                    VA node 
 *     GetVarVAL                    : get the formal var from the current
 *                                    VA node 
 *     PutVarVAL                    : put the formal var in the current
 *                                    VA node 
 *     LookExprVAL                  : look at the actual expression in the
 *                                    current VA node 
 *     GetExprVAL                   : get the actual expression from the
 *                                    current  VA node
 *     PutExprVAL                   : put the the actual expression in the
 *                                    current VA node 
 *     FormalVL_VAL                 : formal variable list of a VAL
 *     ActualEL_VAL                 : actual expression list of a VAL
 *     IsNotPrintableVAL            : actual expression list of a VAL
 *     IsVoidVAL                    : say if all are void assigments
 *     EqualVA                      : say whether 2 VA are equal
 *     SubSet_VAL                   : say whether a VAL is contained in another
 *     InitGD                       : init GD usage
 *     StatGD                       : statistics on GD nodes usage
 *     StatisticGDL                 : statistics of a GDL
 *     MakeGD                       : make a GD with a gate list and a gate set
 *     FreeGD                       : free a GD
 *     CopyGD                       : copy a GD
 *     SPrintGD                     : sprint a GD
 *     EqualGD                      : say if 2 GD are equal
 *     CreateGDL                    : create an empty GDL
 *     FreeGDL                      : free a GDL
 *     CopyGDL                      : copy a GDL
 *     PrintGDL                     : print a GDL
 *     SPrintGDL                    : sprint a GDL
 *     AddGDL                       : add a GD to a GDL
 *     InsertGDL                    : insert a GD into a GDL
 *     EqualGDL                     : say whether two GDL are equal
 *
 *     ----------- ITCALCULUS ATTRIBUTES FUNCTIONS -----------
 *
 *     InitTerm                     : intialize global termination counter
 *     NewTerm                      : get a brandnew termination
 *     CurrentTerm                  : look at the current term count value
 *     DisposeTerm                  : release a termination number
 *     SetTerm                      : set temporarily the termination counter
 *                                    to a given value
 *     ResetTerm                    : reset the termination counter to
 *                                    its previous value
 *     FreeLabel                    : free a label
 *     EqualLabel                   : say whether two labels are equal
 *     InsertLabel                  : append a termination to a label
 *     CopyLabel                    : copy a label
 *     JoinLabel                    : merge two labels
 *     HashKeyLabel                 : label hash function
 *     PrintLabel                   : print a label
 *     LookForLabel                 : look for a termination in a label
 *     SubLabel                     : say if a label is sublabel of another
 *     SubLabelList                 : say if a label is sublabel of the label
 *                                    made by a list of integers
 *     Free_LL                      : free a list of labels (LL)
 *     Copy_LL                      : copy a LL
 *     Print_LL                     : print a LL
 *     HashF_LL                     : LL hash funtion
 *     Equal_LL                     : say whether two LL are equal
 *     SubSet_LL                    : say whether a LL is subset of another.
 *     Insert_LL                    : insert a label into a label list
 *     InitITC                      : init ITC usage
 *     NewITC                       : create an ITC node
 *     DispITC                      : dispose an ITC node
 *     FreeITC                      : free an ITC and its contents
 *     StatITC                      : statistics on ITC nodes usage
 *     CopyITC                      : copy an ITC
 *     CopyShareITC                 : copy an ITC sharing all its shareable
 *                                    contents.
 *     LookLabelITC                 : look at the label of an ITC
 *     LookBehITC                   : look at the behaviour of an ITC
 *     PrintITC                     : print an ITC
 *     FreeITCL                     : free an ITCL
 *     CopyITCL                     : copy an ITCL
 *     InsertITCL                   : insert an ITC into an ITCL 
 *     PrintITCL                    : print an ITCL
 *     StatisticITC                   : statistics of an ITC node
 *     LookForITCL                  : look for an ITC by label
 *     LookForNodeITCL              : look for an ITC by label and return the
 *                                    list node
 *     LookFor_SubSet_ITCL          : look for a continuation by label, subset
 *                                    another label 
 *     LookFor_IncluderITCL         : look for a continuation with the same
 *                                    label and cset label included
 *                                    in the cset_labels of an itcl.
 *     LookFor_IdenticalITCL        : look for a continuation with the same
 *                                    label and cset labels in an itcl.
 *     LookFor_Update_IdenticalITCL : look for an identical continuation and
 *                                    update its cset's label 
 *     LookFor_Update_IncluderITCL  : look for an includer continuation and
 *                                    update its cset's label 
 *     CSets_Labels_in_Beh          : list of labels of all the continuations
 *                                    sets of a behaviour 
 *
 *     ----------- DEBUGGER ATTRIBUTES FUNCTIONS -----------
 *
 *     VPrintST                     : verbose print a synchronization tree (ST)
 *     PrintST                      : print a synchronization tree (ST)
 *     FreeST                       : free a ST
 *     CopyST                       : copy a ST
 *     IsEventLeafST                : say whether an event is a leaf of the ST
 *     FreeSSL                      : free a specification source line (SSL)
 *     PrintSSL                     : print a SSL
 *     SPrintSSL                    : sprint a SSL
 *
 *  LOG:
 *     25/06/92. santiago.
 *     Introduced a function to calculate the intersection of two
 *     expression lists.
 *
 *     25/06/92. santiago.
 *     Introduced a function to get a list with the variables defined in an
 *     offer list.
 *
 *     25/06/92. santiago.
 *     New function to decompose a multiple predicate into single predicates.
 *
 *     06/07/92. dlarra.
 *     New function to determine whether two varassign are equal or not.
 *     
 *     06/07/92. dlarra.
 *     New function to determine if a varassign list is a subset of another.
 *
 *     20/07/92. dlarra.
 *     New function to locate a variable definition in an offer list.
 *
 *     27/01/94. dlarra.
 *     Review all remarks and function names to prepare a library.
 *
 ********************************************************************/


#ifndef baattr_H
#define baattr_H

#ifdef TIME 
#include "batime.h" 
#else
#include "listdh.h"
#include "lilists.h"
#include "lihash.h"
#include "babeh.h"
#include "baexpr.h"
#endif

/******************************************************************
 *                                                                *
 *                 ATTRIBUTE TYPE DEFINITIONS                     *
 *                                                                *
 ******************************************************************/


/******************************************************************
 *                                                                *
 *            GLA   -> Gate List Attribute (GateListTyp)          *
 *                                                                *
 ******************************************************************/


/* GateListTyp
 * Gate DescriptorTyp list.
 */
typedef ListTyp  GateListTyp;


/******************************************************************
 *                                                                *
 *            GSA   -> Gate Set Attribute                         *
 *                                                                *
 ******************************************************************/

/*
 *  Maximum size of the gate sets.
 */

#define MAX_GATES MAX_GATE_TABLE

#define GATESET_WORDS ((MAX_GATES/(WORDLENGTH+1))+1)


/* GateSetTyp
 * Set of GateMaskTyp
 */
typedef unsigned * GateSetTyp;


/* GateMaskTyp
 * Mask of a gate. It is a set of one element.
 */
typedef  GateSetTyp GateMaskTyp;


/******************************************************************
 *                                                                *
 *            PA    -> Predicate Attribute (PredicateTyp)         *
 *                                                                *
 ******************************************************************/

/* PredicateTyp
 * Premises in selection predicates and guards.
 * It is a list of structs with two Meta-Bool expressions. One of them is the
 * predicate in its canonical form and the other one in its original form.
 */
typedef ListTyp PredicateTyp;

typedef struct predicate { ExprTyp rewritten;
                           ExprTyp original; 
                         } *PredNodeTyp; 

/******************************************************************
 *                                                                *
 *            ELA   -> Expr List Attribute (ExprListTyp)          *
 *                                                                *
 ******************************************************************/

/* ExprListTyp
 * List of expressions (ExprTyp).
 */
typedef ListTyp ExprListTyp;


/******************************************************************
 *                                                                *
 *          OLA  -> Offer List Attribute (OfferListTyp)           *
 *                                                                *
 ******************************************************************/

/*
 * Offer class: ? or !.
 */
#define QUESTION    1
#define EXCLAMATION 2

/*
 *  A single offer
 */
typedef struct OfferNode{ struct OfferNode * next;
                          int                class;
                          ExprTyp            value;
                        } OfferTyp, *POfferTyp;

/* OfferListTy
 * List of OfferTyp.
 */
typedef POfferTyp OfferListTyp;


/******************************************************************
 *                                                                *
 *       RFLA  -> Relab Func List Attribute (RelabFuncListTyp)    *
 *                                                                *
 *       RelabFunctions composing a RelabFunctionList             *
 *       are supposed to have different Formal Gates.             *
 *       ( The opposite would be meanningless ).                  *
 *       ( Besides, this enables Formal Gate to be the            *
 *         search key to locate RelabFunctions in a list ).       *
 *                                                                *
 ******************************************************************/

/*
 * A single gate relabel function.
 */
typedef struct relabfuncnode { struct relabfuncnode * next;
                               DescriptorTyp          gateAct;
                               DescriptorTyp          gateFor;
                             } RelabFuncTyp,*PRelabFuncTyp;

/* RelabFuncListTyp
 * List of Gate relabel function.
 */
typedef PRelabFuncTyp RelabFuncListTyp;


/******************************************************************
 *                                                                *
 *     VALA  -> Var Assign List Attribute (VarAssignListTyp)      *
 *                                                                *
 *     VarAssigns composing a VarAssignList are supposed to refer *
 *     to different variables.                                    *
 *     ( The opposite would be meaningless ).                     *
 *     ( Besides, this enables the Formal Var to be the           *
 *       search key to locate VarAssigns in a list ).             *
 *     But this is NOT detected : the responsability to           *
 *      deal with duplicates is left to the user.                 *
 *                                                                *
 ******************************************************************/

/*
 * A single Variable assignment.
 */
typedef struct { DescriptorTyp varFor;
                 ExprTyp       expAct;
               } VarAssignTyp, *PVarAssignTyp;

/* VarAssignListTyp
 * list of Variable assign.
 * The list elements are of type VarAssignTyp.
 */
typedef ListTyp VarAssignListTyp;


/******************************************************************
 *                                                                *
 *     GDLA -> Gate Declaration List Attribute (GateDecListTyp)   *
 *                                                                *
 ******************************************************************/

/* 
 * A single gate declaration.
 */
typedef struct { GateListTyp agl;
                 GateSetTyp  fgs; 
               } GateDecTyp,*PGateDecTyp;

/* GateDecListTyp
 * List of GateDecTyp.
 */
typedef ListTyp GateDecListTyp;


/******************************************************************
 *                                                                *
 *        ITCLA -> Interleaved Continuation list Attribute        *
 *                 (ITContListTyp)                                *
 *                                                                *
 ******************************************************************/

/* LabelTyp
 * sorted string (set) of terminations < n1, .., nm >
 */
typedef BehTyp LabelTyp;


/* ITContTyp
 * A single Continuation ( labelled sub-behaviour ) .
 */
typedef struct {
  
  LabelTyp label;     /* list(set) of integers(terminations) < n1, .., nm >. */
  BehTyp   b;         /* attached sub-behaviour.                             */
  int      n_label;   /* n(label) : term count to start exploring with.      */
  
  /* auxiliary */
  
  HashDTyp cset_labels_ht; /* table of list of labels of the continuation sets
                              of all the continuations with the same label */
  ListTyp  cset_labels;   /* list of labels of the continuation sets*/
  boolean  isDeadlock;    /* this cont has a descendant which does not lead
                             to success   */
  ListTyp  deadlocks;     /* list of labels identifying deadlocks */
  BehTyp   int_b, sync_b; /* auxiliary fields for CMatrix */
  LabelTyp path;          /* list of terminations escaped through to reach
                             this continuation from the root */
} ITContTyp, *PITContTyp;


/* ITContListTyp
 * List of ITContTyp ( set of continuations )
 */
typedef ListTyp ITContListTyp;


/******************************************************************
 *                                                                *
 *              FUNCTIONS TO MANAGE THE ATTRIBUTES                *
 *                                                                *
 ******************************************************************/


/******************************************************************
 *                                                                *
 *            GLA   -> Gate List Attribute (GateListTyp)          *
 *                                                                *
 ******************************************************************/


/* FreeGL
 * Free the memory used by the gate list gl.
 */
extern void FreeGL( /* gl */ );
/*  GateListTyp  gl; */


/* CopyGL
 * Copy the gate list gl.
 */
extern GateListTyp CopyGL( /* gl */ );
/* GateListTyp gl; */


/* DrawGL
 * Draw the gate list gl
 * pstr is the function used to print strings.
 */
extern void DrawGL( /* gl, pstr */ );
/*  ListTyp    gl;
    void (*pstr)(); */


/* AddGL
 * Add a gate to a gate list
 */
extern GateListTyp AddGL( /* g, gl */ );
/*    DescriptorTyp g;
      ListTyp     gl; */


/* InsertGL
 * Insert a gate in a gate list
 */
extern GateListTyp InsertGL( /*g,gl */ );
/*    DescriptorTyp g;
      ListTyp     gl; */


/* InGL
 * return TRUE if g is in gl
 */
extern boolean InGL( /*gl,g */ );
/* GateListTyp gl;
   DescriptorTyp g */


/* JoinGL
 * return the concatenation gl1,gl2
 */
extern GateListTyp JoinGL( /*gl1, gl2*/ );
/* GateListTyp gl1,gl2; */


/* JunctionGL
 * return the union of two gates lists as sets ( removing equal elements )
 */
extern GateListTyp JunctionGL( /*gl1,gl2*/ );
/* GateListTyp gl1,gl2;   */


/* GateList_to_GateSet
 * Transform a gate list into a gate set
 */
extern GateSetTyp GateList_to_GateSet( /*gl */ );
/* GateListTyp gl   */


/* GateSet_to_GateList
 * Transform a gate set into a gate list
 */
extern GateListTyp GateSet_to_GateList( /*gs */ );
/*    GateSetTyp  gs */


/* PrintGL
 * Print the gate list gl.
 * pstr is the function used to print strings.
 */
extern void PrintGL( /* gl, pstr */ );
/* GateListTyp gl;
   void (*pstr)(); */


/* SPrintGL
 * Make a string with the name of a list of gates
 */
extern char * SPrintGL( /* gl */ );
/*    GateListTyp gl; */


/* EqualGL
 * Say if two GLs are equal ( in the same order )
 */
extern boolean EqualGL( /* gl1, gl2 */ );
/* GateListTyp gl1,gl2; */


/******************************************************************
 *                                                                *
 *            GSA   -> Gate Set Attribute                         *
 *                                                                *
 ******************************************************************/

/* InitGS
 * Init the GS module
 */
extern void InitGS();


/* NewGS
 * Create an empty gate set
 */
extern GateSetTyp NewGS();


/* FreeGS
 * Free a gate set
 */
extern void FreeGS( /* gs */ );
/*  GateSetTyp  gs; */


/* CopyGS
 * Copy a gate set
 */
extern GateSetTyp CopyGS( /* gs */ );
/* GateSetTyp gs; */


/* GateInGS
 * Say if a gate belongs to a gate set
 */
extern boolean GateInGS( /* g, gs */ );
/*  DescriptorTyp  g;
    GateSetTyp     gs; */


/* JunctionGS
 * Union of two gate sets.
 */
extern GateSetTyp JunctionGS( /* gs1,gs2 */ );
/* GateSetTyp gs1,gs2; */


/* IntersGS
 * Intersection of two gate sets
 */
extern GateSetTyp IntersGS( /* gs1, gs2 */ );
/* GateSetTyp gs1,gs2 */


/* DiffGS
 * Difference of gate sets
 */
extern GateSetTyp DiffGS( /* gs1,gs2 */ );
/* GateSetTyp gs1,gs2; */


/* EqualGS
 * return TRUE if the gate sets are equal
 */
extern boolean EqualGS( /* gs1, gs2 */ );
/* GateSetTyp gs1,gs2;  */


/* IsEmptyGS
 * return TRUE if gs is an empty gate set, else FALSE
 */
extern boolean IsEmptyGS( /* gs */ );
/* GateSetTyp  gs; */


/* IsFullGS
 * Say whether the Gate Set is full ( contains all gates up to max).
 * max is the last element of any set.
 */
extern boolean IsFullGS( /* gs, max */ );
/*     GateSetTyp gs;
       unsigned   max; */


/* SubSetGS
 * return TRUE if a gate set is included in another
 */
extern boolean SubSetGS( /* gs1, gs2 */ );
/* GateSetTyp gs1,gs2;  */


/* ClearGS
 * Clear up a gate set
 */
extern GateSetTyp ClearGS( /* gs */ );
/* GateSetTyp gs; */


/* FullGS
 * return a gate set filled up to a given descriptor g.
 * example: gs = FullGS( LastTableG() );
 *          would return a gate set containing all the gates in the table. 
 */
extern GateSetTyp FullGS( /* g */ );
/*     DescriptorTyp g; */


/* AddGS
 * Add a gate to a gate set 
 */
extern GateSetTyp AddGS( /* gs,g */ );
/* GateSetTyp    gs;
   DescriptorTyp g;    */


/* RemoveGS
 * Remove a gate from a gate set
 */
extern GateSetTyp RemoveGS( /* gs, g */ );
/* GateSetTyp    gs;
   DescriptorTyp g;    */


/* DrawGS
 * Draw the Gate Set gs.
 * pstr is the function used to print strings.
 */
extern void DrawGS( /* gs, pstr */ );
/* GateSetTyp gs;
   void       (*pstr)(); */


/* PrintGS
 * Print the gate set gs.
 * pstr is the function used to print strings.
 */
extern void PrintGS( /* gs, pstr */ );
/*  GateSetTyp   gs;
    void       (*pstr)(); */


/* SPrintGS
 * Make a string with the names of gates given for a mask
 */
extern char * SPrintGS( /* gs */ );
/* GateSetTyp gs; */


/* StatGS
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatGS(/* new, released, max */);
/*  int *new, *released, *max; */


/* Descr_to_Mask
 * Return the gate mask for the descriptor d.
 */
extern GateMaskTyp Descr_to_Mask( /* d */ );
/*  DescriptorTyp  d;  */


/* Mask_to_Descr
 * Return the gate descriptor for the gate mask m.
 */
extern DescriptorTyp Mask_to_Descr( /* m */ );
/*  GateMaskTyp  m;  */


/******************************************************************
 *                                                                *
 *            PA    -> Predicate Attribute (PredicateTyp)         *
 *                                                                *
 ******************************************************************/


/* InitPred
 * Init the module
 */
extern void InitPred();


/* StatPred
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatPred( /* new, released, max */ );
/* int * new, *released, *max; */


/* NewPred
 * Create a predicate.
 */
extern PredicateTyp NewPred( /* er,eo */ );
/* ExprTyp er,eo; */


/* AddPremisePred
 * Add another premise to the predicate p.
 */
extern PredicateTyp AddPremisePred( /* p, er, eo */ );
/* PredicateTyp  p;
   ExprTyp       er,eo; */


/* PrintPred
 * Prints the predicate p
 * pstr is the function used to print strings.
 */
extern void PrintPred( /* p, pstr */ );
/* PredicateTyp  p;
   void         (*pstr)(); */


/* SPrintPred
 * return a char string block with the predicate p.
 */
extern char * SPrintPred( /* p */ );
/* PredicateTyp   p; */


/* LookRwPred
 * Look at the rewritten value of the first node of p
 */
extern ExprTyp LookRwPred( /* p */ );
/* PredicateTyp p; */


/* LookOrPred
 * Look the original value of the first node of p.
 */
extern ExprTyp LookOrPred( /* p */ );
/* PredicateTyp p; */


/* FreePred
 * Free a predicate p
 */
extern void FreePred( /* p */ );
/* PredicateTyp p; */


/* CopyPred
 * Copy a predicate p
 */
extern PredicateTyp CopyPred( /* p */ );
/* PredicateTyp p; */


/* UnsharePred
 * Unshare a predicate p.
 */
extern PredicateTyp UnsharePred( /* p */ );
/* PredicateTyp p; */


/* SharePred
 * Share a predicate p.
 */
extern PredicateTyp SharePred( /* p */ );
/* PredicateTyp p; */


/* VarsInPred
 * Return a list with the variables used in the predicate p.
 */
extern ExprListTyp VarsInPred( /* p */ );
/* PredicateTyp p; */


/* MakeAndPred
 * Create a new predicate that is equal to "p1 and p2".
 */
extern PredicateTyp MakeAndPred( /* p1, p2 */ );
/* PredicateTyp p1,p2; */


/* RemoveEqualExprPred
 * Remove from the predicate p the duplicated premises.
 */
extern PredicateTyp RemoveEqualExprPred( /* p */ );
/* PredicateTyp p; */


/******************************************************************
 *                                                                *
 *            ELA   -> Expr List Attribute (ExprListTyp)          *
 *                                                                *
 ******************************************************************/


/* StatisticEL
 * Statistics of the expression list el.
 * Returns the number of variable and operation cells, and list nodes used.
 * nv,vv and ov are virtual values of number of list nodes, variable and
 * operation cell, i.e. without paying attention to the sharing feature.
 * nr,vr and or are the real values, i.e. nodes and cells already counted in
 * other expressions are not counted again here.
 * nl is the number of list nodes used to build the expression list.
 */
extern void StatisticEL( /* el, nv, vv, ov, nr, vr, or, nl */ );
/* ExprListTyp  el;
   int         *nv, *vv, *ov, *nr, *vr, *or, *nl; */


/* CreateEL
 * Create an expression list or a variable list . ( return an empty one )
 */
extern ExprListTyp CreateEL();


/* PrintEL
 * Prints the expression list el.
 * pstr is the function used to print strings.
 */
extern void PrintEL( /* el, pstr */ );
/* ExprListTyp  el;
   void         (*pstr)(); */


/* SPrintEL
 * return a char string block with an expression list el.
 */
extern char * SPrintEL( /* el */ );
/* ExprListTyp   el; */


/* PrintVL
 * Print the variable list vl.
 * pstr is the function used to print strings.
 */
extern void PrintVL( /* vl, pstr */ );
/* ExprListTyp   vl;
   void         (*pstr)(); */


/* SPrintVL
 * return a char string block with a variable list vl.
 */
extern char * SPrintVL( /* vl */ );
/*     ExprListTyp   vl; */


/* FreeEL
 * Free an expression list el.
 */
extern void FreeEL( /* el */ );
/* ExprListTyp el; */


/* CopyEL
 * Copy the expression list el.
 */
extern ExprListTyp CopyEL( /* el */ );
/* ExprListTyp el; */


/* UnshareEL
 * Unshare the expression list el.
 */
extern ExprListTyp UnshareEL( /* el */ );
/* ExprListTyp el; */


/* DrawEL
 * Draw an expression list el.
 * pstr is the function used to print strings.
 */
extern void DrawEL( /* el, pstr */ );
/* ExprListTyp  el;
   void         (*pstr)(); */


/* InEL
 * If an expression e is in expression list el then return TRUE else FALSE.
 */
extern boolean InEL( /* e, el */ );
/* ExprTyp   e;
   ExprListTyp   el;*/


/* InsertEL
 * Insert expression e in an expression list. (At the header).
 */
extern ExprListTyp InsertEL( /* e , el */ );
/* ExprTyp   e;
   ExprListTyp   el;*/


/* IntersEL
 * Return the intersection of two expression lists,
 * i.e. a list with the expressions both in el1 and in el2.
 * The lists el1 and el2 are disposed.
 */
extern ExprListTyp IntersEL( /* el1,el2 */ );
/* ExprListTyp el1,el2; */


/* JoinEL
 * Return the concatenation el1,el2
 */ 
extern ExprListTyp JoinEL( /* el1, el2 */ );
/*  ExprListTyp   el1,el2;*/


/* AddEL
 * Append expression e to the tail of expression list el.
 */
extern ExprListTyp AddEL( /* e, el */ );
/* ExprTyp   e;
   ExprListTyp   el;*/


/* VarsOfEL
 * Return a list of variable names used in an expression list el
 */
extern ListTyp VarsOfEL( /* el */ );
/* ExprListTyp el; */


/* LookVarsInExpr
 * Return a list of pointers to the variables in the expression e.
 */
extern ListTyp LookVarsInExpr( /* e */ );
/*     ExprTyp e; */


/* EqualEL
 * return el1 equal to el2
 */
extern boolean EqualEL( /* el1, el2 */ );
/*   ExprListTyp el1,el2; */


/******************************************************************
 *                                                                *
 *            OLA  -> Offer List Attribute (OfferLIstTyp)         *
 *                                                                *
 ******************************************************************/

/* InitOffer
 * Init the module of offers
 */
extern void InitOffer();


/* StatOffer
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatOffer( /* new, released, max */ );
/*   int * new, *released, *max; */


/* StatisticOL
 * Statistic of an offer list ol.
 * Returns the number of Offer-nodes (no) used in the offer list ol, and
 * the number of variable and operator cells and list nodes used.
 * nv,vv and ov are virtual values of number of list nodes, variable and
 * operation cell, i.e. without paying attention to the sharing feature.
 * nr,vr and or are the real values, i.e. nodes and cells already counted
 * in other expressions are not counted again here.
 */
extern void StatisticOL( /* ol, nv, vv, ov, nr, vr, or, no */ );
/* OfferListTyp ol;
   int          *nv, *vv, *ov, *nr, *vr, *or, *no; */


/* NewOffer
 * Get memory for a new offer.
 */
extern POfferTyp NewOffer();


/* DispOffer
 * Free the memory used by an offer cell.
 */
extern void DispOffer( /* c */ );
/*  POfferTyp    c;  */


/* FreeOffer
 * Free an offer.
 */
extern void FreeOffer( /* o */ );
/*  POfferTyp  o;  */


/* CopyOffer
 * Copy an offer o.
 */
extern POfferTyp CopyOffer( /* o */ );
/*  POfferTyp  o;  */


/* LookExprOffer
 * Look at the variable or the expression of an offer.
 * It must not be modified, it is only to examine.
 * o is either an offer list or an offer.
 */
extern ExprTyp LookExprOffer( /* o */ );
/* OfferListTyp  o; */


/* GetExprOffer
 * Get the variable or the expression of an offer.
 * It may be modified. After this, it must be restored into the offer
 * using the function PutExprOffer.
 * o is either an offer list or an offer.
 */
extern ExprTyp GetExprOffer( /* o */ );
/* OfferListTyp  o; */


/* PutExprOffer
 * Restore either a variable or an expression into an offer.
 * See the function GetExprOffer.
 * o is either an offer list or an offer.
 * ve points to either a variable or an expression.
 */
extern void PutExprOffer( /* o,ve */ );
/*  OfferListTyp  o; 
    ExprTyp  ve;  */


/* LookKindOffer
 * Return QUESTION or EXCLAMATION depending on the offer kind.
 * o is either an offer list or an offer.
 */
extern int LookKindOffer( /* o */ );
/* OfferListTyp  o; */


/* PutKindOffer
 * Puts the kind QUESTION or EXCLAMATION to the offer o.
 * o is either an offer list or an offer.
 * k is QUESTION or EXCLAMATION.
 */
extern void PutKindOffer( /* o, k */ );
/* OfferListTyp  o; 
   int           k;  */



/* MakeOffer
 * Makes an offer with k and ve.
 * k is QUESTION or EXCLAMATION.
 * ve is a variable or an expression.
 */
extern POfferTyp MakeOffer( /* k,ve */ );
/*  int      k; 
    ExprTyp  ve;  */


/* CreateOL
 * Create an empty offer list.
 */
#define CreateOL()  NULL


/* FreeOL
 * Free the memory used by the offer list ol.
 */
extern void FreeOL( /* ol */ );
/* OfferListTyp  ol; */


/* LengthOL
 * Return the length of an offer list ol.
 */
extern int LengthOL( /* ol */ );
/* OfferListTyp  ol; */


/* CopyOL
 * Copy an offer list ol.
 */
extern OfferListTyp CopyOL( /* ol */ );
/* OfferListTyp ol; */


/* UnshareOL
 * Unshare an offer list ol.
 */
extern OfferListTyp UnshareOL( /* ol */ );
/* OfferListTyp ol; */


/* JoinOL
 * Join the offer list ol1 and ol2. Return ol1,ol2.
 */
extern OfferListTyp JoinOL( /* ol1, ol2 */ );
/* OfferListTyp ol1,ol2; */


/* PrintOL
 * Print an offer list ol.
 * pstr is the function used to print strings.
 */
extern void PrintOL( /* ol, pstr */ );
/* OfferListTyp   ol;
   void (*pstr)(); */


/* SPrintOL
 * Make a string with the offer list ol.
 */
extern char * SPrintOL( /* ol */ );
/*   OfferListTyp   ol; */


/* PrintExitOL
 * Print the offer list ol using exit format.
 * pstr is the function used to print strings.
 */
extern void PrintExitOL( /* ol, pstr */ );
/* OfferListTyp   ol;
   void (*pstr)(); */


/* SPrintExitOL
 * Make a string with an offer list using exit format.
 */
extern char * SPrintExitOL( /* ol */ );
/*   OfferListTyp   ol; */


/* MvNextOffer
 * Move to the next offer.
 * o points to an offer list, and the next node is returned.
 */
extern OfferListTyp MvNextOffer( /* o */ );
/* OfferListTyp  o; */


/* AddOL
 * Add an offer o to the offer list ol.
 */
extern OfferListTyp AddOL( /* o,ol */ );
/* POfferTyp  o;
   OfferlistTyp ol;  */


/* InsertOL
 * Insert the offer o into the offer list ol.
 */
extern OfferListTyp InsertOL( /* o,ol */ );
/* POfferTyp  o;
   OfferlistTyp ol;  */


/* IsThereQuestionOL
 * Return TRUE if there is an offer QUESTION in the offer list ol.
 * otherwise FALSE.
 */
extern boolean IsThereQuestionOL( /* ol */ );
/* OfferListTyp  ol;  */


/* IsThereExclamationOL
 * Return TRUE if there is an offer EXCLAMATION in the offer list ol.
 * otherwise FALSE.
 */
extern boolean IsThereExclamationOL( /* ol */ );
/* OfferListTyp  ol;  */


/* VarsDefinedInOL
 * Return a list with the variables defined in the offer list ol.
 */
extern ExprListTyp VarsDefinedInOL( /* ol */ );
/* OfferListTyp ol; */


/* LookForVarOL
 * Look for the offer where variable v is being defined
 */
extern OfferListTyp LookForVarOL( /* vd, ol */ );
/* DescriptorTyp vd;
   OfferListTyp ol; */

/* Convert_to_AdmirationOL
 * Transform all the QUESTION offers into ADMIRATION offers
 */
extern void Convert_to_AdmirationOL( /* ol */ );
/* OfferListTyp ol; */


/******************************************************************
 *                                                                *
 *      RFLA  -> Relab Func List Attribute (RelabFuncListTyp)     *
 *                                                                *
 ******************************************************************/

/* InitRF
 * Init the RF module
 */
extern void InitRF();


/* StatRF
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatRF( /* new, released, max */ );
/*   int * new, *released, *max; */


/* NewRF
 * Get memory for a new RF struct.
 */
extern PRelabFuncTyp NewRF();


/* FreeRF
 * Free memory used by an RF.
 */
extern void FreeRF( /* rf */ );
/* PRelabFuncTyp   rf; */ 


/* CopyRF
 * Copy the RF rf.
 */
extern PRelabFuncTyp CopyRF( /* rf */ );
/* PRelabFuncTyp rf; */


/* MakeRF
 * Create the relab function [ga/gf]
 */
extern PRelabFuncTyp MakeRF( /* ga, gf */ );
/*  DescriptorTyp ga, gf; */


/* CreateRFL
 * Create an empty RelabFuncList.
 */
#define CreateRFL() (RelabFuncListTyp)NULL


/* FreeRFL
 * Free the memory used by the RelabFuncList rfl.
 */
extern void FreeRFL( /* rfl */ );
/* RelabFuncListTyp rfl; */


/* LengthRFL
 * Return the length of the relab func list rfl.
 */
extern int LengthRFL( /* rfl */ );
/*  RelabFuncListTyp  rfl; */


/* CopyRFL
 * Copy the RelabFuncList rfl.
 */
extern RelabFuncListTyp CopyRFL( /* rfl */ );
/* RelabFuncListTyp rfl; */


/* JoinRFL
 * Join the relab func list rfl1 and rfl2. Returns rfl1,rfl2.
 */
extern RelabFuncListTyp JoinRFL( /* rfl1, rfl2 */ );
/* RelabFuncListTyp rfl1,rfl2; */


/* JunctionRFL
 * Return the junction of relabel function lists : rfl1 ( rfl2() ).
 * rfl1 is applied upon rfl2. ( It is non-conmutative ):
 *
 *   rfl1     Example: [ b/a, x/b, x/c ]   ==    [ y/a, x/c ]
 *    |                        |                       |
 *   rfl2                [ a/b, y/a ]                  B
 *    |                        |
 * Behaviour                   B
 *
 * rfl1 and rfl2 are destroyed in order to create the junction.
 * Parameters must be copied,
 */
extern RelabFuncListTyp JunctionRFL( /* rfl1, rfl2 */ );
/* RelabFuncListTyp rfl1,rfl2; */


/* PrintRFL
 * Print the relab function List rfl,
 * in the format  ga1/gf1, ga2/gf2,...,gan/gfm  where gai gaj are gate names.
 * pstr is the function used to print strings.
 */
extern void PrintRFL( /* rfl, pstr */ );
/* RelabFuncListTyp   rfl;
   void (*pstr)(); */


/* SPrintRFL
 * Make a string with the Relab Function list rfl.
 * in the format ga1/gf1, ga2/gf2,...,gan/gfm where gai,gfj are gate names. 
 */
extern char * SPrintRFL( /* rfl */ );
/*   RelabFuncListTyp   rfl;  */


/* AddRF
 * Add the relab func rf to the relab func list rfl.
 */
extern RelabFuncListTyp AddRF( /* rf,rfl */ );
/* PRelabFuncTyp    rf;
   RelabFuncListTyp rfl;  */


/* AddRFL
 * Add [ga/gf] to the RelabFuncList rfl.
 * If it already exists : no append.
 * Conditions: gf can not belong to Range(rfl) or else execution will be halted
 */
extern RelabFuncListTyp AddRFL( /* rfl, ga, gf */ );
/*RelabFuncListTyp rfl;
  DescriptorTyp    ga,gf;*/


/* ActualRFL
 * Return the actual gate associated to the formal gate gf
 * If it doesn't exist : return 0
 */
extern DescriptorTyp ActualRFL( /* rfl, gf */ );
/* RelabFuncListTyp rfl;
   DescriptorTyp    gf;*/


/* FormalRFL
 * Return the n-th Formal gate associated to the actual gate ga
 * If it doesn't exist : return 0
 */
extern DescriptorTyp FormalRFL( /* rfl, ga, n */ );
/*   RelabFuncListTyp rfl; 
     DescriptorTyp    ga;
     int              n; */


/* LookForGateRF
 * Return the formal gate in the current rfl node.
 */
extern DescriptorTyp LookForGateRF( /* rfl */ );
/*     RelabFuncListTyp rfl; */


/* LookActGateRF
 * Return the Actual gate in the current rfl node.
 */
extern DescriptorTyp LookActGateRF( /* rfl */ );
/*     RelabFuncListTyp rfl;*/


/* RangeRFL
 * Return Range(rfl) = Formal gate set
 */
extern GateSetTyp RangeRFL( /* rfl */ );
/* RelabFuncListTyp rfl; */


/* ImageRFL
 * Return Image(rfl) = Actual gates set
 */
extern GateSetTyp ImageRFL( /* rfl */ );
/* RelabFuncListTyp rfl; */


/* InvRFL
 * Return the inverse gate relabel function list of rfl.
 * rfl is modified by exchanging ga and gf.
 * Therefore the new relabel function may not be an application.
 */
extern RelabFuncListTyp InvRFL( /* rfl */ );
/* RelabFuncListTyp rfl; */


/* ApplyRFL
 * Return the gate set output from applying the relabel function
 * defined by rfl to the input gate set gs.
 */
extern GateSetTyp ApplyRFL( /* rfl, gs */ );
/* RelabFuncListTyp rfl;
   GateSetTyp        gs; */


/* ApplyGL_RFL
 * Return the gate list output from applying the relabel function
 * defined by rfl to the input gate list gl.
 */
extern GateListTyp ApplyGL_RFL( /* rfl, gl */ );
/*   RelabFuncListTyp rfl;
     GateListTyp        gl; */


/* InvApplyRFL
 * Return the gate set output from applying reversely the relabel function
 * defined by rfl to the input gate set gs.
 */
extern GateSetTyp InvApplyRFL( /* rfl, gs */ );
/* RelabFuncListTyp rfl;
   GateSetTyp       gs;*/


/* Mk_GLs_RFL
 * Make a new relabel function list by combining
 * an actual gate list ,gla, and a formal one ,glf.
 * The gate list lengths must be equal.
 * The RFL is NOT a literal transcription of [ga1/gf1,ga2/gf2,...] :
 * The RFs are added through the AddRFL command which filters 
 * duplicated RFs off and verifies inequality of formal gates.
 */
extern RelabFuncListTyp Mk_GLs_RFL( /* gla, glf */ );
/* GateListTyp gla,glf;*/


/* EqualRFL
 * Return TRUE if rfl1 and rfl2 are equal (in the same order).
 */
extern boolean EqualRFL( /* rfl1, rfl2 */ );
/* RelabFuncListTyp rfl1,rfl2; */


/* DeleteNodeRFL
 * Delete the current node n of rfl.
 * Returns the new rfl.
 * Conditions: 
 *   n must belong to rfl.
 *   n !=NULL. l !=NULL.
 */
extern RelabFuncListTyp DeleteNodeRFL( /* n, l */ );
/*  PRelabFuncTyp     n; 
    RelabFuncListTyp  l; */


/* RemoveWhenRFL
 * Delete the rfl nodes which hold the boolean condition "when".
 * Return the new rfl.
 */
extern RelabFuncListTyp RemoveWhenRFL( /* rfl, when */ );
/*     RelabFuncListTyp rfl; 
       boolean          (*when)(); */


/* RFL_to_GDL
 * Compute the equivalent gate declaration list of a rfl.
 */
extern GateDecListTyp RFL_to_GDL( /* rfl */ );
/*     RelabFuncListTyp rfl; */


/* SimplifyRFL
 * Remove from rfl those RFs whose formal gates belong to gs.
 * ( gs is supposed to be an invisible (to the rfl) gate set )
 */
extern RelabFuncListTyp SimplifyRFL( /* rfl, gs */ );
/*     RelabFuncListTyp rfl;
       GateSetTyp       gs; */


/******************************************************************
 *                                                                *
 *       VALA  -> Var Assign List Attribute (VarAssignListTyp)    *
 *                                                                *
 ******************************************************************/


/* InitVA
 * Init the VA module
 */
extern void InitVA();


/* StatVA
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatVA( /* new, released, max */ );
/*   int * new, *released, *max; */


/* StatisticVAL
 * Statistics of the variable assign list val.
 * Return the number of var-assign nodes (va) used in val,
 * the number of list nodes used to build the list (nl),
 * and the number of variable and operator cells and list nodes used 
 * in the expressions.
 * nv,vv and ov are virtual values of number of list nodes, variables and
 * operation cells, i.e. without paying attention to the sharing feature.
 * nr,vr and or are the real values, i.e. nodes and cells already counted in
 * other expressions are not counted again here.
 */
extern void StatisticVAL( /* val,nv,vv,ov,nr,vr,or,va,nl */ );
/* VarAssignListTyp val;
   int              *nv, *vv, *ov, *nr, *vr, *or, *va, *nl; */


/* MakeVA
 * Create a node [variable/expression]
 */
extern PVarAssignTyp MakeVA( /* vf, ea */ );
/*    DescriptorTyp vf;
      ExprTyp       ea;  */


/* FreeVA
 * Free a single var assign.
 */
extern void FreeVA( /* va */ );
/* PVarAssignTyp  va; */


/* CopyVA
 * Copy a single var assign
 */
extern PVarAssignTyp CopyVA( /* vaPt */ );
/* PVarAssignTyp vaPt; */


/* DrawVA
 * Print the var assign vaPt in a not LOTOS format.
 * pstr is the function used to print strings.
 */
extern void DrawVA( /* vaPt, pstr */ );
/*  PVarAssignTyp   vaPt;
    void            (*pstr)(); */


/* CreateVAL
 * Create a VAL. (Returns an empty VarAssignList.)
 */
extern VarAssignListTyp CreateVAL();


/* FreeVAL
 * Free the memory used by the VarAssignList val.
 */
extern void FreeVAL( /* val */ );
/* VarAssignListTyp val; */


/* CopyVAL
 * Copy the VarAssignList val.
 */
extern VarAssignListTyp CopyVAL( /* val */ );
/* VarAssignListTyp val; */


/* UnshareVAL
 * Unshare the var assign list val.
 */
extern VarAssignListTyp UnshareVAL( /* val */ );
/* VarAssignListTyp val; */


/* PrintVAL
 * Print the var assign list val in the format x.s1=expr1, y.s2=expr2,...
 * pstr is the function used to print strings.
 */
extern void PrintVAL( /* val, pstr */ );
/* VarAssignListTyp   val;
   void (*pstr)(); */


/* SPrintVAL
 * return a string with the var assign list val
 * in the format x:s1=expr1, y:s2=expr2,...
 * all => print even x:s=x assignments.
 */
extern char * SPrintVAL( /* val */ );
/*     VarAssignListTyp val; */ 


/* DrawVAL
 * Prints the var assign list val.
 * pstr is the function used to print strings.
 */
extern void DrawVAL( /* val,pstr */ );
/* VarAssignListTyp  val;
   void              (*pstr)(); */


/* JoinVAL
 * Join two var assign lists.
 * If the expressions of val2 contain variables defined ( "assigned") in val1,
 * these variables are replaced in the output VAL with the expressions assigned
 * in val1.   val1      EX.: ..,x=3,..
 *              |                |
 *            val2           ..,y=x+1,..        ==>    ..,x=3,..,y=3+1,..
 *              |                |                             |
 *              B                B                             B
 */
extern VarAssignListTyp JoinVAL( /* VAl1, VAl2 */ );
/* VarAssignListTyp VAl1,VAl2; */


/* InsertVAL
 * Insert VA item 'let var=exp' into the VarAssignList val.
 * (No previous check : variable var may have two assignations, that's to say,
 * if 'let x:s=E' were inserted , another 'let x:s=E2' could be unnoticeably
 * inserted.)
 */
extern VarAssignListTyp InsertVAL( /* val, vd, e */ );
/*VarAssignListTyp val;
  DescriptorTyp    vd;
  ExprTyp          e;*/


/* AddVAL
 * Add item 'let var=exp' into the VarAssignList val.
 * (No previous check : variable var may have two assignations, that's to say,
 * if 'let x=anyexpr' was inserted , another 'let x=...' could be unnoticeably
 * inserted.)
 */
extern VarAssignListTyp AddVAL( /* val, vd, e */ );
/* VarAssignListTyp val;
   DescriptorTyp    vd;
   ExprTyp          e;  */


/* ActExprVAL
 * Return the Actual Expression associated to the var descriptor vd.
 * If it doesn't exist : return NULL.
 */
extern DescriptorTyp ActExprVAL( /* val, vd */ );
/* VarAssignListTyp val;
   DescriptorTyp    vd; */


/* Mk_VLEL_VAL
 * Make a new var assign list by combining
 * an Actual Var list ,vl, and a Formal Expression list , el.
 * The lists lengths must be equal.
 * The val is a literal transcription of v1:s1=e1, v2:s2=e2,...as
 * the VAs are joined together through the InsertVAL function, which
 * does not test inequality of FormalVars v1 v2 ... .
 * vl is used only to look at its var names, so it can be reused.
 */
extern VarAssignListTyp Mk_VLEL_VAL( /* vl, el */ );
/* ExprListTyp  vl,el; */


/* LookVarVAL
 * Look at (return) the formal variable in the current VarAssign node valn.
 */
extern DescriptorTyp LookVarVAL( /* valn */ );
/*  VarAssignListTyp valn; */


/* GetVarVAL
 * Get (return) the formal variable in the current VarAssign node valn 
 * (of a list) and the varFor is set to 0.
 */
extern DescriptorTyp GetVarVAL ( /* valn */ );
/*  VarAssignListTyp valn;*/


/* PutVarVAL
 * Put a new formal variable to the current VarAssign node valn (of a list)
 * The old varFor must be NULL.
 */
extern void PutVarVAL ( /* valn, fv */ );
/*   VarAssignListTyp valn;
     DescriptoTyp      fv;*/


/* LookExprVAL
 * Look at (return) the actual Expression in the current VarAssign node valn 
 */
extern ExprTyp LookExprVAL( /* valn */ );
/*  VarAssignListTyp valn;*/


/* GetExprVAL
 * Get the actual actual Expression in the current VarAssign node valn 
 * and the actExp is set to NULL.
 */
extern ExprTyp GetExprVAL( /* valn */ );
/*  VarAssignListTyp valn;*/


/* PutExprVAL
 * Put a new actual Expr to the current VarAssign node valn (of a list)
 * The old actExpr must be NULL.
 */
extern void PutExprVAL( /* valn, ae */ );
/*  VarAssignListTyp valn;
    ExprTyp ae;*/


/* FormalVL_VAL
 * Build the formal variable list of a VAL.
 */
extern ExprListTyp FormalVL_VAL( /* val */ );
/* VarAssignListTyp val; */


/* ActualEL_VAL
 * Make the actual expression list of a VAL.
 */
extern ExprListTyp ActualEL_VAL( /* val */ );
/* VarAssignListTyp val; */

/* IsNotPrintableVAL
 * Say whether the val contains only void assignments:
 * val == NULL  or  val == x:s=x, y:s=y, ...
 */
extern boolean IsNotPrintableVAL( /* val */ );
/*     VarAssignListTyp val; *
       
       
       /* IsVoidVAL
	* Say if the val contains only void assignments:
	* val == NULL  or  val == x:s=x, y:s=y, ...
	*/
extern boolean IsVoidVAL( /* val */ );
/*  VarAssignListTyp val;  */


/* EqualVA
 * Say if two VarAssigns are equal
 */
extern boolean EqualVA( /* vaPt1, vaPt2 */  );
/*     PVarAssignTyp vaPt1, vaPt2; */


/* SubSet_VAL
 * Determine if every VA of val1 is in val2.
 */
extern boolean SubSet_VAL( /* val1, val2 */ );
/*     VarAssignListTyp val1,val2; */


/******************************************************************
 *                                                                *
 *     GDLA -> Gate Declaration List Attribute (GateDecListTyp)   *
 *                                                                *
 ******************************************************************/


/* InitGD
 * Init the GD module
 */
extern void InitGD();


/* StatGD
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatGD( /* new, released */ );
/*   int * new, *released; */


/* StatisticGDL
 * Return the number of list nodes (n) used in the gate list, and
 * the number of gate sets (gs) used in the declaration list gdl.
 */
extern void StatisticGDL( /* gdl,n,gs */ );
/* GateDecListTyp gdl;
   int            *n, *gs; */


/* MakeGD
 * Make a gate declaration with gl and gs.
 */
extern PGateDecTyp MakeGD( /* gl,gs */ );
/* GateListTyp gl;
   GateSetTyp  gs;  */


/* FreeGD
 * Free the memory used by the gate declaration
 */
extern void FreeGD( /* gd */ );
/* PGateDecTyp gd */


/* CopyGD
 * Copy the gate declaration gd
 */
extern PGateDecTyp CopyGD( /* gd */ );
/* PGateDecTyp gd */


/* SPrintGD
 * Make a string with the gate declaration gd.
 */
extern char * SPrintGD( /* gd */ );
/*     PGateDecTyp gd; */


/* EqualGD
 * Decide if 2 gatedecs are equal.
 */
extern boolean EqualGD( /* gd1, gd2 */ );
/* PGateDecTyp gd1,gd2; */


/* CreateGDL
 * Create an empty gate declaration list.
 */
extern GateDecListTyp CreateGDL();


/* FreeGDL
 * Free the memory used by the gate declaration list gdl
 */
extern void FreeGDL( /* gdl */ );
/* GateDecListTyp gdl; */


/* CopyGDL
 * Copy the gate declaration list gdl
 */
extern GateDecListTyp CopyGDL( /* gdl */ );
/* GateDecListTyp gdl; */


/* PrintGDL
 * Print the gate declaration list gdl.
 * pstr is the function used to print strings.
 */
extern void PrintGDL( /* gdl, pstr */ );
/* GateDecListTyp gdl;
   void (*pstr)(); */


/* SPrintGDL
 * Make a string with the gate declaration list gdl
 */
extern char * SPrintGDL( /* gdl */ );
/*   GateDecListTyp gdl; */


/* AddGDL
 * Add the gate declaration gd to the gate declaration list gdl
 */
extern GateDecListTyp AddGDL( /* gd,gdl */ );
/* PGateDecTyp    gd;
   GateDecListTyp gdl; */


/* InsertGDL
 * Insert the gate declaration gd into the gate declaration list gdl
 */
extern GateDecListTyp InsertGDL( /* gd,gdl */ );
/* PGateDecTyp    gd;
   GateDecListTyp gdl; */


/* EqualGDL
 * Decide if 2 gatedec lists are equal.
 */
extern boolean EqualGDL( /* gdl1, gdl2 */ );
/* GateDecListTyp gdl1,gdl2; */


/******************************************************************
 *                                                                *
 *     ITCLA -> Interleaved Continuation list Attribute           *
 *              (ITContListTyp).                                  *
 *                                                                *
 ******************************************************************/

/******************************************************************
 *                                                                *
 *                  Global Termination Counter                    *
 *                                                                *
 ******************************************************************/

/* InitTerm
 * Reset to 1 the termination counter.
 */
extern int InitTerm();


/* NewTerm
 * Return a new termination value.
 */
extern int NewTerm();


/* CurrentTerm
 * Return the current termination value.
 */
extern int CurrentTerm();


/* SetTerm
 * Set temporarily the termination counter to n.
 */
extern void SetTerm( /* n */ );
/*     int n; */


/* ResetTerm
 * Reset the termination counter to a brandnew value, after having been
 * set to a temporary value.
 */
extern void ResetTerm();


/* DisposeTerm
 *  Release the last termination value. ( decrement term-counter ).
 */
extern void DisposeTerm();


/******************************************************************
 *                                                                 *
 *               Labels                                            *
 *                                                                 *
 *        A label is a concatenation of termination cells sorted   *
 *        by name and joined by their first argument               *
 *                                                                 *
 *        Example of label :                                       *
 *                                                                 *
 *        < 3(x:s), 11, 24(z:s,w:s2), 3847 >                       *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *******************************************************************/

/* FreeLabel
 * Free a label
 */
extern void FreeLabel( /* label */ );
/*   LabelTyp label; */


/* EqualLabel
 * Decide whether 2 labels are equal. Only numbers are compared.
 */
extern boolean EqualLabel( /* label1, label2 */ );
/*   LabelTyp  label1, label2; */


/* InsertLabel
 * Append a termination to a label in a sorted way.
 * Example : InsertLabel( 3, <1,4,9> ) = <1,3,4,9>
 */
extern LabelTyp InsertLabel( /* t, label */ );
/*   BehTyp   t;
     LabelTyp label; */


/* CopyLabel
 * Copy a label
 */
extern LabelTyp CopyLabel( /* label */ );
/*   LabelTyp  label; */


/* JoinLabel
 * Join 2 labels in a sorted way. ( label1 & label2 no longer exist ).
 * Example : JoinLabel( <3,7>, <1,4,9> ) = <1,3,4,7,9>
 */
extern LabelTyp JoinLabel( /* label1, label2 */ );
/*   LabelTyp  label1, label2; */


/* HashKeyLabel
 * hash value for a label
 */
extern int HashKeyLabel( /* p */ );
/*   LabelTyp p; */


/* PrintLabel
 * Print a label with pstr ( only descriptors ).
 */
extern void PrintLabel( /* label, pstr */ );
/*   LabelTyp label;
     void (*pstr)(); *
     
     
     /* LookForLabel
      * Determine whether a termination belongs to a label.
      * return a pointer to the matched termination in the label
      */
extern LabelTyp LookForLabel( /* t, label */ );
/*     int       t;
       LabelTyp  label; */


/* SubLabel
 * Determine whether label sl is a sublabel of label.
 * Only descriptors are taken into account.
 */
extern boolean SubLabel( /* sl, label */ );
/*   LabelTyp sl, label; */


/* SubLabelList
 * Determine whether a label is a sublabel of the label made by
 * the list of integers tl.
 */
extern boolean SubLabelList( /* label, tl */ );
/*   LabelTyp label;
     ListTyp  tl;      */


/******************************************************************
 *                                                                *
 *              Label lists (LL)                                  *
 *                                                                *
 ******************************************************************/


/* Free_LL
 * Free a list of labels
 */
extern void Free_LL( /* labl */ );
/*   ListTyp labl; */


/* Copy_LL
 * Copy a label list
 */
extern ListTyp Copy_LL( /* labl */ );
/*   ListTyp labl; */


/* Print_LL
 * Print a list of labels
 */
extern void Print_LL( /* pstr, labl */ );
/*   void (*pstr)(); 
     ListTyp labl; */


/* HashF_LL
 * Label list hash function. Only descriptors are considered.
 */
extern int HashF_LL( /* labl */ );
/*   ListTyp labl; */


/* Equal_LL
 * Label list hash function. 
 */
extern boolean Equal_LL( /* labl1, labl2 */ );
/*   ListTyp labl1, labl2; */


/* SubSet_LL
 * Say whether labl1 is a subset of labl2.
 */
extern boolean SubSet_LL( /* labl1, labl2 */ );
/*   ListTyp labl1, labl2; */


/* Insert_LL
 * Insert a label into a label list
 */
extern ListTyp Insert_LL( /* label, labl */ );
/*   LabelTyp label;
     ListTyp  labl; */


/******************************************************************
 *                                                                 *
 *               IT continuations                                  *
 *                                                                 *
 *******************************************************************/

/* InitITC
 * Init the ITC module
 */
extern void InitITC();


/* NewITC
 * Get memory for a new interleaved continuation.
 */
extern PITContTyp NewITC();


/* DispITC
 * Free memory used by the PITContTyp struct.
 */
extern void DispITC( /* itc */ );
/* PITContTyp itc; */


/* FreeITC
 * Deallocate the memory used by the interleaved continuation itc.
 */
extern void FreeITC( /* itc */ );
/* PITContTyp itc; */


/* StatITC
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
extern void StatITC( /* new, released, max */ );
/*     int * new, *released, *max; */


/* CopyITC
 * Copy the interleaved continuation itc, copying its behaviour until actions.
 * The cset_labels hash table is not copied.
 */
extern PITContTyp CopyITC( /* itc */ );    
/* PITContTyp itc; */


/* CopyShareITC
 * Make a new continuation sharing all shareable contents of itc
 */
extern PITContTyp CopyShareITC( /* itc */ );
/*    PITContTyp itc; */

/* LookLabelITC
 * Look at an itc label.
 */
extern LabelTyp LookLabelITC( /* itc */ );
/* PITContTyp itc; */


/* LookBehITC
 * Look at an itc behaviour.
 */
extern BehTyp LookBehITC( /* itc */ );
/*    PITContTyp itc; */


extern void PrintITC( /* itc , pstr */ );
/* PITContTyp itc;
   void (*pstr)(); */


/* FreeITCL
 * Deallocate the memory used by the interleaved continuation list itcl.
 */
extern void FreeITCL( /* itcl */ );
/* ITContListTyp itcl; */


/* CopyITCL
 * Copy the interleaved continuation list itcl.
 */
extern ITContListTyp CopyITCL( /* itcl */ );    
/* ITContListTyp itcl; */


/* InsertITCL
 * Insert a itc in a list
 */
extern ITContListTyp InsertITCL( /* itcl, label, b, n_m */ );
/*   ITContListTyp itcl;
     LabelTyp      label;
     BehTyp        b;
     int           n_m; */


/* PrintITCL
 * Print the interleaved continuation list itcl.
 * pstr is the function used to print strings.
 */
extern void PrintITCL( /* itcl , pstr */ );
/* ITContListTyp itcl;
   void (*pstr)(); */


/* StatisticITC
 * Return the number of itc nodes (itcn) and list nodes (ln),
 * used in the interleaved continuation list itcl.
 * Return also a list of behaviours to be processed by StatSpecification()
 */
extern ListTyp StatisticITC( /* itcl, itcn, ln */ );
/* ITContListTyp itcl;
   int          *ln, *itcn; */


/* LookForITCL
 * Look for a continuation labelled <label> in an itcl.
 * NULL if <label> does not belong to itcl.
 */
extern PITContTyp LookForITCL( /* itcl, label */ );
/*   ITContListTyp itcl;
     LabelTyp      label; */


/* LookForNodeITCL
 * Look for a continuation labelled <label> in an itcl.
 * return the list node of that continuation
 * NULL if <label> does not belong to itcl.
 */
extern ListTyp LookForNodeITCL( /* itcl, label */ );
/*     ITContListTyp itcl;
       LabelTyp      label; */


/* LookFor_SubSet_ITCL
 * Look for a continuation labelled <c> subset of <label> in itcl.
 * NULL if there is not such a <c> in itcl.
 */
extern PITContTyp LookFor_SubSet_ITCL( /* itcl, label */ );
/*     ITContListTyp itcl;
       LabelTyp      label; */


/* LookFor_IncluderITCL
 * Look for a continuation with the same label and cset label included
 * in the cset_labels of an itcl.
 * There can be several candidates.
 * NULL if <label> does not belong to itcl.
 */
extern PITContTyp LookFor_IncluderITCL( /* itcl, itc */ );
/*     ITContListTyp itcl;
       PITContTyp    itc; */


/* LookFor_IdenticalITCL
 *  Look for a continuation with the same label and cset labels in an itcl.
 *  NULL if <label> does not belong to itcl.
 */
extern PITContTyp LookFor_IdenticalITCL( /* itcl, itc */ );
/*     ITContListTyp itcl;
       PITContTyp    itc;  */


/* LookFor_Update_IdenticalITCL
 * Look for a continuation with the same label and cset labels in an itcl.
 * return NULL if <label> does not belong to itcl.
 * if found then
 *  if its cset labels is already registered in the duplicated
 *    return the duplicate pit
 *  else
 *    return NULL
 */
extern PITContTyp LookFor_Update_IdenticalITCL( /* itcl, itc */ );
/*     ITContListTyp itcl;
       PITContTyp    itc; */


/* LookFor_Update_IncluderITCL
 * Look for a continuation with the same label and cset labels in an itcl.
 * return NULL if <label> does not belong to itcl.
 * if found then
 *  if its cset labels is already registered in a subset of the duplicated
 *    return the duplicate pit
 *  else
 *    return NULL
 */
extern PITContTyp LookFor_Update_IncluderITCL( /* itcl, itc */ );
/*     ITContListTyp itcl;
       PITContTyp    itc; */


/* CSets_Labels_in_Beh
 * Return the list of labels of the subbehaviors of all the continuations sets
 * of a behaviour
 */ 
extern ListTyp CSets_Labels_in_Beh( /* b */ );
/*   BehTyp b; */


/******************************************************************
 *                                                                 *
 *                          Paths                                  *
 *                                                                 *
 *          A path is a special label that behaves like            *
 *          an ordered set.                                        *
 *                                                                 *
 *          Example :                                              *
 *                                                                 *
 *          <3(x:s)> U < 3(x:s), 11(z:n) > = < 3(x:s), 11(z:n) >   *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *******************************************************************/


/* InsertPath
 * Append a termination into a path in a sorted and univocal way.
 * Example : InsertPath( 3, <1,3,4,9> ) = <1,3,4,9>
 */
extern LabelTyp InsertPath( /* t, label */ );
/*     BehTyp   t;
       LabelTyp label; */


/* JoinPath
 * Join 2 labels in a sorted way. ( label1 & label2 no longer exist ).
 * Example : JoinPath( <3,7>, <1,3,4,9> ) = <1,3,4,7,9>
 */
extern LabelTyp JoinPath( /* label1, label2 */ );
/*     LabelTyp  label1, label2; */



/******************************************************************
 *                                                                *
 *          STA -> Synchronization Tree Attribute                 *
 *                                                                *
 ******************************************************************/


typedef BehTyp SyncTreeTyp;


/* VPrintST
 * Verbose printing of the synchronization Tree st.
 * pstr is the function used to print strings.
 * proc is the selected process ( only instantiations to this process will be
 * printed )
 */
extern void VPrintST( /* st, pstr, proc, indent */ );
/*   SyncTreeTyp   st;
     void        (*pstr)();
     DescriptorTyp proc;
     int indent; */


/* PrintST
 * Print the synchronization Tree st.
 * pstr is the function used to print strings.
 */
extern void PrintST( /* st, pstr */ );
/*   SyncTreeTyp   st;
     void        (*pstr)(); */


/* FreeST
 * Free a Synchronization Tree
 */
extern void FreeST( /* st */ );
/*   SyncTreeTyp st; */


/* CopyST
 * Copy a synchronization Tree
 */
extern SyncTreeTyp CopyST( /* st */ );


/* IsEventLeafST
 * Say whether an event is a leaf of the ST or not.
 * ( if it is, its STA is a process insts list )
 */
extern boolean IsEventLeafST( /* event */ );
/*   BehTyp event; */


/******************************************************************
 *                                                                *
 *       SSLA -> Specification Source Line Attribute              *
 *                                                                *
 ******************************************************************/


/* FreeSSL
 * Free a SSL
 */
extern void FreeSSL( /* sl */ );
/*   int sl; */


/* PrintSSL
 * Print the attribute specification source line
 * pstr is the function used to print strings.
 */
extern void PrintSSL( /* sl, pstr */ );
/*   int sl;
     void (*pstr)(); */


/* SPrintSSL
 * Make a string with the specification source line.
 */
extern char * SPrintSSL( /* sl */ );
/*   int   sl; */


#endif


