/**CFile*********************************************************************** FileName [imcCmd.c] PackageName [imc] Synopsis [Command interface for the imc package.] Author [Jae-Young Jang ] 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.] ******************************************************************************/ #include "imcInt.h" #include "fsm.h" static char rcsid[] UNUSED = "$Id: imcCmd.c,v 1.24 2002/09/10 04:07:38 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static jmp_buf timeOutEnv; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CommandImc(Hrc_Manager_t ** hmgr, int argc, char ** argv); static void IterativeModelCheckUsage(void); static void TimeOutHandle(void); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the imc package.] SideEffects [] SeeAlso [Imc_End] ******************************************************************************/ void Imc_Init(void) { Cmd_CommandAdd("iterative_model_check", CommandImc, 0); } /**Function******************************************************************** Synopsis [Ends the imc package.] SideEffects [] SeeAlso [Imc_Init] ******************************************************************************/ void Imc_End(void) { } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static int CommandImc( Hrc_Manager_t ** hmgr, int argc, char ** argv) { 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; } /**Function******************************************************************** Synopsis [Prints the usage of the iterative_model_checking command.] SideEffects [] SeeAlso [CommandImc] ******************************************************************************/ static void IterativeModelCheckUsage(void) { fprintf(vis_stderr, "usage: iterative_model_check [-h] [-x]"); fprintf(vis_stderr, "[-t ] [-v ] [-D ] [-r ]"); fprintf(vis_stderr, "[-i