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

  FileName    [mcDecls.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 [Generated by genStubs.tcl, see http://wiki.tcl.tk/3358]
  SeeAlso     [mc.h, mc.decls, mcStubInit.c, mcStubLib.c]

  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.]
  ************************************************************************/

/* !BEGIN!: Do not edit below this line. */

/*
 * Exported function declarations: implemented in mc.h
 */

typedef struct McStubs {
    int magic;
    const struct McStubHooks *hooks;

    int *mc_status; /* 0 */
    int *mc_formulae; /* 1 */
    Mc_Formula * *mc_formulaTable; /* 2 */
    const int *mC_SIMPLE; /* 3 */
    const int *mC_TRACE; /* 4 */
    const int *mC_XTRACE; /* 5 */
    const int *mC_EXPLAIN; /* 6 */
    const int *mC_TRACEPATH; /* 7 */
    const int *mC_DIAGNOSTIC; /* 8 */
    const int *mC_AUTOMATON; /* 9 */
    const int *mC_MINIMIZE; /* 10 */
    const int *mC_TREE; /* 11 */
    const int *mC_PROGRESS; /* 12 */
    void (*mc_InitPkg) (); /* 13 */
    void (*mc_ExitPkg) (); /* 14 */
    void (*mc_AboutPkg) (); /* 15 */
    int (*mc_AddNewFormula) (Est_String name, Est_String formula); /* 16 */
    int (*mc_FOANextFormula) (Est_String f, Est_String prefix); /* 17 */
    int (*mc_FindFormula) (Est_String name); /* 18 */
    void (*mc_WriteKnownFormulae) (); /* 19 */
    void (*mc_WriteFormula) (Est_String ime, char type); /* 20 */
    void (*mc_CheckACTL) (int par, Est_String name, Est_String f, int parserSettings); /* 21 */
    void (*mc_CheckACTLString) (int par, Est_String name, Est_String f, int parserSettings); /* 22 */
    void (*mc_CheckACTLFile) (int par, Est_String name, Est_String f, int parserSettings); /* 23 */
    void (*mc_GenerateWCA) (Est_String name, Est_String f, Est_String aname); /* 24 */
    void (*mc_ReadACTL) (Est_String name, Est_String f); /* 25 */
    void (*mc_ReadACTLFile) (Est_String f); /* 26 */
    Bdd_Edge (*mc_CheckEEU) (Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2); /* 27 */
    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); /* 28 */
    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); /* 29 */
    Bdd_Edge (*mc_CheckAAW) (Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2); /* 30 */
    Bdd_Edge (*mc_CheckEEX) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 31 */
    Bdd_Edge (*mc_CheckAAX) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 32 */
    Bdd_Edge (*mc_CheckEEF) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 33 */
    Bdd_Edge (*mc_CheckAAF) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 34 */
    Bdd_Edge (*mc_CheckEEG) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 35 */
    Bdd_Edge (*mc_CheckAAG) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 36 */
    Bdd_Edge (*mc_CheckEU) (Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2, Bdd_Edge s2); /* 37 */
    Bdd_Edge (*mc_CheckAU) (Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2, Bdd_Edge s2); /* 38 */
    Bdd_Edge (*mc_CheckEX) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 39 */
    Bdd_Edge (*mc_CheckAX) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 40 */
    Bdd_Edge (*mc_CheckHME) (Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2); /* 41 */
    Bdd_Edge (*mc_CheckHMA) (Bdd_Edge D, Bdd_Edge a, Bdd_Edge s); /* 42 */
    Bdd_Edge (*mc_CheckEF) (Bdd_Edge D, Bdd_Edge s); /* 43 */
    Bdd_Edge (*mc_CheckAF) (Bdd_Edge D, Bdd_Edge s); /* 44 */
    Bdd_Edge (*mc_CheckEG) (Bdd_Edge D, Bdd_Edge a); /* 45 */
    Bdd_Edge (*mc_CheckAG) (Bdd_Edge D, Bdd_Edge a); /* 46 */
    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); /* 47 */
    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); /* 48 */
    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); /* 49 */
    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); /* 50 */
    void (*mc_InevitableCheckEEX) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 51 */
    void (*mc_InevitableCheckAAX) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 52 */
    void (*mc_InevitableCheckEEF) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 53 */
    void (*mc_InevitableCheckEEG) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 54 */
    void (*mc_InevitableCheckAAF) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 55 */
    void (*mc_InevitableCheckAAG) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 56 */
    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); /* 57 */
    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); /* 58 */
    void (*mc_InevitableCheckEX) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 59 */
    void (*mc_InevitableCheckAX) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx); /* 60 */
    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); /* 61 */
    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); /* 62 */
    void (*mc_InevitableCheckEF) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge *f1, Bdd_Edge *f1x, Bdd_Edge s, Bdd_Edge sx); /* 63 */
    void (*mc_InevitableCheckEG) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge *f1, Bdd_Edge *f1x, Bdd_Edge s, Bdd_Edge sx); /* 64 */
    void (*mc_InevitableCheckAF) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge *f1, Bdd_Edge *f1x, Bdd_Edge s, Bdd_Edge sx); /* 65 */
    void (*mc_InevitableCheckAG) (int cn, Bdd_Edge *f, Bdd_Edge *fx, Bdd_Edge *f1, Bdd_Edge *f1x, Bdd_Edge s, Bdd_Edge sx); /* 66 */
} McStubs;

#ifdef __cplusplus
extern "C" {
#endif
extern const McStubs *mcStubsPtr;
#ifdef __cplusplus
}
#endif

#if defined(USE_MC_STUBS)

/*
 * Inline function declarations:
 */

#define mc_status \
	(*mcStubsPtr->mc_status) /* 0 */
#define mc_formulae \
	(*mcStubsPtr->mc_formulae) /* 1 */
#define mc_formulaTable \
	(*mcStubsPtr->mc_formulaTable) /* 2 */
#define MC_SIMPLE \
	(*mcStubsPtr->mC_SIMPLE) /* 3 */
#define MC_TRACE \
	(*mcStubsPtr->mC_TRACE) /* 4 */
#define MC_XTRACE \
	(*mcStubsPtr->mC_XTRACE) /* 5 */
#define MC_EXPLAIN \
	(*mcStubsPtr->mC_EXPLAIN) /* 6 */
#define MC_TRACEPATH \
	(*mcStubsPtr->mC_TRACEPATH) /* 7 */
#define MC_DIAGNOSTIC \
	(*mcStubsPtr->mC_DIAGNOSTIC) /* 8 */
#define MC_AUTOMATON \
	(*mcStubsPtr->mC_AUTOMATON) /* 9 */
#define MC_MINIMIZE \
	(*mcStubsPtr->mC_MINIMIZE) /* 10 */
#define MC_TREE \
	(*mcStubsPtr->mC_TREE) /* 11 */
#define MC_PROGRESS \
	(*mcStubsPtr->mC_PROGRESS) /* 12 */
#define Mc_InitPkg \
	(mcStubsPtr->mc_InitPkg) /* 13 */
#define Mc_ExitPkg \
	(mcStubsPtr->mc_ExitPkg) /* 14 */
#define Mc_AboutPkg \
	(mcStubsPtr->mc_AboutPkg) /* 15 */
#define Mc_AddNewFormula \
	(mcStubsPtr->mc_AddNewFormula) /* 16 */
#define Mc_FOANextFormula \
	(mcStubsPtr->mc_FOANextFormula) /* 17 */
#define Mc_FindFormula \
	(mcStubsPtr->mc_FindFormula) /* 18 */
#define Mc_WriteKnownFormulae \
	(mcStubsPtr->mc_WriteKnownFormulae) /* 19 */
#define Mc_WriteFormula \
	(mcStubsPtr->mc_WriteFormula) /* 20 */
#define Mc_CheckACTL \
	(mcStubsPtr->mc_CheckACTL) /* 21 */
#define Mc_CheckACTLString \
	(mcStubsPtr->mc_CheckACTLString) /* 22 */
#define Mc_CheckACTLFile \
	(mcStubsPtr->mc_CheckACTLFile) /* 23 */
#define Mc_GenerateWCA \
	(mcStubsPtr->mc_GenerateWCA) /* 24 */
#define Mc_ReadACTL \
	(mcStubsPtr->mc_ReadACTL) /* 25 */
#define Mc_ReadACTLFile \
	(mcStubsPtr->mc_ReadACTLFile) /* 26 */
#define Mc_CheckEEU \
	(mcStubsPtr->mc_CheckEEU) /* 27 */
#define Mc_CheckAAU \
	(mcStubsPtr->mc_CheckAAU) /* 28 */
#define Mc_CheckEEW \
	(mcStubsPtr->mc_CheckEEW) /* 29 */
#define Mc_CheckAAW \
	(mcStubsPtr->mc_CheckAAW) /* 30 */
#define Mc_CheckEEX \
	(mcStubsPtr->mc_CheckEEX) /* 31 */
#define Mc_CheckAAX \
	(mcStubsPtr->mc_CheckAAX) /* 32 */
#define Mc_CheckEEF \
	(mcStubsPtr->mc_CheckEEF) /* 33 */
#define Mc_CheckAAF \
	(mcStubsPtr->mc_CheckAAF) /* 34 */
#define Mc_CheckEEG \
	(mcStubsPtr->mc_CheckEEG) /* 35 */
#define Mc_CheckAAG \
	(mcStubsPtr->mc_CheckAAG) /* 36 */
#define Mc_CheckEU \
	(mcStubsPtr->mc_CheckEU) /* 37 */
#define Mc_CheckAU \
	(mcStubsPtr->mc_CheckAU) /* 38 */
#define Mc_CheckEX \
	(mcStubsPtr->mc_CheckEX) /* 39 */
#define Mc_CheckAX \
	(mcStubsPtr->mc_CheckAX) /* 40 */
#define Mc_CheckHME \
	(mcStubsPtr->mc_CheckHME) /* 41 */
#define Mc_CheckHMA \
	(mcStubsPtr->mc_CheckHMA) /* 42 */
#define Mc_CheckEF \
	(mcStubsPtr->mc_CheckEF) /* 43 */
#define Mc_CheckAF \
	(mcStubsPtr->mc_CheckAF) /* 44 */
#define Mc_CheckEG \
	(mcStubsPtr->mc_CheckEG) /* 45 */
#define Mc_CheckAG \
	(mcStubsPtr->mc_CheckAG) /* 46 */
#define Mc_InevitableCheckEEU \
	(mcStubsPtr->mc_InevitableCheckEEU) /* 47 */
#define Mc_InevitableCheckAAU \
	(mcStubsPtr->mc_InevitableCheckAAU) /* 48 */
#define Mc_InevitableCheckEEW \
	(mcStubsPtr->mc_InevitableCheckEEW) /* 49 */
#define Mc_InevitableCheckAAW \
	(mcStubsPtr->mc_InevitableCheckAAW) /* 50 */
#define Mc_InevitableCheckEEX \
	(mcStubsPtr->mc_InevitableCheckEEX) /* 51 */
#define Mc_InevitableCheckAAX \
	(mcStubsPtr->mc_InevitableCheckAAX) /* 52 */
#define Mc_InevitableCheckEEF \
	(mcStubsPtr->mc_InevitableCheckEEF) /* 53 */
#define Mc_InevitableCheckEEG \
	(mcStubsPtr->mc_InevitableCheckEEG) /* 54 */
#define Mc_InevitableCheckAAF \
	(mcStubsPtr->mc_InevitableCheckAAF) /* 55 */
#define Mc_InevitableCheckAAG \
	(mcStubsPtr->mc_InevitableCheckAAG) /* 56 */
#define Mc_InevitableCheckEU \
	(mcStubsPtr->mc_InevitableCheckEU) /* 57 */
#define Mc_InevitableCheckAU \
	(mcStubsPtr->mc_InevitableCheckAU) /* 58 */
#define Mc_InevitableCheckEX \
	(mcStubsPtr->mc_InevitableCheckEX) /* 59 */
#define Mc_InevitableCheckAX \
	(mcStubsPtr->mc_InevitableCheckAX) /* 60 */
#define Mc_InevitableCheckHME \
	(mcStubsPtr->mc_InevitableCheckHME) /* 61 */
#define Mc_InevitableCheckHMA \
	(mcStubsPtr->mc_InevitableCheckHMA) /* 62 */
#define Mc_InevitableCheckEF \
	(mcStubsPtr->mc_InevitableCheckEF) /* 63 */
#define Mc_InevitableCheckEG \
	(mcStubsPtr->mc_InevitableCheckEG) /* 64 */
#define Mc_InevitableCheckAF \
	(mcStubsPtr->mc_InevitableCheckAF) /* 65 */
#define Mc_InevitableCheckAG \
	(mcStubsPtr->mc_InevitableCheckAG) /* 66 */

#endif /* defined(USE_MC_STUBS) */

/* !END!: Do not edit above this line. */
