/**CHeaderFile*************************************************************
  PackageName [pa]
  Synopsis    [Package 'pa' is a framework for implementation of
               process algebrae similar to Milner's CCS and Hoare's CSP.]

  FileName    [pa.h]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File pa.h contains declaration of all external
               data structures.]
  SeeAlso     [paInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#ifndef _PA
#define _PA

#include <est.h>
#include <bdd.h>

/* ON WIN32 THERE HAS TO BE DEFINED ESTWIN32 */
/* ON UNIX THERE HAS TO BE DEFINED ESTUNIX */
/* ON MACOSX THERE HAS TO BE DEFINED ESTMACOSX */

#ifdef ESTUNIX
#  ifndef EXTERN
#    define EXTERN extern
#  endif
#endif

#ifdef ESTMACOSX
#  ifndef EXTERN
#    define EXTERN extern
#  endif
#endif

#ifdef ESTWIN32
#  ifdef TCL
#    undef EXTERN
#    define EXTERN extern
#  else
#    if defined(BUILD_EST) || defined(BUILD_PA)
#      undef EXTERN
#      define EXTERN __declspec (dllexport)
#    else
#      if defined(USE_EST) || defined(USE_PA)
#        undef EXTERN
#        define EXTERN __declspec (dllimport)
#      else
#        undef EXTERN
#        define EXTERN extern
#      endif
#    endif
#  endif
#endif

/*-----------------------------------------------------------------------*/
/* Constant declarations                                                 */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Type declarations                                                     */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Structure declarations                                                */
/*-----------------------------------------------------------------------*/

/* SPECIFIC FIELDS CONNECTED TO BDD VARIABLES */
typedef struct {
  int weight;                         /*  weight = 1,2,4... (decoding )  */
  int proccomp;                       /* used in decoding of composition */
} Pa_Variable;

typedef struct {
  Est_String  name;            /* action name */
  Bdd_Edge    p;               /* BDD representation of an action */
} Pa_Action;

typedef struct {
  Est_String  name;            /* state name */
  Bdd_Edge    bddR ;           /* BDD with 'r' variables (current state) */
  Bdd_Edge    bddS;            /* BDD with 's' variables (next state) */
  Bdd_Edge    bddComp;         /* represents how the state is composed */
  Bdd_Edge    acc;             /* acceptance set */
  Bdd_Edge    minacc;          /* minimized acceptance set */
  Est_String  ccs;             /* outgoing transition in CCS format */
  Est_Boolean final;           /* TRUE for final states, used for w/c automata */
} Pa_State;

typedef struct {
  int source;                  /* source state */
  int action;                  /* action */
  int type;                    /* action type, 0 = output, 1 = input */
  int dest;                    /* destination state */
} Pa_Transition;

typedef struct {
  Est_String   name;                         /* sort name */
  int          encoded;                      /* 1 = yes, 0 = no */
  int          numVar;                       /* number of variables */
  int          numActions;                   /* number of actions */
  Pa_Action    *table;                       /* table of actions */
  Bdd_Edge     a0;                           /* first variable */
  Est_Boolean  deleted;                      /* TRUE = deleted */
} Pa_Sort;

typedef struct {
  Est_String     name;                       /* process name */
  Est_String     compname;                   /* optionally, if states are composed */
  int            encoded;                    /* 1 = yes, 0 = no */
  int            sort;                       /* sort */
  int            numStates;                  /* number of states */
  Pa_State       *tableS;                    /* table of states */
  int            initial;                    /* initial state */
  Bdd_Edge       stateBDD;                   /* BDD of all states */
  int            numTransitions;             /* number of transitions */
  Pa_Transition  *tableT;                    /* table of transitions */
  int            numVar;                     /* number of variables */
  Bdd_Edge       d;                          /* transition relation */
  Bdd_Edge       stab;                       /* stab BDD for process */
  Est_Boolean    trace;                      /* TRUE = use trace minimized process for composition */
  Est_Boolean    weak;                       /* TRUE = use weak minimized process for composition */
  Est_Boolean    deleted;                    /* TRUE = deleted */
} Pa_Process;

typedef struct {
  Est_String  name;                       /* composition name */
  int         type;                       /* type of composition */
  int         numProcesses;               /* number of processes */
  int         *tableP;                    /* table of processes */
  int         numActions;                 /* number of given actions */
  int         *tableA;                    /* table of actions */
  int         sort;                       /* sort */
  Bdd_Edge    initialBDD;                 /* BDD of initial state */
  Bdd_Edge    stateBDD;                   /* BDD of all states */
  Bdd_Edge    transitionBDD;              /* BDD of transition relation */
  Bdd_Edge    actionsBDD;                 /* BDD of actions given to the composition */
  Bdd_Edge    *di;                        /* di BDDs for processes */
  Bdd_Edge    *dij;                       /* dij BDDs for processes */
  Bdd_Edge    *alphabet;                  /* alphabets of processes */
  Bdd_Edge    snew;                       /* used for step-by-step composition */
  Est_Boolean onthefly;                   /* TRUE = used for on-the-fly algorithms */
  Est_Boolean full;                       /* TRUE = used in CCS parser */
  Est_Boolean trace;                      /* TRUE = used in CCS parser */
  Est_Boolean weak;                       /* TRUE = used in CCS parser */
  Est_Boolean strong;                     /* TRUE = used in CCS parser */
} Pa_Composition;

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

EXTERN int pa_status;

EXTERN int pa_variables;                     /* number of BDD variables */

EXTERN int pa_sorts;                         /* number of sorts */

EXTERN int pa_processes;                     /* number of processes */

EXTERN int pa_compositions;                  /* number of compositions */

EXTERN Pa_Variable *pa_variableTable;        /* table of BDD variables */

EXTERN Pa_Sort *pa_sortTable;                /* table of sorts */

EXTERN Pa_Process *pa_processTable;          /* table of processes */

EXTERN Pa_Composition *pa_compositionTable;  /* table of compositions */

/*-----------------------------------------------------------------------*/
/* Macro declarations                                                    */
/*-----------------------------------------------------------------------*/

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Function prototypes                                                   */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* paMain.c                                                              */
/*-----------------------------------------------------------------------*/

EXTERN void Pa_InitPkg();

EXTERN void Pa_ExitPkg();

EXTERN void Pa_AboutPkg();

EXTERN void Pa_InitVariable(int i);

EXTERN int Pa_AddNewSort(Est_String name);

EXTERN int Pa_FindSort(Est_String name);

EXTERN int Pa_FOASortAction(Pa_Sort *sort, Est_String name);

EXTERN int Pa_FindSortAction(Pa_Sort *sort, Est_String name);

EXTERN int Pa_AddNewProcess(Est_String name);

EXTERN int Pa_FindProcess(Est_String name);

EXTERN void Pa_RenameProcess(Est_String old, Est_String new);

EXTERN int Pa_CopyProcess(Est_String name, Est_String copy,
                Est_String copysort, Est_String old, Est_String new);

EXTERN Est_Boolean Pa_IsGate(Est_String name);

EXTERN int Pa_FOAStateProcess(Pa_Process *proc, Est_String name);

EXTERN int Pa_FOAGateProcess(Pa_Process *proc, Est_String name);

EXTERN int Pa_FOAComposedStateProcess(Pa_Process *proc, Bdd_Edge F,
                                      Est_String prefix);

EXTERN int Pa_FindStateProcess(Pa_Process *proc, Est_String name);

EXTERN int Pa_AddStateProcess(Pa_Process *proc, Est_String name);

EXTERN int Pa_FOANextStateProcess(Pa_Process *proc, Est_String prefix);

EXTERN int Pa_NumberStateProcess(Pa_Process *proc);

EXTERN int Pa_FOATransition(Pa_Process *proc, int state1,
                            int action, int type, int state2);

EXTERN int Pa_AddNewComposition(Est_String name, int type,
                                int numP, int numA);

EXTERN void Pa_DeleteStateProcess(Pa_Process *proc, int num);

EXTERN void Pa_DeleteSort(int num);

EXTERN void Pa_RemoveDeletedSorts();

EXTERN void Pa_DeleteProcess(int num);

EXTERN void Pa_RemoveDeletedProcesses();

EXTERN void Pa_RemoveComposition(int num);

EXTERN int Pa_FindComposition(Est_String name);

EXTERN int Pa_FindProcessComp(Pa_Composition *c, Est_String name);

EXTERN Bdd_Edge Pa_AddStab(Bdd_Edge d, Est_String name);

EXTERN void PaSaveSortActions(Pa_Sort *s);

EXTERN void PaSaveProcStates(Pa_Process *p);

/*-----------------------------------------------------------------------*/
/* paKod.c                                                               */
/*-----------------------------------------------------------------------*/

EXTERN void Pa_EncodeSort(Est_String name);

EXTERN void Pa_EncodeProcess(Est_String name);

EXTERN void Pa_EncodeMultiProcesses(Est_String plist);

EXTERN int Pa_ExpandGates(Pa_Process *p);

EXTERN int Pa_Process2Composition(Est_String name);

EXTERN int Pa_Composition2Process(Est_String name, Est_Boolean full);

EXTERN int Pa_DecodeSortActions(Pa_Sort *s, Bdd_Edge F, Est_Boolean write);

EXTERN Est_String Pa_DecodeSortActions1(Pa_Sort *s, Bdd_Edge F, Est_Boolean write);

EXTERN void Pa_DecodeProcess(Est_String name, Est_Boolean write);

EXTERN int Pa_DecodeProcessStates(Pa_Process *p, Bdd_Edge F,
                                   Est_Boolean write);

EXTERN int Pa_DecodeProcessTR(Pa_Process *p, Bdd_Edge F,
                               Est_Boolean write);

EXTERN void Pa_DecodeComposition(Est_String name, Est_Boolean write);

EXTERN int Pa_DecodeCompStates(Pa_Composition *c, Bdd_Edge F,
                                Est_Boolean write);

EXTERN int Pa_DecodeCompTR(Pa_Composition *c, Bdd_Edge F, Est_Boolean write);

EXTERN int Pa_DecodeProcProcPair(Pa_Process *p1, Pa_Process *p2, Bdd_Edge F,
                                  Est_Boolean write);

EXTERN int Pa_DecodeCompProcPair(Pa_Composition *c, Pa_Process *p,
                                  Bdd_Edge F, Est_Boolean write);

EXTERN int Pa_DecodeCompCompPair(Pa_Composition *c1, Pa_Composition *c2,
                                  Bdd_Edge F, Est_Boolean write);

EXTERN Bdd_Edge Pa_ExtractProcTransition(Pa_Process *p, Bdd_Edge f);

EXTERN Bdd_Edge Pa_ExtractCompTransition(Pa_Composition *c, Bdd_Edge f);

EXTERN Bdd_Edge Pa_ExtractProcState(Pa_Process *p, Bdd_Edge f);

EXTERN int Pa_EnumerateProcState(Pa_Process *p, Bdd_Edge f);

EXTERN Bdd_Edge Pa_ExtractCompState(Pa_Composition *c, Bdd_Edge f);

EXTERN Bdd_Edge Pa_ExtractSortAction(Pa_Sort *s, Bdd_Edge f);

EXTERN int Pa_EnumerateSortAction(Pa_Sort *s, Bdd_Edge f);

/*-----------------------------------------------------------------------*/
/* paOutput.c                                                            */
/*-----------------------------------------------------------------------*/

EXTERN void Pa_WriteKnownSorts();

EXTERN void Pa_WriteSort(Est_String name);

EXTERN void Pa_WriteKnownProcesses();

EXTERN void Pa_WriteProcess(Est_String name, char type);

EXTERN void Pa_WriteKnownCompositions();

EXTERN void Pa_WriteProcessCCS(Est_String name, char type);

EXTERN void Pa_WriteProcessFSP(Est_String name, char type);

/*-----------------------------------------------------------------------*/
/* paParser.y                                                            */
/*-----------------------------------------------------------------------*/

EXTERN int Pa_ParseSortProcess(Est_String ime);

/**AutomaticEnd***********************************************************/

#endif  /* _PA */

