#include "ctlpInt.h"#include "grab.h"#include "puresat.h"#include "mcInt.h"
Include dependency graph for mcCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandMc (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static McOptions_t * | ParseMcOptions (int argc, char **argv) |
| static int | CommandLe (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static McOptions_t * | ParseLeOptions (int argc, char **argv) |
| static int | CommandInv (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static McOptions_t * | ParseInvarOptions (int argc, char **argv) |
| static void | TimeOutHandle (void) |
| static int | UpdateResultArray (mdd_t *reachableStates, array_t *invarStatesArray, int *resultArray) |
| static void | PrintInvPassFail (array_t *invarFormulaArray, int *resultArray) |
| void | Mc_Init (void) |
| void | Mc_End (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mcCmd.c,v 1.27 2009/04/11 01:43:30 fabio Exp $" |
| static jmp_buf | timeOutEnv |
| static int | mcTimeOut |
| static long | alarmLapTime |
Function Documentation
| static int CommandInv | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [checks that all reachable states in flattened network satisfy invariants]
CommandName [check_invariant]
CommandSynopsis [check all states reachable in flattened network satisfy specified invariants]
CommandArguments [ \[-c\] \[-d <dbg_level>\] \[-g <hints_file>\] \[-f\] \[-h\] \[-i\] \[-m\] \[-r\] \[-t <time_out_period>\] \[-v <verbosity_level>\] \[-A <reachability_analysis_type>\] \[-D\] <invar_file>]
CommandDescription [Performs invariant checking on a flattened network. Before calling this command, the user should have initialized the design by calling the command init_verify.
If the option -A3 (abstraction refinement method GRAB) is used, the command build_partition_maigs should also have been executed. However, in this case, the default BDD manager and network partition are not mandatory, though they will be used if available. (In other words, the user must run the commands flatten_hierarchy and build_partition_maigs, but doesn't have to run the commands static_order and build_partition_mdds before calling this command.) For extremely large networks, it is actually favorable not to build them for the entire concrete model, but let this procedure assign bdd ids and construct the partition incrementally.
Option -A4 means abstraction refinement approach using puresat algorithm, which is entirely based on SAT solver.
An invariant is a set of states. Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant.
One way of defining an invariant is through a CTL formula which has no path operators. Such formulas should be specified in the file invar_file. Note that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.
check_invariant ignores all fairness conditions associated with the FSM.
check_invariant involves reachability analysis where at every step of the reachability computation all the specified invariants are checked in the reachable states computed thus far. If some invariant does not hold, a proof of failure is demonstrated. This consists of a path starting from an initial state to a state lying outside the invariant. This path is made as short as possible. For the -A 0 option or default -A option, it is the shortest path leading to a state outside the invariant. If a set of invariants is specified, the failed formulas are reported as soon as they are detected. The check is continued with the remaining invariants.
Command options:
- -d
<dbg_level> Specify the amount of debugging performed when the system fails a formula being checked.
dbg_levelmust be one of the following:0: No debugging performed. This is the default.1: Generate a path from an initial state to a state lying outside the invariant. This option stores the onion rings just as specifying -f would have. Therefore, it may take more time and memory if the formula passes. This option is incompatible with -A 2 option.- -f
Store the set of new states (onion rings) reached at each step of invariant. This option is likely to use more memory but possibly faster results for invariants that fail. Therefore, the debug information for a failed invariant, if requested, may be provided faster. This option is not compatible with -A 2 options.
- -g <
hints_file> Use guided search. The file
hints_filecontains a series of hints. A hint is a formula that does not contain any temporal operators, sohints_filehas the same syntax as a file of invariants used for check_invariant. The hints are used in the order given to change the transition relation. The transition relation is conjoined with the hint to yield an underapproximation of the transition relation. If the hints are cleverly chosen, this may speed up the computation considerably, because a search with the changed transition relation may be much simpler than one with the original transition relation, and results obtained can be reused, so that we may never have to do an expensive search with the original relation. See also: Ravi and Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, DAC'00. This option is not compatible with -A 2 option. The description of some options for guided search can be found in the help page for print_guided_search_options.- -h
Print the command usage.
- -c
Use the formula tree so that subformulae are not shared among the CTL formulae in the input file. This option is useful in the following scenario - formulae A, B and C are being checked in order and there is sub-formula sharing between A and C. If the BDDs corresponding to the shared sub-formula is huge then computation for B might not be able to finish without using this option.
- -i
Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.
- -m
Pipe debugger output through the UNIX utility more.
- -r
Reduce the FSM derived from the flattened network with respect to each of the invariants in the input file. By default, the FSM is reduced with respect to the conjunction of the invariants in the input file. If this option is used and don't cares are being used for simplification, then subformula sharing is disabled (result might be incorrect otherwise).
The truth of an invariant may be independant of parts of the network (such as when wires have been abstracted; see
flatten_hierarchy). These parts are effectively removed when this option is invoked; this may result in more efficient invariant checking.- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
- -v
<verbosity_level> Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_levelmust be one of the following:0: No feedback provided. This is the default.1: Feedback on code location.2: Feedback on code location and CPU usage.- -A <reachability_analysis_type>
This option allows specification of the type of reachability computation.
0: (default) Breadth First Search. No approximate reachability computation.
1: High Density Reachability Analysis (HD). Computes reachable states in a manner that keeps BDD sizes under control. May be faster than BFS in some cases. For larger circuits, this option could compute more reachable states than the -A 0 option for the same memory constraints, consequently may prove more invariants false. For help on controlling options for HD, look up help on the command: print_hd_options
print_hd_options. Refer Ravi & Somenzi, ICCAD95. The path generated for a failed invariant using this method may not be the shortest path. This option is available only when compiled with the CUDD package.2. Approximate Reachability Don't Cares(ARDC). Computes over-approximated reachable states in the reachability analysis step. This may be faster than the -A 0 option . The invariants are checked in the over-approximation. This may produce false negatives, but these are resolved internally using the exact reachable states. The final results produced are the same as those for exact reachable states. For help on controlling options for ARDC, look up help on the command: print_ardc_options.
print_ardc_optionsRefer 2 papers in TCAD96 Dec. Cho et al, one is for State Space Decomposition and the other is for Approximate FSM Traversal. This option is incompatible with -d 1 and -g options.3. The GRAB Abstraction Refinement Method. Conducts the reachability analysis on an abstract model. If the invariants are true in the abstract model, they are also true in the original model. If the invariants are false, the abstract counter-examples are used to refine the abstract model (since it is still inconclusive). This procedure iterates until a conclusive result is reached. Note that, with this option, "build_partitioned_mdds" and "static_order" does not have to be executed before calling "check_invariants," though the default BDD partition and order will be reused if available. (When checking extremely large models, skipping either or both "static_order" and "build_partitioned_mdds" can often make the verification much faster.) The grainularity of abstraction refinement also depends on the parameter "partition_threshold", which by default is 5000; one can use the VIS command "set partition_threshold 1000" to change its value. For experienced users who want to fine-tune the different parameters of GRAB, please try the test command "_grab_test" ("_grab_test -h" prints out its usage information). Refer to Wang et al., ICCAD2003 and ICCD2004 for more information about the GRAB algorithm. Note that this option is incompatible with the "-d 1" and "-g" options.
4. Abstraction refinement approach using puresat algorithm, which is entirely based on SAT solver. It has several parts:
Localization base Abstraction K-induction to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs UNSAT proof based method to obtain refinement Refinement minization to guarrantee a minimal refinement
For more information, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"
- -D
First compute an overapproximation to the reachable states. Minimize the transition relation using this approximation, and then compute the set of reachable states exactly. This may accelerate reachability analysis. Refer to the paper by Moon et al, ICCAD98. The BDD minimizing method can be chosen by using "set image_minimize_method <method>"
set. This option is incompatible with -g.- -F <
dbg_file> Write the debugger output to
dbg_file.- -w <
node_file> This option invokes the algorithm to generate an error trace divided into fated and free segements. Fate represents the inevitability and free is asserted when there is no inevitability. This can be formulated as a two-player concurrent reachability game. The two players are the environment and the system. The node_file is given to specify the variables the are controlled by the system. - -W
- This option represents the case that all input variables are controlled by system.
- -G
- We proposed two algorithms to generate segmented counterexamples: general and restricted. By default we use the restricted algorithm. We can invoke the general algorithm with -G option. For more information, please read the STTT'04 paper by Jin et al., "Fate and Free Will in Error Traces"
- <invarFile>
File containing invariants to be checked.
Related "set" options:
rch_simulate <#> The set option can be used to set this flag rch_simulate to specify the number of random vectors to be simulated. Default value for this number is 0.
ctl_change_bracket <yes/no> Vl2mv automatically converts "\[\]" to "<>" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no". Default is "yes".
See also command : compute_reach
]
SideEffects []
SeeAlso [CommandMc]
Definition at line 2374 of file mcCmd.c.
{
int i, j;
mdd_t *tautology;
McOptions_t *options;
FILE *invarFile;
array_t *invarArray, *formulas, *sortedFormulaArray;
static Fsm_Fsm_t *totalFsm, *modelFsm;
mdd_manager *mddMgr;
Ntk_Network_t *network;
Mc_VerbosityLevel verbosity;
Mc_DcLevel dcLevel;
array_t *invarNormalFormulaArray, *invarStatesArray;
int timeOutPeriod = 0;
int debugFlag;
int buildOnionRings;
Fsm_RchType_t approxFlag;
int ardc;
int someLeft;
Ctlp_Formula_t *invarFormula;
mdd_t *invarFormulaStates;
mdd_t *reachableStates;
array_t *fsmArray;
int printStep = 0;
long initTime, finalTime;
array_t *careSetArray;
FILE *guideFile;
FILE *systemFile;
st_table *systemVarBddIdTable;
Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t);
array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
error_init();
initTime = util_cpu_time();
/* get command line options */
if (!(options = ParseInvarOptions(argc, argv))) {
return 1;
}
verbosity = McOptionsReadVerbosityLevel(options);
dcLevel = McOptionsReadDcLevel(options);
invarFile = McOptionsReadCtlFile(options);
timeOutPeriod = McOptionsReadTimeOutPeriod(options);
approxFlag = McOptionsReadInvarApproxFlag(options);
buildOnionRings = (int)McOptionsReadInvarOnionRingsFlag(options);
/* read the array of invariants */
invarArray = Ctlp_FileParseFormulaArray(invarFile);
fclose(invarFile);
if (invarArray == NIL(array_t)) {
(void) fprintf(vis_stderr, "** inv error: Error in parsing invariants from file\n");
McOptionsFree(options);
return 1;
}
if (array_n(invarArray) == 0) {
(void) fprintf(vis_stderr, "** inv error: No formula in file\n");
McOptionsFree(options);
return 1;
}
/* read the netwrok */
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
fprintf(vis_stderr, "%s\n", error_string());
error_init();
McOptionsFree(options);
return 1;
}
/**************************************************************************
* if "-A 3" is enabled (using the abstraction refinement method GRAB ),
* call GRAB.
**************************************************************************/
if (approxFlag == Fsm_Rch_Grab_c) {
if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
McOptionsFree(options);
fprintf(vis_stderr,
"** inv error: To use GRAB, please run build_partition_maigs first\n");
/*McOptionsFree(options);*/
return 1;
}
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# INV: Checking Invariant: timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
alarm(0);
return 1;
}
}
Grab_NetworkCheckInvariants(network,
invarArray,
"GRAB", /* refineAlgorithm, */
TRUE, /* fineGrainFlag, */
TRUE, /* refineMinFlag, */
FALSE, /* useArdcFlag, */
2, /* cexType = SOR */
verbosity,
McOptionsReadDbgLevel(options),
McOptionsReadPrintInputs(options),
McOptionsReadDebugFile(options),
McOptionsReadUseMore(options),
"INV" /* driverName */
);
McOptionsFree(options);
return 0;
}
if (approxFlag == Fsm_Rch_PureSat_c) {
if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
McOptionsFree(options);
fprintf(vis_stderr,
"** inv error: Please run build_partition_maigs first\n");
McOptionsFree(options);
return 1;
}
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# INV by PURESAT: Checking Invariant using PURESAT: timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# INV by PURESAT: data may be corrupted.\n");
alarm(0);
return 1;
}
}
PureSat_CheckInvariant(network,invarArray,
(int)options->verbosityLevel,
options->dbgLevel,McOptionsReadDebugFile(options),
McOptionsReadPrintInputs(options),options->incre,
options->sss, options->flatIP, options->IPspeed);
McOptionsFree(options);
return 0;
}
guideFile = McOptionsReadGuideFile(options);
if(guideFile != NIL(FILE) ){
hintsArray = Mc_ReadHints(guideFile);
fclose(guideFile); guideFile = NIL(FILE);
if( hintsArray == NIL(array_t) ){
McOptionsFree(options);
return 1;
}
} /* if guided search */
if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
Img_UserSpecifiedMethod() != Img_Monolithic_c &&
Img_UserSpecifiedMethod() != Img_Mlp_c &&
guideFile != NIL(FILE)){
fprintf(vis_stdout,
"** inv error: The Tfm and Hybrid image methods are incompatible with -g\n");
McOptionsFree(options);
return 1;
}
if (dcLevel == McDcLevelArdc_c)
ardc = 1;
else
ardc = 0;
/* obtain the fsm and mdd manager */
totalFsm = Fsm_NetworkReadOrCreateFsm(network);
if (totalFsm == NIL(Fsm_Fsm_t)) {
fprintf(vis_stderr, "%s\n", error_string());
error_init();
McOptionsFree(options);
return 1;
}
systemVarBddIdTable = 0;
systemFile = McOptionsReadSystemFile(options);
if(systemFile != NIL(FILE) ){
systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
fclose(systemFile); systemFile = NIL(FILE);
if(systemVarBddIdTable == (st_table *)-1 ){
McOptionsFree(options);
return 1;
}
} /* if FAFW */
if(options->FAFWFlag && systemVarBddIdTable == 0) {
systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
}
mddMgr = Fsm_FsmReadMddManager(totalFsm);
tautology = mdd_one(mddMgr);
/* set time out */
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "# INV: Checking Invariant: timeout occurred after %d seconds.\n", timeOutPeriod);
(void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
alarm(0);
return 1;
}
}
/* debugFlag = 1 -> need to store/compute onion shells, else not */
debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
/* use formula tree if reduce option and dont-care level is high */
if ((McOptionsReadReduceFsm(options) == TRUE) &&
(dcLevel != McDcLevelNone_c)) {
McOptionsSetUseFormulaTree(options, TRUE);
}
/* derive the normalized array of invariant formulas */
if (McOptionsReadUseFormulaTree(options) == TRUE) {
invarNormalFormulaArray =
Ctlp_FormulaArrayConvertToExistentialFormTree(invarArray);
} else {
array_t *temp = Ctlp_FormulaArrayConvertToDAG( invarArray );
array_free( invarArray );
invarArray = temp;
invarNormalFormulaArray = Ctlp_FormulaDAGConvertToExistentialFormDAG(
invarArray );
}
if (array_n(invarNormalFormulaArray) == 0) {
array_free(invarNormalFormulaArray);
Ctlp_FormulaArrayFree(invarArray);
mdd_free(tautology);
return 1;
}
fsmArray = array_alloc(Fsm_Fsm_t *, 0);
sortedFormulaArray = SortFormulasByFsm(totalFsm, invarNormalFormulaArray,
fsmArray, options);
if (sortedFormulaArray == NIL(array_t)) {
array_free(invarNormalFormulaArray);
Ctlp_FormulaArrayFree(invarArray);
mdd_free(tautology);
return 1;
}
assert(array_n(fsmArray) == array_n(sortedFormulaArray));
careSetArray = array_alloc(mdd_t *, 0);
/* main loop for array of array of formulas. Each of the latter
arrays corresponds to one reduced fsm. */
arrayForEachItem(array_t *, sortedFormulaArray, i, formulas) {
int *resultArray;
int fail;
/* initialize pass, fail array */
resultArray = ALLOC(int, array_n(formulas));
for (j = 0; j < array_n(formulas); j++) {
resultArray[j] = 1;
}
/* get reduced fsm for this set of formulas */
modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, i);
/* evaluate hints for this reduced fsm, stop if the hints contain variables
* outside this model FSM.
*/
if (hintsArray != NIL(Ctlp_FormulaArray_t)) {
int k;
hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
if( hintsStatesArray == NIL(array_t)) { /* something wrong, clean up */
int l;
fprintf(vis_stdout, "Hints dont match the reduced FSM for this set of invariants.\n");
fprintf(vis_stdout, "Continuing with the next set of invariants\n");
for (k = i; k < array_n(sortedFormulaArray); k++) {
formulas = array_fetch(array_t *, sortedFormulaArray, k);
arrayForEachItem(Ctlp_Formula_t *, formulas, l, invarFormula) {
Ctlp_FormulaFree(invarFormula);
}
array_free(formulas);
/* get reduced fsm for this set of formulas */
modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, k);
/* free the Fsm if it was reduced here */
if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
}
array_free(careSetArray);
array_free(fsmArray);
array_free(sortedFormulaArray);
array_free(invarNormalFormulaArray);
(void) fprintf(vis_stdout, "\n");
Ctlp_FormulaArrayFree(invarArray);
McOptionsFree(options);
mdd_free(tautology);
return 1;
}
}/* hints exist */
if(options->FAFWFlag > 1) {
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, 1, 0, 0,
approxFlag, ardc, 0, 0, (verbosity > 1),
hintsStatesArray);
mdd_free(reachableStates);
}
invarStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, careSetArray, 0, tautology);
arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
/* compute the set of states represented by the invariant. */
invarFormulaStates =
Mc_FsmEvaluateFormula(modelFsm, invarFormula, tautology,
NIL(Fsm_Fairness_t), careSetArray,
MC_NO_EARLY_TERMINATION,
NIL(Fsm_HintsArray_t), Mc_None_c,
verbosity, dcLevel, buildOnionRings,
McGSH_EL_c);
array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
}
printStep = (verbosity == McVerbosityMax_c) && (totalFsm == modelFsm);
/* main loop to check a set of invariants. */
do {
boolean compute = FALSE;
/* check if the computed reachable set in the total FSM already violates an invariant. */
compute = TestInvariantsInTotalFsm(totalFsm, invarStatesArray, (debugFlag ||
buildOnionRings));
/* compute reachable set or until early failure */
if (compute)
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, (debugFlag || buildOnionRings), 0, 0,
approxFlag, ardc, 0, invarStatesArray, (verbosity > 1),
hintsStatesArray);
else if (debugFlag || buildOnionRings) {
(void)Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
} else {
reachableStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(totalFsm));
}
ardc = 0; /* once ardc is applied, we don't need it again. */
/* updates result array and sets fail if any formula failed.*/
fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
mdd_free(reachableStates);
someLeft = 0;
if (fail) {
/* some invariant failed */
if (debugFlag) {
assert (approxFlag != Fsm_Rch_Oa_c);
Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
InvarPrintDebugInformation(modelFsm, formulas, invarStatesArray,
resultArray, options, hintsStatesArray);
Fsm_FsmSetFAFWFlag(modelFsm, 0);
Fsm_FsmSetSystemVariableFAFW(modelFsm, 0);
} else if (approxFlag == Fsm_Rch_Oa_c) {
assert(!buildOnionRings);
/* May be a false negative */
/* undo failed results in the result array, report passed formulae */
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* print all formulae that are known to have passed */
if (resultArray[j] == 1) {
mdd_free(invarFormulaStates);
array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
(void) fprintf(vis_stdout, "# INV: Early detection - formula passed --- ");
invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
} else resultArray[j] = 1;
}
fprintf(vis_stdout, "# INV: Invariant violated by over-approximated reachable states\n");
fprintf(vis_stdout, "# INV: Switching to BFS (exact computation) to resolve false negatives\n");
/* compute reachable set or until early failure */
reachableStates = Fsm_FsmComputeReachableStates(
modelFsm, 0, verbosity , 0, 0, 0, 0, 0, Fsm_Rch_Bfs_c, ardc, 0,
invarStatesArray, (verbosity > 1), hintsStatesArray);
/* either invariant has failed or all reachable states are computed */
/* updates result array */
fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
mdd_free(reachableStates);
}
/* remove the failed invariants from the invariant list. */
if (fail) {
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* free the failed invariant mdds */
if (resultArray[j] == 0) {
mdd_free(invarFormulaStates);
array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
if (!debugFlag) {
(void) fprintf(vis_stdout, "# INV: Early detection - formula failed --- ");
invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
fprintf(vis_stdout, "\n");
}
} else {
someLeft = 1;
}
}
}
} /* end of recomputation dur to over approximate computation */
} while (someLeft);
arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
if (invarFormulaStates == NIL(mdd_t)) continue;
/* free the passed invariant mdds */
mdd_free(invarFormulaStates);
}
array_free(invarStatesArray);
if (printStep) {
finalTime = util_cpu_time();
Fsm_FsmReachabilityPrintResults(modelFsm,finalTime-initTime ,approxFlag);
}
/* free the Fsm if it was reduced here */
if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
PrintInvPassFail(formulas, resultArray);
arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
Ctlp_FormulaFree(invarFormula);
}
array_free(formulas);
FREE(resultArray);
} /* end of processing the sorted array of array of invariants */
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
if(hintsArray)
Ctlp_FormulaArrayFree(hintsArray);
array_free(careSetArray);
array_free(fsmArray);
array_free(sortedFormulaArray);
array_free(invarNormalFormulaArray);
(void) fprintf(vis_stdout, "\n");
if (options->FAFWFlag) {
st_free_table(systemVarBddIdTable);
}
Ctlp_FormulaArrayFree(invarArray);
McOptionsFree(options);
mdd_free(tautology);
alarm(0);
return 0;
}
Here is the caller graph for this function:
| static int CommandLe | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Check whether language of FSM is empty.]
CommandName [lang_empty]
CommandSynopsis [perform language emptiness check on a flattened network]
CommandArguments [ \[-b\] \[-d <dbg_level>\] \[-f <dbg_file>\] \[-h\] \[-i\] \[-s\] \[-t <time_out_period>\] \[-v <verbosity_level>\] \[-A <le_method>\] \[-D <dc_level>\] \[-S <schedule>\] \[-L <lockstep_mode>\] ]
CommandDescription [ Performs language emptiness check on a flattened network. The language is not empty when there is a fair path starting at an initial state. Before calling this command, the user should have initialized the design by calling the command init_verify.
A fairness constraint can be read in by calling the read_fairness command; if none is specified, all paths are taken to be fair.
The system is reduced automatically with respect to the set of fairness constraints. If the language is not empty, a proof of this fact is generated. A proof is a fair path starting at an initial state. This is represented by a finite sequence of states starting at an initial state (the stem) leading to a fair cycle, i.e., a cycle on which there lies a state from each fairness condition.
Command options:
- -b
Use backward analysis when performing debugging; the default is to use forward analysis. This should be tried when the debugger spends a large amount of time when creating a path to a fair cycle.
- -d
<dbg_level> Specify whether to demonstrate a proof of the language non-emptiness
dbg_levelmust be one of the following:0: No debugging performed. This is the default.1: Generate a path to a fair cycle.- -f <
dbg_file> Write the debugger output to
dbg_file.- -h
Print the command usage.
- -m
Pipe debugger output through the UNIX utility more.
- -i
Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.
- -s
Print debug output in the format accepted by the
simulatecommand.- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
- -v
<verbosity_level> Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_levelmust be one of the following:0: No feedback provided. This is the default.1: Feedback on code location.2: Feedback on code location and CPU usage.- -A
<le_method> Specify whether the compositional SCC analysis algorithm, Divide and Compose (DnC), is enabled for language emptiness checking. The DnC algorithm first enumerates fair SCCs in an over-approximated abstract model, and then successively refines them in the more concrete models. Since non-fair SCCs can be ignored in the more concrete models, a potentially large part of the state space are pruned away early on when the computations are cheap.
le_methodmust be one of the following:0: no use of Divide and Compose (Default).1: use Divide and Compose.- -D
<dc_level> Specify extent to which don't cares are used to simplify MDDs. Don't cares are minterms on which the value taken by functions does not affect the computation; potentially, these minterms can be used to simplify MDDs and reduce time taken to perform MDD computations.
dc_levelmust be one of the following:0: No don't cares are used.1: Use unreachable states as don't cares. This is the default.- -S
<schedule> Specify schedule for GSH algorithm, which generalizes the Emerson-Lei algorithm and is used to compute greatest fixpoints. The choice of schedule affects the sequence in which EX and EU operators are applied. It makes a difference only when fairness constraints are specified.
<schedule>must be one of the following:EL: EU and EX operators strictly alternate. This is the default.EL1: EX is applied once for every application of all EUs.EL2: EX is applied repeatedly after each application of all EUs.budget: a hybrid of EL and EL2.random: enabled operators are applied in (pseudo-)random order.off: GSH is disabled, and the old algorithm is used instead. The old algorithm uses theEL, but the termination checks are less sophisticated than in GSH.- -F
Use forward analysis in the computation of the greatest fixpoint. This option is incompatible with -d 1 or higher and can only be used with -D 1.
- -L
<lockstep_mode> Use the lockstep algorithm, which is based on fair SCC enumeration.
<lockstep_mode>must be one of the following:off: Lockstep is disabled. This is the default. Language emptiness is checked by computing a hull of the fair SCCs.on: Lockstep is enabled.all: Lockstep is enabled; all fair SCCs are enumerated instead of terminating as soon as one is found. This can be used to study the SCCs of a graph, but it is slower than the default option.n: (n is a positive integer). Lockstep is enabled and up tonfair SCCs are enumerated. This is less expensive thanall, but still less efficient thanon, even whenn = 1.
]
SideEffects []
SeeAlso []
Definition at line 1668 of file mcCmd.c.
{
McOptions_t *options;
Mc_VerbosityLevel verbosity;
Mc_LeMethod_t leMethod;
Mc_DcLevel dcLevel;
McDbgLevel dbgLevel;
FILE *dbgFile= NIL(FILE);
boolean printInputs = FALSE;
int timeOutPeriod = 0;
Mc_GSHScheduleType GSHschedule;
Mc_FwdBwdAnalysis GSHdirection;
int lockstep;
int useMore;
int simValue;
int reduceFsm_flag = 1;
long startRchTime;
mdd_t *modelCareStates;
Fsm_Fsm_t *totalFsm;
Fsm_Fsm_t *modelFsm, *reducedFsm = NIL(Fsm_Fsm_t);
mdd_t *fairInitStates;
array_t *modelCareStatesArray;
long initialTime, finalTime; /* for lang_empty checking */
Img_ResetNumberOfImageComputation(Img_Both_c);
/* Read options and set timeout if requested. */
if (!(options = ParseLeOptions(argc, argv))) {
return 1;
}
totalFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
if (totalFsm == NIL(Fsm_Fsm_t)) {
(void) fprintf(vis_stdout, "%s\n", error_string());
error_init();
McOptionsFree(options);
return 1;
}
initialTime = util_cpu_time();
verbosity = McOptionsReadVerbosityLevel(options);
leMethod = McOptionsReadLeMethod(options);
dcLevel = McOptionsReadDcLevel(options);
dbgLevel = McOptionsReadDbgLevel(options);
printInputs = McOptionsReadPrintInputs(options);
timeOutPeriod = McOptionsReadTimeOutPeriod(options);
GSHschedule = McOptionsReadSchedule(options);
GSHdirection = McOptionsReadTraversalDirection(options);
lockstep = McOptionsReadLockstep(options);
dbgFile = McOptionsReadDebugFile(options);
useMore = McOptionsReadUseMore(options);
simValue = McOptionsReadSimValue(options);
if (dbgLevel != McDbgLevelNone_c && GSHdirection == McFwd_c) {
(void) fprintf(vis_stderr, "** le error: -d is incompatible with -F\n");
McOptionsFree(options);
return 1;
}
if (dcLevel != McDcLevelRch_c && GSHdirection == McFwd_c) {
(void) fprintf(vis_stderr, "** le error: -F can only be used with -D1\n");
McOptionsFree(options);
return 1;
}
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# LE: language emptiness - timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "# LE: data may be corrupted.\n");
if (verbosity > McVerbosityNone_c) {
(void) fprintf(vis_stdout,
"-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
}
alarm(0);
return 1;
}
}
/* Reduce FSM to cone of influence of fairness constraints. */
if (reduceFsm_flag) {
Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
array_t *ctlNormalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
array_free(ctlNormalFormulaArray);
}
if (reducedFsm == NIL(Fsm_Fsm_t)) {
modelFsm = totalFsm;
}else {
modelFsm = reducedFsm;
}
/* Find care states and put them in an array */
if (dcLevel == McDcLevelArdc_c) { /* aRDC */
Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
array_t *tmpArray;
Fsm_ArdcGetDefaultOptions(ardcOptions);
if (verbosity > 0)
startRchTime = util_cpu_time();
else /* to remove uninitialized variable warning */
startRchTime = 0;
tmpArray = Fsm_ArdcComputeOverApproximateReachableStates(
modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
modelCareStatesArray = mdd_array_duplicate(tmpArray);
FREE(ardcOptions);
if (verbosity > 0 )
Fsm_ArdcPrintReachabilityResults(modelFsm,
util_cpu_time() - startRchTime);
}else if (dcLevel >= McDcLevelRch_c) { /*RDC*/
if (verbosity > 0)
startRchTime = util_cpu_time();
else /* to remove uninitialized variable warning */
startRchTime = 0;
modelCareStates =
Fsm_FsmComputeReachableStates(modelFsm, 0, verbosity, 0, 0,
(lockstep != MC_LOCKSTEP_OFF), 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
if (verbosity > 0) {
Fsm_FsmReachabilityPrintResults(modelFsm,
util_cpu_time() - startRchTime,
Fsm_Rch_Default_c);
}
modelCareStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
} else { /* mdd_one */
modelCareStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
modelCareStatesArray = array_alloc(mdd_t *, 0);
array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
}
fairInitStates = Mc_FsmCheckLanguageEmptiness(modelFsm,
modelCareStatesArray,
Mc_Aut_Strong_c,
leMethod,
dcLevel,
dbgLevel,
printInputs,
verbosity,
GSHschedule,
GSHdirection,
lockstep,
dbgFile,
useMore,
simValue,
"LE");
if (verbosity > McVerbosityNone_c) {
finalTime = util_cpu_time();
fprintf(vis_stdout, "-- total le time = %10g\n",
(double)(finalTime - initialTime) / 1000.0);
fprintf(vis_stdout,
"-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
}
/* Clean up. */
if (fairInitStates) {
mdd_free(fairInitStates);
}
mdd_array_free(modelCareStatesArray);
McOptionsFree(options);
if (reducedFsm) {
Fsm_FsmFree(reducedFsm);
}
alarm(0);
return 0;
} /* CommandLe */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandMc | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Check CTL formulas given in file are modeled by flattened network]
CommandName [model_check]
CommandSynopsis [perform fair CTL model checking on a flattened network]
CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\] \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\] \[-t <time_out_period>\]\[-v <verbosity_level>\] \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\] \[-C\] \[-w <node_file>\] \[-W\] \[-G\] <ctl_file>]
CommandDescription [Performs fair CTL model checking on a flattened network. Before calling this command, the user should have initialized the design by calling the command init_verify. Regardless of the options, no 'false positives' or 'false negatives' will occur: the result is correct for the given circuit.
Properties to be verified should be provided as CTL formulas in the file ctl_file. Note that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.
Properties of the form AG f, where f is a formula not involving path quantifiers are referred to as invariants; for such properties it may be substantially faster to use the check_invariant command.
A fairness constraint can be specified by invoking the read_fairness command; if none is specified, all paths are taken to be fair. If some initial states do not lie on a fair path, the model checker prints a message to this effect.
A formula passes iff it is true for all initial states of the system. Therefore, in the presence of multiple initial states, if a formula fails, the negation of the formula may also fail.
If a formula does not pass, a (potentially partial) proof of failure (referred to as a debug trace) is demonstrated. Fair paths are represented by a finite sequence of states (the stem) leading to a fair cycle, i.e. a cycle on which there is a state from each fairness condition. The level of detail of the proof can be specified (see option -d).
Both backward (future tense CTL formulas) and forward (past tense CTL formulas) model checking can be performed. Forward model checking is based on Iwashita's ICCAD96 paper. Future tense CTL formulas are automatically converted to past tense ones as much as possible in forward model checking.
Command options:
- -b
Use backward analysis when performing debugging; the default is to use forward analysis. This should be tried when the debugger spends a large amount of time when creating a path to a fair cycle. This option is not compatible with forward model checking option (-F).
- -c
Use the formula tree so that there is no sharing of sub-formulae among the formulae in the input file. This option is useful in the following scenario - formulae A, B and C are being checked in order and there is sub-formula sharing between A and C. If the BDDs corresponding to the shared sub-formula is huge then computation for B might not be able to finish without using this option.
- -d
<dbg_level> Specify the amount of debugging performed when the system fails a formula being checked. Note that it may not always be possible to give a simple counter-example to show that a formula is false, since this may require enumerating all paths from a state. In such a case the model checker will print a message to this effect. This option is incompatible with -F.
dbg_levelmust be one of the following:0: No debugging performed.dbg_level=0is the default.1: Debugging with minimal output: generate counter-examples for universal formulas (formulas of the formAX|AF|AU|AG) and witnesses for existential formulas (formulas of the formEX|EF|EU|EG). States on a path are not further analyzed.2: Same asdbg_level=1, but more verbose. (The subformulas are printed, too.)3: Maximal automatic debugging: as for level1, except that states occurring on paths will be recursively analyzed.4: Manual debugging: at each state, the user is queried if more feedback is desired.- -f <
dbg_file> Write the debugger output to
dbg_file. This option is incompatible with -F. Notes: when you use -d4 (interactive mode), -f is not recommended, since you can't see the output of vis on stdout.- -g <
hints_file> Use guided search. The file
hints_filecontains a series of hints. A hint is a formula that does not contain any temporal operators, sohints_filehas the same syntax as a file of invariants used for check_invariant. The hints are used in the order given to change the transition relation. In the case of least fixpoints (EF, EU), the transition relation is conjoined with the hint, whereas for greatest fixpoints the transition relation is disjoined with the negation of the hint. If the hints are cleverly chosen, this may speed up the computation considerably, because a search with the changed transition relation may be much simpler than one with the original transition relation, and results obtained can be reused, so that we may never have to do a complicated search with the original relation. Note: hints in terms of primary inputs are not useful for greatest fixpoints. See also: Ravi and Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, DAC'00.For formulae that contain both least and greatest fixpoints, the behavior depends on the flag
guided_search_hint_type. If it is set to local (default) then every subformula is evaluated to completion, using all hints in order, before the next subformula is started. For pure ACTL or pure ECTL formulae, we can also set guided_search_hint_type to global, in which case the entire formula is evaluated for one hint before moving on to the next hint, using underapproximations. The description of the options for guided search can be found in the help page for print_guided_search_options.model_check will call reachability without any guided search, even if -g is used. If you want to perform reachability with guided search, call rch directly.
Incompatible with -F.
- -h
Print the command usage.
- -i
Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed. This option is incompatible with -F.
- -m
Pipe debugger output through the UNIX utility more. This option is incompatible with -F.
- -r
Reduce the FSM derived from the flattened network with respect to each formula being checked. By default, the FSM is reduced with respect to the conjunction of the formulae in the input file. If this option is used and don't cares are being used for simplification, then subformula sharing is disabled (result might be incorrect otherwise).
The truth of a formula may be independent of parts of the network (such as when wires have been abstracted; see
flatten_hierarchy). These parts are effectively removed when this option is invoked; this may result in more efficient model checking.- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
- -v
<verbosity_level> Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_levelmust be one of the following:0: No feedback provided. This is the default.1: Feedback on code location.2: Feedback on code location and CPU usage.- -B
Check for vacuously passing formulae using the algorithm of Beer et al. (CAV97). The algorithm applies to a subset of ACTL (w-ACTL) and replaces the smallest important subformula of a passing property with either FALSE or TRUE depending on its negation parity. It then applies model checking to the resulting witness formula. If the witness formula also passes, then the original formula is deemed to pass vacuously. If the witness formula fails, a counterexample to it provides an interesting witness to the original passing formula. See the CAV97 paper for the definitions of w-ACTL, important subformula, and interesting witness. In short, one of the operands of a binary operator in a w-ACTL formula must be a propositional formula. See also the -V option.
- -C
Compute coverage of all observable signals in a set of CTL formulae using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity level (-v option) is equal to 0, only the coverage stats are printed. If verbosity level is greater than zero, then detailed information of the computation at each step of the algorithm is also provided. Debug information is provided in the form of states not covered for each observable signal if the dbg_level (-d option) is greater than 0. The number of states printed is set by the vis environment variable 'nr_uncoveredstates'. By default the number of states printed is 1. The value of nr_uncoveredstates can be set using the set command. See also the -I option.
- -D
<dc_level> Specify extent to which don't cares are used to simplify MDDs in model checking. Don't cares are minterms on which the values taken by functions do not affect the computation; potentially, these minterms can be used to simplify MDDs and reduce the time taken to perform model checking. The -g flag for guided search does not affect the way in which the don't-care conditions are computed.
dc_levelmust be one of the following:0: No don't cares are used.1: Use unreachable states as don't cares. This is the default.2: Use unreachable states as don't cares and in the EU computation, use 'frontiers' for image computation.3: First compute an overapproximation of the reachable states (ARDC), and use that as the cares set. Use `frontiers' for image computation. For help on controlling options for ARDC, look up help on the command: print_ardc_options. Refer to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD December 1996: one is for State Space Decomposition and the other is for Approximate FSM Traversal.- -F
Use forward model checking based on Iwashita's method in ICCAD96. Future tense CTL formulas are automatically converted to past tense ones as much as possible. Converted forward formulas are printed when verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m) are ignored with this option. We have seen that forward model checking was much faster than backward in many cases, also forward was much slower than backward in many cases.
- -I
Compute coverage of all observable signals in a set of CTL formulae using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If the verbosity level (-v option) is equal to 0, only the coverage stats are printed. If verbosity level is greater than zero, then detailed information of the computation at each step of the algorithm is also provided. Debug information is provided in the form of states not covered for each observable signal if the dbg_level (-d option) is greater than 0. The number of states printed is set by the vis environment variable 'nr_uncoveredstates'. By default the number of states printed is 1. The value of nr_uncoveredstates can be set using the set command. Compared to the -C option, this one produces more accurate results and deals with a larger subset of CTL.
- -S
<schedule> Specify schedule for GSH algorithm, which generalizes the Emerson-Lei algorithm and is used to compute greatest fixpoints. The choice of schedule affects the sequence in which EX and EU operators are applied. It makes a difference only when fairness constraints are specified.
<schedule>must be one of the following:EL: EU and EX operators strictly alternate. This is the default.EL1: EX is applied once for every application of all EUs.EL2: EX is applied repeatedly after each application of all EUs.budget: a hybrid of EL and EL2.random: enabled operators are applied in (pseudo-)random order.off: GSH is disabled, and the old algorithm is used instead. The old algorithm uses theELschedule, but the termination checks are less sophisticated than in GSH.- -V
Check for vacuously passing formulae with the algorithm of Purandare and Somenzi (CAV2002). The algorithm applies to all of CTL, and to both passing and failing properties. It says whether a passing formula may be strengthened and still pass, and whether a failing formula may be weakened and still fail. It considers all leaves of a formula that are under one negation parity (e.g., not descendants of a XOR or EQ node) for replacement by either TRUE or FALSE. See also the -B option.
- -w <
node_file> This option invoked the algorithm to generate an error trace divided into fated and free segements. Fate represents the inevitability and free is asserted when there is no inevitability. This can be formulated as a two-player concurrent reachability game. The two players are the environment and the system. The node_file is given to specify the variables the are controlled by the system. - -W
- This option represents the case that all input variables are controlled by system.
- -G
- We proposed two algorithm to generate segemented counter example. They are general and restrcited algorithm. Bu default we use restricted algorithm. We can invoke general algorithm with -G option. For more information, please check the STTT'04 paper of Jin et al., "Fate and Free Will in Error Traces"
<ctl_file>- File containing CTL formulas to be model checked.
Related "set" options:
- ctl_change_bracket <yes/no>
Vl2mv automatically converts "\[\]" to "<>" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no". Default is "yes".
- guided_search_hint_type
- Switches between local and global hints (see the -g option, or the help page for set).
See also commands : approximate_model_check, incremental_ctl_verification ]
Description [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.]
Comment [Ctlp creates duplicate formulas when converting to existential form; e.g. when converting AaUb. We aren't using this fact, which leads to some performance degradation.
A system satisfies a formula if all its initial states are in the satisfying set of the formula. Hence, we do not need to continue the computation if we know that all initial states are in the satisfying set, or if there are initial states that we are sure are not in the satisfying set. This is what early termination does: it supplies an extra termination condition for the fixpoints that kicks in when we can decide the truth of the formula. Note that this leads to some nasty consequences in storing the satisfying sets. A computation that has terminated early does not yield the exact satisfying set, and hence we can not always reuse this result when there is subformula sharing.]
SideEffects []
SeeAlso [CommandInv]
Definition at line 539 of file mcCmd.c.
{
/* options */
McOptions_t *options;
Mc_VerbosityLevel verbosity;
Mc_DcLevel dcLevel;
FILE *ctlFile;
int timeOutPeriod = 0;
Mc_FwdBwdAnalysis traversalDirection;
int buildOnionRings = 0;
FILE *guideFile;
FILE *systemFile;
Mc_GuidedSearch_t guidedSearchType = Mc_None_c;
Ctlp_FormulaArray_t *hintsArray = NIL(Fsm_HintsArray_t);
array_t *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
st_table *systemVarBddIdTable;
boolean noShare = 0;
Mc_GSHScheduleType GSHschedule;
boolean checkVacuity;
boolean performCoverageHoskote;
boolean performCoverageImproved;
/* CTL formulae */
array_t *ctlArray;
array_t *ctlNormalFormulaArray;
int i;
int numFormulae;
/* FSM, network and image */
Fsm_Fsm_t *totalFsm = NIL(Fsm_Fsm_t);
Fsm_Fsm_t *modelFsm = NIL(Fsm_Fsm_t);
Fsm_Fsm_t *reducedFsm = NIL(Fsm_Fsm_t);
Ntk_Network_t *network;
mdd_t *modelCareStates = NIL(mdd_t);
array_t *modelCareStatesArray = NIL(array_t);
mdd_t *modelInitialStates;
mdd_t *fairStates;
Fsm_Fairness_t *fairCond;
mdd_manager *mddMgr;
array_t *bddIdArray;
Img_ImageInfo_t *imageInfo;
Mc_EarlyTermination_t *earlyTermination;
/* Coverage estimation */
mdd_t *totalcoveredstates = NIL(mdd_t);
array_t *signalTypeList = array_alloc(int,0);
array_t *signalList = array_alloc(char *,0);
array_t *statesCoveredList = array_alloc(mdd_t *,0);
array_t *newCoveredStatesList = array_alloc(mdd_t *,0);
array_t *statesToRemoveList = array_alloc(mdd_t *,0);
/* Early termination is only partially implemented right now. It needs
distribution over all operators, including limited cases of temporal
operators. That should be relatively easy to implement. */
/* time keeping */
long totalInitialTime; /* for model checking */
long initialTime, finalTime; /* for model checking */
error_init();
Img_ResetNumberOfImageComputation(Img_Both_c);
/* read options */
if (!(options = ParseMcOptions(argc, argv))) {
return 1;
}
verbosity = McOptionsReadVerbosityLevel(options);
dcLevel = McOptionsReadDcLevel(options);
ctlFile = McOptionsReadCtlFile(options);
timeOutPeriod = McOptionsReadTimeOutPeriod(options);
traversalDirection = McOptionsReadTraversalDirection(options);
buildOnionRings =
(McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
noShare = McOptionsReadUseFormulaTree(options);
GSHschedule = McOptionsReadSchedule(options);
checkVacuity = McOptionsReadVacuityDetect(options);
/* for the command mc -C foo.ctl */
performCoverageHoskote = McOptionsReadCoverageHoskote(options);
/* for the command mc -I foo.ctl */
performCoverageImproved = McOptionsReadCoverageImproved(options);
/* Check for incompatible options and do some option-specific
* intializations.
*/
if (traversalDirection == McFwd_c) {
if (checkVacuity) {
fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n");
McOptionsFree(options);
return 1;
}
if (performCoverageHoskote || performCoverageImproved) {
fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n");
McOptionsFree(options);
return 1;
}
}
if (checkVacuity) {
if (performCoverageHoskote || performCoverageImproved) {
fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n");
McOptionsFree(options);
return 1;
}
}
guideFile = McOptionsReadGuideFile(options);
if(guideFile != NIL(FILE) ){
guidedSearchType = Mc_ReadGuidedSearchType();
if(guidedSearchType == Mc_None_c){ /* illegal setting */
fprintf(vis_stderr, "** mc error: Unknown hint type\n");
fclose(guideFile);
McOptionsFree(options);
return 1;
}
if(traversalDirection == McFwd_c){ /* illegal combination */
fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n");
fclose(guideFile);
McOptionsFree(options);
return 1;
}
if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
Img_UserSpecifiedMethod() != Img_Monolithic_c &&
Img_UserSpecifiedMethod() != Img_Mlp_c){
fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n");
fclose(guideFile);
McOptionsFree(options);
return 1;
}
hintsArray = Mc_ReadHints(guideFile);
fclose(guideFile); guideFile = NIL(FILE);
if( hintsArray == NIL(array_t) ){
McOptionsFree(options);
return 1;
}
} /* if guided search */
/* If don't-cares are used, -r implies -c. Note that the satisfying
sets of a subformula are only in terms of propositions therein
and their cone of influence. Hence, we can share satisfying sets
among formulae. I don't quite understand what the problem with
don't-cares is (RB) */
if (McOptionsReadReduceFsm(options))
if (dcLevel != McDcLevelNone_c)
McOptionsSetUseFormulaTree(options, TRUE);
if (traversalDirection == McFwd_c &&
McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
McOptionsSetDbgLevel(options, McDbgLevelNone_c);
(void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n");
}
/* Read CTL formulae */
ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile);
fclose(ctlFile); ctlFile = NIL(FILE);
if (ctlArray == NIL(array_t)) {
(void) fprintf(vis_stderr,
"** mc error: error in parsing formulas from file\n");
McOptionsFree(options);
return 1;
}
/* read network */
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
fprintf(vis_stdout, "%s\n", error_string());
error_init();
Ctlp_FormulaArrayFree(ctlArray);
McOptionsFree(options);
return 1;
}
/* read fsm */
totalFsm = Fsm_NetworkReadOrCreateFsm(network);
if (totalFsm == NIL(Fsm_Fsm_t)) {
fprintf(vis_stdout, "%s\n", error_string());
error_init();
Ctlp_FormulaArrayFree(ctlArray);
McOptionsFree(options);
return 1;
}
/* Assign variables to system if doing FAFW */
systemVarBddIdTable = NIL(st_table);
systemFile = McOptionsReadSystemFile(options);
if (systemFile != NIL(FILE)) {
systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
fclose(systemFile); systemFile = NIL(FILE);
if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */
Ctlp_FormulaArrayFree(ctlArray);
McOptionsFree(options);
return 1;
}
} /* if FAFW */
if(options->FAFWFlag && systemVarBddIdTable == 0) {
systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
}
if (verbosity > McVerbosityNone_c)
totalInitialTime = util_cpu_time();
else /* to remove uninitialized variable warning */
totalInitialTime = 0;
if(traversalDirection == McFwd_c){
mdd_t *totalInitialStates;
double nInitialStates;
totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm);
nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm),
totalInitialStates,
Fsm_FsmReadPresentStateVars(totalFsm));
mdd_free(totalInitialStates);
/* If the number of initial states is only one, we can use both
* conversion formulas(init ^ f != FALSE and init ^ !f == FALSE),
* however, if we have multiple initial states, we should use
* p0 ^ !f == FALSE.
*/
ctlNormalFormulaArray =
Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0),
noShare);
/* end conversion for forward traversal */
} else if (noShare) { /* conversion for backward, no sharing */
ctlNormalFormulaArray =
Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
}else{ /* conversion for backward, with sharing */
/* Note that converting to DAG after converting to existential form would
lead to more sharing, but it cannot be done since equal subformula that
are converted from different formulae need different pointers back to
their originals */
if (checkVacuity) {
ctlNormalFormulaArray =
Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
}
else {
array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray );
array_free( ctlArray );
ctlArray = temp;
ctlNormalFormulaArray =
Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray);
}
}
/* At this point, ctlNormalFormulaArray contains the formulas that are
actually going to be checked, and ctlArray contains the formulas from
which the conversion has been done. Both need to be kept around until the
end, for debugging purposes. */
numFormulae = array_n(ctlNormalFormulaArray);
/* time out */
if (timeOutPeriod > 0) {
/* Set the static variables used by the signal handler. */
mcTimeOut = timeOutPeriod;
alarmLapTime = util_cpu_ctime();
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# MC: timeout occurred after %d seconds.\n", timeOutPeriod);
(void) fprintf(vis_stdout, "# MC: data may be corrupted.\n");
if (verbosity > McVerbosityNone_c) {
fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
}
alarm(0);
return 1;
}
}
/* Create reduced fsm, if necessary */
if (!McOptionsReadReduceFsm(options)){
/* We want to minimize only when "-r" option is not specified */
/* reduceFsm would be NIL, if there is no reduction observed */
assert (reducedFsm == NIL(Fsm_Fsm_t));
reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) {
mddMgr = Fsm_FsmReadMddManager(reducedFsm);
bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
Fsm_FsmReadPresentStateVars(reducedFsm));
(void)fprintf(vis_stdout,"Local system includes ");
(void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
array_n(bddIdArray));
array_free(bddIdArray);
}
}
/************** for all formulae **********************************/
for(i = 0; i < numFormulae; i++) {
int nImgComps, nPreComps;
boolean result;
Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
ctlNormalFormulaArray, i);
modelFsm = NIL(Fsm_Fsm_t);
/* do a check */
if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
(void) fprintf(vis_stdout,
"** mc error: error in parsing Atomic Formula:\n%s\n",
error_string());
error_init();
Ctlp_FormulaFree(ctlFormula);
continue;
}
/* Create reduced fsm */
if (McOptionsReadReduceFsm(options)) {
/* We have not done top level reduction. */
/* Using the same variable reducedFsm here */
array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
assert(reducedFsm == NIL(Fsm_Fsm_t));
array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula);
reducedFsm = McConstructReducedFsm(network, oneFormulaArray);
array_free(oneFormulaArray);
if (reducedFsm && verbosity != McVerbosityNone_c) {
mddMgr = Fsm_FsmReadMddManager(reducedFsm);
bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
Fsm_FsmReadPresentStateVars(reducedFsm));
(void)fprintf(vis_stdout,"Local system includes ");
(void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
array_n(bddIdArray));
array_free(bddIdArray);
}
}/* if readreducefsm */
/* Let us see if we got any reduction via top level or via "-r" */
if (reducedFsm == NIL(Fsm_Fsm_t))
modelFsm = totalFsm; /* no reduction */
else
modelFsm = reducedFsm; /* some reduction at some point */
/* compute initial states */
modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
if (modelInitialStates == NIL(mdd_t)) {
int j;
(void) fprintf(vis_stdout,
"** mc error: Cannot build init states (mutual latch dependency?)\n%s\n",
error_string());
if (modelFsm != totalFsm)
Fsm_FsmFree(reducedFsm);
alarm(0);
for(j = i; j < numFormulae; j++)
Ctlp_FormulaFree(
array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
array_free( ctlNormalFormulaArray );
Ctlp_FormulaArrayFree( ctlArray );
McOptionsFree(options);
return 1;
}
earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
if(hintsArray != NIL(Ctlp_FormulaArray_t)) {
hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
if( hintsStatesArray == NIL(array_t) ||
(guidedSearchType == Mc_Global_c &&
Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) {
int j;
if( guidedSearchType == Mc_Global_c &&
Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)
fprintf(vis_stderr, "** mc error: global hints incompatible with "
"mixed formulae\n");
Mc_EarlyTerminationFree(earlyTermination);
mdd_free(modelInitialStates);
if (modelFsm != totalFsm)
Fsm_FsmFree(reducedFsm);
alarm(0);
for(j = i; j < numFormulae; j++)
Ctlp_FormulaFree(
array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
array_free( ctlNormalFormulaArray );
Ctlp_FormulaArrayFree( ctlArray );
McOptionsFree(options);
return 1;
} /* problem with hints */
} /* hints exist */
/* stats */
if (verbosity > McVerbosityNone_c) {
initialTime = util_cpu_time();
nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
} else { /* to remove uninitialized variable warnings */
initialTime = 0;
nImgComps = 0;
nPreComps = 0;
}
mddMgr = Fsm_FsmReadMddManager(modelFsm);
/* compute don't cares. */
if (modelCareStatesArray == NIL(array_t)) {
long iTime; /* starting time for reachability analysis */
if (verbosity > McVerbosityNone_c && i == 0)
iTime = util_cpu_time();
else /* to remove uninitialized variable warnings */
iTime = 0;
/* ardc */
if (dcLevel == McDcLevelArdc_c) {
Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options);
modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates(
modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
if (verbosity > McVerbosityNone_c && i == 0)
Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime);
/* rch dc */
} else if (dcLevel >= McDcLevelRch_c) {
modelCareStates =
Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
if (verbosity > McVerbosityNone_c && i == 0) {
Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime,
Fsm_Rch_Default_c);
}
modelCareStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
} else {
modelCareStates = mdd_one(mddMgr);
modelCareStatesArray = array_alloc(mdd_t *, 0);
array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
}
}
Fsm_MinimizeTransitionRelationWithReachabilityInfo(
modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c,
verbosity > 1);
/* fairness conditions */
fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
verbosity, dcLevel, GSHschedule,
McBwd_c, FALSE);
fairCond = Fsm_FsmReadFairnessConstraint(modelFsm);
if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) {
(void)fprintf(vis_stdout,
"** mc warning: There are no fair initial states\n");
}
else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) {
(void)fprintf(vis_stdout,
"** mc warning: Some initial states are not fair\n");
}
/* some user feedback */
if (verbosity != McVerbosityNone_c) {
(void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1);
Ctlp_FormulaPrint(vis_stdout,
Ctlp_FormulaReadOriginalFormula(ctlFormula));
(void)fprintf (vis_stdout, "\n");
if (traversalDirection == McFwd_c) {
(void)fprintf(vis_stdout, "Forward formula : ");
Ctlp_FormulaPrint(vis_stdout, ctlFormula);
(void)fprintf(vis_stdout, "\n");
}
}
/************** the actual computation **********************************/
if (checkVacuity) {
McVacuityDetection(modelFsm, ctlFormula, i,
fairStates, fairCond, modelCareStatesArray,
earlyTermination, hintsStatesArray,
guidedSearchType, modelInitialStates,
options);
}
else { /* Normal Model Checking */
mdd_t *ctlFormulaStates =
Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
fairCond, modelCareStatesArray,
earlyTermination, hintsStatesArray,
guidedSearchType, verbosity, dcLevel,
buildOnionRings, GSHschedule);
McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond,
modelCareStatesArray, earlyTermination,
hintsStatesArray, guidedSearchType, verbosity,
dcLevel, buildOnionRings, GSHschedule,
traversalDirection, modelInitialStates,
ctlFormulaStates, &totalcoveredstates,
signalTypeList, signalList, statesCoveredList,
newCoveredStatesList, statesToRemoveList,
performCoverageHoskote, performCoverageImproved);
Mc_EarlyTerminationFree(earlyTermination);
if(hintsStatesArray != NIL(array_t))
mdd_array_free(hintsStatesArray);
/* Set up things for possible FAFW analysis of counterexample. */
Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
/* user feedback on succes/fail */
result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
ctlFormula, ctlFormulaStates,
modelInitialStates, modelCareStatesArray,
options, verbosity);
Fsm_FsmSetFAFWFlag(modelFsm, 0);
Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL);
mdd_free(ctlFormulaStates);
}
if (verbosity > McVerbosityNone_c) {
finalTime = util_cpu_time();
fprintf(vis_stdout, "-- mc time = %10g\n",
(double)(finalTime - initialTime) / 1000.0);
fprintf(vis_stdout,
"-- %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
}
mdd_free(modelInitialStates);
mdd_free(fairStates);
Ctlp_FormulaFree(ctlFormula);
if ((McOptionsReadReduceFsm(options)) &&
(reducedFsm != NIL(Fsm_Fsm_t))) {
/*
** We need to free the reducedFsm only if it was created under "-r"
** option and was non-NIL.
*/
Fsm_FsmFree(reducedFsm);
reducedFsm = NIL(Fsm_Fsm_t);
modelFsm = NIL(Fsm_Fsm_t);
if (modelCareStates) {
mdd_array_free(modelCareStatesArray);
modelCareStates = NIL(mdd_t);
modelCareStatesArray = NIL(array_t);
} else if (modelCareStatesArray) {
modelCareStatesArray = NIL(array_t);
}
}
}/* for all formulae */
if (verbosity > McVerbosityNone_c) {
finalTime = util_cpu_time();
fprintf(vis_stdout, "-- total mc time = %10g\n",
(double)(finalTime - totalInitialTime) / 1000.0);
fprintf(vis_stdout,
"-- total %d image computations and %d preimage computations\n",
Img_GetNumberOfImageComputation(Img_Forward_c),
Img_GetNumberOfImageComputation(Img_Backward_c));
/* Print tfm options if we have a global fsm. */
if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) {
imageInfo = Fsm_FsmReadImageInfo(modelFsm);
if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
Img_TfmPrintStatistics(imageInfo, Img_Both_c);
}
}
}
/* Print results of coverage computation */
McPrintCoverageSummary(modelFsm, dcLevel,
options, modelCareStatesArray,
modelCareStates, totalcoveredstates,
signalTypeList, signalList, statesCoveredList,
performCoverageHoskote, performCoverageImproved);
mdd_array_free(newCoveredStatesList);
mdd_array_free(statesToRemoveList);
array_free(signalTypeList);
array_free(signalList);
mdd_array_free(statesCoveredList);
if (totalcoveredstates != NIL(mdd_t))
mdd_free(totalcoveredstates);
if (modelCareStates) {
mdd_array_free(modelCareStatesArray);
}
if(hintsArray)
Ctlp_FormulaArrayFree(hintsArray);
if ((McOptionsReadReduceFsm(options) == FALSE) &&
(reducedFsm != NIL(Fsm_Fsm_t))) {
/* If "-r" was not specified and we did some reduction at top
level, we need to free it */
Fsm_FsmFree(reducedFsm);
reducedFsm = NIL(Fsm_Fsm_t);
modelFsm = NIL(Fsm_Fsm_t);
}
if(systemVarBddIdTable)
st_free_table(systemVarBddIdTable);
array_free(ctlNormalFormulaArray);
(void) fprintf(vis_stdout, "\n");
Ctlp_FormulaArrayFree(ctlArray);
McOptionsFree(options);
alarm(0);
return 0;
}
Here is the caller graph for this function:
| void Mc_End | ( | void | ) |
| void Mc_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initialize mc package]
SideEffects []
Definition at line 120 of file mcCmd.c.
{
Cmd_CommandAdd("model_check", CommandMc, /* doesn't changes_network */ 0);
Cmd_CommandAdd("check_invariant", CommandInv, /* doesn't changes_network */ 0);
Cmd_CommandAdd("lang_empty", CommandLe, /* doesn't changes_network */ 0);
Cmd_CommandAdd("_init_state_formula", McCommandInitState, /* doesn't changes_network */ 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McOptions_t * ParseInvarOptions | ( | int | argc, |
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Parse command line options for invar.]
SideEffects []
Definition at line 2845 of file mcCmd.c.
{
unsigned int i;
int c;
boolean useMore = FALSE;
boolean reduceFsm = FALSE;
boolean printInputs = FALSE;
boolean useFormulaTree = FALSE;
FILE *inputFp=NIL(FILE);
FILE *debugOut=NIL(FILE);
char *debugOutName=NIL(char);
McDbgLevel dbgLevel = McDbgLevelNone_c;
Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
int timeOutPeriod = 0;
McOptions_t *options = McOptionsAlloc();
int approxFlag = 0, ardc = 0, shellFlag = 0;
Fsm_RchType_t rchType;
FILE *guideFile;
FILE *systemFile = NIL(FILE);
boolean FAFWFlag = FALSE;
boolean GFAFWFlag = FALSE;
char *guideFileName = NIL(char);
char *variablesForSystem = NIL(char);
int incre, speed;
/* int sss; */
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "ifcrt:g:hmv:d:A:DO:Ww:I:SPs:")) != EOF) {
switch(c) {
case 'g':
guideFileName = util_strsav(util_optarg);
break;
case 'h':
goto usage;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
break;
case 'd':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dbgLevel = (McDbgLevel) atoi(util_optarg);
break;
case 'f':
shellFlag = 1;
break;
case 'r' :
reduceFsm = TRUE;
break;
case 'm':
useMore = TRUE;
break;
case 'i' :
printInputs = TRUE;
break;
case 'c' :
useFormulaTree = TRUE;
break;
case 'A':
approxFlag = atoi(util_optarg);
if ((approxFlag > 4) || (approxFlag < 0)) {
goto usage;
}
break;
case 'D':
ardc = 1;
break;
case 'O':
debugOutName = util_strsav(util_optarg);
break;
case 'w':
variablesForSystem = util_strsav(util_optarg);
case 'W':
FAFWFlag = 1;
break;
case 'G':
GFAFWFlag = 1;
break;
case 'I':
incre = atoi(util_optarg);
options->incre = (incre==0)? FALSE:TRUE;
break;
case 'S':
/*sss = atoi(util_optarg);*/
/*options->sss = (sss==0)? FALSE:TRUE;*/
options->sss = TRUE;
break;
case 'P':
options->flatIP = TRUE;
break;
case 's':
speed = atoi(util_optarg);
options->IPspeed = speed;
break;
default:
goto usage;
}
}
if((FAFWFlag > 0 || GFAFWFlag > 0) && dbgLevel == 0) {
fprintf(vis_stderr, "** inv warning : -w and -W options are ignored without -d option\n");
}
if((FAFWFlag > 0 || GFAFWFlag > 0) && printInputs == 0) {
fprintf(vis_stderr, "** inv warning : -i is recommended with -w or -W option\n");
}
if(FAFWFlag) {
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** inv warning : -w and -W option is only available with CUDD\n");
FAFWFlag = 0;
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
}
/* translate approx flag */
switch(approxFlag) {
case 0: rchType = Fsm_Rch_Bfs_c; break;
case 1: rchType = Fsm_Rch_Hd_c; break;
case 2: rchType = Fsm_Rch_Oa_c; break;
case 3: rchType = Fsm_Rch_Grab_c; break;
case 4: rchType = Fsm_Rch_PureSat_c; break;
default: rchType = Fsm_Rch_Default_c; break;
}
if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
fprintf(vis_stderr, "** inv error: check_invariant with -A 1 option is currently supported by only CUDD.\n");
return NIL(McOptions_t);
}
if (rchType == Fsm_Rch_Oa_c) {
if (dbgLevel > 0) {
fprintf(vis_stdout, "Over approximation and debug level 1 are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
} else if (shellFlag == 1) {
fprintf(vis_stdout, "Over approximation and shell flag are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (rchType == Fsm_Rch_Grab_c) {
if (guideFileName != NIL(char)) {
fprintf(vis_stdout, "Abstraction refinement Grab and guided search are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (rchType == Fsm_Rch_PureSat_c) {
if (guideFileName != NIL(char)) {
fprintf(vis_stdout, "Abstraction refinement PureSat and guided search are incompatible\n");
fprintf(vis_stdout, "Read check_invariant help page\n");
goto usage;
}
}
if (guideFileName != NIL(char)) {
guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
FREE(guideFileName);
if (guideFile == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
McOptionsSetGuideFile(options, guideFile);
}
/*
* Open the ctl file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** inv error: file containing invariant formulas not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** inv error: too many arguments\n");
goto usage;
}
McOptionsSetUseMore(options, useMore);
McOptionsSetReduceFsm(options, reduceFsm);
McOptionsSetPrintInputs(options, printInputs);
McOptionsSetUseFormulaTree(options, useFormulaTree);
McOptionsSetTimeOutPeriod(options, timeOutPeriod);
McOptionsSetInvarApproxFlag(options, rchType);
if (ardc)
McOptionsSetDcLevel(options, McDcLevelArdc_c);
else
McOptionsSetDcLevel(options, McDcLevelNone_c);
McOptionsSetInvarOnionRingsFlag(options, shellFlag);
McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
if (inputFp == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
McOptionsSetCtlFile(options, inputFp);
if (debugOutName != NIL(char)) {
debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
if (debugOut == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
}
McOptionsSetDebugFile(options, debugOut);
if ((verbosityLevel != McVerbosityNone_c) &&
(verbosityLevel != McVerbosityLittle_c) &&
(verbosityLevel != McVerbositySome_c) &&
(verbosityLevel != McVerbosityMax_c)) {
goto usage;
}
else {
McOptionsSetVerbosityLevel(options, verbosityLevel);
}
if ((dbgLevel != McDbgLevelNone_c) &&
(dbgLevel != McDbgLevelMin_c)) {
if(((rchType == Fsm_Rch_Grab_c) && (dbgLevel == McDbgLevelMinVerbose_c)))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
if((rchType == Fsm_Rch_PureSat_c) && (options->flatIP == TRUE) && (dbgLevel == McDbgLevelMinVerbose_c))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
if((rchType == Fsm_Rch_Bfs_c) && (dbgLevel == McDbgLevelMinVerbose_c))
{
McOptionsSetDbgLevel(options, dbgLevel);
}
else
{
goto usage;
}
}
}
}
else {
McOptionsSetDbgLevel(options, dbgLevel);
}
if (variablesForSystem != NIL(char)) {
systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
if (systemFile == NIL(FILE)) {
fprintf(vis_stderr, "** inv error: cannot open system variables file for FAFW %s.\n",
variablesForSystem);
FREE(variablesForSystem);
variablesForSystem = NIL(char);
McOptionsFree(options);
return NIL(McOptions_t);
}
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
McOptionsSetVariablesForSystem(options, systemFile);
return options;
usage:
(void) fprintf(vis_stderr, "usage: check_invariant [-c][-d dbg_level][-f][-g <hintfile>][-h][-i][-m][-r][-v verbosity_level][-t time_out][-A <number>][-D dc_level] [-O <dbg_out>] <invar_file>\n");
(void) fprintf(vis_stderr, " -c avoid sub-formula sharing between formulae\n");
(void) fprintf(vis_stderr, " -d <dbg_level>");
(void) fprintf(vis_stderr, " dbg_level = 0 => no debug output (Default)\n");
(void) fprintf(vis_stderr, " dbg_level = 1 => print debug trace. (available for all options)\n ");
(void) fprintf(vis_stderr, " dbg_level = 2 => print debug trace in Aiger format. (available for -A0, -A3, -A4 and -A4 -P)\n");
(void) fprintf(vis_stderr, " -f \tStore the onion rings at each step.\n");
(void) fprintf(vis_stderr, " -g <hint_file> \tSpecify file for guided search.\n");
(void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n");
(void) fprintf(vis_stderr, " -m pipe debugger output through UNIX utility more\n");
(void) fprintf(vis_stderr, " -r reduce FSM with respect to invariant being checked\n");
(void) fprintf(vis_stderr, " -t <period> Time out period.\n");
(void) fprintf(vis_stderr, " -v <verbosity_level>\n");
(void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
(void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n");
(void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n");
(void) fprintf(vis_stderr, " -A <number> Use Different types of reachability analysis\n");
(void) fprintf(vis_stderr, " 0 (default) - BFS method.\n");
(void) fprintf(vis_stderr, " 1 - HD method.\n");
(void) fprintf(vis_stderr, " 2 - Over-approximation.\n");
(void) fprintf(vis_stderr, " 3 - Abstraction refinement GRAB.\n");
(void) fprintf(vis_stderr, " -D minimize transition relation with ARDCs\n");
(void) fprintf(vis_stderr, " -O <dbg_out>\n");
(void) fprintf(vis_stderr, " write error trace to dbg_out\n");
(void) fprintf(vis_stderr, " -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
(void) fprintf(vis_stderr, " -G \tUse general fate and free will algorithm.\n");
(void) fprintf(vis_stderr, " -w <node file> \tSpecify variables controlled by system.\n");
(void) fprintf(vis_stderr, " <invar_file> The input file containing invariants to be checked.\n");
(void) fprintf(vis_stderr, " -h \tPrints this usage message.\n");
(void) fprintf(vis_stderr, " -I \tSwitch for Incremental SAT solver in PureSAT method abstraction refinement\n");
McOptionsFree(options);
return NIL(McOptions_t);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McOptions_t * ParseLeOptions | ( | int | argc, |
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Parse command line options for lang_empty.]
SideEffects []
Definition at line 1867 of file mcCmd.c.
{
unsigned int i;
int c;
boolean useSimFormat = FALSE;
FILE *debugOut=NIL(FILE);
char *debugOutName=NIL(char);
Mc_DcLevel dcLevel = McDcLevelRch_c;
Mc_LeMethod_t leMethod = Mc_Le_Default_c;
McDbgLevel dbgLevel = McDbgLevelNone_c;
Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
McOptions_t *options = McOptionsAlloc();
boolean printInputs = FALSE;
boolean useMore = FALSE;
int timeOutPeriod = 0;
Mc_GSHScheduleType schedule = McGSH_EL_c;
Mc_FwdBwdAnalysis direction = McBwd_c;
int lockstep = MC_LOCKSTEP_OFF;
Fsm_ArdcOptions_t *ardcOptions;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "bihmt:v:d:A:D:f:sS:L:F")) != EOF) {
switch(c) {
case 'h':
goto usage;
case 'v':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
break;
case 'd':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dbgLevel = (McDbgLevel) atoi(util_optarg);
break;
case 'A':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
leMethod = (Mc_LeMethod_t) atoi(util_optarg);
break;
case 'D':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dcLevel = (Mc_DcLevel) atoi(util_optarg);
break;
case 'f':
debugOutName = util_strsav(util_optarg);
break;
case 's':
useSimFormat = TRUE;
break;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'i':
printInputs = TRUE;
break;
case 'm':
useMore = TRUE;
break;
case 'b':
fwdBwd = McBwd_c;
break;
case 'S' :
schedule = McStringConvertToScheduleType(util_optarg);
break;
case 'L' :
lockstep = McStringConvertToLockstepMode(util_optarg);
break;
case 'F' :
direction = McFwd_c;
break;
default:
goto usage;
}
}
if (schedule == McGSH_Unassigned_c) {
(void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
goto usage;
} else {
McOptionsSetSchedule(options, schedule);
}
McOptionsSetTraversalDirection(options, direction);
if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
(void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
goto usage;
} else {
McOptionsSetLockstep(options, lockstep);
}
if ((verbosityLevel != McVerbosityNone_c) &&
(verbosityLevel != McVerbosityLittle_c) &&
(verbosityLevel != McVerbositySome_c) &&
(verbosityLevel != McVerbosityMax_c)) {
goto usage;
}
else {
McOptionsSetVerbosityLevel(options, verbosityLevel);
}
if (debugOutName != NIL(char)) {
debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
if (debugOut == NIL(FILE)) {
McOptionsFree(options);
return NIL(McOptions_t);
}
}
McOptionsSetDebugFile(options, debugOut);
if ((dbgLevel != McDbgLevelNone_c) &&
(dbgLevel != McDbgLevelMin_c)) {
goto usage;
}
else {
McOptionsSetDbgLevel(options, dbgLevel);
}
if ((dcLevel != McDcLevelNone_c) &&
(dcLevel != McDcLevelRch_c ) &&
(dcLevel != McDcLevelRchFrontier_c ) &&
(dcLevel != McDcLevelArdc_c )) {
goto usage;
}
else {
McOptionsSetDcLevel(options, dcLevel);
}
if ((leMethod != Mc_Le_Default_c) &&
(leMethod != Mc_Le_Dnc_c)) {
goto usage;
}
else {
McOptionsSetLeMethod(options, leMethod);
}
/* set Ardc options for le : C.W. */
if (dcLevel == McDcLevelArdc_c) {
ardcOptions = Fsm_ArdcAllocOptionsStruct();
Fsm_ArdcGetDefaultOptions(ardcOptions);
} else
ardcOptions = NIL(Fsm_ArdcOptions_t);
McOptionsSetArdcOptions(options, ardcOptions);
McOptionsSetFwdBwd(options, fwdBwd);
McOptionsSetSimValue(options, useSimFormat);
McOptionsSetUseMore(options, useMore);
McOptionsSetPrintInputs(options, printInputs);
McOptionsSetTimeOutPeriod(options, timeOutPeriod);
return options;
usage:
(void) fprintf(vis_stderr, "usage: lang_empty [-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A <le_method>][-D <dc_level>][-S <schedule>][-F][-L <lockstep_mode>]\n");
(void) fprintf(vis_stderr, " -b \tUse backward analysis in debugging\n");
(void) fprintf(vis_stderr, " -d <dbg_level>\n");
(void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n");
(void) fprintf(vis_stderr, " debug_level = 1 => automatic debugging\n");
(void) fprintf(vis_stderr, " -f <dbg_out>\n");
(void) fprintf(vis_stderr, " write error trace to dbg_out\n");
(void) fprintf(vis_stderr, " -h \tPrints this usage message.\n");
(void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n");
(void) fprintf(vis_stderr, " -m \tPipe debug output through more\n");
(void) fprintf(vis_stderr, " -s \tWrite error trace in sim format.\n");
(void) fprintf(vis_stderr, " -t <period> time out period\n");
(void) fprintf(vis_stderr, " -v <verbosity_level>\n");
(void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
(void) fprintf(vis_stderr, " verbosity_level = 1 => feedback\n");
(void) fprintf(vis_stderr, " verbosity_level = 2 => feedback and CPU usage profile\n");
(void) fprintf(vis_stderr, " -A <le_method>\n");
(void) fprintf(vis_stderr, " le_method = 0 => no use of Divide and Compose (Default)\n");
(void) fprintf(vis_stderr, " le_method = 1 => use Divide and Compose\n");
(void) fprintf(vis_stderr, " -D <dc_level>\n");
(void) fprintf(vis_stderr, " dc_level = 0 => no use of don't cares\n");
(void) fprintf(vis_stderr, " dc_level = 1 => use unreached states as don't cares (Default)\n");
(void) fprintf(vis_stderr, " dc_level = 2 => use unreached states as don't cares\n");
(void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n");
(void) fprintf(vis_stderr, " dc_level = 3 => use over-approximate unreached states as don't cares\n");
(void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n");
(void) fprintf(vis_stderr, " -S <schedule>\n");
(void) fprintf(vis_stderr, " schedule is one of {EL,EL1,EL2,budget,random,off}\n");
(void) fprintf(vis_stderr, " -F \tUse forward analysis in fixpoint computation.\n");
(void) fprintf(vis_stderr, " -L <lockstep_mode>\n");
(void) fprintf(vis_stderr, " lockstep_mode is one of {off,on,all,n}\n");
McOptionsFree(options);
return NIL(McOptions_t);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static McOptions_t * ParseMcOptions | ( | int | argc, |
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Parse command line options for mc.]
SideEffects []
Definition at line 1158 of file mcCmd.c.
{
unsigned int i;
int c;
char *guideFileName = NIL(char);
char *variablesForSystem = NIL(char);
FILE *guideFile = NIL(FILE);
FILE *systemFile = NIL(FILE);
boolean doCoverageHoskote = FALSE;
boolean doCoverageImproved = FALSE;
boolean useMore = FALSE;
boolean reduceFsm = FALSE;
boolean printInputs = FALSE;
boolean useFormulaTree = FALSE;
boolean vd = FALSE;
boolean beer = FALSE;
boolean FAFWFlag = FALSE;
boolean GFAFWFlag = FALSE;
FILE *inputFp=NIL(FILE);
FILE *debugOut=NIL(FILE);
char *debugOutName=NIL(char);
Mc_DcLevel dcLevel = McDcLevelRch_c;
McDbgLevel dbgLevel = McDbgLevelNone_c;
Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
McOptions_t *options = McOptionsAlloc();
int timeOutPeriod = 0;
Mc_FwdBwdAnalysis traversalDirection = McBwd_c;
Fsm_ArdcOptions_t *ardcOptions;
Mc_GSHScheduleType schedule = McGSH_EL_c;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "bcirmg:hv:d:D:VBf:t:CIFR:S:GWw:")) != EOF) {
switch(c) {
case 'g':
guideFileName = util_strsav(util_optarg);
break;
case 'h':
goto usage;
case 'v':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
break;
case 'd':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dbgLevel = (McDbgLevel) atoi(util_optarg);
break;
case 'D':
for (i = 0; i < strlen(util_optarg); i++) {
if (!isdigit((int)util_optarg[i])) {
goto usage;
}
}
dcLevel = (Mc_DcLevel) atoi(util_optarg);
break;
case 'b':
fwdBwd = McBwd_c;
break;
case 'V': /*Vacuity detection option*/
vd = TRUE;
break;
case 'B': /*Vacuity detection Beer et al method option*/
vd = TRUE;
beer = TRUE;
break;
case 'f':
debugOutName = util_strsav(util_optarg);
break;
case 'm':
useMore = TRUE;
break;
case 'r' :
reduceFsm = TRUE;
break;
case 'c':
useFormulaTree = TRUE;
break;
case 't' :
timeOutPeriod = atoi(util_optarg);
break;
case 'i' :
printInputs = TRUE;
break;
case 'F' :
traversalDirection = McFwd_c;
break;
case 'S' :
schedule = McStringConvertToScheduleType(util_optarg);
break;
case 'w':
variablesForSystem = util_strsav(util_optarg);
case 'W':
FAFWFlag = 1;
break;
case 'G':
GFAFWFlag = 1;
break;
case 'C' :
doCoverageHoskote = TRUE;
break;
case 'I' :
doCoverageImproved = TRUE;
break;
default:
goto usage;
}
}
/*
* Open the ctl file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** mc error: file containing ctl formulas not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** mc error: too many arguments\n");
goto usage;
}
McOptionsSetFwdBwd(options, fwdBwd);
McOptionsSetUseMore(options, useMore);
McOptionsSetReduceFsm(options, reduceFsm);
McOptionsSetVacuityDetect(options, vd);
McOptionsSetBeerMethod(options, beer);
McOptionsSetUseFormulaTree(options, useFormulaTree);
McOptionsSetPrintInputs(options, printInputs);
McOptionsSetTimeOutPeriod(options, timeOutPeriod);
McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
McOptionsSetCoverageHoskote(options, doCoverageHoskote);
McOptionsSetCoverageImproved(options, doCoverageImproved);
if((FAFWFlag > 0 || GFAFWFlag > 0) && dbgLevel == 0) {
fprintf(vis_stderr, "** mc warning : -w and -W options are ignored without -d option\n");
}
if((FAFWFlag > 0 || GFAFWFlag > 0) && printInputs == 0) {
fprintf(vis_stderr, "** mc warning : -i is recommended with -w or -W option\n");
}
if(FAFWFlag) {
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stderr, "** mc warning : -w and -W option is only available with CUDD\n");
FAFWFlag = 0;
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
}
if (schedule == McGSH_Unassigned_c) {
(void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
goto usage;
} else {
McOptionsSetSchedule(options, schedule);
}
inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
if (inputFp == NIL(FILE)) {
McOptionsFree(options);
if (guideFileName != NIL(char)) FREE(guideFileName);
return NIL(McOptions_t);
}
McOptionsSetCtlFile(options, inputFp);
if (debugOutName != NIL(char)) {
debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
FREE(debugOutName);
if (debugOut == NIL(FILE)) {
McOptionsFree(options);
if (guideFileName != NIL(char)) FREE(guideFileName);
return NIL(McOptions_t);
}
}
McOptionsSetDebugFile(options, debugOut);
if (guideFileName != NIL(char)) {
guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
if (guideFile == NIL(FILE)) {
fprintf(vis_stderr, "** mc error: cannot open guided search file %s.\n",
guideFileName);
FREE(guideFileName);
guideFileName = NIL(char);
McOptionsFree(options);
return NIL(McOptions_t);
}
FREE(guideFileName);
guideFileName = NIL(char);
}
McOptionsSetGuideFile(options, guideFile);
if (variablesForSystem != NIL(char)) {
systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
if (systemFile == NIL(FILE)) {
fprintf(vis_stderr, "** mc error: cannot open system variables file for FAFW %s.\n",
variablesForSystem);
FREE(variablesForSystem);
variablesForSystem = NIL(char);
McOptionsFree(options);
return NIL(McOptions_t);
}
FREE(variablesForSystem);
variablesForSystem = NIL(char);
}
McOptionsSetVariablesForSystem(options, systemFile);
if ((verbosityLevel != McVerbosityNone_c) &&
(verbosityLevel != McVerbosityLittle_c) &&
(verbosityLevel != McVerbositySome_c) &&
(verbosityLevel != McVerbosityMax_c)) {
goto usage;
}
else {
McOptionsSetVerbosityLevel(options, verbosityLevel);
}
if ((dbgLevel != McDbgLevelNone_c) &&
(dbgLevel != McDbgLevelMin_c) &&
(dbgLevel != McDbgLevelMinVerbose_c) &&
(dbgLevel != McDbgLevelMax_c) &&
(dbgLevel != McDbgLevelInteractive_c)) {
goto usage;
}
else {
McOptionsSetDbgLevel(options, dbgLevel);
}
if ((dcLevel != McDcLevelNone_c) &&
(dcLevel != McDcLevelRch_c ) &&
(dcLevel != McDcLevelRchFrontier_c ) &&
(dcLevel != McDcLevelArdc_c )) {
goto usage;
}
else {
McOptionsSetDcLevel(options, dcLevel);
}
McOptionsSetTraversalDirection(options, traversalDirection);
if (dcLevel == McDcLevelArdc_c) {
ardcOptions = Fsm_ArdcAllocOptionsStruct();
Fsm_ArdcGetDefaultOptions(ardcOptions);
} else
ardcOptions = NIL(Fsm_ArdcOptions_t);
McOptionsSetArdcOptions(options, ardcOptions);
return options;
usage:
(void) fprintf(vis_stderr, "usage: model_check [-b][-c][-d dbg_level][-f dbg_file][-g <hintfile>][-h][-i][-m][-r][-V][-B][-t period][-C][-I][-P][-v verbosity_level][-D dc_level][-F][-S <schedule>] <ctl_file>\n");
(void) fprintf(vis_stderr, " -b \tUse backward analysis in debugging\n");
(void) fprintf(vis_stderr, " -c \tNo sharing of CTL parse tree. This option does not matter for vacuity detection.\n");
(void) fprintf(vis_stderr, " -d <dbg_level>\n");
(void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n");
(void) fprintf(vis_stderr, " debug_level = 1 => automatic minimal debugging\n");
(void) fprintf(vis_stderr, " debug_level = 2 => automatic minimal debugging with extra verbosity\n");
(void) fprintf(vis_stderr, " debug_level = 3 => automatic maximal debugging\n");
(void) fprintf(vis_stderr, " debug_level = 4 => interactive debugging\n");
(void) fprintf(vis_stderr, " -f <dbg_out>\n");
(void) fprintf(vis_stderr, " write error trace to dbg_out\n");
(void) fprintf(vis_stderr, " -g <hint_file> \tSpecify file for guided search.\n");
(void) fprintf(vis_stderr, " -h \tPrints this usage message.\n");
(void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n");
(void) fprintf(vis_stderr, " -m \tPipe debug output through more.\n");
(void) fprintf(vis_stderr, " -r reduce FSM with respect to formula being verified\n");
(void) fprintf(vis_stderr, " -t <period> time out period\n");
(void) fprintf(vis_stderr, " -v <verbosity_level>\n");
(void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
(void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n");
(void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n");
(void) fprintf(vis_stderr, " -w <node file> \tSpecify variables controlled by system.\n");
(void) fprintf(vis_stderr, " -B vacuity detection for w-ACTL formulae using method of Beer et al \n");
(void) fprintf(vis_stderr, " -C Compute coverage of all observable signals using Hoskote et.al's implementation\n");
(void) fprintf(vis_stderr, " -D <dc_level>\n");
(void) fprintf(vis_stderr, " dc_level = 0 => no use of don't cares\n");
(void) fprintf(vis_stderr, " dc_level = 1 => use unreached states as don't cares (Default)\n");
(void) fprintf(vis_stderr, " dc_level = 2 => use unreached states as don't cares\n");
(void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n");
(void) fprintf(vis_stderr, " dc_level = 3 => use over-approximate unreached states as don't cares\n");
(void) fprintf(vis_stderr, " and aggressive use of DC's to simplify MDD's\n");
(void) fprintf(vis_stderr, " -F \tUse forward model checking.\n");
(void) fprintf(vis_stderr, " -G \tUse general fate and free will algorithm.\n");
(void) fprintf(vis_stderr, " -I Compute coverage of all observable signals using improved coverage implementation\n");
(void) fprintf(vis_stderr, " -S <schedule>\n");
(void) fprintf(vis_stderr, " schedule is one of {EL,EL1,EL2,budget,random,off}\n");
(void) fprintf(vis_stderr, " -V thorough vacuity detection\n");
(void) fprintf(vis_stderr, " -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
(void) fprintf(vis_stderr, " <ctl_file> The input file containing CTL formula to be checked.\n");
if (guideFileName != NIL(char)) FREE(guideFileName);
McOptionsFree(options);
return NIL(McOptions_t);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void PrintInvPassFail | ( | array_t * | invarFormulaArray, |
| int * | resultArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Prints whether the set of invariants passed or failed]
Description [Prints whether the set of invariants passed or failed.]
SideEffects []
Definition at line 3233 of file mcCmd.c.
{
int i;
Ctlp_Formula_t *formula;
fprintf(vis_stdout, "\n# INV: Summary of invariant pass/fail\n");
arrayForEachItem(Ctlp_Formula_t *, invarFormulaArray, i, formula) {
if (resultArray[i]) {
(void) fprintf(vis_stdout, "# INV: formula passed --- ");
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
fprintf(vis_stdout, "\n");
} else {
(void) fprintf(vis_stdout, "# INV: formula failed --- ");
Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
fprintf(vis_stdout, "\n");
}
}
return;
} /* end of PrintInvPassFail */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle function for timeout.]
Description [This function is called when the time out occurs. Since alarm is set with an elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire again later.]
SideEffects []
Definition at line 3178 of file mcCmd.c.
{
int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
if (seconds < mcTimeOut) {
unsigned slack = (unsigned) (mcTimeOut - seconds);
(void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
(void) alarm(slack);
} else {
longjmp(timeOutEnv, 1);
}
} /* TimeOutHandle */
Here is the caller graph for this function:
| static int UpdateResultArray | ( | mdd_t * | reachableStates, |
| array_t * | invarStatesArray, | ||
| int * | resultArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Check whether the reachable states violate the array of invariants.]
Description [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.]
SideEffects []
Definition at line 3205 of file mcCmd.c.
{
int i;
mdd_t *invariant;
int fail = 0;
arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
if (invariant == NIL(mdd_t)) continue;
if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
fail = 1;
resultArray[i] = 0;
}
}
return fail;
} /* end of UpdateResultArray */
Here is the caller graph for this function:
Variable Documentation
long alarmLapTime [static] |
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: mcCmd.c,v 1.27 2009/04/11 01:43:30 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mcCmd.c]
PackageName [mc]
Synopsis [Functions for CTL model checking commands.]
Description [This file contains the functions implementing the CTL model checking commands.]
SeeAlso []
Author [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Roderick Bloem, and others]
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.]
