/**CHeaderFile*************************************************************
  PackageName [versis]
  Synopsis    [Package 'versis' provides basic tools for formal
               verification of concurrent systems]

  FileName    [versisInt.h]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Mirjam Sepesy Maucec (mirjam.sepesy@uni-mb.si),
               Tatjana Kapus (kapus@uni-mb.si)]
  Description [File versisInt.h contains declaration of internal
               data structures.]
  SeeAlso     [versis.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 _VERSISINT
#define _VERSISINT

#include "versis.h"

#ifdef USE_BDD_STUBS
#  include <bddDecls.h>
#endif

#ifdef USE_PA_STUBS
#  include <paDecls.h>
#endif

#ifdef TCLOUT
#  include <gui.h>
#  define printf Gui_Printf
#  ifdef USE_GUI_STUBS
#    include <guiDecls.h>
#  endif
#endif

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

typedef int *TTabIndexov;   /* tabela indeksov spremenljivk */

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

typedef struct {
  Bdd_Edge S;
  Est_Boolean b;
  int t;
} VersisST;

typedef struct {
  int num;
  VersisST *table;
} VersisStateTable;

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

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

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

extern void Versis_Compose_Thr(Est_String name, int type, int numP,
   Est_String process, int numA, Est_String actions, Est_Boolean onthefly);

extern Est_Boolean Versis_Equivalence_Thr(int type, int par1,
                           Est_String name1, int par2, Est_String name2);

extern void Versis_Minimization_Thr(int type, int par, Est_String name);

extern Est_Boolean VersisStrongEquivalence(Bdd_Edge *eqv,
                                      int par1, int n1, int par2, int n2);

extern Est_Boolean VersisWeakEquivalence(Bdd_Edge *eqv,
                                      int par1, int n1, int par2, int n2);

extern Est_Boolean VersisTestEquivalence(Bdd_Edge *eqv,
                                      int par1, int n1, int par2, int n2,
                                      int *acc1, int *acc2);

extern Est_Boolean VersisTraceEquivalence(int type, Bdd_Edge *eqv,
                                      int par1, int n1, int par2, int n2,
                                      int *det1, int *det2);

extern int VersisStrongMinimization(Est_String name, int par, int n);

extern int VersisWeakMinimization(Est_String name, int par, int n);

extern int VersisTraceMinimization(int type, Est_String name, int par, int n);

extern int VersisWCAMinimization(Est_String name, int par, int n);

extern Bdd_Edge VersisBuildDet(Est_String orgname, Est_String newname,
			Bdd_Edge init, Bdd_Edge Ptau, Bdd_Edge trcl, int s);

extern Bdd_Edge VersisTrCl(Bdd_Edge f);

extern Bdd_Edge VersisComposeActions(Pa_Composition *c);

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

#endif /* _VERSISINT */











