#include "imcInt.h"#include "fsm.h"
Include dependency graph for imcCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandImc (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | IterativeModelCheckUsage (void) |
| static void | TimeOutHandle (void) |
| void | Imc_Init (void) |
| void | Imc_End (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imcCmd.c,v 1.24 2002/09/10 04:07:38 fabio Exp $" |
| static jmp_buf | timeOutEnv |
Function Documentation
| static int CommandImc | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [The iterative_model_check command.]
Description [The function starts by parsing the options. After that it checks for the network structure. The CTL formulas are read and checked for correctness. Once the formulas have been read, they need to be translated from the CTL representation to the operational graph representation required for the iterative algorithm. The next state functions of the variables are computed according to partition option when 'build_partition_mdds' has not been invoked. Then iterative model checking is applied to each formula. The value specified by -i option is used as incremental size (let's say N). At first, the state transion functions of N state variables shown in the formula are computed exactly. All the others are approximated. If a conclusive answer cannot be computed, the system is refined by converting N approximate next state functions to be exact and try to verify again. This procedure continues until a correct answer is found. See \[1,2\] for details.]
CommandName [iterative_model_check]
CommandSynopsis [Perform CTL model checking on an abstracted system with automatic refinement algorithm.]
CommandArguments [\[-h\] \[-x\] \[-t <seconds>\] \[-v <number>\]\ \[-D <number>\] \[-r <number>\] \[-i <number>\] \ \[-p <number>\] \[-g <number>\] <ctlfile>]]
CommandDescription [
Command options:
- -h
Print the command usage.
- -x
Perform the verification exactly. No approximation is done.
- -t <secs>
Time in seconds allowed for verification. The default is no limit.
- -v <number>
Specify verbosity level. Use 0 for no feedback (default), 1 for more, and 2 for maximum feedback.
- -D <number>
Specify extent to which don't cares are used to simplify the MDDs.
- 0: No don't cares used. This is the default.
- 1: Use reachability information to compute the don't-care set.
- 2: Use reachability information, and minimize the transition relation with respect to the `frontier set' (aggresive minimization).
- 3: Use approximate reachability information.
- -r <number>
Specify refinement method.
- 0: Static scheduling by name sorting. Fast, easy, but less accurate.
- 1: Static scheduling by latch affinity. Slow, but more accurate. This is the default.
- -i <number>
The number of state variables to be added for exact computation at each iteration. The default is 4.
- -l <number>
Type of lower-bound approximation method.
- 0: Take a subset of each transition sub-relation by BDD subsetting.
- 1: Take a subset by universal quantification. This is the default.
- -p <number>
Type of partition method. If 'build_partition_mdds' is already invoked, this option is ignored. Notice that some next state functions might not be available after iterative_model_checking command is performed because of this option.
- 0: Build all next state functions. Same as 'build_partition_mdds'. This is the default.
- 1: Build the next state functions related to the formulas. Build all next state functions that are necessary to prove all formulas.
- 2: Build the next state functions incrementally. None of next state functions are removed.
- -g <number>
Type of operational graph.
- 0: Negative Operational Graph. Good to prove a formula true.
- 1: Positive Operational Graph. Good to prove a formula false.
- 2: Mixed Operational Graph. Good to prove any formula, but it may be slower. This is the default.
- <ctlfile>
File containing the CTL formulas to be verified.
- 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".
- See also commands : model_check, incremental_ctl_verification
1. Jae-Young Jang, In-Ho Moon, and Gary D. Hachtel. Iterative Abstraction-based CTL Model Checking. Design, Automation and Test in Europe (DATE), 2000
2. Jae-Young Jang. Iterative Abstraction-based CTL Model Checking. Ph. D. Thesis. University of Colorado, 1999. ]
SideEffects []
Definition at line 226 of file imcCmd.c.
{
static int timeOutPeriod; /* CPU seconds allowed */
char *ctlFileName; /* Name of file containing formulas */
FILE *ctlFile; /* File to read the formulas from */
Ntk_Network_t *network; /* Pointer to the current network */
array_t *ctlFormulaArray; /* Array of read ctl formulas */
array_t *ctlNormalForm; /* Array of normal ctl formulas */
Ctlp_Formula_t *formula; /* Formula being verified */
Ctlp_Formula_t *orgFormula;
Ctlp_Formula_t *currentFormula;
char *modelName;
Hrc_Node_t *currentNode;
int c, i;
array_t *dagFormula;
Imc_RefineMethod refine; /* Refine Method */
mdd_t *careStates; /* Care States */
Imc_DcLevel dcLevel; /* Don't Care Level */
Imc_VerbosityLevel verbosity; /* Verbosity level */
Fsm_Fsm_t *reducedFsm;
Fsm_Fsm_t *exactFsm;
int incrementalSize;
int option;
Fsm_ArdcOptions_t *ardcOptions;
Imc_GraphType graphType;
Imc_LowerMethod lowerMethod;
Imc_UpperMethod upperMethod;
boolean needLower, needUpper;
boolean computeExact;
Imc_PartMethod partMethod;
graph_t *partition;
long globalTimeStart;
long globalTimeEnd;
long initialTime;
long finalTime;
/* Initialize Default Values */
timeOutPeriod = 0;
ctlFileName = NIL(char);
verbosity = Imc_VerbosityNone_c;
dcLevel = Imc_DcLevelNone_c;
incrementalSize = 4;
lowerMethod = Imc_LowerUniversalQuantification_c;
upperMethod = Imc_UpperExistentialQuantification_c;
computeExact = FALSE;
partMethod = Imc_PartAll_c;
refine = Imc_RefineLatchRelation_c;
graphType = Imc_GraphMOG_c;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "hxt:r:i:l:p:v:D:g:")) != EOF) {
switch(c) {
case 'h':
IterativeModelCheckUsage();
return 1;
case 'x':
computeExact = TRUE;
break;
case 't':
timeOutPeriod = atoi(util_optarg);
if (timeOutPeriod < 0){
fprintf(vis_stdout,"** imc warning : Timeout Option -t %s is not defined.\n",
util_optarg);
IterativeModelCheckUsage();
return 1;
}
break;
case 'r':
option = atoi(util_optarg);
if (option == 0) refine = Imc_RefineSort_c;
else if (option == 1) refine = Imc_RefineLatchRelation_c;
else{
fprintf(vis_stdout,"** imc warning : Refine option -r %d is not defined.\n",
option);
IterativeModelCheckUsage();
return 1;
}
break;
case 'i':
incrementalSize = atoi(util_optarg);
if (incrementalSize<1){
fprintf(vis_stdout,"** imc warning : Incremental size option -i %d",
incrementalSize);
fprintf(vis_stdout," is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
case 'l':
option = atoi(util_optarg);
if (option==0){
lowerMethod = Imc_LowerSubsetTR_c;
}else if (option==1){
lowerMethod = Imc_LowerUniversalQuantification_c;
}else{
fprintf(vis_stdout,"** imc warning : Lower bound option option -l %d",
option);
fprintf(vis_stdout," is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
case 'p':
option = atoi(util_optarg);
if (option==0){
partMethod = Imc_PartAll_c;
}else if (option==1){
partMethod = Imc_PartDepend_c;
}else if (option==2){
partMethod = Imc_PartInc_c;
}else{
fprintf(vis_stdout,"** imc warning : Partition option -p %d",
option);
fprintf(vis_stdout," is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
case 'v':
option = atoi(util_optarg);
if (option == 0) verbosity = Imc_VerbosityNone_c;
else if (option == 1) verbosity = Imc_VerbosityMin_c;
else if (option == 2) verbosity = Imc_VerbosityMax_c;
else{
fprintf(vis_stdout,"** imc warning : Verbosity option -v %d",
option);
fprintf(vis_stdout, " is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
case 'D':
option = atoi(util_optarg);
if (option == 0) dcLevel = Imc_DcLevelNone_c;
else if (option == 1) dcLevel = Imc_DcLevelRch_c;
else if (option == 2) dcLevel = Imc_DcLevelMax_c;
else if (option == 3) dcLevel = Imc_DcLevelArdc_c;
else{
fprintf(vis_stdout,"** imc warning : Don't care option -D %d",
option);
fprintf(vis_stdout, " is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
case 'g':
option = atoi(util_optarg);
if (option == 0) graphType = Imc_GraphNDOG_c;
else if (option == 1) graphType = Imc_GraphPDOG_c;
else if (option == 2) graphType = Imc_GraphMOG_c;
else{
fprintf(vis_stdout,"** imc warning : Graph type option -g %d",
option);
fprintf(vis_stdout," is not defined.\n");
IterativeModelCheckUsage();
return 1;
}
break;
default:
IterativeModelCheckUsage();
return 1;
}
}
/* Make sure the CTL file has been provided */
if (argc == util_optind) {
IterativeModelCheckUsage();
return 1;
}
else {
ctlFileName = argv[util_optind];
}
/*
* Obtain the network from the hierarchy manager
*/
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
return 1;
}
/*
* Read in the array of CTL formulas provided in ctlFileName
*/
ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
if (ctlFile == NIL(FILE)) {
return 1;
}
ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
fclose(ctlFile);
if (ctlFormulaArray == NIL(array_t)) {
fprintf(vis_stderr, "** imc error: Error while parsing ctl formulas in file.\n");
return 1;
}
/*
* Start the timer.
*/
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
/* The second time setjmp is called, it returns here !!*/
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "IMC: Timeout occurred after %d seconds.\n",
timeOutPeriod);
alarm(0);
/* Note that there is a huge memory leak here. */
Ctlp_FormulaArrayFree(ctlFormulaArray);
return 1;
}
}
currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
modelName = Hrc_NodeReadModelName(currentNode);
partition = Part_NetworkReadPartition(network);
exactFsm = NIL(Fsm_Fsm_t);
reducedFsm = NIL(Fsm_Fsm_t);
careStates = NIL(mdd_t);
if ((computeExact)&&(partMethod == Imc_PartInc_c)){
partMethod = Imc_PartDepend_c;
}
if ((dcLevel != Imc_DcLevelNone_c) && (partMethod == Imc_PartInc_c)){
partMethod = Imc_PartDepend_c;
}
if (partition == NIL(graph_t) && (partMethod != Imc_PartInc_c)){
if (partMethod == Imc_PartAll_c){
partition = Part_NetworkCreatePartition(network, currentNode, modelName,
(lsList)0, (lsList)0, NIL(mdd_t),
Part_InOut_c, (lsList)0, FALSE,
verbosity, 0);
Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
(void *) partition);
}else if (partMethod == Imc_PartDepend_c){
partition = Part_PartCreatePartitionWithCTL(hmgr, Part_InOut_c, verbosity,
0, FALSE, ctlFormulaArray, NIL(array_t));
/* Register the partition in the network if any */
Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
(void *) partition);
}
}
if (partition != NIL(graph_t)){
exactFsm = Fsm_NetworkReadOrCreateFsm(network);
reducedFsm = Mc_ConstructReducedFsm(network, ctlFormulaArray);
if (reducedFsm==NIL(Fsm_Fsm_t)){
reducedFsm = exactFsm;
}
/*
* Check whether the fairness was read. Fairnedd is ignored.
*/
{
Fsm_Fairness_t *fairCons = Fsm_FsmReadFairnessConstraint(exactFsm);
int numOfConj = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
if (numOfConj > 1) {
/* Buchi */
fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
}else if (numOfConj == 1){
/* check if fairness is simply default fairness formula, which is TRUE */
Ctlp_Formula_t *formula = Fsm_FairnessReadFinallyInfFormula(fairCons, 0, 0);
if (Ctlp_FormulaReadType(formula) != Ctlp_TRUE_c){
fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
}
}
}
}
globalTimeStart = util_cpu_time();
if (partition != NIL(graph_t)){
if (dcLevel == Imc_DcLevelArdc_c){
if (verbosity != Imc_VerbosityNone_c){
fprintf(vis_stdout, "IMC: Computing approximate reachable states.\n");
}
ardcOptions = Fsm_ArdcAllocOptionsStruct();
Fsm_ArdcGetDefaultOptions(ardcOptions);
initialTime = util_cpu_time();
(void) Fsm_ArdcComputeOverApproximateReachableStates(
reducedFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
finalTime = util_cpu_time();
if (verbosity != Imc_VerbosityNone_c) {
Fsm_ArdcPrintReachabilityResults(reducedFsm, finalTime - initialTime);
}
/* CW::user is responsible to free Fsm_ArdcGetMdd...
careStates
= mdd_dup(Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm));
*/
careStates
= Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm);
}else if (dcLevel >= Imc_DcLevelRch_c){
if (verbosity != Imc_VerbosityNone_c){
fprintf(vis_stdout, "IMC: Computing exact reachable states.\n");
}
initialTime = util_cpu_time();
careStates = Fsm_FsmComputeReachableStates(reducedFsm,
0, 1, 0, 0, 0, 0, 0,
Fsm_Rch_Default_c, 0, 0,
NIL(array_t), FALSE, NIL(array_t));
finalTime = util_cpu_time();
if (verbosity != Imc_VerbosityNone_c) {
Fsm_FsmReachabilityPrintResults(reducedFsm, finalTime - initialTime,
Fsm_Rch_Default_c);
}
}else{
careStates = NIL(mdd_t);
}
if (reducedFsm != NIL(Fsm_Fsm_t) &&
Fsm_FsmReadImageInfo(reducedFsm) != NIL(Img_ImageInfo_t)) {
Fsm_FsmFreeImageInfo(reducedFsm);
}
}
ctlNormalForm = Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
ctlFormulaArray);
/*
* Loop over every CTL formula in the array
*/
arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
Ctlp_FormulaClass formulaClass;
array_t * singleFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
array_insert(Ctlp_Formula_t *, singleFormulaArray, 0, currentFormula);
dagFormula = Ctlp_FormulaArrayConvertToDAG(singleFormulaArray);
array_free(singleFormulaArray);
formula = array_fetch(Ctlp_Formula_t *, dagFormula, 0);
array_free(dagFormula);
formulaClass = Ctlp_CheckClassOfExistentialFormula(formula);
/*
* Type of approximation needed for verification
*
* pDOG nDOG MOG
* ---------------------
* ACTL L U B
* ECTL U L B
* Mixed B B B
*/
if ((formulaClass == Ctlp_Mixed_c) || (graphType == Imc_GraphMOG_c)){
needLower = TRUE;
needUpper = TRUE;
}else if (((formulaClass == Ctlp_ACTL_c) && (graphType == Imc_GraphPDOG_c)) ||
((formulaClass == Ctlp_ECTL_c) && (graphType == Imc_GraphNDOG_c))){
needLower = TRUE;
needUpper = FALSE;
}else{
needLower = FALSE;
needUpper = TRUE;
}
if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula,network,FALSE)){
(void) fprintf(vis_stdout, "\n** imc error: Error in parsing formula:\n%s\n",
error_string());
error_init();
continue;
}
error_init();
initialTime = util_cpu_time();
orgFormula = array_fetch(Ctlp_Formula_t *, ctlFormulaArray, i);
Imc_ImcEvaluateFormulaLinearRefine(network, orgFormula, formula,
formulaClass, incrementalSize, verbosity, refine, careStates, reducedFsm,
dcLevel, graphType, lowerMethod, upperMethod, computeExact, needLower,
needUpper, partMethod, currentNode, modelName);
finalTime = util_cpu_time();
if(verbosity != Imc_VerbosityNone_c) {
(void) fprintf(vis_stdout, "%-20s%10ld\n\n",
"IMC: Verification time for this formula =",
(finalTime - initialTime) / 1000);
}
fprintf(vis_stdout, "\n");
} /* End of arrayForEachItem in ctlFormulaArray */
if (careStates)
mdd_free(careStates); /* FIXED */
globalTimeEnd = util_cpu_time();
if (verbosity != Imc_VerbosityNone_c) {
(void) fprintf(vis_stdout, "%-20s%10ld\n\n",
"IMC: Total verification time =",
(globalTimeEnd - globalTimeStart) / 1000);
}
/* Deactivate the alarm */
alarm(0);
if ((reducedFsm != NIL(Fsm_Fsm_t)) && (exactFsm != reducedFsm)){
Fsm_FsmFree(reducedFsm);
}
Ctlp_FormulaArrayFree(ctlFormulaArray);
Ctlp_FormulaArrayFree(ctlNormalForm);
error_cleanup();
/* normal exit */
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Imc_End | ( | void | ) |
| void Imc_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the imc package.]
SideEffects []
SeeAlso [Imc_End]
Definition at line 72 of file imcCmd.c.
{
Cmd_CommandAdd("iterative_model_check", CommandImc, 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void IterativeModelCheckUsage | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Prints the usage of the iterative_model_checking command.]
SideEffects []
SeeAlso [CommandImc]
Definition at line 667 of file imcCmd.c.
{
fprintf(vis_stderr, "usage: iterative_model_check [-h] [-x]");
fprintf(vis_stderr, "[-t <secs>] [-v <number>] [-D <number>] [-r <number>]");
fprintf(vis_stderr, "[-i <number] [-l <number] [-p <number] [-g <number] ctlfile\n");
fprintf(vis_stderr, " -h print the command usage\n");
fprintf(vis_stderr, " -x Exact verification\n");
fprintf(vis_stderr, " -t secs Seconds allowed for computation\n");
fprintf(vis_stderr, " -v number verbosity level (0:none, 1:mid, 2:max)\n");
fprintf(vis_stderr, " -D number Don't care level. DC's are used to\n");
fprintf(vis_stderr, " reduce transition relation\n");
fprintf(vis_stderr, " 0 No don't care (default)\n");
fprintf(vis_stderr, " 1 Exact reachable states\n");
fprintf(vis_stderr, " 2 Aggressively use DC's\n");
fprintf(vis_stderr, " 3 Approximate reachable states\n");
fprintf(vis_stderr, " -r number Refinement method\n");
fprintf(vis_stderr, " 0 Static scheduling by name sorting\n");
fprintf(vis_stderr, " 1 Static scheduling by latch affinity (defualt)\n");
fprintf(vis_stderr, " -i number Incremental size (default = 4)\n");
fprintf(vis_stderr, " -l number Type of lower-bound approximation method\n");
fprintf(vis_stderr, " 0 Take a subset of each transition sub-relation\n");
fprintf(vis_stderr, " 1 Take a subset by universal quantification (default)\n");
fprintf(vis_stderr, " -p number Type of partition method\n");
fprintf(vis_stderr, " 0 Build all next state functions (default)\n");
fprintf(vis_stderr, " 1 Build the next state functions related to formulas\n");
fprintf(vis_stderr, " 2 Build the next state functions incrementally\n");
fprintf(vis_stderr, " -g number Type of operational graph\n");
fprintf(vis_stderr, " 0 Negative Operational Graph\n");
fprintf(vis_stderr, " 1 Positive Operational Graph\n");
fprintf(vis_stderr, " 2 Mixed Operational Graph (default)\n");
fprintf(vis_stderr, " ctlfile File containing the ctl formulas\n");
return;
} /* End of IterativeModelCheckUsage */
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle the timeout signal.]
Description [This function is called when the time out occurs. In principle it could do something smarter, but so far it just transfers control to the point in the code where setjmp was called.]
SideEffects [This function gains control at any point in the middle of the computation, therefore the memory allocated so far leaks.]
Definition at line 716 of file imcCmd.c.
{
longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */
Here is the caller graph for this function:
Variable Documentation
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: imcCmd.c,v 1.24 2002/09/10 04:07:38 fabio Exp $" [static] |
CFile***********************************************************************
FileName [imcCmd.c]
PackageName [imc]
Synopsis [Command interface for the imc package.]
Author [Jae-Young Jang <jjang@vlsi.colorado.edu>]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
