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

  FileName    [mcInt.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 mcInt.h contains declaration of internal
               data structures neded for ACTL model checking.]
  SeeAlso     [mc.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 _MCINT
#define _MCINT

#include "mc.h"

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

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

#ifdef USE_VERSIS_STUBS
#  include <versisDecls.h>
#endif

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

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

/* CONSTANT */
#define MC_CONST 0

/* ACTL OPERATORS */
#define MC_EU 1
#define MC_AU 2
#define MC_EX 3
#define MC_AX 4
#define MC_HME 5
#define MC_HMA 6
#define MC_EF 7
#define MC_AF 8
#define MC_EG 9
#define MC_AG 10

/* STRICT ACTL-W OPERATORS */
#define MC_EEU 11
#define MC_AAU 12
#define MC_EEW 13
#define MC_AAW 14
#define MC_EEX 15
#define MC_AAX 16
#define MC_EEF 17
#define MC_AAF 18
#define MC_EEG 19
#define MC_AAG 20

/* NON-STRICT ACTL-W OPERATORS */
#define MC_EEU_NS 21
#define MC_AAU_NS 22
#define MC_EEW_NS 23
#define MC_AAW_NS 24
#define MC_EEG_NS 25
#define MC_AAG_NS 26

/* BOOLEAN OPERATORS */
#define MC_NOT 27
#define MC_AND 28
#define MC_OR 29
#define MC_EQV 30
#define MC_IMPL 31

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

typedef struct {
  int num;
  int *tableT;
  int *tableS;
} McTypeR;

typedef struct McFunctionSequence {
  Bdd_Edge f;       /* r1 for first item, -- a --> r2  for others */
  struct McFunctionSequence *nextFunction;
  struct McFunctionSequence *prevFunction;
} McFunctionSequence;

typedef struct McDiagnosticItem {
   int num;                 /* label */
   Est_Boolean ready;       /* is diagnostic ready for printing? */
   Bdd_Edge state1;         /* state, where ACTL formula is checking */
   Bdd_Edge state2;         /* optionally, where to continue */
   Bdd_Edge lastaction;     /* optionally, last action on the path */
   Bdd_Edge act1;
   Bdd_Edge form1;
   Bdd_Edge act2;
   Bdd_Edge form2;
   int type;                    /* EU, EW, AU, AW, ... */
   Est_Boolean r;               /* ACTL formula valid or not valid */
   Bdd_Edge global;             /* the set of all states, where formula is valid */
   Est_String s;                /* input string */
   Est_String sx;               /* extended input string */
   McFunctionSequence *path;    /* witness or counterexample */
   McTypeR R;                   /* R is used for WCA generation */
   struct McDiagnosticItem *nextPrefix;
   struct McDiagnosticItem *nextFormula;
} McDiagnosticItem;

typedef struct {
  int proc;                 /* process or ... */
  int comp;                 /* ... composition */
  Bdd_Edge D;               /* transition relation */
  Bdd_Edge init;            /* initial state */
  McDiagnosticItem *item;   /* root of subformula items */
  Bdd_Edge automaton; /* w/c automaton - only experimental, maybe move to McDiagnosticItem*/
  Bdd_Edge tree;      /* diagnostic tree - only experimental, maybe move to McDiagnosticItem*/
} McDiagnosticType;

typedef struct McInevitableItem {
   Bdd_Edge inevitableT;  /* the set of states, where formula is inevitable valid */
   Bdd_Edge inevitableF;  /* the set of states, where formula is inevitable invalid */
   Bdd_Edge inevitableT1;  /* the set of states, where subformula is inevitable valid */
   Bdd_Edge inevitableF1;  /* the set of states, where subformula is inevitable invalid */
   Bdd_Edge inevitableT2;  /* the set of states, where subformula is inevitable valid */
   Bdd_Edge inevitableF2;  /* the set of states, where subformula is inevitable invalid */
   Est_String s;          /* input string */
   Est_String sx;         /* extended input string */
   struct McInevitableItem *next;
} McInevitableItem;

typedef struct {
   Est_String name;         /* the name of macro*/
   Est_String body;         /* the body of macro */
} McMacro;

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

extern Est_Boolean trace;          /* trace of ACTL parsing */
extern Est_Boolean xtrace;         /* extended trace of ACTL parsing */
extern Est_Boolean explain;        /* explain generated diagnostic */
extern Est_Boolean tracepath;      /* full paths in diagnostic */
extern Est_Boolean diagnostic;     /* generate linear w/c */
extern Est_Boolean automaton;      /* generate w/c automaton */
extern Est_Boolean minimize;       /* minimize w/c automaton */
extern Est_Boolean tree;           /* generate tree-like w/c */
extern Est_Boolean progress ;      /* report progress of MC */

extern Bdd_Edge McTau;             /* McTau is defined in Mc_CheckACTL */
extern McDiagnosticType McDgn;     /* McDgn is defined in Mc_CheckACTL */

extern int mcMacros;               /* number of macros */
extern McMacro *mcMacroTable;      /* table of macros */

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

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

/* THIS IS FROM THE NET, THANKS TO PETE BATARD */
/* http://lists.gnu.org/archive/html/libcdio-devel/2012-01/msg00004.html */

#ifdef ESTWIN32
static inline char *strndup(const char *s, size_t n)
{
    char *result;
    size_t len = strlen (s);
    if (n < len) len = n;
    result = (char *) malloc (len + 1);
    if (!result) return 0;
    result[len] = '\0';
    return (char *) strncpy (result, s, len);
}
#endif

/*-----------------------------------------------------------------------*/
/* FUNCTIONS FROM mcMain.c                                               */
/*-----------------------------------------------------------------------*/

extern void McAddMacro(Est_String name, Est_String body);

extern int McFindMacro(Est_String name);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS FROM mcThread.c                                             */
/*-----------------------------------------------------------------------*/

extern void Mc_CheckACTL_Thr(int par, Est_String name, Est_String f,
                             int parserSettings);

extern void Mc_CheckACTLString_Thr(int par, Est_String name, Est_String f,
                             int parserSettings);

extern void Mc_CheckACTLFile_Thr(int par, Est_String name, Est_String f,
                         int parserSettings);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS FROM mcDiagnostic.c                                         */
/*-----------------------------------------------------------------------*/

extern McDiagnosticType McCreateDiagnostic(Bdd_Edge D, Bdd_Edge init,
                            int proc, int comp);

extern void McAddDiagnostic(McDiagnosticItem **item, Bdd_Edge result,
                            Bdd_Edge act1, Bdd_Edge form1,
                            Bdd_Edge act2, Bdd_Edge form2, int type,
                            Est_String s, Est_String sx,
                            McDiagnosticItem *itemPrefix,
                            McDiagnosticItem *itemFormula);

extern void McPrepareDiagnostic(McDiagnosticType dgn,
                                Bdd_Edge D, McDiagnosticItem **item,
                                Bdd_Edge init, Est_Boolean first);

extern void McPrintDiagnostic(McDiagnosticType dgn,
              McDiagnosticItem *item, int indent, Est_String *path,
              Est_String *spntrl, Est_String *msc, Est_Boolean write,
              Est_Boolean tracepath);

extern void McDeleteDiagnostic(McDiagnosticItem *item);

extern void McDeleteFunctionSequence(McFunctionSequence *path);

extern McInevitableItem * McAddEmptyInevitable(Est_String s, Est_String sx);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS FROM mcTree.c                                               */
/*-----------------------------------------------------------------------*/

extern Bdd_Edge McTreeEEU(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
			    Bdd_Edge s2, Bdd_Edge valid);

extern Bdd_Edge McTreeAAU(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
			 Bdd_Edge s2, Bdd_Edge formAW, Bdd_Edge formAF);

extern Bdd_Edge McTreeEEW(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
                          Bdd_Edge s2, Bdd_Edge formEU, Bdd_Edge formEG);

extern Bdd_Edge McTreeAAW(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
                             Bdd_Edge s2, Bdd_Edge valid);

extern Bdd_Edge McTreeEEX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAAX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeEEF(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAAF(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeEEG(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAAG(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeEU(Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2,
                         Bdd_Edge s2, Bdd_Edge valid);

extern Bdd_Edge McTreeEX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeEF(Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeEG(Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAU(Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2,
                         Bdd_Edge s2, Bdd_Edge valid);

extern Bdd_Edge McTreeAX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAF(Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeAG(Bdd_Edge s, Bdd_Edge valid);

extern Bdd_Edge McTreeHME(Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2,
                          Bdd_Edge valid);

extern Bdd_Edge McTreeHMA(Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2,
                          Bdd_Edge valid);

/*-----------------------------------------------------------------------*/
/* FUNCTIONS FROM mcAutomata.c                                           */
/*-----------------------------------------------------------------------*/

extern int WCAgenerator(Est_String LTSname, Est_String WCAname,
       McDiagnosticItem *item, int explain);

extern Est_Boolean WCAgen(int LTS, int WCA, McDiagnosticItem *item,
       int s, int t, Est_Boolean WCAtype, int explain);

extern Est_Boolean WAbuild(int LTS, int WCA, McDiagnosticItem *item,
       int s, int t, Bdd_Edge chi1, Bdd_Edge phi1, Bdd_Edge chi2,
       Bdd_Edge phi2, Est_Boolean WCAtype, int explain);

extern Est_Boolean CAbuild(int LTS, int WCA, McDiagnosticItem *item,
       int s, int t, Bdd_Edge chi1, Bdd_Edge phi1, Bdd_Edge chi2,
       Bdd_Edge phi2, Est_Boolean WCAtype, int explain);

extern Est_Boolean conbuild(int LTS, int WCA, McDiagnosticItem *item,
       int act, int type, int sprime, int t, Est_Boolean WCAtype,
       int explain);

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

#endif  /* _MCINT */

