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

  FileName    [versis.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 [The file versis.h contains declaration of all external
               data structures.]
  SeeAlso     [versisInt.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 _VERSIS
#define _VERSIS

#include <est.h>
#include <bdd.h>
#include <pa.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_VERSIS)
#      undef EXTERN
#      define EXTERN __declspec (dllexport)
#    else
#      if defined(USE_EST) || defined(USE_VERSIS)
#        undef EXTERN
#        define EXTERN __declspec (dllimport)
#      else
#        undef EXTERN
#        define EXTERN extern
#      endif
#    endif
#  endif
#endif

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

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

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

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

EXTERN int versis_status;

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

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

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

EXTERN void Versis_InitPkg();

EXTERN void Versis_ExitPkg();

EXTERN void Versis_AboutPkg();

EXTERN void Versis_Compose(Est_String name, int type,
              Est_String process, Est_String actions, Est_Boolean onthefly);

EXTERN void Versis_ComposeInit(Est_String name);

EXTERN int Versis_ComposeStep(int numcomp, int N);

EXTERN void Versis_ComposeFinish(int numcomp);

EXTERN Est_Boolean Versis_Equivalence(int type, int par1, Est_String name1,
                                      int par2, Est_String name2);

EXTERN int Versis_Minimization(int type, int par, Est_String name);

EXTERN void Versis_ChangeRename(Est_String process, Est_String name1,
                                Est_String name2);

EXTERN void Versis_ChangeHide(Est_String process, Est_String name1);

EXTERN void Versis_ChangeForbid(Est_String process, Est_String name1);

EXTERN Bdd_Edge Versis_CheckDeadlock(Bdd_Edge D);

EXTERN Bdd_Edge Versis_CheckDivergence(Bdd_Edge D, Bdd_Edge tau);

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

#endif /* _VERSIS */

