static boolean 
AtomicFormulaCheckSemantics(
  Ctlp_Formula_t * formula, 
  Ntk_Network_t * network, 
  boolean  inputsAllowed 
)
Perform simple static semantic checks on formula.

See Also Mc_FormulaStaticSemanticCheckOnNetwork
Defined in mcUtil.c 

static int 
CommandInv(
  Hrc_Manager_t ** hmgr, 
  int  argc, 
  char ** argv 
)
checks that all reachable states in flattened network satisfy invariants

See Also CommandMc
Defined in mcMc.c 

static int 
CommandLe(
  Hrc_Manager_t ** hmgr, 
  int  argc, 
  char ** argv 
)
Check to see if language of FSM is empty.

Defined in mcMc.c 

static int 
CommandMc(
  Hrc_Manager_t ** hmgr, 
  int  argc, 
  char ** argv 
)
First argument is a file containing a set of CTL formulas - see ctlp package for grammar. Second argument is an FSM that we will check the formulas on. Formulas are checked by calling the recursive function Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.

See Also CommandInv
Defined in mcMc.c 

static void 
DebugBoolean(
  McOptions_t * options, 
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug a Boolean formula

Defined in mcDbg.c 

static McPath_t * 
DebugEG(
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray, 
  McOptions_t * options 
)
Debug a formula of type EG at specified state. It is assumed that state fails formula. Refer to Clarke et al DAC 1995 for details of the algorithm.

Defined in mcDbg.c 

static McPath_t * 
DebugEU(
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug a formula of type EU at specified state. It is assumed that state fails formula.

Defined in mcDbg.c 

static McPath_t * 
DebugEX(
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug a formula of type EX at specified state. It is assumed that aState satisfies the EX formula.

Defined in mcDbg.c 

static void 
DebugID(
  McOptions_t * options, 
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm 
)
Debug an Atomic Formula. As per the semantics of fair CTL, a state satisfies an Atomic Formula just in case the given wire computes the appropriate Boolean function on that state as input. The state has to be fair; however we do NOT justify the fairness by printing a path to a fair cycle. THe user can achieve this effect by adding ANDing in a formula EG TRUE.

Defined in mcDbg.c 

static void 
DebugTrueFalse(
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm 
)
Debug a TRUE/FALSE formula

Defined in mcDbg.c 

mdd_t * 
EvaluateEGFormulaWithGivenTR(
  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 
)
Does the same as Mc_FsmEvaluateEGFormula, minus the hints.

See Also Mc_FsmEvaluateEGFormula
Defined in mcMc.c 

mdd_t * 
EvaluateEUFormulaWithGivenTR(
  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 
)
Does the same as Mc_FsmEvaluateEUFormula, minus the hints.

See Also Mc_FsmEvaluateEUFormula
Defined in mcMc.c 

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, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel, 
  int  buildOnionRings 
)
This is the recursive part of Mc_FsmEvaluateFormula

Defined in mcMc.c 

static void 
FreeArrayOfArraysOfMdds(
  array_t * mddarrayarray 
)
Frees the array mddarrayarray, the arrays it contains, and the mdds they in turn contain. The array, or any of its constituents, can be NIL. Any NIL arrays are just ignored.

See Also mdd_array_free
Defined in mcMc.c 

static void 
FsmPathDebugAFFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * counterExamplePath, 
  array_t * careSetArray 
)
Debug a AF formula

Defined in mcDbg.c 

static void 
FsmPathDebugAGFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * counterExamplePath, 
  array_t * careSetArray 
)
Debugs an AG formula. What it really wants is a formula of the form !EF! phi, that was converted from the formula AG phi, with all the converted pointers set as required: the top ! points to the original AG formula, and top node of phi points to the original phi.

Defined in mcDbg.c 

static void 
FsmPathDebugAUFormula(
  McOptions_t * options, 
  mdd_t * aState, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug a AU formula

Defined in mcDbg.c 

static void 
FsmPathDebugAXFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * counterExamplePath, 
  array_t * careSetArray 
)
Debug a AX formula

Defined in mcDbg.c 

static void 
FsmPathDebugEFFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * witnessPath, 
  array_t * careSetArray 
)
Debug a EF formula

Defined in mcDbg.c 

static void 
FsmPathDebugEGFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * witnessPath, 
  array_t * careSetArray 
)
Debug a path for EG type formula.

Defined in mcDbg.c 

static void 
FsmPathDebugEUFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * witnessPath, 
  array_t * careSetArray 
)
Debug a path for EU type formula.

Defined in mcDbg.c 

static void 
FsmPathDebugEXFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * witnessPath, 
  array_t * careSetArray 
)
Debug a path for EX type formula.

Defined in mcDbg.c 

static void 
FsmPathDebugFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  McPath_t * witnessPath, 
  array_t * careSetArray 
)
Debug a formula of the form EX, EG, EU, EF.

Defined in mcDbg.c 

static void 
FsmStateDebugConvertedFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug a converted formula

Defined in mcDbg.c 

static void 
InvarPrintDebugInformation(
  Fsm_Fsm_t * modelFsm, 
  array_t * invarFormulaArray, 
  array_t * invarStatesArray, 
  int * resultArray, 
  McOptions_t * options, 
  array_t * hintsStatesArray 
)
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.

Defined in mcMc.c 

McPath_t * 
McBuildFairPath(
  mdd_t * startState, 
  mdd_t * invariantStates, 
  array_t * arrayOfOnionRings, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel, 
  Mc_FwdBwdAnalysis  fwdBwd 
)
Build fair path starting from aState, using given array of onion rings. Each member of this array of onion rings is an array of rings of states leading to a fairness constraint. Function returns an McPath_t, which consists of a stem array which is a sequence of states, and a path array which is a sequence of states starting from the last state in stem array, leading back to a state existing in stem array. In this sense, it is confusing, since the "cycle" is not a true cycle (it just completes a cycle).

Defined in mcDbg.c 

boolean 
McCheckEarlyTerminationForOverapprox(
  Mc_EarlyTermination_t * earlyTermination, 
  mdd_t * overApprox, 
  array_t * careStatesArray 
)
Check if an overapproximation of the evaluation guarantees that the early termination conditions hold, modulo a care set modeled by an implicitly conjoined array of bdds. If we are looking for ALL of ETstates, then we are done if we have overapprox is not a superset of ETstates, because the exact set will not hold all of ETstates. If we are looking for SOME of ETstates, we are done if overapprox is disjoint from ETstates, because that means that the exact set is also disjoint from ETstates. If earlyTermination == MC_NO_EARLY_TERMINATION, the result of the function is false.

Defined in mcUtil.c 

boolean 
McCheckEarlyTerminationForUnderapprox(
  Mc_EarlyTermination_t * earlyTermination, 
  mdd_t * underApprox, 
  array_t * careStatesArray 
)
Check if an underapproximation of the evaluation guarantees that the early termination conditions hold, modulo a care set modeled by an implicitly conjoined array of bdds. If we are looking for ALL of ETstates, then we are done if underapprox subseteq ETstates, because that implies exactset subseteq ETstates. If we are looking for SOME of ETstates, we are done if underapprox and ETstates overlap, because that means that the exact set and ETstates also overlap. If you pass in MC_NO_EARLY_TERMINATION, the result of the function is false.

Defined in mcUtil.c 

int 
McCommandInitState(
  Hrc_Manager_t ** hmgr, 
  int  argc, 
  char ** argv 
)
Write resettability condition as a CTL formula

Defined in mcUtil.c 

Mc_EarlyTermination_t * 
McComplementEarlyTerminationCondition(
  Mc_EarlyTermination_t * earlyTermination 
)
Change the type of the early termination condition: all becomes some and vice versa. The complement of MC_NO_EARLY_TERMINATION is itself.

Defined in mcUtil.c 

array_t * 
McCompletePathBwd(
  mdd_t * aState, 
  mdd_t * bState, 
  mdd_t * invariantStates, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from bState and does backward reachability till it hits aState or a fixed point.

Defined in mcUtil.c 

array_t * 
McCompletePathFwd(
  mdd_t * aState, 
  mdd_t * bState, 
  mdd_t * invariantStates, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members. This function starts from aState and does forward reachability till it hits bState or a fixed point.

Defined in mcUtil.c 

int 
McComputeOnionRingsWithClosestCore(
  mdd_t * aState, 
  array_t * arrayOfOnionRings, 
  Fsm_Fsm_t * modelFsm 
)
Search the given array of "Onion Rings" for the Onion Rings with the core closest to specified state. By "Onion Rings" we refer to an array of sets of states (so arrayOfOnionRings is an array of arrays of states). The first member of a set of onion rings is referred to as the "core". The "Onion Rings" array has the property that the first set is all states that can reach the core (this may be mod a care set like the reached states). The succesive sets are those which can reach the core in successively fewer iterations. We find the i with the smallest index j for which arrayOfOnionRings[i

Defined in mcUtil.c 

Fsm_Fsm_t * 
McConstructReducedFsm(
  Ntk_Network_t * network, 
  array_t * ctlFormulaArray 
)
Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.

Defined in mcUtil.c 

array_t * 
McConvertMintermToValueArray(
  mdd_t * aMinterm, 
  array_t * aSupport, 
  mdd_manager * mddMgr 
)
Convert a minterm to an array of integers

Defined in mcUtil.c 

array_t * 
McCreateJoinedPath(
  array_t * aPath, 
  array_t * bPath 
)
Utility function - joins two paths. Note that the joins is done by adding the elements of the second array starting from the first element onwards.

See Also McCreateMergedPath
Defined in mcUtil.c 

array_t * 
McCreateMergedPath(
  array_t * aPath, 
  array_t * bPath 
)
Utility function - merges two paths. Note that the merge is done by adding the elements of the second array starting from the second element onwards. This is because we often have to merge paths where the end point of the first is the starting point of the second.

Defined in mcUtil.c 

Mc_EarlyTermination_t * 
McEarlyTerminationAlloc(
  Mc_SomeOrAll_t  someOrAll, 
  mdd_t * states 
)
Allocate an earlytermination struct and initialize with arguments

Defined in mcUtil.c 

void 
McEarlyTerminationFree(
  Mc_EarlyTermination_t * earlyTermination 
)
Free an earlytermination struct (you are allowed to pass MC_NO_EARLY_TERMINATION, or NULL, and it will have no effect.

Defined in mcUtil.c 

void 
McFormulaFreeDebugData(
  Ctlp_Formula_t * formula 
)
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.

Defined in mcMc.c 

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 
)
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.

Defined in mcMc.c 

int 
McFsmDebugFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug CTL formula in existential normal form. The extent to which debug information is generated is a function of options settings. The debugger works with ctlformula, but uses the pointers back to the original formula that it was converted from, to give the user more sensible feedback. To do this, it relies on a specific translation: only EU, AU, AF, AG, and AX are converted. Hence, the only times that the converted bit is set, we have a conversion of one of these formulas, and the operator is either EU, or negation. in the latter case, we can conclude from the child of the negation what formula we converted from:E means AU, EG means AF, EU means AG, and OR means AU.

Side Effects Affects vis_stdpipe

Defined in mcDbg.c 

void 
McFsmStateDebugFormula(
  McOptions_t * options, 
  Ctlp_Formula_t * ctlFormula, 
  mdd_t * aState, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray 
)
Debug CTL formula in existential normal form at state aState. Formula is assumed to have been CONVERTED to existential normal form.

Defined in mcDbg.c 

mdd_t * 
McGetSuccessorInTarget(
  mdd_t * aState, 
  mdd_t * targetStates, 
  Fsm_Fsm_t * modelFsm 
)
Obtain a successor of aState which is in targetStates

Defined in mcUtil.c 

McOptions_t * 
McOptionsAlloc(
    
)
Allocate an McOptions_t struct.

Defined in mcUtil.c 

void 
McOptionsFree(
  McOptions_t * options 
)
Free an McOptions_t struct.

Defined in mcUtil.c 

Fsm_ArdcOptions_t * 
McOptionsReadArdcOptions(
  McOptions_t * options 
)
Read ARDC options.

Defined in mcUtil.c 

FILE * 
McOptionsReadCtlFile(
  McOptions_t * options 
)
Return ctl file set at options.

Defined in mcUtil.c 

McDbgLevel 
McOptionsReadDbgLevel(
  McOptions_t * options 
)
Return Dbg level set at options.

Defined in mcUtil.c 

Mc_DcLevel 
McOptionsReadDcLevel(
  McOptions_t * options 
)
Return Dbg level of options.

Defined in mcUtil.c 

FILE * 
McOptionsReadDebugFile(
  McOptions_t * options 
)
Return debug file set at options.

Defined in mcUtil.c 

Mc_FwdBwdAnalysis 
McOptionsReadFwdBwd(
  McOptions_t * options 
)
Read whether to use forward or backward analysis

Defined in mcUtil.c 

FILE * 
McOptionsReadGuideFile(
  McOptions_t * options 
)
Return filepointer for guide file (NULL if guided search is disabled)

Defined in mcUtil.c 

Fsm_RchType_t 
McOptionsReadInvarApproxFlag(
  McOptions_t * options 
)
Read reachability analysis type for check_invariant

Defined in mcUtil.c 

boolean 
McOptionsReadInvarOnionRingsFlag(
  McOptions_t * options 
)
Read onion rings flag for check_invariant

Defined in mcUtil.c 

int 
McOptionsReadPrintInputs(
  McOptions_t * options 
)
Read print inputs in debug trace.

Defined in mcUtil.c 

int 
McOptionsReadReduceFsm(
  McOptions_t * options 
)
Read use CTL formula specific reduction.

Defined in mcUtil.c 

int 
McOptionsReadSimValue(
  McOptions_t * options 
)
Read sim flag at options.

Defined in mcUtil.c 

int 
McOptionsReadTimeOutPeriod(
  McOptions_t * options 
)
Return time out period set at options.

Defined in mcUtil.c 

Mc_FwdBwdAnalysis 
McOptionsReadTraversalDirection(
  McOptions_t * options 
)
Read whether to use forward or backward traversal.

Defined in mcUtil.c 

int 
McOptionsReadUseFormulaTree(
  McOptions_t * options 
)
Read use of CTL formula tree.

Defined in mcUtil.c 

int 
McOptionsReadUseMore(
  McOptions_t * options 
)
Read use more as pipe at options.

Defined in mcUtil.c 

Mc_VerbosityLevel 
McOptionsReadVerbosityLevel(
  McOptions_t * options 
)
Return Verbosity level of options.

Defined in mcUtil.c 

void 
McOptionsSetArdcOptions(
  McOptions_t * options, 
  Fsm_ArdcOptions_t * ardcOptions 
)
Set ARDC options.

Defined in mcUtil.c 

void 
McOptionsSetCtlFile(
  McOptions_t * options, 
  FILE * file 
)
Set CTL File at options.

Defined in mcUtil.c 

void 
McOptionsSetDbgLevel(
  McOptions_t * options, 
  McDbgLevel  dbgLevel 
)
Set Dbg level at options.

Defined in mcUtil.c 

void 
McOptionsSetDcLevel(
  McOptions_t * options, 
  Mc_DcLevel  dcLevel 
)
Set Dc level at options.

Defined in mcUtil.c 

void 
McOptionsSetDebugFile(
  McOptions_t * options, 
  FILE * file 
)
Set Debug File at options.

Defined in mcUtil.c 

void 
McOptionsSetFwdBwd(
  McOptions_t * options, 
  Mc_FwdBwdAnalysis  fwdBwd 
)
Set use forward or backward analysis

Defined in mcUtil.c 

void 
McOptionsSetGuideFile(
  McOptions_t * options, 
  FILE * guideFile 
)
Set guided search file (set to NULL if no guided search)

Defined in mcUtil.c 

void 
McOptionsSetInvarApproxFlag(
  McOptions_t * options, 
  Fsm_RchType_t  approxFlag 
)
Set reachability analysis type

Defined in mcUtil.c 

void 
McOptionsSetInvarOnionRingsFlag(
  McOptions_t * options, 
  int  shellFlag 
)
Set a flag to store onion rings during invariant checking.

Defined in mcUtil.c 

void 
McOptionsSetPrintInputs(
  McOptions_t * options, 
  boolean  printInputs 
)
Set print inputs flag

Defined in mcUtil.c 

void 
McOptionsSetReduceFsm(
  McOptions_t * options, 
  boolean  reduceFsm 
)
Set reduce fsm flag

Defined in mcUtil.c 

void 
McOptionsSetSimValue(
  McOptions_t * options, 
  boolean  simValue 
)
Set sim flag at options.

Defined in mcUtil.c 

void 
McOptionsSetTimeOutPeriod(
  McOptions_t * options, 
  int  timeOutPeriod 
)
Set ime out periopd at options.

Defined in mcUtil.c 

void 
McOptionsSetTraversalDirection(
  McOptions_t * options, 
  Mc_FwdBwdAnalysis  fwdBwd 
)
Set use forward or backward traversal

Defined in mcUtil.c 

void 
McOptionsSetUseFormulaTree(
  McOptions_t * options, 
  boolean  useFormulaTree 
)
Set use formula tree flag

Defined in mcUtil.c 

void 
McOptionsSetUseMore(
  McOptions_t * options, 
  boolean  useMore 
)
Set use more pipe flag at options.

Defined in mcUtil.c 

void 
McOptionsSetVerbosityLevel(
  McOptions_t * options, 
  Mc_VerbosityLevel  verbosityLevel 
)
Set Verbosity at options.

Defined in mcUtil.c 

McPath_t * 
McPathAlloc(
    
)
Allocate a Path Struct

Defined in mcUtil.c 

void 
McPathFree(
  McPath_t * aPath 
)
Free a Path Struct

Defined in mcUtil.c 

McPath_t * 
McPathNormalize(
  McPath_t * aPath 
)
Utility function - convert McPath_t to normal form. A normal McPath_t is one where the stem leads to a state, which then returns it self in the cycle.

Defined in mcUtil.c 

array_t * 
McPathReadCycleArray(
  McPath_t * aPath 
)
Obtain cycle of fair path

Defined in mcUtil.c 

array_t * 
McPathReadStemArray(
  McPath_t * aPath 
)
Obtain stem of fair path

Defined in mcUtil.c 

void 
McPathSetCycleArray(
  McPath_t * aPath, 
  array_t * cycleArray 
)
Set cycle of fair path

Defined in mcUtil.c 

void 
McPathSetStemArray(
  McPath_t * aPath, 
  array_t * stemArray 
)
Set stem of fair path

Defined in mcUtil.c 

int 
McPrintSimPath(
  FILE * outputFile, 
  array_t * aPath, 
  Fsm_Fsm_t * modelFsm 
)
Print path as sim trace

Defined in mcUtil.c 

void 
McPrintSupport(
  mdd_t * aMdd, 
  mdd_manager * mddMgr, 
  Ntk_Network_t * aNetwork 
)
Print Support of Function

Defined in mcUtil.c 

void 
McPrintTransition(
  mdd_t * aState, 
  mdd_t * bState, 
  mdd_t * uInput, 
  mdd_t * vInput, 
  array_t * stateSupport, 
  array_t * inputSupport, 
  boolean  printInputs, 
  Fsm_Fsm_t * modelFsm, 
  int  seqNumber 
)
Print a transition to vis_stdout. The transition is supposed to be from aState to bState on input vInput. If uInput is not NIL, instead of printing vInput, we only print the places where it differs from uInput. If there is no difference anywhere, we print "-Unchanged-". Similarly, we print only the incremental difference from aState to bState; if there is none, we print "-Unchanged-". If aState is NIL we simply print bState and return.

Defined in mcUtil.c 

boolean 
McQueryContinue(
  char * query 
)
Query user to continue.

Defined in mcUtil.c 

array_t * 
McRemoveIndexedOnionRings(
  int  index, 
  array_t * arrayOfOnionRings 
)
Remove array indexed by index from array of arrays. Does NOT free the input arrayOfOnionRings.

Defined in mcUtil.c 

void 
McStateFailsFormula(
  mdd_t * aState, 
  Ctlp_Formula_t * formula, 
  McDbgLevel  debugLevel, 
  Fsm_Fsm_t * modelFsm 
)
Print message saying given state fails formula.

Defined in mcUtil.c 

void 
McStatePassesFormula(
  mdd_t * aState, 
  Ctlp_Formula_t * formula, 
  McDbgLevel  debugLevel, 
  Fsm_Fsm_t * modelFsm 
)
Print message saying given state passes formula.

Defined in mcUtil.c 

void 
McStatePassesOrFailsFormula(
  mdd_t * aState, 
  Ctlp_Formula_t * formula, 
  int  pass, 
  McDbgLevel  debugLevel, 
  Fsm_Fsm_t * modelFsm 
)
Utility function - prints state passes or fails formula

Defined in mcUtil.c 

char * 
McStatePrintAsFormula(
  mdd_t * aMinterm, 
  array_t * aSupport, 
  Fsm_Fsm_t * modelFsm 
)
Return a CTL formula for a minterm.

Defined in mcUtil.c 

boolean 
McStateSatisfiesFormula(
  Ctlp_Formula_t * aFormula, 
  mdd_t * aState 
)
Check to see if aState lies in set of states satisfying aFormula

Defined in mcUtil.c 

boolean 
McStateTestMembership(
  mdd_t * aState, 
  mdd_t * setOfStates 
)
Tests aState is a member of setOfStates

Defined in mcUtil.c 

array_t * 
Mc_BuildPathFromCore(
  mdd_t * aState, 
  array_t * onionRings, 
  Fsm_Fsm_t * modelFsm, 
  Mc_PathLengthType  PathLengthType 
)
Build Path starting at a Core state (a state in the first onion ring) to aState. For paths of length at least one, set PathLengthType to McGreaterZero_c; otherwise, use McGreaterOrEqualZero_c. The function returns a sequence of states from the core of onionRings to a aState.

In the case of BFS search, the onion rings are built forward, so that any state in ring i+1 has at least one predecessor in ring i-1. In non-BFS search that may not be true, but we will have that every state in ring i+1 has a predecessor in ring i or less. The fsm is checked to see if the search was BFS. If not, every ring from the beginning is searched to find the shortest path. This is a greedy heuristic and the shortest path is not guaranteed to be found. McBuildPathToCore takes a different approach.

It is the users responsibility to free the array returned as well as its members.

See Also Mc_BuildPathToCore
Defined in mcUtil.c 

array_t * 
Mc_BuildPathToCore(
  mdd_t * aState, 
  array_t * onionRings, 
  Fsm_Fsm_t * modelFsm, 
  Mc_PathLengthType  PathLengthType 
)
Build Path to Core (the first onion ring) starting at aState.

For the onion rings should be built in such a way that for every state v in ring i+1 there is a state v' in ring i such that there is an edge from v to v'. This function will also works for non-BFS rings, where we just require that for every state v in a ring i > 0, there is a state in a ring 0 <= j < i that is a successor of v.

For paths of length at least one, set PathLengthType to McGreaterZero_c. Otherwise, use McGreaterOrEqualZero_c. The function returns a sequence of states to a state in the core of onionRings, starting at aState. It is the users responsibility to free the array returned as well as its members.

Defined in mcUtil.c 

array_t * 
Mc_CompletePath(
  mdd_t * aState, 
  mdd_t * bState, 
  mdd_t * invariantStates, 
  Fsm_Fsm_t * modelFsm, 
  array_t * careSetArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel, 
  Mc_FwdBwdAnalysis  dirn 
)
Make a path from aState to bState which only passes through invariantStates; it is assumed that aState and bState lie in invariantStates. Returns a sequence of states starting from aState, leading to bState. If aState == bState, a non trivial path is returned (ie a cycle). If no path exists, return NIL. It is the users responsibility to free the returned array as well as its members.

Defined in mcUtil.c 

mdd_t * 
Mc_ComputeACloseMinterm(
  mdd_t * aSet, 
  mdd_t * target, 
  array_t * Support, 
  mdd_manager * mddMgr 
)
Pick a minterm from the given set close to target. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.

Defined in mcUtil.c 

mdd_t * 
Mc_ComputeACloseState(
  mdd_t * states, 
  mdd_t * target, 
  Fsm_Fsm_t * modelFsm 
)
Select a state from the given set close to target.

Defined in mcUtil.c 

mdd_t * 
Mc_ComputeAMinterm(
  mdd_t * aSet, 
  array_t * Support, 
  mdd_manager * mddMgr 
)
Pick an arbitrary minterm from the given set. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend.

Defined in mcUtil.c 

mdd_t * 
Mc_ComputeAState(
  mdd_t * states, 
  Fsm_Fsm_t * modelFsm 
)
Select an arbitrary state from the given set

Defined in mcUtil.c 

array_t * 
Mc_ComputeGuideArray(
  Fsm_Fsm_t * fsm, 
  FILE * guideFP 
)
Read the guide file and compute the BDDs of the hints and store in an array. Adds the 1 hint to the end of the array. Closes the guideFP. Returns NIL if something goes wrong.

Defined in mcUtil.c 

Fsm_Fsm_t * 
Mc_ConstructReducedFsm(
  Ntk_Network_t * network, 
  array_t * ctlFormulaArray 
)
Form an FSM reduced with respect to the CTL formula array. All latches and inputs which affect the given formula AND the fairness conditions of the system are included in this reduced fsm.

Defined in mcUtil.c 

void 
Mc_End(
    
)
End mc package

Defined in mcMc.c 

array_t * 
Mc_EvaluateHints(
  Fsm_Fsm_t * fsm, 
  Ctlp_FormulaArray_t * invarArray 
)
Flushes the states associated with the hints,and reevaluates them in the current fsm. Quantifies out variables in the hint that are not in present state or primary input set of the current FSM. Returns NIL if something goes wrong (the hint does not fit the fsm).

Defined in mcUtil.c 

boolean 
Mc_FormulaStaticSemanticCheckOnNetwork(
  Ctlp_Formula_t * formula, 
  Ntk_Network_t * network, 
  boolean  inputsAllowed 
)
Perform static semantic check of ctl formula on network. Specifically, given an atomic formula of the form LHS=RHS, check that the LHS is the name of a latch/wire in the network, and that RHS is of appropriate type (enum/integer) and is lies in the range of the latch/wire values. If LHS is a wire, and inputsAllowed is false, check to see that the algebraic support of the wire consists of only latches and constants.

Defined in mcUtil.c 

mdd_t * 
Mc_FsmComputeDrivingInputMinterms(
  Fsm_Fsm_t * fsm, 
  mdd_t * aState, 
  mdd_t * bState 
)
Return all inputs which cause a transition from aState to bState. It is assumed that aState,bState are truly minterms over the PS variables.

Defined in mcUtil.c 

int 
Mc_FsmComputeStatesReachableFromSet(
  Fsm_Fsm_t * modelFsm, 
  mdd_t * initialStates, 
  array_t * careStatesArray, 
  mdd_t * specialStates, 
  array_t * onionRings, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
Return Boolean TRUE/FALSE depending on whether states in specialStates are reachable from initialStates.If true, onionRings is set to results of fixed point computation going forward from initialStates to specialStates. Otherwise onionRings is freed.

Defined in mcUtil.c 

int 
Mc_FsmComputeStatesReachingToSet(
  Fsm_Fsm_t * modelFsm, 
  mdd_t * targetStates, 
  array_t * careStatesArray, 
  mdd_t * specialStates, 
  array_t * onionRings, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
Return Boolean TRUE/FALSE depending on whether states in specialStates can reach states in targetStates. If true, onionRings is set to results of fixed point computation going back from targetStates to specialStates.

Defined in mcUtil.c 

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 
)
Evaluate states satisfying EG invariant. Conceptually, this is done by starting with all states marked with the invariant. From this initial set, recursively remove states which 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.

Defined in mcMc.c 

mdd_t * 
Mc_FsmEvaluateEHFormula(
  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 
)
Evaluate states satisfying EH invariant.

Defined in mcMc.c 

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 
)
Evaluate states satisfying EU(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 greatest fixed point computation are stored in the array, starting from the target. The evaluation will stop ones all (some) of earlyTermination.states have been found (depending on earlyTermination.someOrAll). See Mc_EvaluateFormula() 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 thelast 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 EU. This is used for debugging.

Side Effects Mc_FsmEvaluateFormula, EvalueteEUFormulaWithGivenTR

Defined in mcMc.c 

mdd_t * 
Mc_FsmEvaluateEXFormula(
  Fsm_Fsm_t * modelFsm, 
  mdd_t * targetMdd, 
  mdd_t * fairStates, 
  array_t * careStatesArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
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. Makes EXTENSIVE use of dont cares. 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.

Defined in mcMc.c 

mdd_t * 
Mc_FsmEvaluateEYFormula(
  Fsm_Fsm_t * modelFsm, 
  mdd_t * targetMdd, 
  mdd_t * fairStates, 
  array_t * careStatesArray, 
  Mc_VerbosityLevel  verbosity, 
  Mc_DcLevel  dcLevel 
)
Evaluate states satisfying EY target.

Defined in mcMc.c 

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 
)
Model check formula on given fsm under fairness.

Defined in mcMc.c 

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 
)
Evaluate states satisfying FwdG invariant.

Defined in mcMc.c 

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 
)
Evaluate states satisfying FwdUntil.

Defined in mcMc.c 

void 
Mc_Init(
    
)
Initialize mc package

Defined in mcMc.c 

void 
Mc_MintermPrint(
  mdd_t * aMinterm, 
  array_t * support, 
  Ntk_Network_t * aNetwork 
)
Print a minterm.

Defined in mcUtil.c 

char * 
Mc_MintermToString(
  mdd_t * aMinterm, 
  array_t * aSupport, 
  Ntk_Network_t * aNetwork 
)
Return a string for a minterm.

Defined in mcUtil.c 

void 
Mc_NodeTableAddCtlFormulaNodes(
  Ntk_Network_t * network, 
  Ctlp_Formula_t * formula, 
  st_table * nodesTable 
)
Add nodes for wires referred to in formula to nodesTable.

Defined in mcUtil.c 

int 
Mc_PrintPath(
  array_t * aPath, 
  Fsm_Fsm_t * modelFsm, 
  boolean  printInput 
)
Utility function - prints states on path, inputs for transitions

Defined in mcUtil.c 

Mc_GuidedSearch_t 
Mc_ReadGuidedSearchType(
    
)
Read and parse the hints_type set flag. If it is not set return the default: local. Return Mc_None_c if there is an error.

Defined in mcUtil.c 

array_t * 
Mc_ReadHints(
  FILE * guideFP 
)
Read the guide file and store the hint formulae in an array. Adds the 1 hint to the end of the array. Returns NIL if something goes wrong: parse error in the file or temporal operators in the hints

Defined in mcUtil.c 

static boolean 
MintermCheckWellFormed(
  mdd_t * aMinterm, 
  array_t * aSupport, 
  mdd_manager * mddMgr 
)
Test that given mdd is a minterm.

Defined in mcUtil.c 

static mdd_t * 
ModelCheckAtomicFormula(
  Fsm_Fsm_t * modelFsm, 
  Ctlp_Formula_t * ctlFormula 
)
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.

Defined in mcMc.c 

static void 
NodeTableAddCtlFormulaNodes(
  Ntk_Network_t * network, 
  Ctlp_Formula_t * formula, 
  st_table * nodesTable 
)
Add nodes for wires referred to in formula to nodesTable.

Defined in mcUtil.c 

static McOptions_t * 
ParseInvarOptions(
  int  argc, 
  char ** argv 
)
Parse command line options for invar.

Defined in mcMc.c 

static McOptions_t * 
ParseLeOptions(
  int  argc, 
  char ** argv 
)
Parse command line options for lang_empty.

Defined in mcMc.c 

static McOptions_t * 
ParseMcOptions(
  int  argc, 
  char ** argv 
)
Parse command line options for mc.

Defined in mcMc.c 

static void 
PrintDeck(
  array_t * mddValues, 
  array_t * mddIdArray, 
  Ntk_Network_t * network 
)
Print an array of nodes

Defined in mcUtil.c 

static void 
PrintInvPassFail(
  array_t * invarFormulaArray, 
  int * resultArray 
)
Prints whether the set of invariants passed or failed.

Defined in mcMc.c 

static void 
PrintMcPassFail(
  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 
)
Prints whether model checking passed or failed, and if requested, a debug trace.

Defined in mcMc.c 

static void 
PrintNodes(
  array_t * mddIdArray, 
  Ntk_Network_t * network 
)
Print an array of nodes

Defined in mcUtil.c 

static boolean 
SetCheckSupport(
  mdd_t * aMinterm, 
  array_t * aSupport, 
  mdd_manager * mddMgr 
)
Test that given mdd is a minterm.

Defined in mcUtil.c 

static array_t * 
SortFormulasByFsm(
  Fsm_Fsm_t * totalFsm, 
  array_t * invarFormulaArray, 
  array_t * fsmArray, 
  McOptions_t * options 
)
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.

Side Effects fsmArray is populated with reduced fsms.

Defined in mcMc.c 

static array_t * 
SortMddIds(
  array_t * mddIdArray, 
  Ntk_Network_t * network 
)
Print an array of nodes

Defined in mcUtil.c 

static int 
StringCheckIsInteger(
  char * string, 
  int * value 
)
Test that the given string is an integer. Returns 0 if string is not an integer, 1 if the integer is too big for int, and 2 if integer fits in int.

Side Effects Sets the pointer value if the string is an integer small enough for int.

Defined in mcUtil.c 

static int 
TestInvariantsInTotalFsm(
  Fsm_Fsm_t * totalFsm, 
  array_t * invarStatesArray, 
  int  shellFlag 
)
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.

Defined in mcMc.c 

static void 
TimeOutHandle(
    
)
This function is called when the time out occurs.

Defined in mcMc.c 

static int 
UpdateResultArray(
  mdd_t * reachableStates, 
  array_t * invarStatesArray, 
  int * resultArray 
)
Check whether the reachable states violate the array of invariants. Return 1 if any formula failed. Update the result array. Entry 0 implies fail, 1 implies pass.

Defined in mcMc.c 

void 
_McPrintSatisfyingMinterms(
  mdd_t * aMdd, 
  Fsm_Fsm_t * fsm 
)
Print satisfying minterms. Just made for debug.

Defined in mcMc.c 

static int 
cmp(
  char ** s1, 
  char ** s2 
)
Compare two strings in the from of char **

Defined in mcUtil.c
Last updated on 20010517 18h00
You are not logged in 
©2002-2012 U.C. Regents