/**CFile*********************************************************************** FileName [mcVacuum.c] PackageName [mc] Synopsis [Functions for vacuity detection.] Description [This file contains the functions implementing vacuity detection for CTL. A CTL formula passes vacuously if it can be strengthened by replacing subformulae by "bottom" (either TRUE or FALSE, depending on the negation parity) without changing the outcome of model checking. Likewise, a formula fails vacuously if it can be weakened by replacing subformulae by top (the negation of bottom) and still fail. Under the assumption that a formula is represented by a parse tree (as opposed to a more general parse DAG) each subformula has a given negation parity. Bottom stands for FALSE if the replaced subformula appears under an even number of negation; it stands for TRUE otherwise. Since all CTL operators besides neagtion are monotonically increasing in their operands, replacing a subformula with bottom result in a stronger property, that is, one that implies the original one. A dual argument applies to replacements with top.

This file contains two algorithms for CTL vacuity detection: The original one of Beer et al. (CAV97), and an extension of the thorough vacuity detection algorithm of Purandare and Somenzi (CAV2002), also known as "CTL vacuum cleaning."

The algorithm of Beer et al. applies to passing weak ACTL (w-ACTL) properties. Roughly speaking, in a w-ACTL property each binary opeartor has at least one child that is a propositional formula. A w-ACTL formula contains a unique smallest important subformula. This is replaced by bottom to produce a witness formula. If the witness formula passes, then the original formula passed vacuously; otherwise, the counterexample to the witness formula is an interesting witness to the original one.

The implementation of the CTL vacuum cleaning algorithm in this file applies to both passing and failing CTL properties. For each formula, replacement is attempted for all leaves, therefore identifying many more cases of vacuity. All the replacements are dealt with in one traversal of the parse tree of the formula, paying attention to combining the cases that produce identical sets of states. For this reason, thorough vacuity detection is usually much cheaper than running as many model checking experiments as there are leaves.] SeeAlso [mcCmd.c mcMc.c] Author [Mitra Purandare] Copyright [Copyright (c) 2002-2005, Regents of the University of Colorado All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ #include "ctlpInt.h" #include "mcInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ #ifndef lint static char rcsid[] UNUSED = "$Id: mcVacuum.c,v 1.1 2005/05/13 05:54:05 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void EvaluateFormulaThoroughVacuity(Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates); static void EvaluateFormulaWactlVacuity(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options); static void PrintVacuousBottom(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity); static void PrintVacuous(mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity); static void ModelcheckAndVacuity(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, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates); static void CreateImportantWitness(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i); static void CreateImportantCounterexample(Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i); static array_t * McMddArrayArrayDup(array_t *arrayBddArray); static void match_top(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement); static void match_bot(Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement); static array_t * GenerateOnionRings(array_t* TempOnionRings, array_t* onionRings); static void FormulaFreeDebugDataVac(Ctlp_Formula_t *formula); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Model checks a formula and checks for its vacuity.] Description [This function dispatches either w-ACTL vacuity detection or CTL vacuum cleaning. In the latter case also takes care of printing results.] SideEffects [Annotates the nodes of the CTL formula with various sets.] SeeAlso [EvaluateFormulaWactlVacuity EvaluateFormulaThoroughVacuity] ******************************************************************************/ void McVacuityDetection( Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options) { if (McOptionsReadBeerMethod(options)) { EvaluateFormulaWactlVacuity(modelFsm, ctlFormula, i, fairStates, fairCond, modelCareStatesArray, earlyTermination, hintsStatesArray, guidedSearchType, modelInitialStates, options); } else { mdd_t *ctlFormulaStates; boolean result; Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options); Mc_DcLevel dcLevel = McOptionsReadDcLevel(options); Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options); int buildOnionRings = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); Mc_FwdBwdAnalysis traversalDirection = McOptionsReadTraversalDirection(options); mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); Ctlp_FormulaNegations(ctlFormula,Ctlp_Even_c); EvaluateFormulaThoroughVacuity(modelFsm, ctlFormula, fairStates, fairCond, modelCareStatesArray, earlyTermination, hintsStatesArray, guidedSearchType, verbosity, dcLevel, buildOnionRings, GSHschedule, modelInitialStates); Mc_EarlyTerminationFree(earlyTermination); if(hintsStatesArray != NIL(array_t)) mdd_array_free(hintsStatesArray); ctlFormulaStates = array_fetch(mdd_t *,ctlFormula->Bottomstates,0); /* user feedback on succes/fail */ result = McPrintPassFail(mddMgr, modelFsm, traversalDirection, ctlFormula, ctlFormulaStates, modelInitialStates, modelCareStatesArray, options, verbosity); if (result == TRUE) { PrintVacuous(modelInitialStates,modelFsm,ctlFormula, traversalDirection,modelCareStatesArray, options, verbosity); } else { PrintVacuousBottom(modelInitialStates,modelFsm,ctlFormula, traversalDirection,modelCareStatesArray, options, verbosity); } FormulaFreeDebugDataVac(ctlFormula); } } /* McVacuityDetection */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Applies vacuum cleaning to a CTL formula.] Description [This function evaluates all possible leaf replacements in parallel and attaches the information to the parse tree. This is a wrapper around ModelcheckAndVacuity; it is mainly responsible of dealing with global/local hints.] SideEffects [Annotates the formula parse tree.] SeeAlso [McVacuityDetection EvaluateFormulaWactlVacuity ModelcheckAndVacuity] ******************************************************************************/ static void EvaluateFormulaThoroughVacuity( Fsm_Fsm_t *fsm, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, array_t *careStatesArray, Mc_EarlyTermination_t *earlyTermination, Fsm_HintsArray_t *hintsArray, Mc_GuidedSearch_t hintType, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRing, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates) { mdd_t *hint; /* to iterate over hintsArray */ int hintnr; /* idem */ assert(hintType == Mc_None_c || hintsArray != NIL(Fsm_HintsArray_t)); if(hintType != Mc_Global_c) { ModelcheckAndVacuity(fsm, ctlFormula, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, Ctlp_Exact_c, verbosity, dcLevel, buildOnionRing, GSHschedule, modelInitialStates); return; } else{ array_t *result = NIL(array_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(array_t)) array_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; ModelcheckAndVacuity(fsm,ctlFormula, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, approx, verbosity, dcLevel, buildOnionRing,GSHschedule, modelInitialStates); /* TBD: take into account (early) termination here */ } Fsm_CleanUpHints(fsm, FALSE, TRUE, (verbosity >= McVerbosityMax_c)); return; } } /* EvaluateFormulaThoroughVacuity */ /**Function******************************************************************** Synopsis [Applies vacuity detection to a w-ACTL formula.] Description [This function applies the algorithm of Beer et al. (CAV97) for vacuity detection of passing w-ACTL formulae. First regular model checking is applied to the given CTL formula. If the formula passes and is in w-ACTL, the witness formula is obtained by replacing the smallest important subformula with bottom. Model checking is then applied to the witness formula. A vacuous pass is reported if the witness property holds. Otherwise, the counterexample is an interesting witness to the original formula, that is, an execution of the model in which the given property holds in a non trivial manner.] SideEffects [Annotates the parse tree of the formula.] SeeAlso [McVacuityDetection EvaluateFormulaThoroughVacuity] ******************************************************************************/ static void EvaluateFormulaWactlVacuity( Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, int i, mdd_t *fairStates, Fsm_Fairness_t *fairCond, array_t *modelCareStatesArray, Mc_EarlyTermination_t *earlyTermination, array_t *hintsStatesArray, Mc_GuidedSearch_t guidedSearchType, mdd_t *modelInitialStates, McOptions_t *options) { mdd_t *ctlFormulaStates; boolean result1, result2; Mc_VerbosityLevel verbosity = McOptionsReadVerbosityLevel(options); Mc_DcLevel dcLevel = McOptionsReadDcLevel(options); Mc_GSHScheduleType GSHschedule = McOptionsReadSchedule(options); int buildOnionRings = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity); Mc_FwdBwdAnalysis traversalDirection = McOptionsReadTraversalDirection(options); mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); ctlFormulaStates = Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, fairCond, modelCareStatesArray, earlyTermination, hintsStatesArray, guidedSearchType, verbosity, dcLevel, buildOnionRings,GSHschedule); Mc_EarlyTerminationFree(earlyTermination); if(hintsStatesArray != NIL(array_t)) mdd_array_free(hintsStatesArray); result1 = McPrintPassFail(mddMgr, modelFsm, traversalDirection, ctlFormula, ctlFormulaStates, modelInitialStates, modelCareStatesArray, options, verbosity); mdd_free(ctlFormulaStates); if (result1 == FALSE) fprintf(vis_stdout, "# MC: Original formula failed. Aborting vacuity detection\n"); else { /* see if we can create a witness formula */ if ((Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_ACTL_c) && (Ctlp_CheckClassOfExistentialFormula(ctlFormula) != Ctlp_QuantifierFree_c)) { fprintf(vis_stdout, "# MC: Not an ACTL Formula. Aborting vacuity detection\n"); } else { if (Ctlp_CheckIfWACTL(Ctlp_FormulaReadOriginalFormula(ctlFormula)) == Ctlp_NONWACTL_c) { fprintf(vis_stdout, "# MC: Not a w-ACTL Formula. Aborting vacuity detection\n"); } else { Ctlp_Formula_t *origFormula, *witFormula; /* We can create a witness formula. Annotate the original * formula with negation parity info and then create a copy * with the smallest important formula replaced by bottom. */ fprintf(vis_stdout, "Model checking the witness formula\n"); origFormula = Ctlp_FormulaReadOriginalFormula(ctlFormula); Ctlp_FormulaNegations(origFormula, Ctlp_Even_c); witFormula = Ctlp_FormulaCreateWitnessFormula(origFormula); ctlFormula = Ctlp_FormulaConvertToExistentialForm(witFormula); /* some user feedback */ if (verbosity != McVerbosityNone_c) { (void)fprintf(vis_stdout, "Checking witness formula[%d] : ", i + 1); Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(ctlFormula)); (void)fprintf (vis_stdout, "\n"); assert(traversalDirection != McFwd_c); } /************** the actual computation *************************/ earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates); ctlFormulaStates = Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates, fairCond, modelCareStatesArray, earlyTermination, hintsStatesArray, guidedSearchType, verbosity, dcLevel, buildOnionRings,GSHschedule); Mc_EarlyTerminationFree(earlyTermination); if(hintsStatesArray != NIL(array_t)) mdd_array_free(hintsStatesArray); /* user feedback on succes/fail */ result2 = McPrintPassFail(mddMgr, modelFsm, traversalDirection, ctlFormula, ctlFormulaStates, modelInitialStates, modelCareStatesArray, options, verbosity); if (result2) (void)fprintf(vis_stdout, "# MC: Vacuous pass\n"); else (void)fprintf(vis_stdout, "# MC: Not a vacuous pass\n"); mdd_free(ctlFormulaStates); Ctlp_FormulaFree(ctlFormula); Ctlp_FormulaFree(witFormula); } } } } /* EvaluateFormulaWactlVacuity */ /**Function******************************************************************** Synopsis [Prints results of vacuum cleaning for a failing CTL property.] Description [For a failing CTL property reports all vacuous failures. If so requested, it also produces interesting counterexamples, that is, computations of the model for which even the weakened property fails.] SideEffects [none] SeeAlso [PrintVacuous] ******************************************************************************/ static void PrintVacuousBottom( mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) { Ctlp_Formula_t *formula,*Int_Counter_CtlFormula; boolean vacuous = FALSE; int i; Ctlp_FormulaType type; if (traversalDirection == McBwd_c){ for (i=1;iTopstates);i++){ if (!(mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Topstates,i),1,1))){ formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1)); type = Ctlp_FormulaReadType(formula); if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) { fprintf(vis_stdout, "# MC: Vacuous failure : "); Ctlp_FormulaPrint(vis_stdout, formula); fprintf(vis_stdout, "\n"); if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){ fprintf(vis_stdout, "# Generating interesting counterexample :\n"); Int_Counter_CtlFormula = Ctlp_FormulaDup(ctlFormula); CreateImportantCounterexample(ctlFormula,Int_Counter_CtlFormula,i); McFsmDebugFormula(options,Int_Counter_CtlFormula,modelFsm, modelCareStatesArray); Ctlp_FormulaFree(Int_Counter_CtlFormula); } vacuous = TRUE; } } } if (vacuous == FALSE){ (void)fprintf(vis_stdout, "# MC: No vacuous failures\n"); } } else{ (void)fprintf(vis_stderr, "# MC: Vacuity can not be checked\n"); } } /* PrintVacuousBottom */ /**Function******************************************************************** Synopsis [Prints results of vacuum cleaning for a passing CTL property.] Description [For a passing CTL property reports all vacuous passes. If so requested, it also produces interesting witnesses, that is, computations of the model for which the original property holds non trivially. (Alternatively, the strengthened property that gave the vacuous pass fails.)] SideEffects [none] SeeAlso [McVacuityDetection PrintVacuousBottom] ******************************************************************************/ static void PrintVacuous( mdd_t *modelInitialStates, Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula, Mc_FwdBwdAnalysis traversalDirection, array_t *modelCareStatesArray, McOptions_t *options, Mc_VerbosityLevel verbosity) { Ctlp_Formula_t *formula,*Int_Wit_CtlFormula; boolean vacuous = FALSE; int i; Ctlp_FormulaType type; if (traversalDirection == McBwd_c) { for (i=1;iBottomstates);i++) { formula = array_fetch(Ctlp_Formula_t *,ctlFormula->leaves,(i-1)); type = Ctlp_FormulaReadType(formula); if (mdd_lequal(modelInitialStates, array_fetch(mdd_t *,ctlFormula->Bottomstates,i),1,1)) { if((type != Ctlp_FALSE_c) && (type != Ctlp_TRUE_c)) { fprintf(vis_stdout, "# MC: Vacuous pass : "); Ctlp_FormulaPrint(vis_stdout, formula); fprintf(vis_stdout, "\n"); vacuous = TRUE; } } else { /* CounterExample Generation */ if (McOptionsReadDbgLevel(options) != McDbgLevelNone_c){ fprintf(vis_stdout, "# MC: Not a vacuous pass : "); Ctlp_FormulaPrint(vis_stdout, formula); fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "# Generating interesting witness :\n"); Int_Wit_CtlFormula = Ctlp_FormulaDup(ctlFormula); CreateImportantWitness(ctlFormula,Int_Wit_CtlFormula,i); McFsmDebugFormula(options,Int_Wit_CtlFormula,modelFsm, modelCareStatesArray); Ctlp_FormulaFree(Int_Wit_CtlFormula); } } } if (vacuous == FALSE){ (void)fprintf(vis_stdout, "# MC: No vacuous passes\n"); } } else{ (void)fprintf(vis_stderr, "# MC: Vacuity cannot be checked\n"); } } /* PrintVacuous */ /**Function******************************************************************** Synopsis [Core algorithm for CTL vacuum cleaning.] Description [This function recursively annotates the parse tree of a CTL formula with the sets of states that satisfy the original formula as well as the various replacements. If debugging is requested, it also stores onion rings. Since it is not known in advance whether the original formula passes or fails, this function computes both bottom and top replacements and tries to use monotonicity properties to accelerate fixpoint computations.] SideEffects [Annotates the formula parse tree.] SeeAlso [EvaluateFormulaThoroughVacuity] ******************************************************************************/ static void ModelcheckAndVacuity( 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, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel, int buildOnionRings, Mc_GSHScheduleType GSHschedule, mdd_t *modelInitialStates) { mdd_t *result = NIL(mdd_t); mdd_t *result_new = NIL(mdd_t); mdd_t *result_bot = NIL(mdd_t); mdd_t *result_top = NIL(mdd_t); mdd_t *result_underapprox = NIL(mdd_t); mdd_manager *mddMgr = Fsm_FsmReadMddManager(modelFsm); array_t *careStatesArray = NIL(array_t); array_t *mddArray_bot = NIL(array_t); array_t *mddArray_top = NIL(array_t); array_t *leavesArray = NIL(array_t); array_t *leavesLeftArray = NIL(array_t); array_t *leavesRightArray = NIL(array_t); array_t *matchfound_bot = NIL(array_t); array_t *matchfound_top = NIL(array_t); array_t *matchelement_bot = NIL(array_t); array_t *matchelement_top = 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_Formula_t *leftChild,*rightChild ; mdd_t *leftMdd = NIL(mdd_t); mdd_t *rightMdd = NIL(mdd_t); 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 approx_decide = FALSE; */ /* We will propagate early termination ONLY to the outmost fixpoint, and only propagate through negation. We should also propagate over other boolean operators, and maybe temporal operators. Propagation over negation is done by complementing the type. */ rightChild = Ctlp_FormulaReadRightChild(ctlFormula); leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); if (leftChild) { if ((leftChild->share) == 1){ Mc_EarlyTermination_t *nextEarlyTermination = McObtainUpdatedEarlyTerminationCondition( earlyTermination, NIL(mdd_t), Ctlp_FormulaReadType(ctlFormula)); ModelcheckAndVacuity(modelFsm, leftChild,fairStates, fairCondition, modelCareStatesArray, nextEarlyTermination, hintsArray, hintType, TRMinimization, verbosity,dcLevel, buildOnionRings, GSHschedule, modelInitialStates); Mc_EarlyTerminationFree(nextEarlyTermination); } } if (rightChild) { if((rightChild->share) == 1) { Mc_EarlyTermination_t *nextEarlyTermination = McObtainUpdatedEarlyTerminationCondition( earlyTermination,NIL(mdd_t) ,Ctlp_FormulaReadType(ctlFormula)); ModelcheckAndVacuity(modelFsm, rightChild, fairStates, fairCondition, modelCareStatesArray, nextEarlyTermination, hintsArray, hintType, TRMinimization, verbosity, dcLevel, buildOnionRings, GSHschedule, modelInitialStates); Mc_EarlyTerminationFree(nextEarlyTermination); } } if (modelCareStatesArray != NIL(array_t)) { careStatesArray = modelCareStatesArray; } else { careStatesArray = array_alloc(mdd_t *, 0); array_insert_last(mdd_t *, careStatesArray, mdd_one(mddMgr)); } mddArray_bot = array_alloc(mdd_t *, 0); mddArray_top = array_alloc(mdd_t *, 0); ctlFormula->share = 2; switch (Ctlp_FormulaReadType(ctlFormula)) { case Ctlp_ID_c :{ result = McModelCheckAtomicFormula(modelFsm, ctlFormula); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); leavesArray = array_alloc(Ctlp_Formula_t *, 0); array_insert(mdd_t *, mddArray_bot , 0, mdd_dup(result)); array_insert(mdd_t *, mddArray_top , 0, result); /* if the formula is an important subformula, we need to find the bottom and top set for it as well. */ if (ctlFormula->negation_parity != Ctlp_EvenOdd_c) { array_insert_last(Ctlp_Formula_t *, leavesArray, ctlFormula); if (ctlFormula->negation_parity == Ctlp_Even_c) { /* if the formula has even negation partity, it should be replaced with FALSE. */ result_bot = mdd_zero(mddMgr); result_top = mdd_one(mddMgr); } else { /* if the formula has odd negation parity, it should be replaced with TRUE. */ result_bot = mdd_one(mddMgr); result_top = mdd_zero(mddMgr); } array_insert_last(mdd_t *,mddArray_bot ,result_bot); array_insert_last(mdd_t *,mddArray_top ,result_top); /* Finding match for bottom sets */ if(mdd_equal(result_bot,array_fetch(mdd_t *, mddArray_bot, 0))){ array_insert(boolean, matchfound_bot, 1 ,TRUE); array_insert(int, matchelement_bot, 1 ,0); } else array_insert(boolean, matchfound_bot, 1 ,FALSE); /* Finding match for top sets */ if(mdd_equal(result_top,array_fetch(mdd_t *, mddArray_top, 0))){ array_insert(boolean, matchfound_top, 1 ,TRUE); array_insert(int, matchelement_top, 1 ,0); } else array_insert(boolean, matchfound_top, 1 ,FALSE); } array_insert(boolean, matchfound_bot, 0 ,FALSE); array_insert(boolean, matchfound_top, 0 ,FALSE); /* only exact set will be there if the formula is not an important subformula. */ ctlFormula->Topstates= mddArray_top; ctlFormula->matchfound_top = matchfound_top; ctlFormula->matchelement_top = matchelement_top; ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_bot = matchfound_bot; ctlFormula->matchelement_bot = matchelement_bot; ctlFormula->leaves = leavesArray; break; } case Ctlp_TRUE_c :{ result = mdd_one(mddMgr); leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); array_insert_last(mdd_t *,mddArray_bot , mdd_dup(result)); array_insert_last(mdd_t *,mddArray_top , result); array_insert(boolean, matchfound_bot, 0 ,FALSE); array_insert(boolean, matchfound_top, 0 ,FALSE); ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_bot = matchfound_bot; ctlFormula->matchelement_bot = matchelement_bot; ctlFormula->Topstates = mddArray_top; ctlFormula->matchfound_top = matchfound_top; ctlFormula->matchelement_top = matchelement_top; ctlFormula->leaves = leavesArray; break; } case Ctlp_FALSE_c :{ result = mdd_zero(mddMgr); leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); array_insert_last(mdd_t *,mddArray_bot ,mdd_dup(result)); array_insert_last(mdd_t *,mddArray_top ,mdd_dup(result)); array_insert(boolean, matchfound_bot, 0 ,FALSE); array_insert(boolean, matchfound_top, 0 ,FALSE); ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_bot = matchfound_bot; ctlFormula->matchelement_bot = matchelement_bot; ctlFormula->Topstates = mddArray_top; ctlFormula->matchfound_top = matchfound_top; ctlFormula->matchelement_top = matchelement_top; ctlFormula->leaves = leavesArray; break; } case Ctlp_NOT_c :{ int i,positionmatch; arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { /* Now we shoud negate the accurate as well bottom mdds */ /* Compute Bottom sets */ if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ result = mdd_not(leftMdd); array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result)); mdd_free(result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); array_insert_last(mdd_t *, mddArray_bot,result); } } arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { /* Compute for Top States */ if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ result = mdd_not(leftMdd); array_insert_last(mdd_t *, mddArray_top, mdd_dup(result)); mdd_free(result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); ctlFormula->Topstates = mddArray_top; ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); break; } case Ctlp_AND_c:{ int number_right_bot = array_n(rightChild->Bottomstates); int number_right_top = array_n(rightChild->Topstates); int number_left_bot = array_n(leftChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int i,positionmatch; leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); /* And operation*/ /* for bottom sets */ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ result = mdd_and(leftMdd, rightMdd, 1, 1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;imatchfound_bot,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); result = mdd_and(leftMdd, rightMdd, 1, 1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch + number_left_bot - 1))); array_insert_last(mdd_t *, mddArray_bot, result); } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); /* for top sets */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ result = mdd_and(leftMdd, rightMdd, 1, 1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;imatchfound_top,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); result = mdd_and(leftMdd, rightMdd, 1, 1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1))); array_insert_last(mdd_t *, mddArray_top, result); } } match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesLeftArray); array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; break; } /* Use of EQ, XOR, THEN, OR is discouraged. Please use convert formula to simple existential form. */ case Ctlp_EQ_c :{ int number_right_bot = array_n(rightChild->Bottomstates); int number_right_top = array_n(rightChild->Topstates); int number_left_bot = array_n(leftChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int i,positionmatch; leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); /* for bottom sets */ rightMdd= array_fetch(mdd_t *,rightChild->Bottomstates,0); arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ result = mdd_xnor(leftMdd,rightMdd); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;imatchfound_bot,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); result = mdd_xnor(leftMdd,rightMdd ); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1))); array_insert_last(mdd_t *, mddArray_bot, result); } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); /* for top sets */ rightMdd= array_fetch(mdd_t *,rightChild->Topstates,0); arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ result = mdd_xnor(leftMdd,rightMdd); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;imatchfound_top,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); result = mdd_xnor(leftMdd,rightMdd ); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch+ number_left_top - 1))); array_insert_last(mdd_t *, mddArray_top, result); } } match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesLeftArray); array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; break; } case Ctlp_XOR_c :{ int number_right_bot = array_n(rightChild->Bottomstates); int number_right_top = array_n(rightChild->Topstates); int number_left_bot = array_n(leftChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int i,positionmatch; leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); /* for bottom sets */ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ result = mdd_xor(leftMdd,rightMdd); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;imatchfound_bot,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); result = mdd_xor(leftMdd,rightMdd ); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot,(positionmatch+ number_left_bot - 1))); array_insert_last(mdd_t *, mddArray_bot, result); } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); /* for top sets */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ result = mdd_xor(leftMdd,rightMdd); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;imatchfound_top,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); result = mdd_xor(leftMdd,rightMdd ); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top,(positionmatch + number_left_top - 1))); array_insert_last(mdd_t *, mddArray_top, result); } } match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesLeftArray); array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; break; } case Ctlp_THEN_c :{ int number_right_bot = array_n(rightChild->Bottomstates); int number_right_top = array_n(rightChild->Topstates); int number_left_bot = array_n(leftChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int i,positionmatch; leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); /* bottom sets */ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ result = mdd_or(leftMdd ,rightMdd,0,1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_bot,positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;imatchfound_bot,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); result = mdd_or(leftMdd,rightMdd ,0,1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1))); array_insert_last(mdd_t *, mddArray_bot, result); } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); /* top sets */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ result = mdd_or(leftMdd ,rightMdd,0,1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *,mddArray_top,positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;imatchfound_top,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); result = mdd_or(leftMdd,rightMdd ,0,1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1))); array_insert_last(mdd_t *, mddArray_top, result); } } match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesLeftArray); array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; break; } case Ctlp_OR_c:{ int number_right_bot = array_n(rightChild->Bottomstates); int number_right_top = array_n(rightChild->Topstates); int number_left_bot = array_n(leftChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int i,positionmatch; leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); /* OR operation*/ /* bottom sets */ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_bot),i) == FALSE){ result = mdd_or(leftMdd,rightMdd,1,1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;imatchfound_bot,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,i); result = mdd_or(leftMdd,rightMdd ,1,1); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, (positionmatch + number_left_bot - 1))); array_insert_last(mdd_t *, mddArray_bot, result); } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); /* top sets */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if (array_fetch(boolean,(leftChild->matchfound_top),i) == FALSE){ result = mdd_or(leftMdd,rightMdd,1,1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;imatchfound_top,i) == FALSE)){ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,i); result = mdd_or(leftMdd,rightMdd ,1,1); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int,rightChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, (positionmatch + number_left_top - 1))); array_insert_last(mdd_t *, mddArray_top, result); } } match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); /* Now attach the array to the ctlFormula */ ctlFormula->Topstates = mddArray_top; ctlFormula->Bottomstates = mddArray_bot; /* ctlFormula->states = array_fetch(mdd_t *, mddArray, 0); */ /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesLeftArray); array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; break; } case Ctlp_EX_c:{ int i,positionmatch; if (ctlFormula->negation_parity == Ctlp_Even_c) { /* bottom sets shoud be computed first i.e underapproximations */ arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } result = array_fetch(mdd_t *, mddArray_bot, 0); /* exact set */ } else{ /* top sets should be computed first i.e., underapproximations */ arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } result = array_fetch(mdd_t *, mddArray_top, 0); /* exact set */ } if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)){ if (ctlFormula->negation_parity == Ctlp_Even_c) { ctlFormula->Bottomstates = mddArray_bot; arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { array_insert_last(mdd_t *, mddArray_top, mdd_dup(result)); } ctlFormula->Topstates = mddArray_top; ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); matchfound_top = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); } else{ ctlFormula->Topstates = mddArray_top; arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { array_insert_last(mdd_t *, mddArray_bot, mdd_dup(result)); } ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_top = array_dup(leftChild->matchfound_bot); ctlFormula->matchelement_top = array_dup(leftChild->matchelement_bot); matchfound_bot = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); } /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); break; } if (ctlFormula->negation_parity == Ctlp_Even_c) { /* top sets */ arrayForEachItem(mdd_t *, leftChild->Topstates, i, leftMdd) { if(array_fetch(boolean,leftChild->matchfound_top,i) == FALSE){ result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); array_insert_last(mdd_t *, mddArray_top, result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_top, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_top, positionmatch)); array_insert_last(mdd_t *, mddArray_top, result); } } } else { arrayForEachItem(mdd_t *, leftChild->Bottomstates, i, leftMdd) { if(array_fetch(boolean,leftChild->matchfound_bot,i) == FALSE){ result = Mc_FsmEvaluateEXFormula(modelFsm, leftMdd, fairStates, careStatesArray, verbosity, dcLevel); array_insert_last(mdd_t *, mddArray_bot, result); } else{ positionmatch = array_fetch(int, leftChild->matchelement_bot, i); result = mdd_dup(array_fetch(mdd_t *, mddArray_bot, positionmatch)); array_insert_last(mdd_t *, mddArray_bot, result); } } } /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); ctlFormula->Topstates = mddArray_top; ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); break; } case Ctlp_EU_c:{ array_t *onionRings = NIL(array_t); array_t *MergeOnionRings = NIL(array_t); array_t *ExactOnionRings = NIL(array_t); array_t *NewOnionRings = NIL(array_t); /* array of mdd_t */ boolean fixpoint; int number_left_bot = array_n(leftChild->Bottomstates); int number_right_bot = array_n(rightChild->Bottomstates); int number_left_top = array_n(leftChild->Topstates); int number_right_top = array_n(rightChild->Topstates); int i; int j = 1; mdd_t *approx_under = NIL(mdd_t); array_t *botrings = NIL(array_t); array_t *toprings = NIL(array_t); leavesArray = array_alloc(Ctlp_Formula_t *, 0); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); approx = Ctlp_FormulaObtainApproxStates( ctlFormula, Ctlp_Underapprox_c ); onionRings = NIL(array_t); if (buildOnionRings) { MergeOnionRings = array_alloc(mdd_t *, 0); botrings = array_alloc(array_t*,0); toprings = array_alloc(array_t*,0); } if (ctlFormula->negation_parity == Ctlp_Even_c) { rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); result_underapprox = mdd_zero(mddMgr); /* Compute the bottom mdds first which provide the underapproximation * to the exact set*/ for(i=1;iBottomstates,i); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, approx, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, j, result); if (buildOnionRings) { if(i==1) { mdd_array_free(MergeOnionRings); MergeOnionRings = mdd_array_duplicate(onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,botrings,j,onionRings); } else { MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,botrings,j,onionRings); } } j++; result_new = mdd_or(result,result_underapprox,1,1); mdd_free(result_underapprox); result_underapprox = result_new; } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;iBottomstates,i); result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd, approx, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, j, result); if (buildOnionRings) { if(i==1) { mdd_array_free(MergeOnionRings); MergeOnionRings = mdd_array_duplicate(onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,botrings,j,onionRings); } else { MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,botrings,j,onionRings); } } j++; result_new = mdd_or(result,result_underapprox,1,1); mdd_free(result_underapprox); result_underapprox = result_new; } /* Use the under approximations to calculate the exact set. */ if (approx != NIL(mdd_t)) { mdd_t *tmp = mdd_or(result_underapprox,approx,1,1); mdd_free(approx); mdd_free(result_underapprox); approx = tmp; } else { approx = result_underapprox; } if (buildOnionRings) { onionRings = array_alloc(mdd_t *, 0); } rightMdd = array_fetch(mdd_t *,rightChild->Bottomstates,0); leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, approx, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result)); array_insert(mdd_t *, mddArray_top, 0, result); if (buildOnionRings) { MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); mdd_array_free(onionRings); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings, McFormulaFreeDebugData); array_insert(array_t *,botrings,0,mdd_array_duplicate(MergeOnionRings)); array_insert(array_t *,toprings,0,mdd_array_duplicate(MergeOnionRings)); } result = array_fetch(mdd_t *,mddArray_bot,0); if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) { leavesLeftArray = leftChild->leaves; array_append(leavesArray,leavesLeftArray); leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; j=1; for(i=1;iBottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); if (buildOnionRings) { ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; } mdd_free(approx); break; /* bottom failing */ } /* top sets * we can use the exact set as an approximation to compute the top * set. */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); j=1; if (buildOnionRings) ExactOnionRings = mdd_array_duplicate(MergeOnionRings); /* Compute the Top mdds now */ for(i=1;iTopstates,i); approx_under = array_fetch(mdd_t *,mddArray_bot,0); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, approx_under, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_top, j, result); if (buildOnionRings) { array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,toprings,j,NewOnionRings); mdd_array_free(onionRings); } j++; } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;iTopstates,i); approx_under = array_fetch(mdd_t *,mddArray_top,0); result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd, approx_under, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_top, j, result); if (buildOnionRings) { array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,toprings,j,NewOnionRings); mdd_array_free(onionRings); } j++; } } else { /* The negation parity is odd. So the top sets will provide underapproximations now. */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); result_underapprox = mdd_zero(mddMgr); /* Compute the top mdds first */ for(i=1;iTopstates,i); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, NIL(mdd_t), fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_top, j, result); if (buildOnionRings){ if(i==1){ mdd_array_free(MergeOnionRings); MergeOnionRings = mdd_array_duplicate(onionRings); array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ } else { array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ MergeOnionRings=GenerateOnionRings(MergeOnionRings,onionRings); } } j++; result_new = mdd_or(result,result_underapprox,1,1); mdd_free(result_underapprox); result_underapprox = result_new; } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); for(i=1;iTopstates,i); result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd, NIL(mdd_t), fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_top, j, result); if (buildOnionRings) { if(j==1){ mdd_array_free(MergeOnionRings); MergeOnionRings = mdd_array_duplicate(onionRings); array_insert(array_t*,toprings,j,onionRings); /* saving the top computation onion rings */ } else { MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); array_insert(array_t*,toprings,j,onionRings); /* saving the bottom computation onion rings */ } } j++; result_new = mdd_or(result,result_underapprox,1,1); mdd_free(result_underapprox); result_underapprox = result_new; } /* Use the under approximations to calculate the exact set. */ if (approx != NIL(mdd_t)) { mdd_t *tmp = mdd_or(result_underapprox,approx,1,1); mdd_free(approx); mdd_free(result_underapprox); approx = tmp; } else { approx = result_underapprox; } if (buildOnionRings) { onionRings = array_alloc(mdd_t *, 0); } /* exact set computation */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, approx, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, 0, mdd_dup(result)); array_insert(mdd_t *, mddArray_top, 0, result); if (buildOnionRings) { MergeOnionRings = GenerateOnionRings(MergeOnionRings,onionRings); mdd_array_free(onionRings); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) MergeOnionRings, McFormulaFreeDebugData); array_insert(array_t *,botrings,0, mdd_array_duplicate(MergeOnionRings)); array_insert(array_t *,toprings,0, mdd_array_duplicate(MergeOnionRings)); } result = array_fetch(mdd_t *,mddArray_bot,0); if(McCheckEarlyTerminationForUnderapprox(earlyTermination,result,careStatesArray)) { leavesLeftArray = leftChild->leaves; array_append(leavesArray,leavesLeftArray); leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; j=1; for(i=1;iBottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; if (buildOnionRings){ ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; } assert(approx != NIL(mdd_t)); mdd_free(approx); break; /* bottom failing */ } if (buildOnionRings) ExactOnionRings = mdd_array_duplicate(MergeOnionRings); /* we can use the exact set as an approximation to compute the bottom set. */ rightMdd = array_fetch(mdd_t *,rightChild->Topstates,0); j=1; /* Compute the botom mdds now */ for(i=1;iBottomstates,i); approx_under = array_fetch(mdd_t *,mddArray_bot,0); result = Mc_FsmEvaluateEUFormula(modelFsm,leftMdd, rightMdd, approx_under, fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, j, result); if (buildOnionRings){ array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); /* saving the bottom computation onion rings */ array_insert(array_t*,botrings,j,NewOnionRings); mdd_array_free(onionRings); } j++; } leftMdd = array_fetch(mdd_t *,leftChild->Bottomstates,0); for(i=1;iBottomstates,i); approx_under = array_fetch(mdd_t *,mddArray_bot,0); result = Mc_FsmEvaluateEUFormula(modelFsm, leftMdd, rightMdd, NIL(mdd_t), fairStates, careStatesArray, earlyTermination, hintsArray, hintType, onionRings, verbosity, dcLevel, &fixpoint); array_insert(mdd_t *, mddArray_bot, j, result); if (buildOnionRings) { array_t *dupOnionRings = mdd_array_duplicate(ExactOnionRings); NewOnionRings = GenerateOnionRings(dupOnionRings,onionRings); array_insert(array_t*,botrings,j,NewOnionRings); mdd_array_free(onionRings); } j++; } } match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; leavesLeftArray = leftChild->leaves; array_append(leavesArray,leavesLeftArray); leavesRightArray = rightChild->leaves; array_append(leavesArray,leavesRightArray); ctlFormula->leaves = leavesArray; if (buildOnionRings) { ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; mdd_array_free(ExactOnionRings); } if(approx != NIL(mdd_t)) mdd_free(approx); /* Can't combine under and overapprox */ if(!fixpoint && TRMinimization == Ctlp_Overapprox_c) TRMinimization = Ctlp_Incomparable_c; break; } case Ctlp_EG_c:{ boolean fixpoint; mdd_t *result_ub; mdd_t *approx_over = NIL(mdd_t) ; int number_bot = array_n(leftChild->Bottomstates); int number_top = array_n(leftChild->Topstates); int i; array_t *arrayOfOnionRings = NIL(array_t); /* array of array of mdd_t* */ array_t *botrings = NIL(array_t); array_t *toprings = NIL(array_t); matchfound_top = array_alloc(boolean, 0); matchfound_bot = array_alloc(boolean, 0); matchelement_top = array_alloc(int, 0); matchelement_bot = array_alloc(int, 0); approx = Ctlp_FormulaObtainApproxStates(ctlFormula, Ctlp_Overapprox_c); if(buildOnionRings) { botrings = array_alloc(array_t*,0); toprings = array_alloc(array_t*,0); } if (approx == NIL(mdd_t)) { result_ub = mdd_one(mddMgr); } else { result_ub = mdd_dup(approx); } if (ctlFormula->negation_parity == Ctlp_Even_c) { /* compute the top sets first which will give us overapproximation to the exact set */ for(i=1;iTopstates,i); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, NIL(mdd_t), fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); array_insert(mdd_t *, mddArray_top, i, result); if(buildOnionRings) { array_insert(array_t*,toprings,i,arrayOfOnionRings); } result_new = mdd_and(result_ub,result,1,1); mdd_free(result_ub); result_ub = result_new; } /* calculate the exact set */ if(buildOnionRings) arrayOfOnionRings = array_alloc(array_t *, 0); leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, NIL(mdd_t), fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result)); array_insert(mdd_t *,mddArray_top,0,mdd_dup(result)); mdd_free(result); if(buildOnionRings) { Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings)); array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings)); } result = array_fetch(mdd_t *,mddArray_bot,0); if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) { leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); for(i=1;iBottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); if (buildOnionRings) { ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; } break;/* top passing */ } /* now calculate the bottom set */ for(i=1;iBottomstates,i); approx_over = array_fetch(mdd_t *,mddArray_bot,0); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx_over, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); array_insert(mdd_t *, mddArray_bot, i, result); if(buildOnionRings) { array_insert(array_t*,botrings,i,arrayOfOnionRings); } } } else { /* compute the bottom sets first which will give us overapproximation to the exact set */ for(i=1;iBottomstates,i); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, NIL(mdd_t), fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); if(buildOnionRings) { array_insert(array_t*,botrings,i,arrayOfOnionRings); } array_insert(mdd_t *, mddArray_bot, i, result); result_new = mdd_and(result_ub,result,1,1); mdd_free(result_ub); result_ub = result_new; } /* calculate the exact set */ if(buildOnionRings){ arrayOfOnionRings = array_alloc(array_t *, 0); } leftMdd = array_fetch(mdd_t *,leftChild->Topstates,0); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, result_ub, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); array_insert(mdd_t *,mddArray_bot,0,mdd_dup(result)); array_insert(mdd_t *,mddArray_top,0,mdd_dup(result)); mdd_free(result); if (buildOnionRings) { Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); array_insert(array_t*,botrings,0,McMddArrayArrayDup(arrayOfOnionRings)); array_insert(array_t*,toprings,0,McMddArrayArrayDup(arrayOfOnionRings)); } result = array_fetch(mdd_t *,mddArray_bot,0); if (McCheckEarlyTerminationForOverapprox(earlyTermination, result, careStatesArray)) { leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); for(i=1;iBottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; match_bot(ctlFormula,mddArray_bot,matchfound_bot,matchelement_bot); match_top(ctlFormula,mddArray_top,matchfound_top,matchelement_top); if (buildOnionRings) { ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; } break; /* top passing */ } /* calculate the top set now */ for(i=1;iTopstates,i); approx_over = array_fetch(mdd_t *,mddArray_bot,0); result = Mc_FsmEvaluateEGFormula(modelFsm, leftMdd, approx, fairStates, fairCondition, careStatesArray, earlyTermination, hintsArray, hintType, &arrayOfOnionRings, verbosity, dcLevel, &fixpoint, GSHschedule); array_insert(mdd_t *, mddArray_top, i, result); if(buildOnionRings) array_insert(array_t*,toprings,i,arrayOfOnionRings); } } mdd_free(result_ub); /* Now attach the array to the ctlFormula */ ctlFormula->Bottomstates = mddArray_bot; ctlFormula->Topstates = mddArray_top; /* Discard previous copies. */ array_free(matchfound_bot); array_free(matchelement_bot); array_free(matchfound_top); array_free(matchelement_top); ctlFormula->matchfound_bot = array_dup(leftChild->matchfound_bot); ctlFormula->matchelement_bot = array_dup(leftChild->matchelement_bot); ctlFormula->matchfound_top = array_dup(leftChild->matchfound_top); ctlFormula->matchelement_top = array_dup(leftChild->matchelement_top); /* find out the leaves attached to this nodes.*/ leavesLeftArray = leftChild->leaves; ctlFormula->leaves = array_dup(leavesLeftArray); if (buildOnionRings) { ctlFormula->BotOnionRings = botrings; ctlFormula->TopOnionRings = toprings; } if(approx != NIL(mdd_t)) mdd_free(approx); /* Can't combine under and overapprox */ if(!fixpoint && TRMinimization == Ctlp_Underapprox_c) TRMinimization = Ctlp_Incomparable_c; break; } case Ctlp_Init_c: result = Fsm_FsmComputeInitialStates(modelFsm); break; default: fail("Encountered unknown type of CTL formula\n"); } tmpMdd = mdd_dup(array_fetch(mdd_t *,mddArray_bot,0)); thisApproxType = ComputeResultingApproximation( Ctlp_FormulaReadType(ctlFormula), leftApproxType, rightApproxType, TRMinimization, earlyTermination, fixpoint); Ctlp_FormulaSetApproxStates(ctlFormula,tmpMdd, TRMinimization); #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); return; } /* ModelcheckAndVacuity */ /**Function******************************************************************** Synopsis [Annotates formula with satisfying sets of i-th replacement.] Description [This function is applied to vacuously passing properties to generate intersting witnesses.] SideEffects [] SeeAlso [CreateImportantCounterexample] ******************************************************************************/ static void CreateImportantWitness( Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i) { Ctlp_Formula_t *rightChild, *leftChild,*OldrightChild, *OldleftChild; int number_left_bot; array_t *onionRings = NIL(array_t); /* array of mdd_t */ array_t *arrayOfOnionRings = NIL(array_t); Ctlp_FormulaType formulaType; formulaType = Ctlp_FormulaReadType(ctlFormula); rightChild = Ctlp_FormulaReadRightChild(ctlFormula); leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula); OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula); if(leftChild) number_left_bot = array_n(OldleftChild->Bottomstates); else number_left_bot = -1; /* don't care */ switch (formulaType) { case Ctlp_EU_c: if(ctlFormula->states != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); #if 0 fprintf(vis_stdout,"Attaching bdd for EU %d",i); bdd_print(ctlFormula->states); mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); #endif onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, McFormulaFreeDebugData); assert(leftChild != NULL && rightChild != NULL); if(istates != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); #if 0 fprintf(vis_stdout,"Attaching bdd for EG %d",i); bdd_print(ctlFormula->states); mdd_array_free(array_fetch(array_t*,OldctlFormula->BotOnionRings,i)); #endif arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->BotOnionRings,i)); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); CreateImportantWitness(OldleftChild,leftChild,i); break; case Ctlp_AX_c: case Ctlp_AG_c: case Ctlp_AF_c: case Ctlp_AU_c: case Ctlp_EX_c: case Ctlp_EF_c: case Ctlp_OR_c: case Ctlp_AND_c: case Ctlp_NOT_c: case Ctlp_THEN_c: case Ctlp_XOR_c: case Ctlp_EQ_c: if(ctlFormula->states != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); #if 0 fprintf(vis_stdout,"Attaching bdd for NOT,THEN %d",i); bdd_print(ctlFormula->states); #endif if(leftChild){ if(istates != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Bottomstates,i)); #if 0 fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i); bdd_print(ctlFormula->states); #endif break; default: break; } } /* CreateImportantWitness */ /**Function******************************************************************** Synopsis [Annotates formula with satisfying sets of i-th replacement.] Description [This function is applied to vacuously failing properties to generate intersting counterexamples.] SideEffects [] SeeAlso [CreateImportantWitness] ******************************************************************************/ static void CreateImportantCounterexample( Ctlp_Formula_t *OldctlFormula, Ctlp_Formula_t *ctlFormula, int i) { Ctlp_Formula_t *rightChild, *leftChild, *OldrightChild, *OldleftChild; int number_left_top; array_t *onionRings = NIL(array_t); /* array of mdd_t */ array_t *arrayOfOnionRings = NIL(array_t); Ctlp_FormulaType formulaType; formulaType = Ctlp_FormulaReadType(ctlFormula); rightChild = Ctlp_FormulaReadRightChild(ctlFormula); leftChild = Ctlp_FormulaReadLeftChild(ctlFormula); OldrightChild = Ctlp_FormulaReadRightChild(OldctlFormula); OldleftChild = Ctlp_FormulaReadLeftChild(OldctlFormula); if(leftChild) number_left_top = array_n(OldleftChild->Topstates); else number_left_top = -1; /* don't care */ switch (formulaType) { case Ctlp_EU_c: if(ctlFormula->states != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); onionRings = mdd_array_duplicate(array_fetch(array_t*,OldctlFormula->TopOnionRings,i)); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *) onionRings, McFormulaFreeDebugData); assert(leftChild != NULL && rightChild != NULL); if(istates != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); arrayOfOnionRings = McMddArrayArrayDup(array_fetch(array_t* ,OldctlFormula->TopOnionRings,i)); Ctlp_FormulaSetDbgInfo(ctlFormula, (void *)arrayOfOnionRings, McFormulaFreeDebugData); CreateImportantCounterexample(OldleftChild,leftChild,i); break; case Ctlp_AX_c: case Ctlp_AG_c: case Ctlp_AF_c: case Ctlp_AU_c: case Ctlp_EX_c: case Ctlp_EF_c: case Ctlp_OR_c: case Ctlp_AND_c: case Ctlp_NOT_c: case Ctlp_THEN_c: case Ctlp_XOR_c: case Ctlp_EQ_c: if(ctlFormula->states != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); if(leftChild){ if(istates != NIL(mdd_t)) mdd_free(ctlFormula->states); ctlFormula->states = mdd_dup(array_fetch(mdd_t *, OldctlFormula->Topstates,i)); #if 0 fprintf(vis_stdout,"Attaching bdd for ID,TRUE %d",i); bdd_print(ctlFormula->states); #endif break; default: break; } } /* CreateImportantCounterexample */ /**Function******************************************************************** Synopsis [Duplicates an array of arrays of MDDs.] Description [Makes sure ref counts are correct.] SideEffects [none] SeeAlso [] ******************************************************************************/ static array_t * McMddArrayArrayDup(array_t *arrayBddArray) { int i; array_t *bddArray, *tmpbddArray; int length; array_t *result; /* put assert for this if (arrayBddArray != NIL(array_t)) { */ length = array_n(arrayBddArray); result = array_alloc(array_t *, length); for (i = 0; i < length; i++) { bddArray = array_fetch(array_t *, arrayBddArray, i); tmpbddArray = mdd_array_duplicate(bddArray); array_insert(array_t *,result,i,tmpbddArray); } return(result); } /* McMddArrayArrayDup */ /**Function******************************************************************** Synopsis [Searches an mdd array of top sets for matches.] Description [] SideEffects [The node of the formula is annotated with the match info.] SeeAlso [match_bot] ******************************************************************************/ static void match_top( Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement) { int i, j, positionmatch; mdd_t *leftMdd1 = NIL(mdd_t); mdd_t *leftMdd2 = NIL(mdd_t); arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){ array_insert(boolean, matchfound, i, FALSE); } arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) { arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) { if((i != 0) && (j != 0) && (i != j)) { if (mdd_equal(leftMdd2, leftMdd1)) { if (array_fetch(boolean, matchfound,i) == TRUE) { if(array_fetch(int, matchelement,i) != j) { positionmatch = array_fetch(int, matchelement, i); array_insert(int, matchelement, j, positionmatch); } } else{ array_insert(int, matchelement, j, i); array_insert(boolean, matchfound, j, TRUE); } } } } } ctlFormula->matchfound_top = matchfound; ctlFormula->matchelement_top = matchelement; return; } /* match_top */ /**Function******************************************************************** Synopsis [Searches an mdd array of bottom sets for matches.] Description [] SideEffects [The node of the formula is annotated with the match info.] SeeAlso [match_top] ******************************************************************************/ static void match_bot( Ctlp_Formula_t *ctlFormula, array_t *mddArray, array_t *matchfound, array_t *matchelement) { int i, j, positionmatch; mdd_t *leftMdd1 = NIL(mdd_t); mdd_t *leftMdd2 = NIL(mdd_t); arrayForEachItem(mdd_t *, mddArray, i, leftMdd1){ array_insert(boolean, matchfound, i, FALSE); } arrayForEachItem(mdd_t *, mddArray, i, leftMdd1) { arrayForEachItem(mdd_t *, mddArray, j, leftMdd2) { if ((i != 0) && (j != 0) && (i != j)) { if (mdd_equal(leftMdd2, leftMdd1)) { if (array_fetch(boolean, matchfound, i) == TRUE) { if (array_fetch(int, matchelement, i) != j) { positionmatch = array_fetch(int, matchelement, i); array_insert(int, matchelement, j, positionmatch); } } else { array_insert(int, matchelement, j, i); array_insert(boolean, matchfound, j ,TRUE); } } } } } ctlFormula->matchfound_bot = matchfound; ctlFormula->matchelement_bot = matchelement; return; } /* match_bot */ /**Function******************************************************************** Synopsis [Merge onion rings for EU operators.] Description [] SideEffects [The first argument is freed.] SeeAlso [ModelcheckAndVacuity] ******************************************************************************/ static array_t * GenerateOnionRings( array_t* TempOnionRings, array_t* onionRings) { array_t* MergeOnionRings; int mdd1number, mdd2number, k; mdd_t *temp,*temp1,*mdd1,*mdd2,*mdd3 = NIL(mdd_t); mdd1number = array_n(TempOnionRings); mdd2number = array_n(onionRings); if(mdd1number == 0) { MergeOnionRings = mdd_array_duplicate(onionRings); array_free(TempOnionRings); return (MergeOnionRings); } MergeOnionRings = array_alloc(mdd_t *, 0); mdd1 = array_fetch(mdd_t *,TempOnionRings,0); mdd2 = array_fetch(mdd_t *,onionRings,0); temp = mdd_or(mdd1,mdd2,1,1); /* Building the core for EU */ array_insert(mdd_t *,MergeOnionRings,0, temp); if(mdd2number>=mdd1number) { for(k=1;ktype != Ctlp_ID_c ){ if (formula->left != NIL(Ctlp_Formula_t)) { FormulaFreeDebugDataVac(formula->left); } if (formula->right != NIL(Ctlp_Formula_t)) { FormulaFreeDebugDataVac(formula->right); } } if (type == Ctlp_EU_c || type == Ctlp_EG_c ) { if (formula->TopOnionRings != NIL(array_t)) { TopOnion = formula->TopOnionRings; for (i = 0; i < array_n(TopOnion); i++) { if (type == Ctlp_EU_c) { mdd_array_free(array_fetch(array_t *, TopOnion, i)); } else if (type == Ctlp_EG_c) mdd_array_array_free(array_fetch(array_t *, TopOnion, i)); } array_free(TopOnion); } if (formula->BotOnionRings != NIL(array_t)) { BottomOnion = formula->BotOnionRings; for (i = 0; i < array_n(BottomOnion); i++) { if (type == Ctlp_EU_c) { mdd_array_free(array_fetch(array_t *, BottomOnion, i)); } else if (type == Ctlp_EG_c) mdd_array_array_free(array_fetch(array_t *, BottomOnion, i)); } array_free(BottomOnion); } } } /* FormulaFreeDebugDataVac */