/**CHeaderFile***************************************************************** FileName [mc.h] PackageName [mc] Synopsis [Fair CTL model checker and debugger.] Description [Fair CTL model checker and debugger. Works on a flattened network.] Author [Adnan Aziz, Tom Shiple, In-Ho Moon] Comment [] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] Revision [$Id: mc.h,v 1.54 2007/04/17 00:01:22 sohail Exp $] ******************************************************************************/ #ifndef _MC #define _MC /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "cmd.h" #include "ctlp.h" #include "ctlsp.h" #include "ntk.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /* Use this if you don't want early termination */ #define MC_NO_EARLY_TERMINATION (NIL(Mc_EarlyTermination_t)) /* Constants for lockstep mode. */ #define MC_LOCKSTEP_UNASSIGNED -3 #define MC_LOCKSTEP_OFF -2 #define MC_LOCKSTEP_EARLY_TERMINATION -1 #define MC_LOCKSTEP_ALL_SCCS 0 /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Enum************************************************************************ Synopsis [Use forward or backward analysis] ******************************************************************************/ typedef enum { McFwd_c, McBwd_c /* someday there may be a mixed method */ } Mc_FwdBwdAnalysis; /**Enum************************************************************************ Synopsis [Extent to which Mc functions provide feedback/stats.] ******************************************************************************/ typedef enum { McVerbosityNone_c, McVerbosityLittle_c, McVerbositySome_c, McVerbosityMax_c } Mc_VerbosityLevel; /**Enum************************************************************************ Synopsis [Extent to which don't cares are used in Mc functions.] ******************************************************************************/ typedef enum { McDcLevelNone_c, McDcLevelRch_c, McDcLevelRchFrontier_c, McDcLevelArdc_c } Mc_DcLevel; /**Enum************************************************************************ Synopsis [When creating a path from aState to bState, make it non trivial (ie a cycle) when aState == bState and McPathLengthType is McGreaterZero_c.] ******************************************************************************/ typedef enum { McGreaterZero_c, McGreaterOrEqualZero_c } Mc_PathLengthType; /**Enum************************************************************************ Synopsis [Some,all or care, for Mc_EarlyTermination_t] ******************************************************************************/ typedef enum { McSome_c, McAll_c, McCare_c } Mc_EarlyTerminationType; /**Enum************************************************************************ Synopsis [What kind of hints?] Description [Would you like that with no hints, global hints or local hints? Paper or plastic?] SideEffects [] SeeAlso [] ******************************************************************************/ typedef enum { Mc_None_c, Mc_Global_c, Mc_Local_c } Mc_GuidedSearch_t; /**Enum************************************************************************ Synopsis [Specifies the method for language emptiness checking] Description [Specifies the method used by command ltl and le for checking the language emptiness.] SideEffects [] SeeAlso [] ******************************************************************************/ typedef enum { Mc_Le_Default_c, Mc_Le_Dnc_c } Mc_LeMethod_t; /**Enum************************************************************************ Synopsis [Specifies the automaton strength] Description [Specifies the automaton strength] SideEffects [] SeeAlso [] ******************************************************************************/ typedef enum { Mc_Aut_Terminal_c, Mc_Aut_Weak_c, Mc_Aut_Strong_c } Mc_AutStrength_t; /**Enum************************************************************************ Synopsis [Type of GSH schedule.] Description [The GSH schedule is the policy followed by the GSH algorithm in applying the EU and EX operators. If there are n fairness constraints, the operators are EU1,...,EUn,EX. Currently, three schedules are supported: EL, EL1, EL2, budget, and random. ] ******************************************************************************/ typedef enum { McGSH_old_c, /* do not use GSH */ McGSH_EL_c, /* Emerson-Lei schedule */ McGSH_EL1_c, /* modified Emerson-Lei schedule */ McGSH_EL2_c, /* Hojati's EL2 schedule (a.k.a. OWCTY) */ McGSH_Budget_c, /* EL2 with EX budget */ McGSH_Random_c, /* Random schedule */ McGSH_Unassigned_c /* invalid schedule */ } Mc_GSHScheduleType; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*----------------------------------------------------------------------------- Synopsis [The type of the onion rings] Description [Onion rings are arrays of mdd_t*s, decribes in onionRings.c] -----------------------------------------------------------------------------*/ typedef array_t OnionRing_t; typedef struct McEarlyTerminationStruct Mc_EarlyTermination_t; typedef struct McSccGenStruct Mc_SccGen_t; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Iterates over the fair SCCs of a FSM.] Description [Iterates over the fair SCCs of a FSM. The parameters are: Mc_FsmForEachFairScc allocates and frees the generator. Therefore the application should not try to do that unless it breaks out of the loop, in which case it must call Mc_FsmSccGenFree explicitly. If earlyTermination is TRUE, at most one fair SCC is enumerated. Setting earlyTermination to TRUE differs from breaking out of hte loop after the first fair SCC is enumerated in three respects. ] SideEffects [none] SeeAlso [Mc_FsmFirstScc Mc_FsmNextScc Mc_FsmIsSccGenEmpty Mc_FsmSccGenFree] ******************************************************************************/ #define Mc_FsmForEachFairScc(fsm, gen, scc, sccClosedSetArray, leftover,\ buechiFairness, onionRings, earlyTermination,\ verbosity, dcLevel)\ for((gen) = Mc_FsmFirstScc(fsm, &scc, sccClosedSetArray, buechiFairness,\ onionRings, earlyTermination,\ verbosity, dcLevel);\ Mc_FsmIsSccGenEmpty(gen) ? Mc_FsmSccGenFree(gen, leftover) : TRUE;\ (void) Mc_FsmNextScc(gen, &scc)) /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "fsm.h" #include "part.h" /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN void Mc_Init(void); EXTERN void Mc_End(void); EXTERN mdd_t * Mc_FsmCheckLanguageEmptiness(Fsm_Fsm_t *modelFsm, array_t *modelCareStatesArray, Mc_AutStrength_t automatonStrength, Mc_LeMethod_t leMethod, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName); EXTERN mdd_t * Mc_FsmEvaluateFormula(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule); EXTERN mdd_t * Mc_FsmEvaluateEXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateMXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateAXFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateEYFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateEUFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint); EXTERN mdd_t * Mc_FsmEvaluateAUFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *target, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint); EXTERN mdd_t * Mc_FsmEvaluateESFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *source, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint); EXTERN mdd_t * Mc_FsmEvaluateEGFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule); EXTERN mdd_t * Mc_FsmEvaluateEHFormula(Fsm_Fsm_t *fsm, mdd_t *invariant, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, Mc_GSHScheduleType GSHschedule); EXTERN mdd_t * Mc_FsmEvaluateFwdUFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, array_t *careStatesArray, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateFwdGFormula(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN mdd_t * Mc_FsmEvaluateFwdEHFormula(Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, array_t *onionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN void Mc_FsmEvaluateFormulaForVacuity(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates); EXTERN mdd_t *Mc_QuantifyInputFAFW(Fsm_Fsm_t *fsm, bdd_t *result); EXTERN Mc_SccGen_t * Mc_FsmFirstScc(Fsm_Fsm_t *fsm, mdd_t **scc, array_t *sccClosedSetArray, array_t *buechiFairness, array_t *onionRings, boolean earlyTermination, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN boolean Mc_FsmNextScc(Mc_SccGen_t *gen, mdd_t **scc); EXTERN boolean Mc_FsmIsSccGenEmpty(Mc_SccGen_t *gen); EXTERN boolean Mc_FsmSccGenFree(Mc_SccGen_t *gen, array_t *leftover); EXTERN int Mc_FsmComputeStatesReachingToSet(Fsm_Fsm_t *modelFsm, mdd_t *targetStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN int Mc_FsmComputeStatesReachableFromSet(Fsm_Fsm_t *modelFsm, mdd_t *initialStates, array_t *careStatesArray, mdd_t *specialStates, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel); EXTERN boolean Mc_FormulaStaticSemanticCheckOnNetwork(Ctlp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed); EXTERN array_t * Mc_BuildPathToCore(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType); EXTERN array_t * Mc_BuildPathToCoreFAFW(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType); EXTERN array_t * Mc_BuildPathFromCore(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType); EXTERN array_t * Mc_BuildPathFromCoreFAFW(mdd_t *aState, array_t *onionRings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType); EXTERN array_t * Mc_CompletePath(mdd_t *aState, mdd_t *bState, mdd_t *invariantStates, Fsm_Fsm_t *modelFsm, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, Mc_FwdBwdAnalysis dirn); EXTERN mdd_t * Mc_ComputeAMinterm(mdd_t *aSet, array_t *Support, mdd_manager *mddMgr); EXTERN mdd_t * Mc_ComputeACloseMinterm(mdd_t *aSet, mdd_t *target, array_t *Support, mdd_manager *mddMgr); EXTERN char * Mc_MintermToString(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork); EXTERN char * Mc_MintermToStringAiger(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork); EXTERN char * Mc_MintermToStringAigerInput(mdd_t *aMinterm, array_t *aSupport, Ntk_Network_t *aNetwork); EXTERN int Mc_PrintPath(array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput); EXTERN int Mc_PrintPathAiger(array_t *aPath, Fsm_Fsm_t *modelFsm, boolean printInput); EXTERN mdd_t * Mc_FsmComputeDrivingInputMinterms(Fsm_Fsm_t *fsm, mdd_t *aState, mdd_t *bState); EXTERN mdd_t * Mc_ComputeAState(mdd_t *states, Fsm_Fsm_t *modelFsm); EXTERN mdd_t * Mc_ComputeACloseState(mdd_t *states, mdd_t *target, Fsm_Fsm_t *modelFsm); EXTERN void Mc_MintermPrint(mdd_t *aMinterm, array_t *support, Ntk_Network_t *aNetwork); EXTERN void Mc_NodeTableAddCtlFormulaNodes(Ntk_Network_t *network, Ctlp_Formula_t *formula, st_table * nodesTable); EXTERN void Mc_NodeTableAddLtlFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table * nodesTable); EXTERN Fsm_Fsm_t * Mc_ConstructReducedFsm(Ntk_Network_t *network, array_t *ctlFormulaArray); EXTERN Mc_GSHScheduleType Mc_StringConvertToScheduleType(char *string); EXTERN int Mc_StringConvertToLockstepMode(char *string); EXTERN Mc_EarlyTermination_t * Mc_EarlyTerminationAlloc(Mc_EarlyTerminationType mode, mdd_t *states); EXTERN void Mc_EarlyTerminationFree(Mc_EarlyTermination_t *earlyTermination); EXTERN boolean Mc_EarlyTerminationIsSkip(Mc_EarlyTermination_t *earlyTermination); EXTERN array_t * Mc_ReadHints(FILE *guideFP); EXTERN st_table * Mc_ReadSystemVariablesFAFW(Fsm_Fsm_t *fsm, FILE *systemFP); EXTERN array_t * Mc_EvaluateHints(Fsm_Fsm_t *fsm, Ctlp_FormulaArray_t *invarArray); EXTERN array_t * Mc_ComputeGuideArray(Fsm_Fsm_t *fsm, FILE *guideFP); EXTERN Mc_GuidedSearch_t Mc_ReadGuidedSearchType(void); EXTERN array_t * Mc_BuildShortestPathFAFW(mdd_t *win, mdd_t *S, mdd_t *T, array_t *rings, mdd_manager *mgr, Fsm_Fsm_t *fsm, int prevFlag); EXTERN st_table *Mc_SetAllInputToSystem(Fsm_Fsm_t *fsm); EXTERN array_t * Mc_BuildFAFWLayer(Fsm_Fsm_t *modelFsm, mdd_t *T, mdd_t *H); EXTERN array_t * MC_BuildCounterExampleFAFWGeneral( Fsm_Fsm_t *modelFsm, mdd_t *I, mdd_t *T, mdd_t *H, array_t *L); EXTERN array_t * Mc_BuildPathFromCoreFAFWGeneral( mdd_t *T, array_t *rings, Fsm_Fsm_t *modelFsm, Mc_PathLengthType PathLengthType); EXTERN array_t * Mc_BuildForwardRingsWithInvariants( mdd_t *S, mdd_t *T, mdd_t *invariants, Fsm_Fsm_t *fsm); EXTERN array_t * Mc_CreateStaticRefinementScheduleArray(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, boolean dynamicIncrease, boolean isLatchNameSort, int verbosity, int incrementalSize, Part_CMethod correlationMethod); EXTERN mdd_t * Mc_FsmCheckLanguageEmptinessByDnC(Fsm_Fsm_t *modelFsm, array_t *modelCareStatesArray, Mc_AutStrength_t automatonStrength, int dcLevel, int dbgLevel, int printInputs, int verbosity, Mc_GSHScheduleType GSHschedule, Mc_FwdBwdAnalysis GSHdirection, int lockstep, FILE *dbgFile, int UseMore, int SimValue, char *driverName); /**AutomaticEnd***************************************************************/ #endif /* _MC */