/**CHeaderFile*************************************************************
  PackageName [mc]
  Synopsis    [Package 'mc' provides a symbolic ACTLW model checker]

  FileName    [mc.h]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si)]
  Description [File mc.h contains declaration of all external
               data structures needed for ACTLW model checking.]
  SeeAlso     [mcInt.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 _MC
#define _MC

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

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

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

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

typedef struct {
  Est_String     name;                       /* formula name */
  Est_String     formula;                    /* formula body */
} Mc_Formula;

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

EXTERN int mc_status;

EXTERN int mc_formulae;                      /* number of formulae */

EXTERN Mc_Formula *mc_formulaTable;          /* table of formulae */

/* ACTL PARSER SETTINGS */
EXTERN const int MC_SIMPLE;
EXTERN const int MC_TRACE;         /* trace of ACTL parsing */
EXTERN const int MC_XTRACE;        /* extended trace of ACTL parsing */
EXTERN const int MC_EXPLAIN;       /* explain generated diagnostic */
EXTERN const int MC_TRACEPATH;     /* full paths in diagnostic */
EXTERN const int MC_DIAGNOSTIC;    /* generate linear w/c */
EXTERN const int MC_AUTOMATON;     /* generate w/c automaton */
EXTERN const int MC_MINIMIZE;      /* minimize w/c automaton */
EXTERN const int MC_TREE;          /* generate tree-like w/c */
EXTERN const int MC_PROGRESS;      /* report progress of on-the-fly MC */

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

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

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

EXTERN void Mc_InitPkg();

EXTERN void Mc_ExitPkg();

EXTERN void Mc_AboutPkg();

EXTERN int Mc_AddNewFormula(Est_String name, Est_String formula);

EXTERN int Mc_FOANextFormula(Est_String f, Est_String prefix);

EXTERN int Mc_FindFormula(Est_String name);

EXTERN void Mc_WriteKnownFormulae();

EXTERN void Mc_WriteFormula(Est_String ime, char type);

EXTERN void Mc_CheckACTL(int par, Est_String name, Est_String f,
                         int parserSettings);

EXTERN void Mc_CheckACTLString(int par, Est_String name, Est_String f,
                               int parserSettings);

EXTERN void Mc_CheckACTLFile(int par, Est_String name, Est_String f,
                         int parserSettings);

EXTERN void Mc_GenerateWCA(Est_String name, Est_String f, Est_String aname);

EXTERN void Mc_ReadACTL(Est_String name, Est_String f);

EXTERN void Mc_ReadACTLFile(Est_String f);

EXTERN Bdd_Edge Mc_CheckEEU(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1,
                           Bdd_Edge a2, Bdd_Edge s2);

EXTERN Bdd_Edge Mc_CheckAAU(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1,
                           Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge *AWfun,
                           Bdd_Edge *AFfun);

EXTERN Bdd_Edge Mc_CheckEEW(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1,
                            Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge *EUfun,
                            Bdd_Edge *EGfun);

EXTERN Bdd_Edge Mc_CheckAAW(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1,
                            Bdd_Edge a2, Bdd_Edge s2);

EXTERN Bdd_Edge Mc_CheckEEX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckAAX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckEEF(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckAAF(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckEEG(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckAAG(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckEU(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1,
                           Bdd_Edge a2, Bdd_Edge s2);

EXTERN Bdd_Edge Mc_CheckAU(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1,
                           Bdd_Edge a2, Bdd_Edge s2);

EXTERN Bdd_Edge Mc_CheckEX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckAX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckHME(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a,
                            Bdd_Edge s2);

EXTERN Bdd_Edge Mc_CheckHMA(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckEF(Bdd_Edge D, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckAF(Bdd_Edge D, Bdd_Edge s);

EXTERN Bdd_Edge Mc_CheckEG(Bdd_Edge D, Bdd_Edge a);

EXTERN Bdd_Edge Mc_CheckAG(Bdd_Edge D, Bdd_Edge a);

EXTERN void Mc_InevitableCheckEEU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
				  Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckAAU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge *f1, Bdd_Edge *f1x,
                                  Bdd_Edge *f2, Bdd_Edge *f2x,
                                  Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
				  Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckEEW(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge *f1, Bdd_Edge *f1x,
                                  Bdd_Edge *f2, Bdd_Edge *f2x,
                                  Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
				  Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckAAW(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
				  Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckEEX(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAAX(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckEEF(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckEEG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAAF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAAG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckEU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
                                 Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a1,
				 Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckAU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
                                 Bdd_Edge *f2, Bdd_Edge *f2x,
                                 Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a1,
				 Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckEX(int cn, Bdd_Edge *f, Bdd_Edge *fx,
				 Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAX(int cn, Bdd_Edge *f, Bdd_Edge *fx,
				 Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckHME(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge *f1, Bdd_Edge *f1x,
                                  Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a,
				  Bdd_Edge s2, Bdd_Edge s2x);

EXTERN void Mc_InevitableCheckHMA(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                  Bdd_Edge *f1, Bdd_Edge *f1x,
				  Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckEF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
				 Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckEG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
				 Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
				 Bdd_Edge s, Bdd_Edge sx);

EXTERN void Mc_InevitableCheckAG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                                 Bdd_Edge *f1, Bdd_Edge *f1x,
				 Bdd_Edge s, Bdd_Edge sx);

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

#endif  /* _MC */
