/**CFile*********************************************************************** FileName [mcMc.c] PackageName [mc] Synopsis [Fair CTL model checker.] Description [This file contains the functions for both backward and forward model checking. Forward model checking is based on Iwashta's ICCAD96 paper. Future tense CTLs are automatically converted to past tense ones as much as possible in forward model checking.] Author [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Roderick Bloem] 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.] ******************************************************************************/ #include "ctlpInt.h" #include "mcInt.h" #include "fsm.h" #include "bmc.h" static char rcsid[] UNUSED = "$Id: mcMc.c,v 1.257 2007/04/17 00:01:22 sohail Exp $"; #ifdef DEBUG_MC void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm); #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static mdd_t * EvaluateFormulaRecur(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Ctlp_Approx_t *resultApproxType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule); static mdd_t * McForwardReachable(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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Compute all the states that lead to a fair cycle] Comment [Used by LE/LTL/CTL* model checking. Different dicision procedures are applied according to the "strength of the buechi automaton": For the strong automaton, we need to compute EG(true) under the fairness constraints; If the automaton is weak, we will check !EFEG(fair); If the automaton is terminal, we only need to check !EF(fair). This is based on the CAV'99 paper of Bloem, Ravi & Somenzi: "Efficient Decision Procedures for Model Checking of Linear Time Logic Properties". Debugging information will be print out if dbgLevel is non-zero. Return the set of initial states from where fair paths exist.] SideEffects [The caller should free the returned mdd_t.] ******************************************************************************/ 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) { mdd_t *result; mdd_t *mddOne; mdd_t *badStates; mdd_t *aBadState; mdd_t *initialStates; mdd_t *fairStates; mdd_manager *mddMgr; Ctlp_Formula_t *ctlFair, *ctlFormula; Mc_EarlyTermination_t *earlyTermination; array_t *arrayOfOnionRings; array_t *stemArray; array_t *cycleArray; McPath_t *fairPath; McPath_t *normalPath; FILE *tmpFile = vis_stdout; extern FILE *vis_stdpipe; int i; if (leMethod == Mc_Le_Dnc_c && automatonStrength == 2) { return Mc_FsmCheckLanguageEmptinessByDnC(modelFsm, modelCareStatesArray, Mc_Aut_Strong_c, dcLevel, dbgLevel, printInputs, verbosity, GSHschedule, GSHdirection, lockstep, dbgFile, UseMore, SimValue, driverName); } /************************************************************************** * CASE1 & CASE2: TERMINAL/WEAK AUTOMATON * problem is reduced to checking !EF (fair) for TERMINAL * or !EF EG (fair) for WEAK **************************************************************************/ if (automatonStrength == 0 || automatonStrength == 1) { Fsm_Fairness_t *modelFairness; modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm); assert(Fsm_FairnessTestIsBuchi(modelFairness)); ctlFair = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav("fair1$AUT$NTK2"), (void *)util_strsav("1")); /* Dup(Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, 0)); */ if (automatonStrength == 0) { Ctlp_Formula_t *ctlTRUE; ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t)); ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlFair); if (dbgLevel || verbosity) fprintf(vis_stdout, "# %s: Terminal automaton -- check EF(states satisfy fairness)\n", driverName); }else { Ctlp_Formula_t *ctlTRUE, *ctlEGfair; ctlTRUE = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t)); ctlEGfair = Ctlp_FormulaCreate(Ctlp_EG_c, ctlFair, NIL(Ctlp_Formula_t)); ctlFormula = Ctlp_FormulaCreate(Ctlp_EU_c, ctlTRUE, ctlEGfair); if (dbgLevel || verbosity) fprintf(vis_stdout, "# %s: Weak automaton -- check EF EG (states satisfy fairness)\n", driverName); } /* Evaluate ctlFormula */ mddMgr = Fsm_FsmReadMddManager(modelFsm); mddOne = mdd_one(mddMgr); initialStates = Fsm_FsmComputeInitialStates(modelFsm); earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates); fairStates = Mc_FsmEvaluateFormula(modelFsm, ctlFormula, mddOne, modelFairness, modelCareStatesArray, earlyTermination, NIL(Fsm_HintsArray_t), Mc_None_c, (Mc_VerbosityLevel) verbosity, (Mc_DcLevel) dcLevel, (dbgLevel != McDbgLevelNone_c || verbosity), GSHschedule); Mc_EarlyTerminationFree(earlyTermination); mdd_free(mddOne); /* If there is at least one fair initial state, language is not empty. */ if (!mdd_lequal(initialStates, fairStates, 1, 0)) { if (strcmp(driverName, "LE") == 0) fprintf(vis_stdout, "# LE: language is not empty\n"); else fprintf(vis_stdout, "# %s: formula failed\n", driverName); result = mdd_and(fairStates, initialStates, 1, 1); } else { if (strcmp(driverName, "LE") == 0) fprintf(vis_stdout, "# LE: language emptiness check passes\n"); else fprintf(vis_stdout, "# %s: formula passed\n", driverName); Ctlp_FormulaFree(ctlFormula); mdd_free(fairStates); mdd_free(initialStates); return NIL(mdd_t); } /* If no wintness is requested, clean up and return. */ if (dbgLevel == McDbgLevelNone_c) { Ctlp_FormulaFree(ctlFormula); mdd_free(initialStates); mdd_free(fairStates); return result; }else { Ctlp_Formula_t *F; array_t *EGArrayOfOnionRings, *EGonionRings, *EFonionRings; array_t *newOnionRings; mdd_t *mdd1; int j; arrayOfOnionRings = array_alloc(array_t *, 0); EFonionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula); if (automatonStrength == 0) { array_insert_last(array_t *, arrayOfOnionRings, mdd_array_duplicate(EFonionRings)); }else if (automatonStrength == 1) { F = Ctlp_FormulaReadRightChild(ctlFormula); /* EG (states labelled fair) */ EGArrayOfOnionRings = (array_t *)Ctlp_FormulaReadDebugData(F); arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) { newOnionRings = mdd_array_duplicate(EGonionRings); arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) { if (j != 0) array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1)); } array_insert_last(array_t *, arrayOfOnionRings, newOnionRings); } } Ctlp_FormulaFree(ctlFormula); fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName); } }else { /************************************************************************* * CASE3: STRONG AUTOMATON * need to solve the problem by computing EG_fair (true) *************************************************************************/ mddMgr = Fsm_FsmReadMddManager(modelFsm); initialStates = Fsm_FsmComputeInitialStates(modelFsm); /* Compute fair states. */ if (lockstep == MC_LOCKSTEP_OFF) { fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray, verbosity, dcLevel, GSHschedule, GSHdirection, FALSE); arrayOfOnionRings = Fsm_FsmReadDebugArray(modelFsm); } else { /* For lockstep, the computed set of states is a subset of the reachable fair states, with the property that the subset is empty only if there are no reachable fair states. Since the onion rings are built for the fairness constraint restricted to the subset of the fair states, they are not valid in general for the FSM. Hence, they are not saved. */ array_t *SCCs = array_alloc(mdd_t *, 0); arrayOfOnionRings = array_alloc(array_t *, 0); fairStates = McFsmComputeFairSCCsByLockStep(modelFsm, lockstep, SCCs, arrayOfOnionRings, (Mc_VerbosityLevel) verbosity, (Mc_DcLevel) dcLevel); mdd_array_free(SCCs); } /* Lockstep guarantees that all fair SCCs are reachable. However, it does not extend the fair states backward unless a counterexample is requested. For the SCC hull approach with backward operators, the language is not empty if there is at least one fair initial state. Finally, For SCC hull with forward operators, currently we do not extend the hull backward, but we enforce reachability of the hull. Hence, nonemptiness of the hull signals that the language is not empty. */ if ((lockstep == MC_LOCKSTEP_OFF && (!mdd_lequal(initialStates, fairStates, 1, 0) || (GSHdirection == McFwd_c && !mdd_lequal_array(fairStates, modelCareStatesArray, 1, 0)))) || (lockstep != MC_LOCKSTEP_OFF && !mdd_is_tautology(fairStates, 0))) { if (strcmp(driverName, "LE") == 0) fprintf(vis_stdout, "# LE: language is not empty\n"); else fprintf(vis_stdout, "# %s: formula failed\n", driverName); result = mdd_and(fairStates, initialStates, 1, 1); } else { if (strcmp(driverName, "LE") == 0) fprintf(vis_stdout, "# LE: language emptiness check passes\n"); else fprintf(vis_stdout, "# %s: formula passed\n", driverName); /* Dispose of onion rings if produced by lockstep. */ if (lockstep != MC_LOCKSTEP_OFF) { mdd_array_array_free(arrayOfOnionRings); } mdd_free(fairStates); mdd_free(initialStates); return NIL(mdd_t); } /* If no witness is requested, clean up and return. */ if (dbgLevel == McDbgLevelNone_c) { /* Dispose of onion rings if produced by lockstep. */ if (lockstep != MC_LOCKSTEP_OFF) { mdd_array_array_free(arrayOfOnionRings); } mdd_free(fairStates); mdd_free(initialStates); return result; } else { (void) fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName); } } /* Generate witness. */ badStates = mdd_and(initialStates, fairStates, 1, 1); mdd_free(fairStates); mdd_free(initialStates); aBadState = Mc_ComputeAState(badStates, modelFsm); mdd_free(badStates); mddOne = mdd_one(mddMgr); fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm, modelCareStatesArray, (Mc_VerbosityLevel) verbosity, (Mc_DcLevel) dcLevel, McFwd_c); mdd_free(mddOne); mdd_free(aBadState); /* Dispose of onion rings if produced by lockstep. */ if (lockstep != MC_LOCKSTEP_OFF || automatonStrength != 2) { mdd_array_array_free(arrayOfOnionRings); } /* Print witness. */ normalPath = McPathNormalize(fairPath); McPathFree(fairPath); stemArray = McPathReadStemArray(normalPath); cycleArray = McPathReadCycleArray(normalPath); /* we should pass dbgFile/UseMore as parameters dbgFile = McOptionsReadDebugFile(options);*/ if (dbgFile != NIL(FILE)) { vis_stdpipe = dbgFile; } else if (UseMore == TRUE) { vis_stdpipe = popen("more","w"); } else { vis_stdpipe = vis_stdout; } vis_stdout = vis_stdpipe; /* We should also pass SimValue as a parameter */ if (SimValue == FALSE) { (void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName); Mc_PrintPath(stemArray, modelFsm, printInputs); fprintf (vis_stdout, "\n"); (void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName); Mc_PrintPath(cycleArray, modelFsm, printInputs); fprintf (vis_stdout, "\n"); }else { array_t *completePath = McCreateMergedPath(stemArray, cycleArray); (void) fprintf(vis_stdout, "# %s: counter-example\n", driverName); McPrintSimPath(vis_stdout, completePath, modelFsm); mdd_array_free(completePath); } if (dbgFile == NIL(FILE) && UseMore == TRUE) { (void) pclose(vis_stdpipe); } vis_stdout = tmpFile; McPathFree(normalPath); return result; } /**Function******************************************************************** Synopsis [Model check formula on given FSM under fairness] Description [Model check formula on given FSM under fairness.] Comment [ Recursive evaluation using Emerson-Lei LICS 1986 algorithms. The states satisfying subformulas are stored and used later if there is sharing of subformulas. Therefore, each subformula is computed just once. Large switch - base case is atomic formula, TRUE, and FALSE. Boolean operators - straightforward. Path modalities are reduced to one of the three - EX, EU, EG which are evaluated under fairness. Note the semantics for atomic formulas carefully - in addition to generating the prescribed output, the state must also be fair. Don't cares from unreached, unfair states are both used. The proof of correctness of using all these dont cares hinges on the invariant that restricted to the reached state set, the computed sets are exactly as they should be. Both backward and forward formulas are handled. This function sets the states and debug info of the formula for use with the debugger. ARGUMENTS: ctlFormula: a ctl formula in simple(!) existential form, using forward and/or backward operators. EarlyTermination: If earlyTermination.mode is McAll_c (McSome_c), the algorithm can stop as soon as 1. it is sure that all (some) of earlyTermination.states are included in the evaluation of the formula, or 2. It is sure that some (all) of these states are not included in the evaluation. If earlyTermination.mode is McCare_c, then the algorithm can stop as soon as it is guaranteed that either all or none of earlyTermination.states are included in the evaluation. These checks are done modulo the care set, but not modulo the fair states, which means that they will not be effective if you require unfair states to be in the evaluation. Typically {ALL, initialStates} will be good. NULL means the option has no effect. Debugging only works if this function is called with {ALL, initialStates}. Otherwise, debugging of the EG formulae may go wrong. hintsArray is an array of hints. Pass NULL and set hintType to Mc_None_c to ignore. If hintType is Mc_Global_c, then the formula is evaluated once for each hint, where every hint defines an underapproximation of the formula. This only works for pure A/E CTL formulae. If hintType is Mc_Local_c, then every fixpoint goes through the sequence of hints until completion, before moving up to the next temporal operator. ] SideEffects [] ******************************************************************************/ 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) { mdd_t *hint; /* to iterate over hintsArray */ int hintnr; /* idem */ Ctlp_Approx_t resultApproxType; assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t)); if(hintType != Mc_Global_c) return EvaluateFormulaRecur(fsm, ctlFormula, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, Ctlp_Exact_c, &resultApproxType, verbosity, dcLevel, buildOnionRing, GSHschedule); else{ mdd_t *result = NIL(mdd_t); Ctlp_Approx_t approx; if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Using global hints\n"); arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ if(result != NIL(mdd_t)) mdd_free(result); if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Instantiating global hint %d\n", hintnr); Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c, (verbosity >= McVerbosityMax_c)); approx = mdd_is_tautology(hint, 1) ? Ctlp_Exact_c : Ctlp_Underapprox_c; result = EvaluateFormulaRecur(fsm, ctlFormula, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, approx, &resultApproxType, verbosity, dcLevel, buildOnionRing, GSHschedule); /* TBD: take into account (early) termination here */ } Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); return result; } } /* Mc_FsmEvaluateFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying EX target] Description [Evaluate states satisfying EX target. Basically, calls the image package -- all the smarts are in there, parameters for it can be set from the VIS prompt. In the presence of fairness, a state satisifies EX foo just in case it has a sucessor where foo is true AND that successor can be continued to an infinite path which is fair.] SideEffects [] ******************************************************************************/ mdd_t * Mc_FsmEvaluateEXFormula( Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *fromLowerBound; mdd_t *fromUpperBound; mdd_t *result; Img_ImageInfo_t * imageInfo; if(Fsm_FsmReadUseUnquantifiedFlag(modelFsm)) imageInfo = Fsm_FsmReadOrCreateImageInfoFAFW(modelFsm, 1, 0); else imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0); /* * The lower bound is the conjunction of the fair states, * and the target states. */ fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1); /* * The upper bound is the same as the lower bound. */ fromUpperBound = mdd_dup(fromLowerBound); result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, careStatesArray); mdd_free(fromLowerBound); mdd_free(fromUpperBound); if (verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); mdd_t *tmpMdd = careStatesArray ? mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result); fprintf(vis_stdout, "--EX called %d (bdd_size - %d)\n", ++refCount, mdd_size(result)); fprintf(vis_stdout, "--There are %.0f care states satisfying EX formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); mdd_free(tmpMdd); } return result; } /* Mc_FsmEvaluateEXFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying MX target] Description [Compute EX with transition relation that contains input varaibles and then apply universial quantification to get MX target. To use this function, one has to run Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation that contains input variables. And Fsm_FsmSetUseUnquantifiedFlag has to be called. That useUnquantifiedFlag is used to specify which imageInfo can be used in image computation. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ mdd_t * Mc_FsmEvaluateMXFormula( Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *resultBar, *result; result = Mc_FsmEvaluateEXFormula(modelFsm, targetMdd, fairStates, careStatesArray, verbosity, dcLevel); if(Fsm_FsmReadUniQuantifyInputCube(modelFsm)) { resultBar = Mc_QuantifyInputFAFW(modelFsm, result); mdd_free(result); result = resultBar; } return(result); } /**Function******************************************************************** Synopsis [Quantify the input variables] Description [Quantify the input variables after applying EX. To use this function, one has to run Fsm_FsmReadOrCreateImageInfoFAFW to create the trasition relation that contains input variables. To get the result of real MX operation, the bdd_smooth_with_cube has to be applied after bdd_consensus_with_cube, but we need those input variables for path generation. If one needs real MX then bdd_smooth_with_cube has to be applied. This is function for FateAndFreeWill counterexample generation.] SideEffects [] ******************************************************************************/ bdd_t * Mc_QuantifyInputFAFW(Fsm_Fsm_t *fsm, bdd_t *result) { bdd_t *uniCube, *extCube, *newResult; bdd_t *oneMdd, *notResult; mdd_manager *mgr = Fsm_FsmReadMddManager(fsm); oneMdd = mdd_one(mgr); uniCube = Fsm_FsmReadUniQuantifyInputCube(fsm); extCube = Fsm_FsmReadExtQuantifyInputCube(fsm); if(!mdd_equal(uniCube, oneMdd)) { /** newResult = bdd_consensus_with_cube(result, uniCube); **/ notResult = bdd_not(result); newResult = bdd_smooth_with_cube(notResult, uniCube); bdd_free(notResult); result = bdd_not(newResult); bdd_free(newResult); } else { result = mdd_dup(result); } mdd_free(oneMdd); return(result); } /**Function******************************************************************** Synopsis [Evaluate states satisfying EY target] Description [Evaluate states satisfying EY target.] SideEffects [] ******************************************************************************/ mdd_t * Mc_FsmEvaluateEYFormula( Fsm_Fsm_t *modelFsm, mdd_t *targetMdd, mdd_t *fairStates, array_t *careStatesArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel) { mdd_t *fromLowerBound; mdd_t *fromUpperBound; mdd_t *result; Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 0, 1); /* * The lower bound is the conjunction of the fair states, * and the target states. */ fromLowerBound = mdd_and(targetMdd, fairStates, 1, 1); /* * The upper bound is the same as the lower bound. */ fromUpperBound = fromLowerBound; result = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, careStatesArray); mdd_free(fromLowerBound); if (verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); mdd_t *tmpMdd = careStatesArray ? mdd_and_array(result, careStatesArray, 1, 1) : mdd_dup(result); fprintf(vis_stdout, "--EY called %d (bdd_size - %d)\n", ++refCount, mdd_size(result)); fprintf(vis_stdout, "--There are %.0f care states satisfying EY formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); mdd_free(tmpMdd); } return result; } /* Mc_FsmEvaluateEYFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying E(invariant U target)] Description [Evaluate states satisfying E(invariant U target). Performed by a least fixed point computation -- start with target AND fair, see what can get to this set by a path solely in invariant. If the onionRings array is not NIL(array_t *), the ``onion rings'' arising in the least fixed point computation are stored in the array, starting from the target. The onion rings explain how to get from any state in the result to the target. The evaluation stops once all (some) of earlyTermination.states have been found (depending on earlyTermination.mode). See Mc_FsmEvaluateFormula() If underapprox is not NIL, it must hold a valid underapproximation of the fixpoint. This is used to kick off the new computation. The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain underapproximations of the transition system. (See Mc_FsmEvaluateFormula.) fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. OnionRings is an array of mdd_t *. It can be NULL, in which case no onion rings are returned. If it is not NULL, there are two possibilities. In the simple case, the onion rings are empty, and underapprox is NULL. In this case, the onion rings returned explain how to get to the target from any state in the result returned (r). If underapprox u is not NULL, the onion rings that are passed in should explain how to get from any state in u to any state in the target. Rings will be added by the procudure to explain how to get from the r to a state in underapprox, resulting in an explanation of how to get from a state in r to the target. ] Comment [Check that evaluation mod reached AND fair will lead to faster convergence. Also, it is possible there is more (?) flexibility in dont care minimization - use only the layer of the onion rings as set for evaluating EX.] SideEffects [] SeeAlso [Mc_FsmEvaluateFormula, McEvaluateEUFormulaWithGivenTR] ******************************************************************************/ 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) { /* should be strengthened to check that rings supply a correct explanation. */ /*check out * assert(underapprox == NULL || onionRings == NULL || * array_n(onionRings) != 0); */ if(hintType != Mc_Local_c) /* postcondition: rings should explain how to get from return value to * target. */ return McEvaluateEUFormulaWithGivenTR(fsm, invariant, target, underapprox, fairStates, careStatesArray, earlyTermination, onionRings, verbosity, dcLevel, fixpoint); else{ mdd_t *iterate, *newiterate; mdd_t *hint; int hintnr; if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Using local hints\n"); if(underapprox != NIL(mdd_t)) iterate = mdd_dup(underapprox); else iterate = mdd_zero(Fsm_FsmReadMddManager(fsm)); arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr); Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c, (verbosity >= McVerbosityMax_c)); newiterate = McEvaluateEUFormulaWithGivenTR(fsm, invariant, target, iterate, fairStates, careStatesArray, earlyTermination, onionRings, verbosity, dcLevel, fixpoint); mdd_free(iterate); iterate = newiterate; /* check if we can terminate without considering all hints */ if(mdd_is_tautology(iterate, 1)){ *fixpoint = 1; break; } if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate, careStatesArray)){ *fixpoint = 0; break; } }/* for all hints */ Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); /* postcondition: rings should explain how to get from return value to * target. */ return iterate; }/* if hinttype */ } /* Mc_FsmEvaluateEUFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying E(invariant S source)] Description [Evaluate states satisfying E(invariant U target). Performed by a least fixed point computation -- start with source AND fair, see what can be reached from this set by a path solely in invariant. If the onionRings array is not NIL(array_t *), the ``onion rings'' arising in the least fixed point computation are stored in the array, starting from the target. The evaluation stops once all (some) of earlyTermination.states have been found (depending on earlyTermination.mode). See Mc_FsmEvaluateFormula() If underapprox is not NIL, it must hold a valid underapproximation of the fixpoint. This is used to kick off the new computation. The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain underapproximations of the transition system. (See Mc_FsmEvaluateFormula.) fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. OnionRIngs is an array of mdd_t *. It should be empty on call if you want debug info, NULL otherwise. After the call, it contains the onion rings (frontier sets) that occured while computing the ES. This is used for debugging.] Comment [Check that evaluation mod reached AND fair will lead to faster convergence. Also, it is possible there is more (?) flexibility in don't care minimization - use only the layer of the onion rings as set for evaluating EX.] SideEffects [] SeeAlso [Mc_FsmEvaluateFormula, McEvaluateESFormulaWithGivenTR] ******************************************************************************/ 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) { /* should be strengthened to check that rings supply a correct explanation. */ assert(underapprox == NULL || onionRings == NULL || array_n(onionRings) != 0); if(hintType != Mc_Local_c) /* postcondition: rings should explain how to get from return value to * target. */ return McEvaluateESFormulaWithGivenTR(fsm, invariant, source, underapprox, fairStates, careStatesArray, earlyTermination, onionRings, verbosity, dcLevel, fixpoint); else{ mdd_t *iterate, *newiterate; mdd_t *hint; int hintnr; if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Using local hints\n"); if(underapprox != NIL(mdd_t)) iterate = mdd_dup(underapprox); else iterate = mdd_zero(Fsm_FsmReadMddManager(fsm)); arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr); Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Underapprox_c, (verbosity >= McVerbosityMax_c)); newiterate = McEvaluateESFormulaWithGivenTR(fsm, invariant, source, iterate, fairStates, careStatesArray, earlyTermination, onionRings, verbosity, dcLevel, fixpoint); mdd_free(iterate); iterate = newiterate; /* check if we can terminate without considering all hints */ if(mdd_is_tautology(iterate, 1)){ *fixpoint = 1; break; } if(McCheckEarlyTerminationForUnderapprox(earlyTermination, iterate, careStatesArray)){ *fixpoint = 0; break; } }/* for all hints */ Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); /* postcondition: rings should explain how to get from return value to * target. */ return iterate; }/* if hinttype */ } /* Mc_FsmEvaluateESFormula */ 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) { return McEvaluateAUFormulaWithGivenTR(fsm, invariant, target, underapprox, fairStates, careStatesArray, earlyTermination, onionRings, verbosity, dcLevel, fixpoint); } /**Function******************************************************************** Synopsis [Evaluate states satisfying EG invariant] Description [Evaluate states satisfying EG invariant. This is done by starting with all states marked with the invariant. From this initial set, recursively remove states that can not reach Buechi contraints (through paths entirely within the current set). If overapprox is not nil, then it is a valid overapproximation to the satisfiable set of the formula that will be used to kick off the computation. pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of arrays of mdd_t *s. Upon calling this formula, it should point to an empty array if you want debug information, or be NIL (or a pointer to NIL) if you do not. After the call, it points to an array that contains one entry for every fairness constraint: entry i contains the onionrings for the last EU computation that was performed for fairness constraint i. There are two exceptions: if the satisfying set is 0, or if early termination kicks in, the onion ring array is not changed. The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain overapproximations of the transition system (See Mc_FsmEvaluateFormula). fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. See Mc_FsmEvaluateFormula for a discussion of early termination.] SideEffects [] SeeAlso [Mc_FsmEvaluateFormula] ******************************************************************************/ 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) { /* Illegal to pass in onion rings. */ #if 0 assert(pOnionRingsArrayForDbg == NIL(array_t *) || *pOnionRingsArrayForDbg == NIL(array_t) || array_n(*pOnionRingsArrayForDbg) == 0); #endif if(hintType != Mc_Local_c) if (GSHschedule == McGSH_old_c) { return McEvaluateEGFormulaWithGivenTR(fsm, invariant, overapprox, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint); } else { return McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, overapprox, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint, GSHschedule); } else { mdd_t *iterate, *newiterate; mdd_t *hint; int hintnr; boolean useRings; useRings = (pOnionRingsArrayForDbg != NIL(array_t *) && *pOnionRingsArrayForDbg != NIL(array_t)); if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "** mc Info: Using local hints\n"); if(overapprox != NIL(mdd_t)) iterate = mdd_dup(overapprox); else iterate = mdd_one(Fsm_FsmReadMddManager(fsm)); arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr); Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c, (verbosity >= McVerbosityMax_c)); /* old onionrings go stale. Fry 'em */ if(useRings){ mdd_array_array_free(*pOnionRingsArrayForDbg); *pOnionRingsArrayForDbg = array_alloc(array_t *, 0); } if (GSHschedule == McGSH_old_c) { newiterate = McEvaluateEGFormulaWithGivenTR(fsm, invariant, iterate, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint); } else { newiterate = McFsmEvaluateEGFormulaUsingGSH(fsm, invariant, iterate, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint, GSHschedule); } mdd_free(iterate); iterate = newiterate; /* check if we can terminate without considering all hints */ if(mdd_is_tautology(iterate, 0)){ *fixpoint = 1; break; } if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate, careStatesArray)){ *fixpoint = 0; break; } } /* For all hints */ Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); return iterate; }/* if hinttype */ } /* Mc_FsmEvaluateEGFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying EH invariant.] Description [Evaluate states satisfying EH invariant. This is done by starting with all states marked with the invariant. From this initial set, recursively remove states that cannot reach Buechi contraints (through paths entirely within the current set). If overapprox is not nil, then it is a valid overapproximation to the satisfiable set of the formula that will be used to kick off the computation. pOnionRingsArrayForDbg is a pointer to (a pointer to) an array of arrays of mdd_t *s. Upon calling this formula, it should point to an empty array if you want debug information, or be NIL (or a pointer to NIL) if you do not. After the call, it points to an array that contains one entry for every fairness constraint: entry i contains the onionrings for the last ES computation that was performed for fairness constraint i. There are two exceptions: if the satisfying set is 0, or if early termination kicks in, the onion ring array is not changed. The arguments hintsArray and hints are used for guided search. Set hintType to Mc_None_c to ignore. If hintType is Mc_Local_c, hintsArray should be an array of mdds, of which the last entry is 1. This array will be used to obtain overapproximations of the transition system (See Mc_FsmEvaluateFormula). fixpoint is a return argument. It is true if the formula is evaluated exactly, false if early termination kicked in. If earlyTermination is NIL, the formula is evaluated exacty, and this argument may be NIL too. See Mc_FsmEvaluateFormula for a discussion of early termination.] SideEffects [] SeeAlso [Mc_FsmEvaluateFormula] ******************************************************************************/ 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) { /* Illegal to pass in onion rings. */ assert(pOnionRingsArrayForDbg == NIL(array_t *) || *pOnionRingsArrayForDbg == NIL(array_t) || array_n(*pOnionRingsArrayForDbg) == 0); if(hintType != Mc_Local_c) if (GSHschedule == McGSH_old_c) { return McEvaluateEHFormulaWithGivenTR(fsm, invariant, overapprox, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint); } else { return McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, overapprox, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint, GSHschedule); } else { mdd_t *iterate, *newiterate; mdd_t *hint; int hintnr; boolean useRings; useRings = (pOnionRingsArrayForDbg != NIL(array_t *) && *pOnionRingsArrayForDbg != NIL(array_t)); if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "** mc Info: Using local hints\n"); if(overapprox != NIL(mdd_t)) iterate = mdd_dup(overapprox); else iterate = mdd_one(Fsm_FsmReadMddManager(fsm)); arrayForEachItem(mdd_t *, hintsArray, hintnr, hint){ if(verbosity >= McVerbosityMax_c) fprintf(vis_stdout, "--Instantiating local hint %d\n", hintnr); Fsm_InstantiateHint(fsm, hint, FALSE, TRUE, Ctlp_Overapprox_c, (verbosity >= McVerbosityMax_c)); /* old onionrings go stale. Fry 'em */ if(useRings){ mdd_array_array_free(*pOnionRingsArrayForDbg); *pOnionRingsArrayForDbg = array_alloc(array_t *, 0); } if (GSHschedule == McGSH_old_c) { newiterate = McEvaluateEHFormulaWithGivenTR(fsm, invariant, iterate, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint); } else { newiterate = McFsmEvaluateEHFormulaUsingGSH(fsm, invariant, iterate, fairStates, modelFairness, careStatesArray, earlyTermination, pOnionRingsArrayForDbg, verbosity, dcLevel, fixpoint, GSHschedule); } mdd_free(iterate); iterate = newiterate; /* check if we can terminate without considering all hints */ if(mdd_is_tautology(iterate, 0)){ *fixpoint = 1; break; } if(McCheckEarlyTerminationForOverapprox(earlyTermination, iterate, careStatesArray)){ *fixpoint = 0; break; } } /* For all hints */ Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); return iterate; }/* if hinttype */ } /* Mc_FsmEvaluateEHFormula */ /**Function******************************************************************** Synopsis [Evaluate states satisfying FwdUntil] Description [Evaluate states satisfying FwdUntil.] Comment [] SideEffects [] ******************************************************************************/ 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) { mdd_t *aMdd; mdd_t *bMdd; mdd_t *cMdd; mdd_t *resultMdd; mdd_t *ringMdd; int nImgComps; /* t ** E[p U q] = lfp Z[q V (p ^ EX(Z))] : p p ... p q ** FwdUntil(p,q) = lfp Z[p V EY(Z ^ q)] : pq q q ... q */ nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); resultMdd = mdd_and(targetMdd, fairStates, 1, 1); ringMdd = mdd_dup(resultMdd); /* if until is trivially satisfied, */ if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } if (mdd_is_tautology(fairStates, 1)) { if (mdd_equal_mod_care_set_array(invariantMdd, resultMdd, careStatesArray)) { bdd_free(ringMdd); return(resultMdd); } } else { bdd_t *trivialCheck = mdd_and(invariantMdd, fairStates, 1, 1); if (mdd_equal_mod_care_set_array(trivialCheck, resultMdd, careStatesArray)) { bdd_free(trivialCheck); bdd_free(ringMdd); return(resultMdd); } bdd_free(trivialCheck); } while (TRUE) { aMdd = mdd_and(ringMdd, invariantMdd, 1, 1); mdd_free(ringMdd); bMdd = Mc_FsmEvaluateEYFormula(modelFsm, aMdd, fairStates, careStatesArray, verbosity, dcLevel); mdd_free(aMdd); cMdd = mdd_or(resultMdd, bMdd, 1, 1); mdd_free(bMdd); if (mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray)) { mdd_free(cMdd); break; } if (dcLevel >= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- FwdU |A(n+1)-A(n)| = %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- FwdU |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ /* Print some debug info */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); if (verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(resultMdd, careStatesArray, 1, 1) : mdd_dup(resultMdd); fprintf(vis_stdout, "--FwdU called %d (bdd_size - %d)\n", ++refCount, mdd_size(resultMdd)); fprintf(vis_stdout, "--There are %.0f care states satisfying FwdU formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "FwdU satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying FwdU formula\n", mdd_count_onset(mddMgr, resultMdd, psVars)); } fprintf(vis_stdout, "--FwdU: %d image computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } return resultMdd; } /**Function******************************************************************** Synopsis [Evaluate states satisfying FwdG invariant] Description [Evaluate states satisfying FwdG invariant.] SideEffects [] ******************************************************************************/ 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) { mdd_t *resultMdd, *invariant; array_t *onionRings; int nImgComps; nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); onionRings = NIL(array_t); invariant = McForwardReachable(modelFsm, targetMdd, invariantMdd, fairStates, careStatesArray, onionRings, verbosity, dcLevel); resultMdd = Mc_FsmEvaluateFwdEHFormula(modelFsm, invariant, fairStates, modelFairness, careStatesArray, onionRingsArrayForDbg, verbosity, dcLevel); mdd_free(invariant); if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--FwdG: %d image computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } #ifdef DEBUG_MC /* The following 2 lines are just for debug */ if ((verbosity == McVerbosityMax_c)) { fprintf(vis_stdout, "FwdG satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(resultMdd, modelFsm); } #endif return resultMdd; } /**Function******************************************************************** Synopsis [Evaluate states satisfying EH invariant] Description [Evaluate states satisfying EH invariant.] SideEffects [] ******************************************************************************/ 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) { int i; array_t *onionRings = NIL(array_t); array_t *tmpOnionRingsArrayForDbg = NIL(array_t); mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm); mdd_t *mddOne = mdd_one(mddManager); mdd_t *Zmdd; int nIterations = 0; int nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); /* ** EG(f) = gfp Z[f ^ EX(Z)] ** EH(f) = gfp Z[f ^ EY(Z)] ** ** EcG(f) = gfp Z[f ^ EX( ^ E[Z U Z ^ c])] ** c= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--EU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- EU |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; /* add onion ring unless fixpoint reached */ if (!term_fixpoint && onionRings != NIL(array_t)) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ mdd_free(ringMdd); /* Print some debug info */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); if (verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(resultMdd, careStatesArray, 1, 1) : mdd_dup(resultMdd); fprintf(vis_stdout, "--EU called %d (bdd_size - %d)\n", ++refCount, mdd_size(resultMdd)); fprintf(vis_stdout, "--There are %.0f care states satisfying EU formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "EU satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying EU formula\n", mdd_count_onset(mddMgr, resultMdd, psVars)); } fprintf(vis_stdout, "--EU: %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); } if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return resultMdd; } /* McEvaluateEUFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [Evaluate states satisfying E(invariant S target), given a transition relation] Description [Does the same as Mc_FsmEvaluateESFormula, minus the hints.] SeeAlso [Mc_FsmEvaluateESFormula] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateESFormulaWithGivenTR( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint ) { mdd_t *aMdd; mdd_t *bMdd; mdd_t *cMdd; mdd_t *resultMdd; mdd_t *ringMdd; int nImgComps; boolean term_tautology = FALSE; /* different termination conditions */ boolean term_early = FALSE; boolean term_fixpoint = FALSE; nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); resultMdd = mdd_and(sourceMdd, fairStates, 1, 1); if(underapprox != NIL(mdd_t)){ mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1); mdd_free(resultMdd); resultMdd = tmp; } ringMdd = mdd_dup(resultMdd); if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } /* if Since is trivially satisfied, or the early termination condition holds*/ { bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1); boolean trivial; trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd, 1, 1, careStatesArray); /* the lequal also takes care of the case where result = 1 */ if(trivial || McCheckEarlyTerminationForUnderapprox(earlyTermination, resultMdd, careStatesArray)){ bdd_free(fairInvariantStates); bdd_free(ringMdd); /* trivially satisfied means that the fixpoint is complete. If this information is requested, give it. */ if(fixpoint != NIL(boolean)) *fixpoint = trivial; return(resultMdd); } bdd_free(fairInvariantStates); } /* The LFP loop */ while (!term_fixpoint && !term_tautology && !term_early) { /* If dclevel is maximal, ringbdd is between the frontier and the reached set */ aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates, careStatesArray, verbosity, dcLevel); mdd_free(ringMdd); bMdd = mdd_and(aMdd, invariantMdd, 1, 1); mdd_free(aMdd); cMdd = mdd_or(resultMdd, bMdd, 1, 1); mdd_free(bMdd); /* Can we stop? The tautology condition can be weakened to cMdd <= careStatesArray */ term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray); if(!term_fixpoint) term_tautology = mdd_is_tautology(cMdd, 1); if(!term_fixpoint && !term_tautology) term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, cMdd, careStatesArray); /* Print some debug info, and set ringmdd */ if (dcLevel >= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; /* add onion ring unless fixpoint reached */ if (!term_fixpoint && onionRings != NIL(array_t)) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ mdd_free(ringMdd); /* Print some debug info */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); if (verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(resultMdd, careStatesArray, 1, 1) : mdd_dup(resultMdd); fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount, mdd_size(resultMdd)); fprintf(vis_stdout, "--There are %.0f care states satisfying ES formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "ES satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying ES formula\n", mdd_count_onset(mddMgr, resultMdd, psVars)); } fprintf(vis_stdout, "--ES: %d image computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return resultMdd; } /* McEvaluateESFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [] Description [] SeeAlso [] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateESFormulaWithGivenTRWithTarget( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint ) { mdd_t *aMdd; mdd_t *bMdd; mdd_t *cMdd; mdd_t *resultMdd; mdd_t *ringMdd; mdd_t *zeroMdd; int nImgComps; boolean term_tautology = FALSE; /* different termination conditions */ boolean term_early = FALSE; boolean term_fixpoint = FALSE; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); resultMdd = mdd_and(sourceMdd, fairStates, 1, 1); if(underapprox != NIL(mdd_t)){ mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1); mdd_free(resultMdd); resultMdd = tmp; } ringMdd = mdd_dup(resultMdd); zeroMdd = mdd_zero(mddMgr); if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } /* if Since is trivially satisfied, or the early termination condition holds*/ { bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1); boolean trivial; trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd, 1, 1, careStatesArray); /* the lequal also takes care of the case where result = 1 */ if(trivial || McCheckEarlyTerminationForUnderapprox(earlyTermination, resultMdd, careStatesArray)){ bdd_free(fairInvariantStates); bdd_free(ringMdd); /* trivially satisfied means that the fixpoint is complete. If this information is requested, give it. */ if(fixpoint != NIL(boolean)) *fixpoint = trivial; return(resultMdd); } bdd_free(fairInvariantStates); } /* The LFP loop */ while (!term_fixpoint && !term_tautology && !term_early) { /* If dclevel is maximal, ringbdd is between the frontier and the reached set */ aMdd = Mc_FsmEvaluateEYFormula(modelFsm, ringMdd, fairStates, careStatesArray, verbosity, dcLevel); mdd_free(ringMdd); bMdd = mdd_and(aMdd, invariantMdd, 1, 1); mdd_free(aMdd); cMdd = mdd_or(resultMdd, bMdd, 1, 1); mdd_free(bMdd); /* Can we stop? The tautology condition can be weakened to cMdd <= careStatesArray */ term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray); if(!term_fixpoint) term_tautology = mdd_is_tautology(cMdd, 1); if(!term_fixpoint && !term_tautology) term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, cMdd, careStatesArray); /* Print some debug info, and set ringmdd */ if (dcLevel >= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; aMdd = mdd_and(resultMdd, targetMdd, 1, 1); if(!mdd_equal(aMdd, zeroMdd)) { array_insert_last(mdd_t *, onionRings, mdd_dup(targetMdd)); mdd_free(aMdd); break; } mdd_free(aMdd); /* add onion ring unless fixpoint reached */ if (!term_fixpoint && onionRings != NIL(array_t)) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ mdd_free(ringMdd); /* Print some debug info */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { static int refCount=0; array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); if (verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(resultMdd, careStatesArray, 1, 1) : mdd_dup(resultMdd); fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount, mdd_size(resultMdd)); fprintf(vis_stdout, "--There are %.0f care states satisfying ES formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "ES satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying ES formula\n", mdd_count_onset(mddMgr, resultMdd, psVars)); } fprintf(vis_stdout, "--ES: %d image computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } mdd_free(zeroMdd); if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return resultMdd; } /* McEvaluateESFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [] Description [] SeeAlso [] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateESFormulaWithGivenTRFAFW( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *sourceMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint, mdd_t *Swin ) { mdd_t *aMdd; mdd_t *bMdd; mdd_t *cMdd; mdd_t *resultMdd; mdd_t *ringMdd; Img_ImageInfo_t *imageInfo; int nImgComps; boolean term_tautology = FALSE; /* different termination conditions */ boolean term_early = FALSE; boolean term_fixpoint = FALSE; nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); resultMdd = mdd_and(sourceMdd, fairStates, 1, 1); if(underapprox != NIL(mdd_t)){ mdd_t *tmp = mdd_or(resultMdd, underapprox, 1, 1); mdd_free(resultMdd); resultMdd = tmp; } ringMdd = mdd_dup(resultMdd); if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } /* if Since is trivially satisfied, or the early termination condition holds*/ { bdd_t *fairInvariantStates = mdd_and(invariantMdd, fairStates, 1, 1); boolean trivial; trivial = mdd_lequal_mod_care_set_array(fairInvariantStates, resultMdd, 1, 1, careStatesArray); /* the lequal also takes care of the case where result = 1 */ if(trivial || McCheckEarlyTerminationForUnderapprox(earlyTermination, resultMdd, careStatesArray)){ bdd_free(fairInvariantStates); bdd_free(ringMdd); /* trivially satisfied means that the fixpoint is complete. If this information is requested, give it. */ if(fixpoint != NIL(boolean)) *fixpoint = trivial; return(resultMdd); } bdd_free(fairInvariantStates); } imageInfo = Fsm_FsmReadOrCreateImageInfoPrunedFAFW(modelFsm, Swin, 0, 1); /* The LFP loop */ while (!term_fixpoint && !term_tautology && !term_early) { /* If dclevel is maximal, ringbdd is between the frontier and the reached set */ aMdd = Img_ImageInfoComputeImageWithDomainVars(imageInfo, ringMdd, ringMdd, careStatesArray); mdd_free(ringMdd); bMdd = mdd_and(aMdd, invariantMdd, 1, 1); mdd_free(aMdd); cMdd = mdd_or(resultMdd, bMdd, 1, 1); mdd_free(bMdd); /* Can we stop? The tautology condition can be weakened to cMdd <= careStatesArray */ term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray); if(!term_fixpoint) term_tautology = mdd_is_tautology(cMdd, 1); if(!term_fixpoint && !term_tautology) term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, cMdd, careStatesArray); /* Print some debug info, and set ringmdd */ if (dcLevel >= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--ES |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- ES |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; /* add onion ring unless fixpoint reached */ if (!term_fixpoint && onionRings != NIL(array_t)) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ /* Img_ImageInfoRecoverFromWinningStrategy(modelFsm, Img_Forward_c); */ Img_ImageInfoFreeFAFW(imageInfo); Img_ImageInfoFree(imageInfo); mdd_free(ringMdd); /* Print some debug info */ if (verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { static int refCount=0; mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); if (verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(resultMdd, careStatesArray, 1, 1) : mdd_dup(resultMdd); fprintf(vis_stdout, "--ES called %d (bdd_size - %d)\n", ++refCount, mdd_size(resultMdd)); fprintf(vis_stdout, "--There are %.0f care states satisfying ES formula\n", mdd_count_onset(mddMgr, tmpMdd, psVars)); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "ES satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying ES formula\n", mdd_count_onset(mddMgr, resultMdd, psVars)); } fprintf(vis_stdout, "--ES: %d image computations\n", Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return resultMdd; } /* McEvaluateESFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [] Description [] SeeAlso [] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateAUFormulaWithGivenTR( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *underapprox, mdd_t *fairStates, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *onionRings, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint ) { mdd_t *aMdd; mdd_t *bMdd; mdd_t *cMdd; mdd_t *resultMdd; mdd_t *ringMdd; boolean term_tautology = FALSE; /* different termination conditions */ boolean term_early = FALSE; boolean term_fixpoint = FALSE; resultMdd = mdd_and(targetMdd, fairStates, 1, 1); ringMdd = mdd_dup(resultMdd); if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } /* The LFP loop */ while (!term_fixpoint && !term_tautology && !term_early) { /* If dclevel is maximal, ringbdd is between the frontier and the reached set */ aMdd = Mc_FsmEvaluateMXFormula(modelFsm, ringMdd, fairStates, careStatesArray, verbosity, dcLevel); bMdd = mdd_and(aMdd, invariantMdd, 1, 1); mdd_free(aMdd); cMdd = mdd_or(resultMdd, bMdd, 1, 1); mdd_free(bMdd); mdd_free(ringMdd); /* Can we stop? The tautology condition can be weakened to cMdd <= careStatesArray */ term_fixpoint = mdd_equal_mod_care_set_array(cMdd, resultMdd, careStatesArray); if(!term_fixpoint) term_tautology = mdd_is_tautology(cMdd, 1); if(!term_fixpoint && !term_tautology) term_early = McCheckEarlyTerminationForUnderapprox(earlyTermination, cMdd, careStatesArray); /* Print some debug info, and set ringmdd */ if (dcLevel >= McDcLevelRchFrontier_c) { mdd_t *tmpMdd = mdd_and(resultMdd, cMdd, 0, 1); ringMdd = bdd_between(tmpMdd, cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "--AU |A(n+1)-A(n)|= %d\t|A(n+1)| = %d\t|between-dc| = %d\n", mdd_size(tmpMdd), mdd_size(resultMdd), mdd_size(ringMdd)); } mdd_free(tmpMdd); } else { ringMdd = mdd_dup(cMdd); if (verbosity == McVerbosityMax_c) { fprintf(vis_stdout, "-- AU |ringMdd| = %d\n", mdd_size(ringMdd)); } } mdd_free(resultMdd); resultMdd = cMdd; /* add onion ring unless fixpoint reached */ if (!term_fixpoint && onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } /* while(!termination) for LFP */ mdd_free(ringMdd); if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return resultMdd; } /**Function******************************************************************** Synopsis [Evaluate states satisfying EG(invariantMdd), given a transition relation] Description [Does the same as Mc_FsmEvaluateEGFormula, minus the hints.] SeeAlso [Mc_FsmEvaluateEGFormula] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateEGFormulaWithGivenTR( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) { int i; array_t *onionRings; boolean useRings; mdd_manager *mddManager; mdd_t *mddOne; mdd_t *iterate; array_t *buchiFairness; int nPreComps; int nIterations; boolean term_fixpoint = FALSE; /* different termination conditions */ boolean term_tautology = FALSE; boolean term_early = FALSE; /* Here's how the onionRingsArrayForDbg works. It is an array of arrays of mdds. It is filled in anew for every pass of the algorithm, that is for every /\_{c inC} EXE(Y U Y*c). There is one entry for every fairness constraint, and this entry contains the onionrings of the EU computation that corresponds to this constraint. */ assert(pOnionRingsArrayForDbg == NIL(array_t *) || *pOnionRingsArrayForDbg == NIL(array_t) || array_n(*pOnionRingsArrayForDbg) == 0); useRings = (pOnionRingsArrayForDbg != NIL(array_t *) && *pOnionRingsArrayForDbg != NIL(array_t)); nIterations = 0; nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c); onionRings = NIL(array_t); mddManager = Fsm_FsmReadMddManager(modelFsm); mddOne = mdd_one(mddManager); /* If an overapproximation of the greatest fixpoint is given, use it. */ if(overapprox != NIL(mdd_t)){ iterate = mdd_and(invariantMdd, overapprox, 1, 1); } else { iterate = mdd_dup(invariantMdd); } /* See if we need to enter the loop at all. If we wanted to test for * early termination here, we should fix the onion rings. In the current * case, we do not need to, since the EG does not hold, and hence a * counterexample does not exist. */ if( mdd_is_tautology(iterate, 0)){ mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0); return(iterate); } /* read fairness constraints */ buchiFairness = array_alloc(mdd_t *, 0); if(modelFairness != NIL(Fsm_Fairness_t)) { if(!Fsm_FairnessTestIsBuchi(modelFairness)) { (void)fprintf(vis_stdout, "** mc error: non-Buechi fairness constraints not supported\n"); array_free(buchiFairness); mdd_free(iterate); mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = FALSE; return NIL(mdd_t); } else { int j; int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0); for (j = 0 ; j < numBuchi; j++) { mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j, careStatesArray, dcLevel); array_insert_last(mdd_t *, buchiFairness, tmpMdd); } } } else { array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager)); } /* GFP. If we know that the result is a subset of a set S, we can conjoin the iterate with that set. We use this to converge faster. */ while (TRUE) { mdd_t *newIterate; /* the new iterate */ nIterations++; newIterate = mdd_dup(iterate); /* for all fairness constraints */ for (i = 0 ; i < array_n(buchiFairness) ; i++) { mdd_t *aMdd, *bMdd, *cMdd, *dMdd; mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i); if(useRings) { onionRings = array_alloc(mdd_t *, 0); array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings); } aMdd = mdd_and(FiMdd, newIterate, 1, 1); bMdd = Mc_FsmEvaluateEUFormula(modelFsm, newIterate, aMdd, NIL(mdd_t), mddOne, careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, onionRings, verbosity, dcLevel, NIL(boolean)); mdd_free(aMdd); cMdd = Mc_FsmEvaluateEXFormula(modelFsm, bMdd, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(bMdd); dMdd = mdd_and(newIterate, cMdd, 1, 1); mdd_free(cMdd); mdd_free(newIterate); newIterate = dMdd; /* invariants that hold here: newiterate <= iterate <= invariant. */ }/* for all fairness constraints */ /* termination */ term_tautology = mdd_is_tautology(newIterate, 0); if(!term_tautology) term_fixpoint = mdd_equal_mod_care_set_array(newIterate, iterate, careStatesArray); if(!term_tautology && !term_fixpoint) term_early = McCheckEarlyTerminationForOverapprox(earlyTermination, newIterate, careStatesArray); if(term_tautology || term_fixpoint || term_early){ mdd_free(iterate); iterate = newIterate; break; /* from the GFP loop */ } /* update iterate */ mdd_free(iterate); iterate = newIterate; if(useRings){ mdd_array_array_free(*pOnionRingsArrayForDbg); *pOnionRingsArrayForDbg = array_alloc(array_t *, 0); } } /* while(true) for gfp */ /* Check if onionrings are OK */ if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { if(useRings){ for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) { int j; mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i); array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg, i); for (j = 0 ; j < array_n(onionRings); j++) { mdd_t *ring = array_fetch(mdd_t *, onionRings, j); if(j == 0) { if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1, careStatesArray)) { fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - "); fprintf(vis_stderr, "inner most ring not in Fi (fairness constraint).\n"); } } if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1, careStatesArray)) { fprintf(vis_stderr, "** mc error: Problem w/ dbg in EG - "); fprintf(vis_stderr, "An onion ring of last EU fails invariant\n"); } } /* for all onionrings in array i */ } /* for all onionringarrays in onionringsarray */ }/* if useRings */ if(verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate); fprintf(vis_stdout, "--There are %.0f care states satisfying EG formula\n", mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd, Fsm_FsmReadPresentStateVars(modelFsm))); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "EG satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying EG formula\n", mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate, Fsm_FsmReadPresentStateVars(modelFsm))); } fprintf(vis_stdout, "--EG: %d iterations, %d preimage computations\n", nIterations, Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps); } mdd_array_free(buchiFairness); mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return iterate; } /* McEvaluateEGFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [Evaluate states satisfying EH(invariantMdd), given a transition relation] Description [Does the same as Mc_FsmEvaluateEHFormula, minus the hints.] SeeAlso [Mc_FsmEvaluateEHFormula] SideEffects [] ******************************************************************************/ mdd_t * McEvaluateEHFormulaWithGivenTR( Fsm_Fsm_t *modelFsm, mdd_t *invariantMdd, mdd_t *overapprox, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t **pOnionRingsArrayForDbg, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, boolean *fixpoint) { int i; array_t *onionRings; boolean useRings; mdd_manager *mddManager; mdd_t *mddOne; mdd_t *iterate; array_t *buchiFairness; int nImgComps; int nIterations; boolean term_fixpoint = FALSE; /* different termination conditions */ boolean term_tautology = FALSE; boolean term_early = FALSE; /* Here's how the onionRingsArrayForDbg works. It is an array of arrays of mdds. It is filled in anew for every pass of the algorithm, that is for every /\_{c inC} EYE(Y S Y*c). There is one entry for every fairness constraint, and this entry contains the onionrings of the ES computation that corresponds to this constraint. */ assert(pOnionRingsArrayForDbg == NIL(array_t *) || *pOnionRingsArrayForDbg == NIL(array_t) || array_n(*pOnionRingsArrayForDbg) == 0); useRings = (pOnionRingsArrayForDbg != NIL(array_t *) && *pOnionRingsArrayForDbg != NIL(array_t)); nIterations = 0; nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c); onionRings = NIL(array_t); mddManager = Fsm_FsmReadMddManager(modelFsm); mddOne = mdd_one(mddManager); /* If an overapproxiamtion of the greatest fixpoint is given, use it. */ if(overapprox != NIL(mdd_t)){ iterate = mdd_and(invariantMdd, overapprox, 1, 1); } else { iterate = mdd_dup(invariantMdd); } /* See if we need to enter the loop at all */ if( mdd_is_tautology(iterate, 0) || McCheckEarlyTerminationForOverapprox(earlyTermination, iterate, careStatesArray)){ mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = mdd_is_tautology(iterate, 0); return(iterate); } /* read fairness constraints */ buchiFairness = array_alloc(mdd_t *, 0); if(modelFairness != NIL(Fsm_Fairness_t)) { if(!Fsm_FairnessTestIsBuchi(modelFairness)) { (void)fprintf(vis_stdout, "** mc error: non-Buechi fairness constraints not supported\n"); array_free(buchiFairness); mdd_free(iterate); mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = FALSE; return NIL(mdd_t); } else { int j; int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0); for (j = 0 ; j < numBuchi; j++) { mdd_t *tmpMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j, careStatesArray, dcLevel); array_insert_last(mdd_t *, buchiFairness, tmpMdd); } } } else { array_insert_last(mdd_t *, buchiFairness, mdd_one(mddManager)); } /* GFP. If we know that the result is a subset of a set S, we can conjoin the iterate with that set. We use this to converge faster. */ while (TRUE) { mdd_t *newIterate; /* the new iterate */ nIterations++; newIterate = mdd_dup(iterate); /* for all fairness constraints */ for (i = 0 ; i < array_n(buchiFairness) ; i++) { mdd_t *aMdd, *bMdd, *cMdd, *dMdd; mdd_t *FiMdd = array_fetch(mdd_t *, buchiFairness, i); if(useRings) { onionRings = array_alloc(mdd_t *, 0); array_insert_last(array_t *, *pOnionRingsArrayForDbg, onionRings); } aMdd = mdd_and(FiMdd, newIterate, 1, 1); bMdd = Mc_FsmEvaluateESFormula(modelFsm, newIterate, aMdd, NIL(mdd_t), mddOne, careStatesArray, MC_NO_EARLY_TERMINATION, NIL(array_t), Mc_None_c, onionRings, verbosity, dcLevel, NIL(boolean)); mdd_free(aMdd); cMdd = Mc_FsmEvaluateEYFormula(modelFsm, bMdd, mddOne, careStatesArray, verbosity, dcLevel); mdd_free(bMdd); dMdd = mdd_and(newIterate, cMdd, 1, 1); mdd_free(cMdd); mdd_free(newIterate); newIterate = dMdd; /* invariants that hold here: newiterate <= iterate <= invariant. */ }/* for all fairness constraints */ /* termination */ term_tautology = mdd_is_tautology(newIterate, 0); if(!term_tautology) term_fixpoint = mdd_equal_mod_care_set_array(newIterate, iterate, careStatesArray); if(!term_tautology && !term_fixpoint) term_early = McCheckEarlyTerminationForOverapprox(earlyTermination, newIterate, careStatesArray); if(term_tautology || term_fixpoint || term_early){ mdd_free(iterate); iterate = newIterate; break; /* from the GFP loop */ } /* update iterate */ mdd_free(iterate); iterate = newIterate; if(useRings){ mdd_array_array_free(*pOnionRingsArrayForDbg); *pOnionRingsArrayForDbg = array_alloc(array_t *, 0); } } /* while(true) for gfp */ /* Check if onionrings are OK */ if(verbosity == McVerbositySome_c || verbosity == McVerbosityMax_c) { if(useRings){ for (i = 0 ; i < array_n(*pOnionRingsArrayForDbg); i++) { int j; mdd_t *Fi = array_fetch(mdd_t *, buchiFairness, i); array_t *onionRings = array_fetch(array_t *, *pOnionRingsArrayForDbg, i); for (j = 0 ; j < array_n(onionRings); j++) { mdd_t *ring = array_fetch(mdd_t *, onionRings, j); if(j == 0) { if(!mdd_lequal_mod_care_set_array(ring, Fi, 1, 1, careStatesArray)) { fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - "); fprintf(vis_stderr, "inner most ring not in Fi (fairness constraint).\n"); } } if(!mdd_lequal_mod_care_set_array(ring, invariantMdd, 1, 1, careStatesArray)) { fprintf(vis_stderr, "** mc error: Problem w/ dbg in EH - "); fprintf(vis_stderr, "An onion ring of last ES fails invariant\n"); } } /* for all onionrings in array i */ } /* for all onionringarrays in onionringsarray */ }/* if useRings */ if(verbosity == McVerbosityMax_c) { mdd_t *tmpMdd = careStatesArray ? mdd_and_array(iterate, careStatesArray, 1, 1) : mdd_dup(iterate); fprintf(vis_stdout, "--There are %.0f care states satisfying EH formula\n", mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), tmpMdd, Fsm_FsmReadPresentStateVars(modelFsm))); #ifdef DEBUG_MC /* The following 2 lines are just for debug */ fprintf(vis_stdout, "EH satisfying minterms :\n"); (void)_McPrintSatisfyingMinterms(tmpMdd, modelFsm); #endif mdd_free(tmpMdd); } else { fprintf(vis_stdout, "--There are %.0f states satisfying EH formula\n", mdd_count_onset(Fsm_FsmReadMddManager(modelFsm), iterate, Fsm_FsmReadPresentStateVars(modelFsm))); } fprintf(vis_stdout, "--EH: %d iterations, %d image computations\n", nIterations, Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps); } mdd_array_free(buchiFairness); mdd_free(mddOne); if(fixpoint != NIL(boolean)) *fixpoint = term_fixpoint || term_tautology; return iterate; } /* McEvaluateEHFormulaWithGivenTR */ /**Function******************************************************************** Synopsis [Frees memory stored at formula corresponding to debug data.] Description [Frees memory stored at formula corresponding to debug data. It is assumed that the debug data is valid. It is an error to call this function on a formula which is not of the type EG or EU.] SideEffects [] ******************************************************************************/ void McFormulaFreeDebugData( Ctlp_Formula_t *formula) { Ctlp_FormulaType type = Ctlp_FormulaReadType(formula); array_t *dbgArray = (array_t *) Ctlp_FormulaReadDebugData(formula); if (type == Ctlp_EU_c || type == Ctlp_FwdU_c) { mdd_array_free(dbgArray); } else if (type == Ctlp_EG_c || type == Ctlp_FwdG_c || type == Ctlp_EH_c) mdd_array_array_free(dbgArray); else { fail("Error - called on non EG/EU formula.\n"); } } /**Function******************************************************************** Synopsis [Print satisfying minterms.] Description [Print satisfying minterms. Just made for debug.] SideEffects [] ******************************************************************************/ void _McPrintSatisfyingMinterms(mdd_t *aMdd, Fsm_Fsm_t *fsm) { array_t *support = Fsm_FsmReadPresentStateVars(fsm); mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm); Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm); int i, n; array_t *mintermArray; mdd_t *aMinterm; n = (int) mdd_count_onset(mddMgr, aMdd, support); mintermArray = mdd_pick_arbitrary_minterms(mddMgr, aMdd, support, n); for (i = 0; i < n; i++) { aMinterm = array_fetch(mdd_t *, mintermArray, i); Mc_MintermPrint(aMinterm, support, network); mdd_free(aMinterm); } array_free(mintermArray); } /**Function******************************************************************** Synopsis [Prints whether model checking passed or failed] Description [Prints whether model checking passed or failed, and if requested, a debug trace.] SideEffects [] ******************************************************************************/ boolean McPrintPassFail( mdd_manager *mddMgr, Fsm_Fsm_t *modelFsm, Mc_FwdBwdAnalysis traversalDirection, Ctlp_Formula_t *ctlFormula, mdd_t *ctlFormulaStates, mdd_t *modelInitialStates, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) { if (mdd_lequal(modelInitialStates, ctlFormulaStates, 1, 1)) { fprintf(vis_stdout, "# MC: formula passed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); fprintf(vis_stdout, "\n"); return TRUE; } else { fprintf(vis_stdout, "# MC: formula failed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); fprintf(vis_stdout, "\n"); if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c) { McFsmDebugFormula(options, ctlFormula,modelFsm, modelCareStatesArray); } return FALSE; } } /**Function******************************************************************** Synopsis [Find Mdd for states satisfying Atomic Formula.] Description [An atomic formula defines a set of states in the following way: it states a designated ``net'' (specified by the full path name) takes a certain value. The net should be purely a function of latches; as a result an evaluation of the net yields a set of states.] SideEffects [] ******************************************************************************/ mdd_t * McModelCheckAtomicFormula( Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula) { mdd_t * resultMdd; mdd_t *tmpMdd; Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm); char *nodeNameString = Ctlp_FormulaReadVariableName(ctlFormula); char *nodeValueString = Ctlp_FormulaReadValueName(ctlFormula); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString); Var_Variable_t *nodeVar; int nodeValue; graph_t *modelPartition; vertex_t *partitionVertex; Mvf_Function_t *MVF; nodeVar = Ntk_NodeReadVariable(node); if (Var_VariableTestIsSymbolic(nodeVar)) { nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString); } else { nodeValue = atoi(nodeValueString); } #if 0 modelPartition = Part_NetworkReadPartition(network); #endif modelPartition = Fsm_FsmReadPartition(modelFsm); if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition, nodeNameString))) { lsGen tmpGen; Ntk_Node_t *tmpNode; array_t *mvfArray; array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0); st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash); array_insert_last(Ntk_Node_t *, tmpRoots, node); Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) { st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED); } mvfArray = Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves, NIL(mdd_t)); MVF = array_fetch(Mvf_Function_t *, mvfArray, 0); array_free(tmpRoots); st_free_table(tmpLeaves); array_free(mvfArray); tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue); resultMdd = mdd_dup(tmpMdd); Mvf_FunctionFree(MVF); } else { MVF = Part_VertexReadFunction(partitionVertex); tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue); resultMdd = mdd_dup(tmpMdd); } if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c && Ntk_NodeTestIsCombOutput(node)) { array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm); mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm)); array_t *supportList; st_table *supportTable = st_init_table(st_numcmp, st_numhash); int i, j; int existIntermediateVars; int mddId; Mvf_Function_t *mvf; vertex_t *vertex; array_t *varBddRelationArray, *varArray; mdd_t *iv, *ivMdd, *relation; for (i = 0; i < array_n(psVars); i++) { mddId = array_fetch(int, psVars, i); st_insert(supportTable, (char *)(long)mddId, NULL); } existIntermediateVars = 1; while (existIntermediateVars) { existIntermediateVars = 0; supportList = mdd_get_support(mgr, resultMdd); for (i = 0; i < array_n(supportList); i++) { mddId = array_fetch(int, supportList, i); if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) { vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId); mvf = Part_VertexReadFunction(vertex); varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf); varArray = mdd_id_to_bdd_array(mgr, mddId); assert(array_n(varBddRelationArray) == array_n(varArray)); for (j = 0; j < array_n(varBddRelationArray); j++) { iv = array_fetch(mdd_t *, varArray, j); relation = array_fetch(mdd_t *, varBddRelationArray, j); ivMdd = bdd_cofactor(relation, iv); mdd_free(relation); tmpMdd = resultMdd; resultMdd = bdd_compose(resultMdd, iv, ivMdd); mdd_free(tmpMdd); mdd_free(iv); mdd_free(ivMdd); } array_free(varBddRelationArray); array_free(varArray); existIntermediateVars = 1; } } array_free(supportList); } st_free_table(supportTable); } return resultMdd; } /* McModelCheckAtomicFormula */ /**Function******************************************************************** Synopsis [Prints out a path from the initial state to a state that violates the invariant. ] Description [Prints out a path from the initial state to a state that violates the invariant. First it checks whether there any onion rings built for this fsm. If the onion rings already exist, it checks whether there is any violation in these rings. If not, additional onion rings are computed.] SideEffects [] ******************************************************************************/ void InvarPrintDebugInformation(Fsm_Fsm_t *modelFsm, array_t *invarFormulaArray, array_t *invarStatesArray, int *resultArray, McOptions_t *options, array_t *hintsStatesArray) { FILE *debugFile = McOptionsReadDebugFile(options); FILE *tmpFile = vis_stdout; extern FILE *vis_stdpipe; mdd_t *outerOnionRing=NIL(mdd_t); mdd_t *reachableBadStates; mdd_t *aBadReachableState, *reachableStates; array_t *aPath; boolean computeReach = TRUE; int ringsUpToDate; array_t *onionRings=NIL(array_t); int i, j; Fsm_RchType_t approxFlag; Ctlp_Formula_t *invarFormula; mdd_t *invarFormulaStates; approxFlag = McOptionsReadInvarApproxFlag(options); if (debugFile) vis_stdpipe = debugFile; else if (McOptionsReadUseMore(options) == TRUE) vis_stdpipe = popen("more", "w"); else vis_stdpipe = vis_stdout; vis_stdout = vis_stdpipe; arrayForEachItem(mdd_t *, invarStatesArray, i, invarFormulaStates) { if ((invarFormulaStates == NIL(mdd_t)) || (resultArray[i] == 1)) continue; onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm); ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm); /* search for onion ring intersecting invarStates' */ if (onionRings != NIL(array_t)) { for (j = 0; j < array_n(onionRings); j++) { outerOnionRing = array_fetch(mdd_t *, onionRings, j); if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) { computeReach = FALSE; break; } } } /* no onion ring found, hence recompute with onion rings */ if (computeReach == TRUE) { Mc_VerbosityLevel verbosity; int debugFlag; int ardc; int dcLevel = McOptionsReadDcLevel(options); verbosity = McOptionsReadVerbosityLevel(options); debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c); if (dcLevel == McDcLevelArdc_c) ardc = 1; else ardc = 0; assert(!ringsUpToDate); reachableStates = Fsm_FsmComputeReachableStates( modelFsm, 0, (int)verbosity , 0, 0, debugFlag, 0, 0, approxFlag, ardc, 0, invarStatesArray, (verbosity > 1), hintsStatesArray); mdd_free(reachableStates); /* find the onion ring with invariant failure */ onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm); if (onionRings == NIL(array_t)) { fprintf(vis_stdout, "Unable to generate onion rings for counterexample.\n"); fprintf(vis_stdout, "Try again with standard (without -A) options.\n"); if (vis_stdout != tmpFile && vis_stdout != debugFile) (void)pclose(vis_stdpipe); vis_stdout = tmpFile; return; } ringsUpToDate = Fsm_FsmTestReachabilityOnionRingsUpToDate(modelFsm); for (j = 0; j < array_n(onionRings); j++) { outerOnionRing = array_fetch(mdd_t *, onionRings, j); if (!mdd_lequal(outerOnionRing, invarFormulaStates, 1, 1)) { break; } } } invarFormula = array_fetch(Ctlp_Formula_t *, invarFormulaArray, i); /* this is the case of true negative */ if (outerOnionRing != NIL(mdd_t)) { /* compute the set of bad states */ if(Fsm_FsmReadFAFWFlag(modelFsm) > 1 && McOptionsReadInvarApproxFlag(options) == Fsm_Rch_Bfs_c) reachableBadStates = mdd_not(invarFormulaStates); else reachableBadStates = mdd_and(invarFormulaStates, outerOnionRing, 0, 1); /* pick one bad state */ aBadReachableState = Mc_ComputeAState(reachableBadStates, modelFsm); mdd_free(reachableBadStates); /* build a path from the initial states to the bad state */ aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings, modelFsm, McGreaterOrEqualZero_c); mdd_free(aBadReachableState); if(McOptionsReadDbgLevel(options)==2) { (void) Mc_PrintPathAiger(aPath, modelFsm, McOptionsReadPrintInputs(options)); } else { (void) fprintf(vis_stdout, "# INV: formula %d failed --- ", i+1); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula)); fprintf(vis_stdout, "\n"); (void) fprintf(vis_stdout, "# INV: calling debugger\n"); if (array_n(aPath) > 1) { (void) fprintf(vis_stdout, "# INV: a sequence of states starting at an initial "); (void) fprintf(vis_stdout, "state leading to a bad state\n"); } else { (void) fprintf(vis_stdout, "# INV: invariant fails at the following initial state\n"); } (void) Mc_PrintPath(aPath, modelFsm, McOptionsReadPrintInputs(options)); } (void) fprintf(vis_stdout, "\n"); McNormalizeBddPointer(aPath); mdd_array_free(aPath); } else { /* Was a false negative */ assert (approxFlag == Fsm_Rch_Oa_c); (void) fprintf(vis_stdout, "# INV: formula passed --- "); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula)); fprintf(vis_stdout, "\n"); } } if (vis_stdout != tmpFile && vis_stdout != debugFile) (void)pclose(vis_stdpipe); vis_stdout = tmpFile; } /* end of InvarPrintDebugInformation */ /**Function******************************************************************** Synopsis [Sort formulae by fsm] Description [Sort formulae by fsm. This creates an array of array of formulae. Each element of the outer array corresponds to an fsm reduced w.r.t the element (array of formulae). Both the array of formulae and the reduced fsms are returned. If there is no reduction, the reduced fsm is set to the totalFsm. While freeing the reduced fsms in the fsmArray, if the reduced fsm is set to total fsm, DO NOT free. ] SideEffects [fsmArray is populated with reduced fsms.] ******************************************************************************/ array_t * SortFormulasByFsm(Fsm_Fsm_t *totalFsm, array_t *invarFormulaArray, array_t *fsmArray, McOptions_t *options) { array_t *resultArray; array_t *formulaArray; array_t *tempArray; int i, j, found; Ctlp_Formula_t *formula; Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm); Fsm_Fsm_t *reducedFsm, *fsm; int reducedFsmPos = -1; if (invarFormulaArray == NIL(array_t)) return invarFormulaArray; if (array_n(invarFormulaArray) == 0) return NIL(array_t); tempArray = array_alloc(array_t *, 0); /* do a semantic check and a quantifier check */ arrayForEachItem (Ctlp_Formula_t *, invarFormulaArray, i, formula) { if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE)){ (void) fprintf(vis_stderr, "** inv error: error in parsing Atomic Formula:\n%s\n", error_string()); error_init(); Ctlp_FormulaFree(formula); continue; } else { if (Ctlp_FormulaTestIsQuantifierFree(formula) == FALSE) { (void) fprintf(vis_stderr, "** inv error: invariant formula refers to path quantifiers\n"); Ctlp_FormulaFree(formula); continue; } } array_insert_last(Ctlp_Formula_t *, tempArray, formula); } if (array_n(tempArray) == 0) { array_free(tempArray); return NIL(array_t); } /* if no -r option, return the original array */ resultArray = array_alloc(array_t *, 0); if (McOptionsReadReduceFsm(options) == FALSE) { array_insert_last(array_t *, resultArray, tempArray); reducedFsm = McConstructReducedFsm(network, tempArray); if (reducedFsm != NIL(Fsm_Fsm_t)) { array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm); } else { array_insert_last(Fsm_Fsm_t *, fsmArray, totalFsm); } return resultArray; } /* We want to minimize per formula only when "-r" option is not specified */ arrayForEachItem (Ctlp_Formula_t *, tempArray, i, formula) { /* Create reduced fsm */ formulaArray = array_alloc(Ctlp_Formula_t *, 0); array_insert_last(Ctlp_Formula_t *, formulaArray, formula); reducedFsm = McConstructReducedFsm(network, formulaArray); if (reducedFsm == NIL(Fsm_Fsm_t)) { /* no reduction */ reducedFsm = totalFsm; } /* Check if fsm already created */ found = 0; for (j = 0; j < array_n(fsmArray); j++) { fsm = array_fetch (Fsm_Fsm_t *, fsmArray, j); found = Fsm_FsmCheckSameSubFsmInTotalFsm(totalFsm, reducedFsm, fsm); if (found) break; } /* If found, add to the existing list. Else add a new reduced fsm */ if (found) { if (reducedFsm != totalFsm) Fsm_FsmFree(reducedFsm); array_free(formulaArray); formulaArray = array_fetch(array_t *, resultArray, j); array_insert_last(Ctlp_Formula_t *, formulaArray, formula); } else { array_insert_last(Fsm_Fsm_t *, fsmArray, reducedFsm); array_insert_last(array_t *, resultArray, formulaArray); if (reducedFsm == totalFsm) reducedFsmPos = array_n(fsmArray)-1; } } array_free(tempArray); /* swap the last reduced fsm with the total fsm. */ if ((reducedFsmPos != -1) && (reducedFsmPos != array_n(fsmArray)-1)) { array_t *totalFsmFormulaArray; assert(array_n(fsmArray) == array_n(resultArray)); fsm = array_fetch(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1); array_insert(Fsm_Fsm_t *, fsmArray, reducedFsmPos, fsm); array_insert(Fsm_Fsm_t *, fsmArray, array_n(fsmArray)-1, totalFsm); formulaArray = array_fetch(array_t *, resultArray, array_n(resultArray)-1); totalFsmFormulaArray = array_fetch(array_t *, resultArray, reducedFsmPos); array_insert(array_t *, resultArray, reducedFsmPos, formulaArray); array_insert(array_t *, resultArray, array_n(resultArray)-1, totalFsmFormulaArray); } return resultArray; } /* end of SortFormulasByFsm */ /**Function******************************************************************** Synopsis [Test if an invariant is violated in the current reachable set of the given FSM.] Description [Test if an invariant is violated in the current reachable set of the given FSM. Returns FALSE if an invariant is violated and TRUE is no invariant is violated.] SideEffects [] ******************************************************************************/ int TestInvariantsInTotalFsm(Fsm_Fsm_t *totalFsm, array_t *invarStatesArray, int shellFlag) { int i; mdd_t *invariant; mdd_t *reachableStates; boolean upToDate = FALSE; /* don't care initialization */ if (shellFlag) { upToDate = Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates); } else { reachableStates = Fsm_FsmReadCurrentReachableStates(totalFsm); } if (reachableStates == NIL(mdd_t)) return TRUE; if (mdd_is_tautology(reachableStates, 0)) return TRUE; arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) { if (invariant == NIL(mdd_t)) continue; if (!mdd_lequal(reachableStates, invariant, 1, 1)) { if (shellFlag) mdd_free(reachableStates); return FALSE; } } if (shellFlag) mdd_free(reachableStates); if ((shellFlag && !upToDate) || (Fsm_FsmReadReachabilityApproxComputationStatus(totalFsm) == Fsm_Rch_Under_c)) return TRUE; else return FALSE; } /**Function******************************************************************** Synopsis [Compute the approximation of the result for EvaluateFormulaRecur.] Description [] SideEffects [None] SeeAlso [EvaluateFormulaRecur] ******************************************************************************/ Ctlp_Approx_t ComputeResultingApproximation( Ctlp_FormulaType formulaType, Ctlp_Approx_t leftApproxType, Ctlp_Approx_t rightApproxType, Ctlp_Approx_t TRMinimization, Mc_EarlyTermination_t *earlyTermination, boolean fixpoint) { Ctlp_Approx_t thisApproxType; switch (formulaType) { case Ctlp_ID_c: case Ctlp_TRUE_c: case Ctlp_FALSE_c: thisApproxType = Ctlp_Exact_c; break; case Ctlp_NOT_c: if (leftApproxType == Ctlp_Incomparable_c) { thisApproxType = Ctlp_Incomparable_c; } else if (leftApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else if (leftApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else { thisApproxType = Ctlp_Exact_c; } break; case Ctlp_AND_c: if (leftApproxType == Ctlp_Incomparable_c || rightApproxType == Ctlp_Incomparable_c || (leftApproxType == Ctlp_Overapprox_c && rightApproxType == Ctlp_Underapprox_c) || (leftApproxType == Ctlp_Underapprox_c && rightApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (rightApproxType == Ctlp_Overapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Overapprox_c; } } else if (leftApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else if (rightApproxType == Ctlp_Underapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Underapprox_c; } } else if (leftApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else { thisApproxType = Ctlp_Exact_c; } break; case Ctlp_EQ_c: case Ctlp_XOR_c: if (leftApproxType != Ctlp_Exact_c || rightApproxType != Ctlp_Exact_c) { thisApproxType = Ctlp_Incomparable_c; } else { thisApproxType = Ctlp_Exact_c; } break; case Ctlp_THEN_c: if (leftApproxType == Ctlp_Incomparable_c || rightApproxType == Ctlp_Incomparable_c || (leftApproxType == Ctlp_Overapprox_c && rightApproxType == Ctlp_Overapprox_c) || (leftApproxType == Ctlp_Underapprox_c && rightApproxType == Ctlp_Underapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (rightApproxType == Ctlp_Overapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Overapprox_c; } } else if (leftApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else if (rightApproxType == Ctlp_Underapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Underapprox_c; } } else if (leftApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else { thisApproxType = Ctlp_Exact_c; } break; case Ctlp_OR_c: if (leftApproxType == Ctlp_Incomparable_c || rightApproxType == Ctlp_Incomparable_c || (leftApproxType == Ctlp_Overapprox_c && rightApproxType == Ctlp_Underapprox_c) || (leftApproxType == Ctlp_Underapprox_c && rightApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (rightApproxType == Ctlp_Overapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Overapprox_c; } } else if (leftApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else if (rightApproxType == Ctlp_Underapprox_c) { if (earlyTermination == MC_NO_EARLY_TERMINATION && leftApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Exact_c; } else { thisApproxType = Ctlp_Underapprox_c; } } else if (leftApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else { thisApproxType = Ctlp_Exact_c; } break; case Ctlp_EX_c: if (leftApproxType == Ctlp_Underapprox_c) { if (TRMinimization == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Incomparable_c; } else { thisApproxType = Ctlp_Underapprox_c; } } else if (leftApproxType == Ctlp_Overapprox_c) { if (TRMinimization == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Incomparable_c; } else { thisApproxType = Ctlp_Overapprox_c; } } else if (leftApproxType == Ctlp_Exact_c) { thisApproxType = TRMinimization; } else { thisApproxType = Ctlp_Incomparable_c; } break; case Ctlp_EU_c: if (leftApproxType == Ctlp_Incomparable_c || rightApproxType == Ctlp_Incomparable_c || (leftApproxType == Ctlp_Overapprox_c && rightApproxType == Ctlp_Underapprox_c) || (leftApproxType == Ctlp_Underapprox_c && rightApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (leftApproxType == Ctlp_Overapprox_c || rightApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else if (leftApproxType == Ctlp_Underapprox_c || rightApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else { thisApproxType = Ctlp_Exact_c; } if (!fixpoint) { if (TRMinimization == Ctlp_Overapprox_c || thisApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Incomparable_c; } else if (thisApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Underapprox_c; } } else { if ((TRMinimization == Ctlp_Overapprox_c && thisApproxType == Ctlp_Underapprox_c) || (TRMinimization == Ctlp_Underapprox_c && thisApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (thisApproxType == Ctlp_Exact_c) { thisApproxType = TRMinimization; } } break; case Ctlp_EG_c: if (leftApproxType == Ctlp_Incomparable_c || rightApproxType == Ctlp_Incomparable_c || (leftApproxType == Ctlp_Overapprox_c && rightApproxType == Ctlp_Underapprox_c) || (leftApproxType == Ctlp_Underapprox_c && rightApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (leftApproxType == Ctlp_Overapprox_c || rightApproxType == Ctlp_Overapprox_c) { thisApproxType = Ctlp_Overapprox_c; } else if (leftApproxType == Ctlp_Underapprox_c || rightApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Underapprox_c; } else { thisApproxType = Ctlp_Exact_c; } if (!fixpoint) { if (TRMinimization == Ctlp_Underapprox_c || thisApproxType == Ctlp_Underapprox_c) { thisApproxType = Ctlp_Incomparable_c; } else if (thisApproxType == Ctlp_Exact_c) { thisApproxType = Ctlp_Overapprox_c; } } else { if ((TRMinimization == Ctlp_Overapprox_c && thisApproxType == Ctlp_Underapprox_c) || (TRMinimization == Ctlp_Underapprox_c && thisApproxType == Ctlp_Overapprox_c)) { thisApproxType = Ctlp_Incomparable_c; } else if (thisApproxType == Ctlp_Exact_c) { thisApproxType = TRMinimization; } } break; case Ctlp_Cmp_c: case Ctlp_Init_c: case Ctlp_FwdU_c: case Ctlp_FwdG_c: case Ctlp_EY_c: /* no early termination and no hints in forward model checking */ thisApproxType = Ctlp_Exact_c; break; default: fail("Encountered unknown type of CTL formula\n"); } return thisApproxType; } /* ComputeResultingApproximation */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Model check formula on given fsm under fairness] Description [This is the recursive part of Mc_FsmEvaluateFormula] Comment [See Mc_EvaluateFormula. The only difference is that EvaluateFormula takes care of global hints, and passes on an extra flag, TRMinimization that indicates how the current TR related to the exact TR. Using this flag, the procedure decides in which field of the formula to store results (states, underapproxStates or overapproxStates) ] SideEffects [] ******************************************************************************/ static mdd_t * EvaluateFormulaRecur( Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Ctlp_Approx_t TRMinimization, Ctlp_Approx_t *resultApproxType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule) { mdd_t *leftMdd = NIL(mdd_t); mdd_t *rightMdd = NIL(mdd_t); mdd_t *result = NIL(mdd_t); mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *careStatesArray = NIL(array_t); mdd_t *tmpMdd; mdd_t *approx = NIL(mdd_t); /* prev computed approx of sat set */ mdd_t *ctlFormulaStates = Ctlp_FormulaObtainStates( ctlFormula ); Ctlp_Approx_t leftApproxType = Ctlp_Exact_c; Ctlp_Approx_t rightApproxType = Ctlp_Exact_c; Ctlp_Approx_t thisApproxType = Ctlp_Exact_c; boolean fixpoint = FALSE; boolean skipRight = FALSE; if ( ctlFormulaStates ) { return ctlFormulaStates; } { Ctlp_Formula_t *leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); if (leftChild) { Mc_EarlyTermination_t *nextEarlyTermination = McObtainUpdatedEarlyTerminationCondition( earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula)); leftMdd = EvaluateFormulaRecur(modelFsm, leftChild, fairStates, fairCondition, modelCareStatesArray, nextEarlyTermination, hintsArray, hintType, TRMinimization, &leftApproxType, verbosity, dcLevel, buildOnionRings, GSHschedule); Mc_EarlyTerminationFree(nextEarlyTermination); if (!leftMdd) { return NIL(mdd_t); } } } {/* read right */ Ctlp_Formula_t *rightChild = Ctlp_FormulaReadRightChild(ctlFormula); if (rightChild) { Mc_EarlyTermination_t *nextEarlyTermination = McObtainUpdatedEarlyTerminationCondition( earlyTermination, leftMdd, Ctlp_FormulaReadType(ctlFormula)); skipRight = Mc_EarlyTerminationIsSkip(nextEarlyTermination); if (!skipRight) { rightMdd = EvaluateFormulaRecur(modelFsm, rightChild, fairStates, fairCondition, modelCareStatesArray, nextEarlyTermination, hintsArray, hintType, TRMinimization, &rightApproxType, verbosity, dcLevel, buildOnionRings, GSHschedule); } Mc_EarlyTerminationFree(nextEarlyTermination); if (!(rightMdd || skipRight)) { if (leftMdd) mdd_free(leftMdd); return NIL(mdd_t); } } }/* read right */ if (modelCareStatesArray != NIL(array_t)) { careStatesArray = modelCareStatesArray; } else { careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr)); } switch (Ctlp_FormulaReadType(ctlFormula)) { case Ctlp_ID_c: assert(!skipRight); result = McModelCheckAtomicFormula(modelFsm, ctlFormula); break; case Ctlp_TRUE_c: assert(!skipRight); result = mdd_one(mddMgr); break; case Ctlp_FALSE_c: assert(!skipRight); result = mdd_zero(mddMgr); break; case Ctlp_NOT_c: assert(!skipRight); result = mdd_not(leftMdd); break; case Ctlp_AND_c: if (skipRight) { result = mdd_dup(leftMdd); rightApproxType = Ctlp_Overapprox_c; } else { result = mdd_and(leftMdd, rightMdd, 1, 1); } break; case Ctlp_EQ_c: assert(!skipRight); result = mdd_xnor(leftMdd, rightMdd); break; case Ctlp_XOR_c: assert(!skipRight); result = mdd_xor(leftMdd, rightMdd); break; case Ctlp_THEN_c: if (skipRight) { result = mdd_dup(leftMdd); rightApproxType = Ctlp_Underapprox_c; } else { result = mdd_or(leftMdd, rightMdd, 0, 1); } break; case Ctlp_OR_c: if (skipRight) { result = mdd_dup(leftMdd); rightApproxType = Ctlp_Underapprox_c; } else { result = mdd_or(leftMdd, rightMdd, 1, 1); } break; case Ctlp_EX_c: assert(!skipRight); result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); break; case Ctlp_EU_c: { array_t *onionRings = NIL(array_t); /* array of mdd_t */ boolean newrings; assert(!skipRight); /* An underapproximation, together with its explanation may be stored. */ approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c ); onionRings = (array_t *) Ctlp_FormulaReadDebugData(ctlFormula); newrings = onionRings == NIL(array_t); if (buildOnionRings){ assert((approx != NIL(mdd_t) && onionRings != NIL(array_t)) || (approx == NIL(mdd_t) && onionRings == NIL(array_t))); if(onionRings == NIL(array_t)) onionRings = array_alloc(mdd_t *, 0); } result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd, approx, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); if(buildOnionRings && newrings) Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, McFormulaFreeDebugData); if(approx != NIL(mdd_t)) mdd_free(approx); break; } case Ctlp_EG_c: { array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */ assert(!skipRight); if(buildOnionRings) arrayOfOnionRings = array_alloc(array_t *, 0); approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Overapprox_c ); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); if(buildOnionRings) Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); if(approx != NIL(mdd_t)) mdd_free(approx); break; } case Ctlp_Cmp_c: { assert(!skipRight); if (Ctlp_FormulaReadCompareValue(ctlFormula) == 0) result = bdd_is_tautology(leftMdd, 0) ? mdd_one(mddMgr) : mdd_zero(mddMgr); else result = bdd_is_tautology(leftMdd, 0) ? mdd_zero(mddMgr) : mdd_one(mddMgr); break; } case Ctlp_Init_c: assert(!skipRight); result = Fsm_FsmComputeInitialStates(modelFsm); break; case Ctlp_FwdU_c: assert(!skipRight); if (buildOnionRings) { array_t *onionRings = array_alloc(mdd_t *, 0); result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd, fairStates, careStatesArray, onionRings, verbosity, dcLevel); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, McFormulaFreeDebugData); } else { if (Ctlp_FormulaReadLeftChild(ctlFormula) && Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(ctlFormula)) == Ctlp_Init_c && Ctlp_FormulaReadRightChild(ctlFormula) && Ctlp_FormulaReadType(Ctlp_FormulaReadRightChild(ctlFormula)) == Ctlp_TRUE_c && Fsm_FsmTestIsReachabilityDone(modelFsm)) { result = mdd_dup(Fsm_FsmReadReachableStates(modelFsm)); break; } result = Mc_FsmEvaluateFwdUFormula(modelFsm, leftMdd, rightMdd, fairStates, careStatesArray, NIL(array_t), verbosity, dcLevel); } break; case Ctlp_FwdG_c: assert(!skipRight); if (buildOnionRings) { array_t *arrayOfOnionRings = array_alloc(array_t *, 0); result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd, fairStates, fairCondition, careStatesArray, arrayOfOnionRings, verbosity, dcLevel); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); } else { result = Mc_FsmEvaluateFwdGFormula(modelFsm, leftMdd, rightMdd, fairStates, fairCondition, careStatesArray, NIL(array_t), verbosity, dcLevel); } break; case Ctlp_EY_c: assert(!skipRight); result = Mc_FsmEvaluateEYFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); break; default: fail("Encountered unknown type of CTL formula\n"); } tmpMdd = mdd_dup(result); thisApproxType = ComputeResultingApproximation( Ctlp_FormulaReadType(ctlFormula), leftApproxType, rightApproxType, TRMinimization, earlyTermination, fixpoint); Ctlp_FormulaSetApproxStates(ctlFormula, tmpMdd, thisApproxType); #ifdef DEBUG_MC /* The following code is just for debugging */ if ((verbosity == McVerbosityMax_c)) { char *type = Ctlp_FormulaGetTypeString(ctlFormula); if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_Cmp_c) { fprintf(vis_stdout, "Info : result for [Cmp]\n"); if (bdd_is_tautology(result, 1)) fprintf(vis_stdout, "TRUE\n"); else fprintf(vis_stdout, "FALSE\n"); } else if (Ctlp_FormulaReadType(ctlFormula) == Ctlp_ID_c) { char *atomic = Ctlp_FormulaConvertToString(ctlFormula); fprintf(vis_stdout, "Info : satisfying minterms for [%s(%s)]:\n", type, atomic); free(atomic); if (bdd_is_tautology(result, 1)) fprintf(vis_stdout, "-- TAUTOLOGY --\n"); else if (bdd_is_tautology(result, 0)) fprintf(vis_stdout, "-- null --\n"); else (void)_McPrintSatisfyingMinterms(result, modelFsm); } else { fprintf(vis_stdout, "Info : satisfying minterms for [%s]:\n", type); if (bdd_is_tautology(result, 1)) fprintf(vis_stdout, "-- TAUTOLOGY --\n"); else if (bdd_is_tautology(result, 0)) fprintf(vis_stdout, "-- null --\n"); else (void)_McPrintSatisfyingMinterms(result, modelFsm); } free(type); } #endif if (modelCareStatesArray == NIL(array_t)) mdd_array_free(careStatesArray); if (leftMdd) mdd_free(leftMdd); if (rightMdd) mdd_free(rightMdd); *resultApproxType = thisApproxType; return result; } /**Function******************************************************************** Synopsis [Reachable(p,q) = FwdUntil(p,q) ^ q] Description [Reachable(p,q) = FwdUntil(p,q) ^ q. This Reachable operation is described in the paper "CTL Model Checking Based on Forward State Traversal" by H. Iwashita et al.] SideEffects [] ******************************************************************************/ static mdd_t * McForwardReachable( 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) { mdd_t *resultMdd, *fuMdd; /* When McForwardReachable is called by Mc_FsmEvaluateFwdEHFormula * with no fairness constraints, this test saves one image * computation. */ if (mdd_is_tautology(fairStates, 1) && mdd_lequal_mod_care_set_array(invariantMdd, targetMdd, 1, 1, careStatesArray)) { resultMdd = mdd_dup(invariantMdd); if (onionRings) { array_insert_last(mdd_t *, onionRings, mdd_dup(resultMdd)); } } else { fuMdd = Mc_FsmEvaluateFwdUFormula(modelFsm, targetMdd, invariantMdd, fairStates, careStatesArray, onionRings, verbosity, dcLevel); resultMdd = mdd_and(fuMdd, invariantMdd, 1, 1); mdd_free(fuMdd); } /* Updates onionRings not to have warning message in * Mc_FsmEvaluateFwdEHFormula since Reachable(p,q) = FwdUntil(p,q) ^ q. */ if (onionRings) { int i; mdd_t *ring, *tmp; for (i = 0 ; i < array_n(onionRings); i++) { tmp = array_fetch(mdd_t *, onionRings, i); ring = mdd_and(tmp, invariantMdd, 1, 1); mdd_free(tmp); array_insert(mdd_t *, onionRings, i, ring); } } return(resultMdd); }