/**CHeaderFile***************************************************************** FileName [ltlInt.h] PackageName [ltl] Synopsis [Internal declarations.] Author [Chao Wang] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id: ltlInt.h,v 1.26 2008/04/22 21:21:45 fabio Exp $] ******************************************************************************/ #ifndef _LTLINT #define _LTLINT /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "io.h" #include "ltl.h" #include "cmd.h" #include "ctlsp.h" #include "fsm.h" #include "ntk.h" #include "ord.h" #include "part.h" #include "mc.h" #include /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ typedef struct LtlMcOption LtlMcOption_t; typedef struct LtlTableauEntry LtlTableauEntry_t; typedef struct LtlTableauStruct LtlTableau_t; typedef struct LtlSetStruct LtlSet_t; typedef struct LtlPairStruct LtlPair_t; /**Enum************************************************************************ Synopsis [Level to which debugging of CTL formulae is performed.] ******************************************************************************/ typedef enum { LtlMcDbgLevelNone_c, LtlMcDbgLevelMin_c, LtlMcDbgLevelMinVerbose_c, LtlMcDbgLevelMax_c, LtlMcDbgLevelInteractive_c } LtlMcDbgLevel; /**Enum************************************************************************ Synopsis [Automaton->File Formats.] Description [] ******************************************************************************/ typedef enum { Aut2File_DOT_c, Aut2File_BLIFMV_c, Aut2File_VERILOG_c, Aut2File_ALL_c }Aut2FileType; /**Enum************************************************************************ Synopsis [LTL->Automaton Translation Algorithm.] Description [] ******************************************************************************/ typedef enum { Ltl2Aut_GPVW_c, Ltl2Aut_GPVWplus_c, Ltl2Aut_LTL2AUT_c, Ltl2Aut_WRING_c } Ltl2AutAlgorithm; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [A struct for keeping the command line options.] ******************************************************************************/ struct LtlMcOption { boolean printInputs; FILE *ltlFile; /* contains the ltl formulae */ FILE *debugFile; boolean useMore; /* use more as pipe for debug output */ boolean simValue; Mc_LeMethod_t leMethod; Mc_DcLevel dcLevel; LtlMcDbgLevel dbgLevel; Mc_GSHScheduleType schedule; Mc_FwdBwdAnalysis direction; int lockstep; Mc_VerbosityLevel verbosity; int timeOutPeriod; Ltl2AutAlgorithm algorithm; /* GPVW/GPVW+/LTL2AUT/WRING */ boolean booleanmin; /* use boolean minimization to simplify cover */ boolean rewriting; /* rewriting the fomula */ boolean prunefair; /* prune the fairness */ boolean iocompatible; /* minimization by io-compatible */ boolean directsim; /* minimization by direct simulation rln */ boolean reversesim; /* minimization by reverse simulation rln */ boolean directsimMaximize; /* adding arcs by direct simulation rln */ int noIncrementalPartition; /* ? build the parition of MxA incrementally */ int noStrengthReduction; /* ? use different decision procedures */ /* for different automaton strength */ int noShuffleToTop; /* ? shuffle automaton vars to the top */ Aut2FileType outputformat; /* write blifmv/verilog/smv/dot file as output */ char *outputfilename; }; /**Struct********************************************************************** Synopsis [A struct for holding the Tableau Rule Expansition of 1 Formula.] ******************************************************************************/ struct LtlTableauEntry { Ctlsp_Formula_t *F; /* the formula */ struct alpha { /* alpha[0].beta[0]*alpha[0].beta[1] + */ int B[2]; /* alpha[1].beta[0]*alpha[1].beta[1] */ int n; } A[2]; int notF_idx; /* negation of 'f' */ Ctlsp_Formula_t *notF; }; /**Struct********************************************************************** Synopsis [A struct for holding the Tableau Rule Expansition of All the sub-Formulae of the given LTL Formula F and its negation.] ******************************************************************************/ struct LtlTableauStruct { Ctlsp_Formula_t *F; /* Formula in NNF */ Ctlsp_Formula_t *notF; /* & its negation */ st_table *formulaUniqueTable; st_table *untilUniqueTable; int abIndex; /* Alpha_Beta_Table */ LtlTableauEntry_t *abTable; array_t *abTableNegate; /* provide Negate method, for set operation */ int labelIndex; /* label table: (ID/TRUE/FALSE) */ Ctlsp_Formula_t **labelTable; array_t *labelTableNegate; /*provide Negate method, for set operation */ int algorithm; /* algorithm GPVW/GPVW+/LTL2AUT/WRING */ int booleanmin; /* switch: for boolean minimization */ int verbosity; }; /**Struct********************************************************************** Synopsis [A struct for holding a set, in which each index corresponds to an elementary formula.] ******************************************************************************/ struct LtlSetStruct { var_set_t *e; }; /**Struct********************************************************************** Synopsis [The Buechi Automaton / Quotient Graph struct.] ******************************************************************************/ struct LtlAutomatonStruct { LtlTableau_t *tableau; /* , the tableau */ Ltl_Automaton_t *Q; /* , Quotion graph */ st_table *SCC; /* , SCC partitions */ int isQuotientGraph; /* in automaton graph, Q->SCC is (component, 0) */ /* in quotient graph, Q->SCC is a mapping (component, Q_vtx) */ /*--below are required fields-------------------------------------------*/ char *name; graph_t *G; st_table *Init; /* initial states (vertices) */ st_table *dontcare; /* these state can be in/out FairSets*/ lsList Fair; /* list of sets (hash tables) */ array_t *labelTable; /* unique table for propositionals (labels), 'node->Labes' is a var_set_t refer to it. Initially it's a Clone of 'tableau->labelTable', from which it shares nothing in common */ array_t *labelTableNegate; /* provide Negate method for each label item */ int node_idx; /* auxilary counter in creating nodes */ bdd_t *transitionRelation; /* Holds the bdd of the translation relation */ bdd_t *initialStates; /* Holds the bdd of the initial states */ bdd_t *fairSets; /* Holds the bdd of the fair states */ array_t *fairSetArray; /* Holda bdd of all fair sets.*/ st_table *psNsTable; /* Maps present state to next state*/ st_table *nsPsTable; /* Maps next state to present state*/ }; /**Struct********************************************************************** Synopsis [The struct for a node in the Buechi Automaton / Quotient graph. It's attached to each vertex (vertex->user_data).] ******************************************************************************/ struct LtlAutomatonNodeStruct { int index; LtlSet_t *Labels; /* a list of constant formulae, state labels */ LtlSet_t *CoverSet; /* */ st_table *Class; mdd_t *Encode; /* Encode the state of automaton */ int *cnfIndex; }; /**Struct********************************************************************** Synopsis [The struct for holding a Generic Pair (ordered).] ******************************************************************************/ struct LtlPairStruct { char *First; char *Second; }; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN Ltl_Automaton_t * LtlMcFormulaToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *Formula, LtlMcOption_t *options, int checkSemantics); EXTERN void LtlFsmLoadFairness(Fsm_Fsm_t *compFsm, Fsm_Fairness_t *designFairness, int NumberOfFairSets, int *AutomatonStrength); EXTERN LtlMcOption_t * LtlMcOptionAlloc(void); EXTERN void LtlMcOptionFree(LtlMcOption_t *result); EXTERN Ltl_Automaton_t * LtlAutomatonGeneration(LtlTableau_t *tableau); EXTERN int LtlAutomatonSetIsFair(LtlTableau_t *tableau, LtlSet_t *r); EXTERN LtlSet_t * LtlAutomatonVertexGetLabels(vertex_t *vtx); EXTERN LtlSet_t * LtlSetNew(int size); EXTERN void LtlSetFree(LtlSet_t *set); EXTERN LtlSet_t * LtlSetCopy(LtlSet_t *from); EXTERN void LtlSetAssign(LtlSet_t *to, LtlSet_t *from); EXTERN int LtlSetEqual(LtlSet_t *s1, LtlSet_t *s2); EXTERN int LtlSetCardinality(LtlSet_t *set); EXTERN int LtlSetCompareCardinality(const void *p1, const void *p2); EXTERN int LtlSetIsContradictory(LtlSet_t *set, array_t *Negate); EXTERN int LtlSetInclude(LtlSet_t *large, LtlSet_t *small); EXTERN void LtlSetOR(LtlSet_t *to, LtlSet_t *from1, LtlSet_t *from2); EXTERN void LtlSetClear(LtlSet_t *set); EXTERN void LtlSetSetElt(LtlSet_t *set, int index); EXTERN void LtlSetClearElt(LtlSet_t *set, int index); EXTERN int LtlSetGetElt(LtlSet_t *set, int index); EXTERN int LtlSetIsEmpty(LtlSet_t *set); EXTERN LtlSet_t * LtlSetIsInList(LtlSet_t *set, lsList list); EXTERN LtlSet_t * LtlSetToLabelSet(LtlTableau_t *tableau, LtlSet_t *set); EXTERN void LtlSetPrint(LtlTableau_t *tableau, LtlSet_t *set); EXTERN void LtlSetPrintIndex(int length, LtlSet_t *set); EXTERN LtlPair_t * LtlPairNew(char *First, char *Second); EXTERN void LtlPairFree(LtlPair_t *pair); EXTERN int LtlPairHash(char *key, int modulus); EXTERN int LtlPairCompare(const char *key1, const char *key2); EXTERN void LtlPairPrint(LtlPair_t *pair); EXTERN void LtlCoverPrintIndex(int length, lsList cover); EXTERN lsList LtlCoverCompleteSum(lsList Cover, array_t *Negate); EXTERN LtlSet_t * LtlSetConsensus(LtlSet_t *first, LtlSet_t *second, array_t *Negate); EXTERN lsList LtlCoverCofactor(lsList Cover, LtlSet_t *c, array_t *Negate); EXTERN int LtlCoverIsTautology(lsList Cover, array_t *Negate); EXTERN int LtlCoverIsImpliedBy(lsList Cover, LtlSet_t *term, array_t *Negate); EXTERN lsList LtlCoverPrimeAndIrredundant(LtlTableau_t *tableau, lsList Cover, array_t *Negate); EXTERN LtlSet_t * LtlCoverGetSuperCube(lsList Cover, array_t *Negate); EXTERN mdd_t * LtlSetModelCheckFormulae(LtlSet_t *set, array_t *labelTable, Fsm_Fsm_t *fsm); EXTERN LtlTableau_t * LtlTableauGenerateTableau(Ctlsp_Formula_t *formula); EXTERN LtlTableau_t * LtlTableauCreate(void); EXTERN void LtlTableauFree(LtlTableau_t *tableau); EXTERN void LtlTableauPrint(FILE *fp, LtlTableau_t *tableau); EXTERN Ctlsp_Formula_t * LtlTableauGetUniqueXFormula(LtlTableau_t *tableau, Ctlsp_Formula_t *F); /**AutomaticEnd***************************************************************/ #endif /* _LTLINT */