source: vis_dev/vis-2.3/src/imc/imcCmd.c @ 93

Last change on this file since 93 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 25.3 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [imcCmd.c]
4
5  PackageName [imc]
6
7  Synopsis    [Command interface for the imc package.]
8
9  Author      [Jae-Young Jang <jjang@vlsi.colorado.edu>]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "imcInt.h"
18#include "fsm.h"
19
20static char rcsid[] UNUSED = "$Id: imcCmd.c,v 1.24 2002/09/10 04:07:38 fabio Exp $";
21
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/*---------------------------------------------------------------------------*/
28/* Structure declarations                                                    */
29/*---------------------------------------------------------------------------*/
30
31/*---------------------------------------------------------------------------*/
32/* Type declarations                                                         */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Variable declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39static jmp_buf timeOutEnv;
40
41/*---------------------------------------------------------------------------*/
42/* Macro declarations                                                        */
43/*---------------------------------------------------------------------------*/
44
45/**AutomaticStart*************************************************************/
46
47/*---------------------------------------------------------------------------*/
48/* Static function prototypes                                                */
49/*---------------------------------------------------------------------------*/
50
51static int CommandImc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
52static void IterativeModelCheckUsage(void);
53static void TimeOutHandle(void);
54
55/**AutomaticEnd***************************************************************/
56
57
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62/**Function********************************************************************
63
64  Synopsis    [Initializes the imc package.]
65
66  SideEffects []
67
68  SeeAlso     [Imc_End]
69
70******************************************************************************/
71void
72Imc_Init(void)
73{
74  Cmd_CommandAdd("iterative_model_check", CommandImc, 0);
75}
76
77
78/**Function********************************************************************
79
80  Synopsis    [Ends the imc package.]
81
82  SideEffects []
83
84  SeeAlso     [Imc_Init]
85
86******************************************************************************/
87void
88Imc_End(void)
89{
90}
91
92
93/*---------------------------------------------------------------------------*/
94/* Definition of internal functions                                          */
95/*---------------------------------------------------------------------------*/
96
97
98/*---------------------------------------------------------------------------*/
99/* Definition of static functions                                            */
100/*---------------------------------------------------------------------------*/
101
102/**Function********************************************************************
103
104  Synopsis         [The iterative_model_check command.]
105
106  Description      [The function starts by parsing the options. After that it
107  checks for the network structure. The CTL formulas are read and checked for
108  correctness. Once the formulas have been read, they need to be translated
109  from the CTL representation to the operational graph representation required
110  for the iterative algorithm. The next state functions of the variables are
111  computed according to partition option when 'build_partition_mdds' has not
112  been invoked. Then iterative model checking is applied to each formula. The
113  value specified by -i option is used as incremental size (let's say N).
114  At first, the state transion functions of N state variables shown in the
115  formula are computed exactly. All the others are approximated. If a
116  conclusive answer cannot be computed, the system is refined by converting
117  N approximate next state functions to be exact and try to verify again.
118  This procedure continues until a correct answer is found. See \[1,2\] for
119  details.]
120
121  CommandName      [iterative_model_check]
122
123  CommandSynopsis  [Perform CTL model checking on an abstracted system with
124  automatic refinement algorithm.]
125
126  CommandArguments [\[-h\] \[-x\] \[-t &lt;seconds&gt;\] \[-v &lt;number&gt;\]\
127  \[-D &lt;number&gt;\] \[-r &lt;number&gt;\] \[-i &lt;number&gt;\] \
128  \[-p &lt;number&gt;\] \[-g &lt;number&gt;\] &lt;ctlfile&gt;]]
129
130  CommandDescription [ 
131  <p>Command options:<p>
132
133  <dl>
134
135  <dt> -h
136  <dd> Print the command usage.
137
138  <dt> -x
139  <dd> Perform the verification exactly. No approximation is done.
140
141  <dt> -t &lt;secs&gt;
142  <dd> Time in seconds allowed for verification.  The default is no limit.
143
144  <dt> -v &lt;number&gt;
145  <dd>Specify verbosity level. Use 0 for no feedback (default), 1
146  for more, and 2 for maximum feedback.
147
148  <dt> -D &lt;number&gt;
149  <dd> Specify extent to which don't cares are used to simplify the MDDs.
150  <ul>
151  <li>0: No don't cares used.  This is the default.
152  <li>1: Use reachability information to compute the don't-care set.
153  <li>2: Use reachability information, and minimize the transition relation
154     with respect to the `frontier set' (aggresive minimization).
155  <li>3: Use approximate reachability information.
156  </ul>
157
158  <dt> -r &lt;number&gt;
159  <dd> Specify refinement method.
160  <ul>
161  <li>0: Static scheduling by name sorting. Fast, easy, but less accurate.
162  <li>1: Static scheduling by latch affinity. Slow, but more accurate.  This
163         is the default.
164  </ul>
165
166  <dt> -i &lt;number&gt;
167  <dd> The number of state variables to be added for exact computation at
168   each iteration.  The default is 4.
169
170  <dt> -l &lt;number&gt;
171  <dd> Type of lower-bound approximation method.
172  <ul>
173  <li>0: Take a subset of each transition sub-relation by BDD subsetting.
174  <li>1: Take a subset by universal quantification.  This is the default.
175  </ul>
176
177  <dt> -p &lt;number&gt;
178  <dd> Type of partition method. If 'build_partition_mdds' is already invoked,
179  this option is ignored. Notice that some next state functions might not be
180  available after iterative_model_checking command is performed because of
181  this option.
182  <ul>
183  <li>0: Build all next state functions. Same as 'build_partition_mdds'.
184         This is the default.
185  <li>1: Build the next state functions related to the formulas. Build all
186         next state functions that are necessary to prove all formulas.
187  <li>2: Build the next state functions incrementally. None of next state
188         functions are removed.
189  </ul>
190
191  <dt> -g &lt;number&gt;
192  <dd> Type of operational graph.
193  <ul>
194  <li>0: Negative Operational Graph. Good to prove a formula true.
195  <li>1: Positive Operational Graph. Good to prove a formula false.
196  <li>2: Mixed Operational Graph. Good to prove any formula, but it may
197         be slower.  This is the default.
198  </ul>
199
200  <dt> &lt;ctlfile&gt;
201  <dd> File containing the CTL formulas to be verified.
202
203  <dt> Related "set" options: <p>
204  <dt> ctl_change_bracket &lt;yes/no&gt;
205  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
206  therefore CTL parser does the same thing. However, in some cases a user
207  does not want to change node names in CTL parsing. Then, use this set
208  option by giving "no".  Default is "yes".
209  <p>
210
211  <dt> See also commands : model_check, incremental_ctl_verification <p>
212
213  </dl>
214
215  <p>1. Jae-Young Jang, In-Ho Moon, and Gary D. Hachtel. Iterative
216  Abstraction-based CTL Model Checking. Design, Automation and Test in Europe
217  (DATE), 2000
218  <p>2. Jae-Young Jang. Iterative Abstraction-based CTL Model Checking.
219  Ph. D. Thesis. University of Colorado, 1999. 
220  ]
221
222  SideEffects []
223
224******************************************************************************/
225static int
226CommandImc(
227  Hrc_Manager_t ** hmgr,
228  int  argc,
229  char ** argv)
230{
231  static int          timeOutPeriod;      /* CPU seconds allowed */
232  char                *ctlFileName;       /* Name of file containing formulas */
233  FILE                *ctlFile;           /* File to read the formulas from */
234  Ntk_Network_t       *network;           /* Pointer to the current network */
235  array_t             *ctlFormulaArray;   /* Array of read ctl formulas */
236  array_t             *ctlNormalForm;     /* Array of normal ctl formulas */
237  Ctlp_Formula_t      *formula;           /* Formula being verified */
238  Ctlp_Formula_t      *orgFormula; 
239  Ctlp_Formula_t      *currentFormula; 
240  char                *modelName;
241  Hrc_Node_t          *currentNode;
242  int                 c, i;
243  array_t             *dagFormula;
244  Imc_RefineMethod    refine;             /* Refine Method */
245  mdd_t               *careStates;        /* Care States */
246  Imc_DcLevel         dcLevel;            /* Don't Care Level */
247  Imc_VerbosityLevel  verbosity;          /* Verbosity level */
248  Fsm_Fsm_t           *reducedFsm;
249  Fsm_Fsm_t           *exactFsm;
250  int                 incrementalSize;
251  int                 option;
252  Fsm_ArdcOptions_t   *ardcOptions;
253  Imc_GraphType       graphType;
254  Imc_LowerMethod     lowerMethod;
255  Imc_UpperMethod     upperMethod;
256  boolean             needLower, needUpper;
257  boolean             computeExact;
258  Imc_PartMethod      partMethod;
259  graph_t             *partition;
260
261  long globalTimeStart;
262  long globalTimeEnd;
263  long initialTime;
264  long finalTime;
265
266
267  /* Initialize Default Values */
268  timeOutPeriod    = 0;
269  ctlFileName      = NIL(char);
270  verbosity        = Imc_VerbosityNone_c;
271  dcLevel          = Imc_DcLevelNone_c;
272  incrementalSize  = 4;
273  lowerMethod      = Imc_LowerUniversalQuantification_c;
274  upperMethod      = Imc_UpperExistentialQuantification_c;
275  computeExact     = FALSE;
276  partMethod       = Imc_PartAll_c;
277  refine           = Imc_RefineLatchRelation_c;
278  graphType        = Imc_GraphMOG_c;
279
280  /*
281   * Parse command line options.
282   */
283  util_getopt_reset();
284  while ((c = util_getopt(argc, argv, "hxt:r:i:l:p:v:D:g:")) != EOF) {
285    switch(c) {
286      case 'h':
287        IterativeModelCheckUsage();
288        return 1;
289      case 'x':
290        computeExact = TRUE;
291        break;
292      case 't':
293        timeOutPeriod = atoi(util_optarg);
294        if (timeOutPeriod < 0){
295          fprintf(vis_stdout,"** imc warning : Timeout Option -t %s is not defined.\n",
296                  util_optarg);
297          IterativeModelCheckUsage();
298          return 1;
299        }
300              break;
301      case 'r':
302        option = atoi(util_optarg);
303        if (option == 0) refine = Imc_RefineSort_c;
304        else if (option == 1) refine = Imc_RefineLatchRelation_c;
305        else{
306          fprintf(vis_stdout,"** imc warning : Refine option -r %d is not defined.\n",
307                  option);
308          IterativeModelCheckUsage();
309          return 1;
310        }
311        break;
312      case 'i':
313        incrementalSize = atoi(util_optarg);
314        if (incrementalSize<1){
315          fprintf(vis_stdout,"** imc warning : Incremental size option -i %d",
316                  incrementalSize);
317          fprintf(vis_stdout," is not defined.\n");
318          IterativeModelCheckUsage();
319          return 1;
320        }
321        break;
322      case 'l':
323        option = atoi(util_optarg);
324        if (option==0){
325          lowerMethod = Imc_LowerSubsetTR_c;
326        }else if (option==1){
327          lowerMethod = Imc_LowerUniversalQuantification_c;
328        }else{
329          fprintf(vis_stdout,"** imc warning : Lower bound option option -l %d",
330                  option);
331          fprintf(vis_stdout," is not defined.\n");
332          IterativeModelCheckUsage();
333          return 1;
334        }
335        break;
336      case 'p':
337        option = atoi(util_optarg);
338        if (option==0){
339          partMethod = Imc_PartAll_c;
340        }else if (option==1){
341          partMethod = Imc_PartDepend_c;
342        }else if (option==2){
343          partMethod = Imc_PartInc_c;
344        }else{
345          fprintf(vis_stdout,"** imc warning : Partition option -p %d",
346                  option);
347          fprintf(vis_stdout," is not defined.\n");
348          IterativeModelCheckUsage();
349          return 1;
350        }
351        break;
352      case 'v':
353        option = atoi(util_optarg);
354        if (option == 0) verbosity = Imc_VerbosityNone_c;
355        else if (option == 1) verbosity = Imc_VerbosityMin_c;
356              else if (option == 2) verbosity = Imc_VerbosityMax_c;
357        else{
358                fprintf(vis_stdout,"** imc warning : Verbosity option -v %d",
359                        option);
360                fprintf(vis_stdout, " is not defined.\n");
361          IterativeModelCheckUsage();
362          return 1;
363              }
364        break;
365      case 'D':
366        option = atoi(util_optarg);
367              if (option == 0) dcLevel = Imc_DcLevelNone_c;
368        else if (option == 1) dcLevel = Imc_DcLevelRch_c;
369              else if (option == 2) dcLevel = Imc_DcLevelMax_c;
370              else if (option == 3) dcLevel = Imc_DcLevelArdc_c;
371        else{
372                fprintf(vis_stdout,"** imc warning : Don't care option -D %d",
373                        option);
374                fprintf(vis_stdout, " is not defined.\n");
375          IterativeModelCheckUsage();
376          return 1;
377              }
378        break;
379      case 'g':
380        option = atoi(util_optarg);
381        if (option == 0) graphType = Imc_GraphNDOG_c;
382        else if (option == 1) graphType = Imc_GraphPDOG_c;
383        else if (option == 2) graphType = Imc_GraphMOG_c;
384        else{
385                fprintf(vis_stdout,"** imc warning : Graph type option -g %d",
386                        option);
387                fprintf(vis_stdout," is not defined.\n");
388          IterativeModelCheckUsage();
389          return 1;
390              }
391        break;   
392      default:
393              IterativeModelCheckUsage();
394              return 1;
395    }
396  }
397
398  /* Make sure the CTL file has been provided */
399  if (argc == util_optind) {
400    IterativeModelCheckUsage();
401    return 1;
402  }
403  else {
404    ctlFileName = argv[util_optind];
405  }
406
407  /*
408   * Obtain the network from the hierarchy manager
409   */
410  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
411  if (network == NIL(Ntk_Network_t)) {
412    return 1;
413  }
414
415  /*
416   * Read in the array of CTL formulas provided in ctlFileName
417   */
418  ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
419  if (ctlFile == NIL(FILE)) {
420    return 1;
421  }
422  ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
423  fclose(ctlFile);
424
425  if (ctlFormulaArray == NIL(array_t)) {
426    fprintf(vis_stderr, "** imc error: Error while parsing ctl formulas in file.\n");
427    return 1;
428  } 
429
430  /*
431   * Start the timer.
432   */
433  if (timeOutPeriod > 0) {
434    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
435    (void) alarm(timeOutPeriod);
436
437    /* The second time setjmp is called, it returns here !!*/
438    if (setjmp(timeOutEnv) > 0) {
439      (void) fprintf(vis_stdout, "IMC: Timeout occurred after %d seconds.\n",
440                     timeOutPeriod);
441      alarm(0);
442
443      /* Note that there is a huge memory leak here. */
444      Ctlp_FormulaArrayFree(ctlFormulaArray);
445      return 1;
446    } 
447  }
448
449  currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
450  modelName = Hrc_NodeReadModelName(currentNode);
451  partition = Part_NetworkReadPartition(network);
452
453  exactFsm = NIL(Fsm_Fsm_t);
454  reducedFsm = NIL(Fsm_Fsm_t);
455  careStates = NIL(mdd_t);
456
457  if ((computeExact)&&(partMethod == Imc_PartInc_c)){
458    partMethod = Imc_PartDepend_c;
459  }
460
461  if ((dcLevel != Imc_DcLevelNone_c) && (partMethod == Imc_PartInc_c)){
462    partMethod = Imc_PartDepend_c;
463  }
464
465  if (partition == NIL(graph_t) && (partMethod != Imc_PartInc_c)){
466    if (partMethod == Imc_PartAll_c){
467
468      partition = Part_NetworkCreatePartition(network, currentNode, modelName,
469                                          (lsList)0, (lsList)0, NIL(mdd_t),
470                                          Part_InOut_c, (lsList)0, FALSE,
471                                          verbosity, 0);
472      Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
473                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
474                          (void *) partition);
475
476    }else if (partMethod == Imc_PartDepend_c){
477      partition = Part_PartCreatePartitionWithCTL(hmgr, Part_InOut_c, verbosity, 
478                                      0, FALSE, ctlFormulaArray, NIL(array_t));
479      /* Register the partition in the network if any */
480      Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
481                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
482                          (void *) partition);
483    }
484  }
485 
486  if (partition != NIL(graph_t)){ 
487    exactFsm = Fsm_NetworkReadOrCreateFsm(network); 
488    reducedFsm = Mc_ConstructReducedFsm(network, ctlFormulaArray);
489    if (reducedFsm==NIL(Fsm_Fsm_t)){
490      reducedFsm = exactFsm;
491    }
492
493    /*
494     * Check whether the fairness was read. Fairnedd is ignored.
495     */
496    {
497      Fsm_Fairness_t *fairCons =  Fsm_FsmReadFairnessConstraint(exactFsm);
498      int numOfConj     = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
499      if (numOfConj > 1) {
500        /* Buchi */
501        fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
502        fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
503      }else if (numOfConj == 1){
504        /* check if fairness is simply default fairness formula, which is TRUE */
505        Ctlp_Formula_t *formula = Fsm_FairnessReadFinallyInfFormula(fairCons, 0, 0);
506        if (Ctlp_FormulaReadType(formula) != Ctlp_TRUE_c){
507          fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
508          fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
509        }
510      }
511    }
512  } 
513
514  globalTimeStart = util_cpu_time();
515
516  if (partition != NIL(graph_t)){
517
518    if (dcLevel == Imc_DcLevelArdc_c){
519      if (verbosity != Imc_VerbosityNone_c){
520        fprintf(vis_stdout, "IMC: Computing approximate reachable states.\n");
521      }
522      ardcOptions = Fsm_ArdcAllocOptionsStruct();
523      Fsm_ArdcGetDefaultOptions(ardcOptions); 
524      initialTime = util_cpu_time();
525      (void) Fsm_ArdcComputeOverApproximateReachableStates(
526        reducedFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
527      finalTime = util_cpu_time();
528      if (verbosity != Imc_VerbosityNone_c) {
529        Fsm_ArdcPrintReachabilityResults(reducedFsm, finalTime - initialTime);
530      }
531      /* CW::user is responsible to free Fsm_ArdcGetMdd...
532      careStates
533        = mdd_dup(Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm));
534      */
535      careStates
536        = Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm);
537     
538    }else if (dcLevel >= Imc_DcLevelRch_c){
539      if (verbosity != Imc_VerbosityNone_c){
540         fprintf(vis_stdout, "IMC: Computing exact reachable states.\n");
541      }
542      initialTime = util_cpu_time();
543      careStates = Fsm_FsmComputeReachableStates(reducedFsm,
544                                         0, 1, 0, 0, 0, 0, 0,
545                                         Fsm_Rch_Default_c, 0, 0,
546                                         NIL(array_t), FALSE, NIL(array_t));
547      finalTime = util_cpu_time();
548      if (verbosity != Imc_VerbosityNone_c) {
549        Fsm_FsmReachabilityPrintResults(reducedFsm, finalTime - initialTime,
550                                      Fsm_Rch_Default_c);
551      }
552    }else{
553      careStates = NIL(mdd_t);
554    }
555 
556    if (reducedFsm != NIL(Fsm_Fsm_t) && 
557        Fsm_FsmReadImageInfo(reducedFsm) != NIL(Img_ImageInfo_t)) {
558      Fsm_FsmFreeImageInfo(reducedFsm);
559    }
560  }
561
562  ctlNormalForm = Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
563                  ctlFormulaArray);
564
565  /*
566   * Loop over every CTL formula in the array
567   */
568  arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
569    Ctlp_FormulaClass formulaClass;   
570    array_t * singleFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
571
572    array_insert(Ctlp_Formula_t *, singleFormulaArray, 0, currentFormula);
573    dagFormula = Ctlp_FormulaArrayConvertToDAG(singleFormulaArray);
574    array_free(singleFormulaArray);
575    formula = array_fetch(Ctlp_Formula_t *, dagFormula, 0);
576    array_free(dagFormula);
577
578    formulaClass = Ctlp_CheckClassOfExistentialFormula(formula);
579
580    /*
581     * Type of approximation needed for verification
582     *
583     *       pDOG  nDOG  MOG
584     * ---------------------
585     * ACTL    L     U    B
586     * ECTL    U     L    B
587     * Mixed   B     B    B
588     */
589
590    if ((formulaClass == Ctlp_Mixed_c) || (graphType == Imc_GraphMOG_c)){
591      needLower = TRUE;
592      needUpper = TRUE;
593
594    }else if (((formulaClass == Ctlp_ACTL_c) && (graphType == Imc_GraphPDOG_c)) ||
595        ((formulaClass == Ctlp_ECTL_c) && (graphType == Imc_GraphNDOG_c))){
596      needLower = TRUE;
597      needUpper = FALSE;     
598
599    }else{
600      needLower = FALSE;
601      needUpper = TRUE;
602    }           
603
604    if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula,network,FALSE)){
605      (void) fprintf(vis_stdout, "\n** imc error: Error in parsing formula:\n%s\n", 
606                     error_string());
607      error_init();
608      continue;
609    }
610
611    error_init();
612    initialTime = util_cpu_time();
613   
614    orgFormula = array_fetch(Ctlp_Formula_t *, ctlFormulaArray, i);
615
616    Imc_ImcEvaluateFormulaLinearRefine(network, orgFormula, formula, 
617      formulaClass, incrementalSize, verbosity, refine, careStates, reducedFsm,
618      dcLevel, graphType, lowerMethod, upperMethod, computeExact, needLower, 
619      needUpper, partMethod, currentNode, modelName);
620
621    finalTime = util_cpu_time();
622    if(verbosity != Imc_VerbosityNone_c) {
623      (void) fprintf(vis_stdout, "%-20s%10ld\n\n",
624                     "IMC: Verification time for this formula =",
625                     (finalTime - initialTime) / 1000);
626    }
627    fprintf(vis_stdout, "\n");
628   
629  } /* End of arrayForEachItem in ctlFormulaArray */
630
631  if (careStates)
632    mdd_free(careStates); /* FIXED */
633
634  globalTimeEnd = util_cpu_time();
635
636  if (verbosity != Imc_VerbosityNone_c) {
637     (void) fprintf(vis_stdout, "%-20s%10ld\n\n",
638                    "IMC: Total verification time =",
639                    (globalTimeEnd - globalTimeStart) / 1000);
640  } 
641 
642  /* Deactivate the alarm */
643  alarm(0);
644
645  if ((reducedFsm != NIL(Fsm_Fsm_t)) && (exactFsm != reducedFsm)){
646    Fsm_FsmFree(reducedFsm);
647  }
648
649  Ctlp_FormulaArrayFree(ctlFormulaArray);
650  Ctlp_FormulaArrayFree(ctlNormalForm);
651  error_cleanup();
652
653  /* normal exit */
654  return 0;
655}
656
657/**Function********************************************************************
658
659   Synopsis     [Prints the usage of the iterative_model_checking command.]
660   
661   SideEffects  []
662   
663   SeeAlso      [CommandImc]
664
665******************************************************************************/
666static void
667IterativeModelCheckUsage(void)
668{
669  fprintf(vis_stderr, "usage: iterative_model_check [-h] [-x]");
670  fprintf(vis_stderr, "[-t <secs>] [-v <number>] [-D <number>] [-r <number>]");
671  fprintf(vis_stderr, "[-i <number] [-l <number] [-p <number] [-g <number] ctlfile\n");
672  fprintf(vis_stderr, "   -h        print the command usage\n");
673  fprintf(vis_stderr, "   -x        Exact verification\n");
674  fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");
675  fprintf(vis_stderr, "   -v number verbosity level (0:none, 1:mid, 2:max)\n");
676  fprintf(vis_stderr, "   -D number Don't care level. DC's are used to\n");
677  fprintf(vis_stderr, "             reduce transition relation\n");
678  fprintf(vis_stderr, "        0    No don't care (default)\n");
679  fprintf(vis_stderr, "        1    Exact reachable states\n");
680  fprintf(vis_stderr, "        2    Aggressively use DC's\n");
681  fprintf(vis_stderr, "        3    Approximate reachable states\n");
682  fprintf(vis_stderr, "   -r number Refinement method\n");
683  fprintf(vis_stderr, "        0    Static scheduling by name sorting\n");
684  fprintf(vis_stderr, "        1    Static scheduling by latch affinity (defualt)\n");
685  fprintf(vis_stderr, "   -i number Incremental size (default = 4)\n");
686  fprintf(vis_stderr, "   -l number Type of lower-bound approximation method\n");
687  fprintf(vis_stderr, "        0    Take a subset of each transition sub-relation\n");
688  fprintf(vis_stderr, "        1    Take a subset by universal quantification (default)\n");
689  fprintf(vis_stderr, "   -p number Type of partition method\n");
690  fprintf(vis_stderr, "        0    Build all next state functions (default)\n");
691  fprintf(vis_stderr, "        1    Build the next state functions related to formulas\n");
692  fprintf(vis_stderr, "        2    Build the next state functions incrementally\n");
693  fprintf(vis_stderr, "   -g number Type of operational graph\n");
694  fprintf(vis_stderr, "        0    Negative Operational Graph\n");
695  fprintf(vis_stderr, "        1    Positive Operational Graph\n");
696  fprintf(vis_stderr, "        2    Mixed Operational Graph (default)\n"); 
697  fprintf(vis_stderr, "   ctlfile   File containing the ctl formulas\n");
698
699  return;
700} /* End of IterativeModelCheckUsage */
701
702
703/**Function********************************************************************
704
705  Synopsis           [Handle the timeout signal.]
706
707  Description [This function is called when the time out occurs. In principle
708  it could do something smarter, but so far it just transfers control to the
709  point in the code where setjmp was called.]
710
711  SideEffects [This function gains control at any point in the middle of the
712  computation, therefore the memory allocated so far leaks.]
713
714******************************************************************************/
715static void
716TimeOutHandle(void)
717{
718  longjmp(timeOutEnv, 1);
719} /* End of TimeOutHandle */
Note: See TracBrowser for help on using the repository browser.