source: vis_dev/vis-2.3/models/transition/mc.html

Last change on this file was 28, checked in by cecile, 13 years ago

exemples de test

File size: 38.2 KB
RevLine 
[28]1
2/**Function********************************************************************
3
4  Synopsis [Check CTL formulas given in file are modeled by flattened network]
5
6  CommandName [model_check]
7
8  CommandSynopsis [perform fair CTL model checking on a flattened network]
9
10  CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\]
11  \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\]
12  \[-t <time_out_period>\]\[-v <verbosity_level>\]
13  \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\]
14  \[-C\] \[-w  <node_file>\] \[-W\] \[-G\] <ctl_file>]
15
16  CommandDescription [Performs fair CTL model checking on a flattened
17  network.  Before calling this command, the user should have
18  initialized the design by calling the command <A
19  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
20  Regardless of the options, no 'false positives' or 'false negatives'
21  will occur: the result is correct for the given circuit.  <p>
22
23  Properties to be verified should be provided as CTL formulas in the
24  file <code>ctl_file</code>.  Note that the support of any wire
25  referred to in a formula should consist only of latches.  For the
26  precise syntax of CTL formulas, see the <A
27  HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A><p>
28
29  Properties of the form <code> AG f</code>, where  <code>f</code> is a formula not
30  involving path quantifiers are referred to as invariants; for such properties
31  it may be substantially faster to use the <A HREF="check_invariantCmd.html">
32  <code> check_invariant</code></A> command.
33  <p>
34
35  A fairness constraint can be specified by invoking the
36  <A HREF="read_fairnessCmd.html"><code>read_fairness</code></A> command;
37  if none is specified, all paths are taken to be fair.
38  If some initial states
39  do not lie on a fair path, the model checker prints a message to this effect.
40  <p>
41
42  A formula passes iff it is true for all initial states of the
43  system.  Therefore, in the presence of multiple initial states, if a
44  formula fails, the negation of the formula may also fail.<p>
45
46  If a formula does not pass, a (potentially partial) proof of failure
47  (referred to as a debug trace) is demonstrated. Fair paths are
48  represented by a finite sequence of states (the stem) leading to a
49  fair cycle, i.e. a cycle on which there is a state from each
50  fairness condition. The level of detail of the proof can be
51  specified (see option <code>-d</code>). <p>
52
53  Both backward (future tense CTL formulas) and forward (past tense CTL
54  formulas) model checking can be performed. Forward model checking is
55  based on Iwashita's ICCAD96 paper. Future tense CTL formulas are
56  automatically converted to past tense ones as much as possible in
57  forward model checking. <p>
58
59  Command options:
60  <p>
61
62  <dl>
63
64  <dt> -b
65  <dd> Use backward analysis when performing debugging; the default is
66  to use forward analysis. This should be tried when the debugger spends a
67  large amount of time when creating a path to a fair cycle. This option is not
68  compatible with forward model checking option (-F).</dd><p>
69
70  <dt> -c
71  <dd> Use the formula tree so that there is no sharing of sub-formulae among
72  the formulae in the input file. This option is useful in the following
73  scenario - formulae A, B and C are being checked in order and there is
74  sub-formula sharing between A and C. If the BDDs corresponding to the shared
75  sub-formula is huge then computation for B might not be able to finish
76  without using this option.
77  </dd><p>
78
79  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify the amount of
80  debugging performed when the system fails a formula being checked.
81  Note that it may not always be possible to give a simple
82  counter-example to show that a formula is false, since this may
83  require enumerating all paths from a state.  In such a case the
84  model checker will print a message to this effect.  This option is
85  incompatible with -F.</dd>  <p>
86  <dd> <code> dbg_level</code> must be one of the following:
87
88  <p><code>0</code>: No debugging performed.
89  <code>dbg_level</code>=<code>0</code> is the default.
90
91  <p><code>1</code>: Debugging with minimal output: generate counter-examples
92  for universal formulas (formulas of the form <code>AX|AF|AU|AG</code>) and
93  witnesses for existential formulas (formulas of the form
94  <code>EX|EF|EU|EG</code>).  States on a path are not further analyzed.
95
96  <p><code>2</code>: Same as <code>dbg_level</code>=<code>1</code>, but more
97  verbose. (The subformulas are printed, too.)
98
99  <p><code>3</code>: Maximal automatic debugging: as for level <code>1</code>,
100  except that states occurring on paths will be recursively analyzed.
101
102  <p><code>4</code>: Manual debugging: at each state, the user is queried if
103  more feedback is desired.
104  </dd>
105
106  <p>
107
108  <dt> -f &lt;<code>dbg_file</code>&gt;
109  <dd> Write the debugger output to <code>dbg_file</code>.
110  This option is incompatible with -F.
111  Notes: when you use -d4 (interactive mode), -f is not recommended, since you
112  can't see the output of vis on stdout.</dd>
113
114  <dt> -g &lt;<code>hints_file</code>&gt; <dd> Use guided search.  The file
115  <code>hints_file</code> contains a series of hints.  A hint is a formula that
116  does not contain any temporal operators, so <code>hints_file</code> has the
117  same syntax as a file of invariants used for check_invariant.  The hints are
118  used in the order given to change the transition relation.  In the case of
119  least fixpoints (EF, EU), the transition relation is conjoined with the hint,
120  whereas for greatest fixpoints the transition relation is disjoined with the
121  negation of the hint.  If the hints are cleverly chosen, this may speed up
122  the computation considerably, because a search with the changed transition
123  relation may be much simpler than one with the original transition relation,
124  and results obtained can be reused, so that we may never have to do a
125  complicated search with the original relation.  Note: hints in terms of
126  primary inputs are not useful for greatest fixpoints.  See also: Ravi and
127  Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
128  Somenzi, Efficient Decision Procedures for Model Checking of Linear Time
129  Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search
130  for CTL Model Checking, DAC'00.
131
132  <p>For formulae that contain both least and greatest fixpoints, the
133  behavior depends on the flag <code>guided_search_hint_type</code>.
134  If it is set to local (default) then every subformula is evaluated
135  to completion, using all hints in order, before the next subformula
136  is started.  For pure ACTL or pure ECTL formulae, we can also set
137  guided_search_hint_type to global, in which case the entire formula
138  is evaluated for one hint before moving on to the next hint, using
139  underapproximations.  The description of the options for guided
140  search can be found in the help page for
141  print_guided_search_options.
142
143  <p>model_check will call reachability without any guided search, even
144  if -g is used.  If you want to perform reachability with guided
145  search, call rch directly.
146
147  <p>Incompatible with -F.</dd>
148
149  <dt> -h
150  <dd> Print the command usage.</dd>
151  <p>
152
153  <dt> -i
154  <dd> Print input values causing transitions between states during debugging.
155  Both primary and pseudo inputs are printed.
156  This option is incompatible with -F.</dd>
157  <p>
158
159  <dt> -m
160  <dd> Pipe debugger output through the UNIX utility  more.
161  This option is incompatible with -F.</dd>
162  <p>
163
164  <dt> -r
165  <dd> Reduce the FSM derived from the flattened network with respect to each
166  formula being checked. By default, the FSM is reduced with respect to the
167  conjunction of the formulae in the input file. If this option is used and
168  don't cares are being used for simplification, then subformula sharing is
169  disabled (result might be incorrect otherwise).</dd>
170  <p>
171
172  <dd> The truth of  a formula may be independent of parts of the network
173  (such as when wires have been abstracted; see
174  <A HREF="flatten_hierarchyCmd.html"><code>flatten_hierarchy</code></A>).
175  These parts are effectively removed when this option is invoked; this may
176  result in more efficient model checking.</dd>
177  <p>
178
179  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
180  <dd> Specify the time out period (in seconds) after which the command
181  aborts. By default this option is set to infinity.</dd>
182  <p>
183
184  <dt> -v  <code>&lt;verbosity_level&gt;</code>
185  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage
186  and code status.
187
188  <br><code>verbosity_level</code>  must be one of the following:<p>
189
190  <code>0</code>: No feedback provided. This is the default.<p>
191
192  <code>1</code>: Feedback on code location.<p>
193
194  <code>2</code>: Feedback on code location and CPU usage.</dd><p>
195
196  <dt> -B
197  <dd> Check for vacuously passing formulae using the algorithm of Beer et al.
198  (CAV97).  The algorithm applies to a subset of ACTL (w-ACTL) and replaces
199  the smallest important subformula of a passing property with either FALSE
200  or TRUE depending on its negation parity.  It then applies model checking
201  to the resulting witness formula.  If the witness formula also passes, then
202  the original formula is deemed to pass vacuously.  If the witness formula
203  fails, a counterexample to it provides an interesting witness to the
204  original passing formula.  See the CAV97 paper for the definitions of
205  w-ACTL, important subformula, and interesting witness.  In short, one of the
206  operands of a binary operator in a w-ACTL formula must be a propositional
207  formula.  See also the -V option.
208  </dd><p>
209
210  <dt> -C
211  <dd> Compute coverage of all observable signals in a set of CTL formulae
212  using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity
213  level (-v option) is equal to 0, only the coverage stats are printed. If
214  verbosity level is greater than zero, then detailed information of the
215  computation at each step of the algorithm is also provided.
216  Debug information is provided in the form of states not covered for each
217  observable signal if the dbg_level (-d option) is greater than 0. The number
218  of states printed is set by the vis environment variable
219  'nr_uncoveredstates'. By default the number of states printed is 1.
220  The value of nr_uncoveredstates can be set using the set command.
221  See also the -I option.</dd>
222  <p>
223
224  <dt> -D <code> &lt;dc_level&gt; </code>
225
226  <dd> Specify extent to which don't cares are used to simplify MDDs in model
227  checking.  Don't cares are minterms on which the values taken by functions
228  do not affect the computation; potentially, these minterms can be used to
229  simplify MDDs and reduce the time taken to perform model checking.  The -g
230  flag for guided search does not affect the way in which the don't-care
231  conditions are computed.
232
233  <br>
234  <code> dc_level </code> must be one of the following:
235  <p>
236
237  <code> 0 </code>: No don't cares are used.
238
239  <p> <code> 1 </code>: Use unreachable states as don't cares. This is the
240  default.
241
242  <p> <code> 2 </code>: Use unreachable states as don't cares and in the EU
243  computation, use 'frontiers' for image computation.<p>
244
245  <code> 3 </code>: First compute an overapproximation of the reachable states
246  (ARDC), and use that as the cares set.  Use `frontiers' for image
247  computation.  For help on controlling options for ARDC, look up help on the
248  command: <A HREF="print_ardc_optionsCmd.html">print_ardc_options</A>. Refer
249  to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares
250  for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD
251  December 1996: one is for State Space Decomposition and the other is for
252  Approximate FSM Traversal.</dd>
253  <p>
254
255  <dt> -F
256  <dd> Use forward model checking based on Iwashita's method in ICCAD96.
257  Future tense CTL formulas are automatically converted to past tense
258  ones as much as possible. Converted forward formulas are printed when
259  verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m)
260  are ignored with this option. We have seen that forward model checking
261  was much faster than backward in many cases, also forward was much slower
262  than backward in many cases.</dd>
263  <p>
264
265  <dt> -I
266  <dd> Compute coverage of all observable signals in a set of CTL formulae
267  using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If
268  the verbosity level (-v option) is equal to 0, only the coverage stats are
269  printed. If verbosity level is greater than zero, then detailed information
270  of the computation at each step of the algorithm is also provided.
271  Debug information is provided in the form of states not covered for each
272  observable signal if the dbg_level (-d option) is greater than 0. The number
273  of states printed is set by the vis environment variable
274  'nr_uncoveredstates'. By default the number of states printed is 1.
275  The value of nr_uncoveredstates can be set using the set command.
276  Compared to the -C option, this one produces more accurate results and deals
277  with a larger subset of CTL.</dd>
278  <p>
279
280  <dt> -S <code> &lt;schedule&gt; </code>
281
282  <dd> Specify schedule for GSH algorithm, which generalizes the
283  Emerson-Lei algorithm and is used to compute greatest fixpoints.
284  The choice of schedule affects the sequence in which EX and EU
285  operators are applied.  It makes a difference only when fairness
286  constraints are specified.
287
288  <br>
289  <code> &lt;schedule&gt; </code> must be one of the following:
290
291  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
292  is the default.
293
294  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.
295
296  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
297  all EUs.
298
299  <p> <code> budget </code>: a hybrid of EL and EL2.
300
301  <p> <code> random </code>: enabled operators are applied in
302  (pseudo-)random order.
303
304  <p> <code> off </code>: GSH is disabled, and the old algorithm is
305  used instead.  The old algorithm uses the <code> EL </code> schedule, but
306  the termination checks are less sophisticated than in GSH.</dd>
307  <p>
308
309  <dt> -V
310  <dd> Check for vacuously passing formulae with the algorithm
311  of Purandare and Somenzi (CAV2002).  The algorithm applies to all of
312  CTL, and to both passing and failing properties.  It says whether a
313  passing formula may be strengthened and still pass, and whether a
314  failing formula may be weakened and still fail.  It considers all
315  leaves of a formula that are under one negation parity (e.g., not
316  descendants of a XOR or EQ node) for replacement by either TRUE or
317  FALSE.  See also the -B option.
318  </dd><p>
319
320
321  <dt> -w  &lt;<code>node_file</code>&gt;
322
323  This option invoked the algorithm to generate an error trace divided
324  into fated and free segements. Fate represents the inevitability and
325  free is asserted when there is no inevitability. This can be formulated
326  as a two-player concurrent reachability game. The two players are
327  the environment and the system. The node_file is given to specify the
328  variables the are controlled by the system.
329
330  <dt> -W <dt>
331
332  This option represents the case that all input variables are controlled
333  by system.
334
335  <dt> -G <dt>
336
337  We proposed two algorithm to generate segemented counter example.
338  They are general and restrcited algorithm. Bu default we use restricted
339  algorithm. We can invoke general algorithm with -G option.
340
341  For more information, please check the STTT'04
342  paper of Jin et al., "Fate and Free Will in Error Traces" <p>
343
344  <dt> <code> &lt;ctl_file&gt; </code>
345
346  <dd> File containing CTL formulas to be model checked.
347  </dl>
348
349  Related "set" options:
350  <dl>
351  <dt> ctl_change_bracket &lt;yes/no&gt;
352  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
353  therefore CTL parser does the same thing. However, in some cases a user
354  does not want to change node names in CTL parsing. Then, use this set
355  option by giving "no". Default is "yes".
356  <p>
357  <dt>guided_search_hint_type</dt> <dd>Switches between local and
358  global hints (see the -g option, or the help page for set).
359  </dl>
360
361  See also commands : approximate_model_check, incremental_ctl_verification
362  ]
363
364  Description [First argument is a file containing a set of CTL formulas - see
365  ctlp package for grammar. Second argument is an FSM that we will check the
366  formulas on. Formulas are checked by calling the recursive function
367  Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.]
368
369  Comment [Ctlp creates duplicate formulas when converting to
370  existential form; e.g.  when converting AaUb. We aren't using this
371  fact, which leads to some performance degradation.
372
373  A system satisfies a formula if all its initial states are in the satisfying
374  set of the formula.  Hence, we do not need to continue the computation if we
375  know that all initial states are in the satisfying set, or if there are
376  initial states that we are sure are not in the satisfying set.  This is what
377  early termination does: it supplies an extra termination condition for the
378  fixpoints that kicks in when we can decide the truth of the formula.  Note
379  that this leads to some nasty consequences in storing the satisfying sets.
380  A computation that has terminated early does not yield the exact satisfying
381  set, and hence we can not always reuse this result when there is subformula
382  sharing.]
383
384  SideEffects []
385
386  SeeAlso [CommandInv]
387
388******************************************************************************/
389static int
390CommandMc(
391  Hrc_Manager_t **hmgr,
392  int argc,
393  char **argv)
394{
395 /* options */
396  McOptions_t         *options;
397  Mc_VerbosityLevel   verbosity;
398  Mc_DcLevel          dcLevel;
399  FILE                *ctlFile;
400  int                 timeOutPeriod     = 0;
401  Mc_FwdBwdAnalysis   traversalDirection;
402  int                 buildOnionRings   = 0;
403  FILE                *guideFile;
404  FILE                *systemFile;
405  Mc_GuidedSearch_t   guidedSearchType  = Mc_None_c;
406  Ctlp_FormulaArray_t *hintsArray       = NIL(Fsm_HintsArray_t);
407  array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
408  st_table            *systemVarBddIdTable;
409  boolean             noShare           = 0;
410  Mc_GSHScheduleType  GSHschedule;
411  boolean             checkVacuity;
412  boolean             performCoverageHoskote;
413  boolean             performCoverageImproved;
414
415  /* CTL formulae */
416  array_t *ctlArray;
417  array_t *ctlNormalFormulaArray;
418  int i;
419  int numFormulae;
420  /* FSM, network and image */
421  Fsm_Fsm_t       *totalFsm = NIL(Fsm_Fsm_t);
422  Fsm_Fsm_t       *modelFsm = NIL(Fsm_Fsm_t);
423  Fsm_Fsm_t       *reducedFsm = NIL(Fsm_Fsm_t);
424  Ntk_Network_t   *network;
425  mdd_t           *modelCareStates = NIL(mdd_t);
426  array_t         *modelCareStatesArray = NIL(array_t);
427  mdd_t           *modelInitialStates;
428  mdd_t           *fairStates;
429  Fsm_Fairness_t  *fairCond;
430  mdd_manager     *mddMgr;
431  array_t         *bddIdArray;
432  Img_ImageInfo_t *imageInfo;
433  Mc_EarlyTermination_t *earlyTermination;
434  /* Coverage estimation */
435  mdd_t           *totalcoveredstates = NIL(mdd_t);
436  array_t         *signalTypeList = array_alloc(int,0);
437  array_t         *signalList = array_alloc(char *,0);
438  array_t         *statesCoveredList = array_alloc(mdd_t *,0);
439  array_t         *newCoveredStatesList = array_alloc(mdd_t *,0);
440  array_t         *statesToRemoveList = array_alloc(mdd_t *,0);
441
442  /* Early termination is only partially implemented right now.  It needs
443     distribution over all operators, including limited cases of temporal
444     operators.  That should be relatively easy to implement. */
445
446  /* time keeping */
447  long totalInitialTime; /* for model checking */
448  long initialTime, finalTime; /* for model checking */
449
450  error_init();
451  Img_ResetNumberOfImageComputation(Img_Both_c);
452
453  /* read options */
454  if (!(options = ParseMcOptions(argc, argv))) {
455    return 1;
456  }
457  verbosity = McOptionsReadVerbosityLevel(options);
458  dcLevel = McOptionsReadDcLevel(options);
459  ctlFile = McOptionsReadCtlFile(options);
460  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
461  traversalDirection = McOptionsReadTraversalDirection(options);
462  buildOnionRings =
463    (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
464  noShare = McOptionsReadUseFormulaTree(options);
465  GSHschedule = McOptionsReadSchedule(options);
466  checkVacuity = McOptionsReadVacuityDetect(options);
467   /* for the command mc -C foo.ctl */
468  performCoverageHoskote = McOptionsReadCoverageHoskote(options);
469  /* for the command mc -I foo.ctl */
470  performCoverageImproved = McOptionsReadCoverageImproved(options);
471
472  /* Check for incompatible options and do some option-specific
473   * intializations.
474   */
475
476  if (traversalDirection == McFwd_c) {
477    if (checkVacuity) {
478      fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n");
479      McOptionsFree(options);
480      return 1;
481    }
482    if (performCoverageHoskote || performCoverageImproved) {
483      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n");
484      McOptionsFree(options);
485      return 1;
486    }
487  }
488
489  if (checkVacuity) {
490    if (performCoverageHoskote || performCoverageImproved) {
491      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n");
492      McOptionsFree(options);
493      return 1;
494    }
495  }
496
497  guideFile =  McOptionsReadGuideFile(options);
498
499  if(guideFile != NIL(FILE) ){
500    guidedSearchType = Mc_ReadGuidedSearchType();
501    if(guidedSearchType == Mc_None_c){  /* illegal setting */
502      fprintf(vis_stderr, "** mc error: Unknown  hint type\n");
503      fclose(guideFile);
504      McOptionsFree(options);
505      return 1;
506    }
507
508    if(traversalDirection == McFwd_c){  /* illegal combination */
509      fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n");
510      fclose(guideFile);
511      McOptionsFree(options);
512      return 1;
513    }
514
515    if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
516       Img_UserSpecifiedMethod() != Img_Monolithic_c &&
517       Img_UserSpecifiedMethod() != Img_Mlp_c){
518      fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n");
519      fclose(guideFile);
520      McOptionsFree(options);
521      return 1;
522    }
523
524    hintsArray = Mc_ReadHints(guideFile);
525    fclose(guideFile); guideFile = NIL(FILE);
526    if( hintsArray == NIL(array_t) ){
527      McOptionsFree(options);
528      return 1;
529    }
530
531  } /* if guided search */
532
533  /* If don't-cares are used, -r implies -c.  Note that the satisfying
534     sets of a subformula are only in terms of propositions therein
535     and their cone of influence.  Hence, we can share satisfying sets
536     among formulae.  I don't quite understand what the problem with
537     don't-cares is (RB) */
538  if (McOptionsReadReduceFsm(options))
539    if (dcLevel != McDcLevelNone_c)
540      McOptionsSetUseFormulaTree(options, TRUE);
541
542  if (traversalDirection == McFwd_c &&
543      McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
544    McOptionsSetDbgLevel(options, McDbgLevelNone_c);
545    (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n");
546  }
547
548  /* Read CTL formulae */
549  ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile);
550  fclose(ctlFile); ctlFile = NIL(FILE);
551  if (ctlArray == NIL(array_t)) {
552    (void) fprintf(vis_stderr,
553                   "** mc error: error in parsing formulas from file\n");
554    McOptionsFree(options);
555    return 1;
556  }
557
558  /* read network */
559  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
560  if (network == NIL(Ntk_Network_t)) {
561    fprintf(vis_stdout, "%s\n", error_string());
562    error_init();
563    Ctlp_FormulaArrayFree(ctlArray);
564    McOptionsFree(options);
565    return 1;
566  }
567
568  /* read fsm */
569  totalFsm = Fsm_NetworkReadOrCreateFsm(network);
570  if (totalFsm == NIL(Fsm_Fsm_t)) {
571    fprintf(vis_stdout, "%s\n", error_string());
572    error_init();
573    Ctlp_FormulaArrayFree(ctlArray);
574    McOptionsFree(options);
575    return 1;
576  }
577
578  /* Assign variables to system if doing FAFW */
579  systemVarBddIdTable = NIL(st_table);
580  systemFile = McOptionsReadSystemFile(options);
581  if (systemFile != NIL(FILE)) {
582    systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
583    fclose(systemFile); systemFile = NIL(FILE);
584    if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */
585      Ctlp_FormulaArrayFree(ctlArray);
586      McOptionsFree(options);
587      return 1;
588    }
589  } /* if FAFW */
590
591  if(options->FAFWFlag && systemVarBddIdTable == 0) {
592    systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
593  }
594
595  if (verbosity > McVerbosityNone_c)
596    totalInitialTime = util_cpu_time();
597  else /* to remove uninitialized variable warning */
598    totalInitialTime = 0;
599
600  if(traversalDirection == McFwd_c){
601    mdd_t *totalInitialStates;
602    double nInitialStates;
603
604    totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm);
605    nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm),
606                                     totalInitialStates,
607                                     Fsm_FsmReadPresentStateVars(totalFsm));
608    mdd_free(totalInitialStates);
609
610    /* If the number of initial states is only one, we can use both
611     * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE),
612     * however, if we have multiple initial states, we should use
613     * p0 ^ !f == FALSE.
614     */
615    ctlNormalFormulaArray =
616      Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0),
617                                        noShare);
618    /* end conversion for forward traversal */
619  } else if (noShare) { /* conversion for backward, no sharing */
620    ctlNormalFormulaArray =
621      Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
622  }else{ /* conversion for backward, with sharing */
623    /* Note that converting to DAG after converting to existential form would
624       lead to more sharing, but it cannot be done since equal subformula that
625       are converted from different formulae need different pointers back to
626       their originals */
627    if (checkVacuity) {
628      ctlNormalFormulaArray =
629        Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
630    }
631    else {
632      array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray );
633      array_free( ctlArray );
634      ctlArray = temp;
635      ctlNormalFormulaArray =
636        Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray);
637    }
638  }
639  /* At this point, ctlNormalFormulaArray contains the formulas that are
640     actually going to be checked, and ctlArray contains the formulas from
641     which the conversion has been done.  Both need to be kept around until the
642     end, for debugging purposes. */
643
644  numFormulae = array_n(ctlNormalFormulaArray);
645
646  /* time out */
647  if (timeOutPeriod > 0) {
648    /* Set the static variables used by the signal handler. */
649    mcTimeOut = timeOutPeriod;
650    alarmLapTime = util_cpu_ctime();
651    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
652    (void) alarm(timeOutPeriod);
653    if (setjmp(timeOutEnv) > 0) {
654      (void) fprintf(vis_stdout,
655                "# MC: timeout occurred after %d seconds.\n", timeOutPeriod);
656      (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n");
657      if (verbosity > McVerbosityNone_c) {
658        fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n",
659                Img_GetNumberOfImageComputation(Img_Forward_c),
660                Img_GetNumberOfImageComputation(Img_Backward_c));
661      }
662      alarm(0);
663      return 1;
664    }
665  }
666
667  /* Create reduced fsm, if necessary */
668  if (!McOptionsReadReduceFsm(options)){
669    /* We want to minimize only when "-r" option is not specified */
670    /* reduceFsm would be NIL, if there is no reduction observed */
671    assert (reducedFsm == NIL(Fsm_Fsm_t));
672    reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
673    if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) {
674      mddMgr = Fsm_FsmReadMddManager(reducedFsm);
675      bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
676                   Fsm_FsmReadPresentStateVars(reducedFsm));
677      (void)fprintf(vis_stdout,"Local system includes ");
678      (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
679                    array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
680                    array_n(bddIdArray));
681      array_free(bddIdArray);
682    }
683  }
684
685  /************** for all formulae **********************************/
686  for(i = 0; i < numFormulae; i++) {
687    int nImgComps, nPreComps;
688    boolean result;
689    Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
690                                             ctlNormalFormulaArray, i);
691
692    modelFsm = NIL(Fsm_Fsm_t);
693
694    /* do a check */
695    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
696      (void) fprintf(vis_stdout,
697                     "** mc error: error in parsing Atomic Formula:\n%s\n",
698                     error_string());
699      error_init();
700      Ctlp_FormulaFree(ctlFormula);
701      continue;
702    }
703
704    /* Create reduced fsm */
705    if (McOptionsReadReduceFsm(options)) {
706      /* We have not done top level reduction. */
707      /* Using the same variable reducedFsm here   */
708      array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
709
710      assert(reducedFsm == NIL(Fsm_Fsm_t));
711      array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula);
712      reducedFsm = McConstructReducedFsm(network, oneFormulaArray);
713      array_free(oneFormulaArray);
714
715      if (reducedFsm && verbosity != McVerbosityNone_c) {
716        mddMgr = Fsm_FsmReadMddManager(reducedFsm);
717        bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
718                       Fsm_FsmReadPresentStateVars(reducedFsm));
719        (void)fprintf(vis_stdout,"Local system includes ");
720        (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
721                      array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
722                      array_n(bddIdArray));
723        array_free(bddIdArray);
724      }
725    }/* if readreducefsm */
726
727    /* Let us see if we got any reduction via top level or via "-r" */
728    if (reducedFsm == NIL(Fsm_Fsm_t))
729      modelFsm = totalFsm; /* no reduction */
730    else
731      modelFsm = reducedFsm; /* some reduction at some point */
732
733    /* compute initial states */
734    modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
735    if (modelInitialStates == NIL(mdd_t)) {
736      int j;
737      (void) fprintf(vis_stdout,
738      "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n",
739                     error_string());
740      if (modelFsm != totalFsm)
741        Fsm_FsmFree(reducedFsm);
742
743      alarm(0);
744
745      for(j = i; j < numFormulae; j++)
746        Ctlp_FormulaFree(
747          array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
748      array_free( ctlNormalFormulaArray );
749
750      Ctlp_FormulaArrayFree( ctlArray );
751
752      McOptionsFree(options);
753
754      return 1;
755    }
756
757    earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
758
759    if(hintsArray != NIL(Ctlp_FormulaArray_t)) {
760      hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
761      if( hintsStatesArray == NIL(array_t) ||
762          (guidedSearchType == Mc_Global_c &&
763           Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) {
764        int j;
765
766        if( guidedSearchType == Mc_Global_c &&
767            Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)
768          fprintf(vis_stderr, "** mc error: global hints incompatible with "
769                  "mixed formulae\n");
770
771        Mc_EarlyTerminationFree(earlyTermination);
772        mdd_free(modelInitialStates);
773        if (modelFsm != totalFsm)
774          Fsm_FsmFree(reducedFsm);
775        alarm(0);
776        for(j = i; j < numFormulae; j++)
777          Ctlp_FormulaFree(
778            array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
779        array_free( ctlNormalFormulaArray );
780        Ctlp_FormulaArrayFree( ctlArray );
781        McOptionsFree(options);
782        return 1;
783      } /* problem with hints */
784    } /* hints exist */
785
786    /* stats */
787    if (verbosity > McVerbosityNone_c) {
788      initialTime = util_cpu_time();
789      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
790      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
791    } else { /* to remove uninitialized variable warnings */
792      initialTime = 0;
793      nImgComps = 0;
794      nPreComps = 0;
795    }
796    mddMgr = Fsm_FsmReadMddManager(modelFsm);
797
798    /* compute don't cares. */
799    if (modelCareStatesArray == NIL(array_t)) {
800      long iTime; /* starting time for reachability analysis */
801      if (verbosity > McVerbosityNone_c && i == 0)
802        iTime = util_cpu_time();
803      else /* to remove uninitialized variable warnings */
804        iTime = 0;
805
806      /* ardc */
807      if (dcLevel == McDcLevelArdc_c) {
808        Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options);
809
810        modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates(
811          modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
812        if (verbosity > McVerbosityNone_c && i == 0)
813          Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime);
814
815      /* rch dc */
816      } else if (dcLevel >= McDcLevelRch_c) {
817        modelCareStates =
818          Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0,
819                                        Fsm_Rch_Default_c, 0, 0,
820                                        NIL(array_t), FALSE, NIL(array_t));
821        if (verbosity > McVerbosityNone_c && i == 0) {
822          Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime,
823                                          Fsm_Rch_Default_c);
824        }
825
826        modelCareStatesArray = array_alloc(mdd_t *, 0);
827        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
828      } else {
829        modelCareStates = mdd_one(mddMgr);
830        modelCareStatesArray = array_alloc(mdd_t *, 0);
831        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
832      }
833    }
834
835    Fsm_MinimizeTransitionRelationWithReachabilityInfo(
836      modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c,
837      verbosity > 1);
838
839    /* fairness conditions */
840    fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
841                                          verbosity, dcLevel, GSHschedule,
842                                          McBwd_c, FALSE);
843    fairCond = Fsm_FsmReadFairnessConstraint(modelFsm);
844
845    if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) {
846      (void)fprintf(vis_stdout,
847                    "** mc warning: There are no fair initial states\n");
848    }
849    else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) {
850      (void)fprintf(vis_stdout,
851                    "** mc warning: Some initial states are not fair\n");
852    }
853
854    /* some user feedback */
855    if (verbosity != McVerbosityNone_c) {
856      (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1);
857      Ctlp_FormulaPrint(vis_stdout,
858                        Ctlp_FormulaReadOriginalFormula(ctlFormula));
859      (void)fprintf (vis_stdout, "\n");
860      if (traversalDirection == McFwd_c) {
861        (void)fprintf(vis_stdout, "Forward formula : ");
862        Ctlp_FormulaPrint(vis_stdout, ctlFormula);
863        (void)fprintf(vis_stdout, "\n");
864      }
865    }
866
867    /************** the actual computation **********************************/
868    if (checkVacuity) {
869      McVacuityDetection(modelFsm, ctlFormula, i,
870                         fairStates, fairCond, modelCareStatesArray,
871                         earlyTermination, hintsStatesArray,
872                         guidedSearchType, modelInitialStates,
873                         options);
874    }
875    else { /* Normal Model Checking */
876      mdd_t *ctlFormulaStates =
877        Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
878                              fairCond, modelCareStatesArray,
879                              earlyTermination, hintsStatesArray,
880                              guidedSearchType, verbosity, dcLevel,
881                              buildOnionRings, GSHschedule);
882
883      McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond,
884                         modelCareStatesArray, earlyTermination,
885                         hintsStatesArray, guidedSearchType, verbosity,
886                         dcLevel, buildOnionRings, GSHschedule,
887                         traversalDirection, modelInitialStates,
888                         ctlFormulaStates, &totalcoveredstates,
889                         signalTypeList, signalList, statesCoveredList,
890                         newCoveredStatesList, statesToRemoveList,
891                         performCoverageHoskote, performCoverageImproved);
892
893      Mc_EarlyTerminationFree(earlyTermination);
894      if(hintsStatesArray != NIL(array_t))
895        mdd_array_free(hintsStatesArray);
896      /* Set up things for possible FAFW analysis of counterexample. */
897      Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
898      Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
899      /* user feedback on succes/fail */
900      result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
901                               ctlFormula, ctlFormulaStates,
902                               modelInitialStates, modelCareStatesArray,
903                               options, verbosity);
904      Fsm_FsmSetFAFWFlag(modelFsm, 0);
905      Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL);
906      mdd_free(ctlFormulaStates);
907    }
908
909    if (verbosity > McVerbosityNone_c) {
910      finalTime = util_cpu_time();
911      fprintf(vis_stdout, "-- mc time = %10g\n",
912        (double)(finalTime - initialTime) / 1000.0);
913      fprintf(vis_stdout,
914              "-- %d image computations and %d preimage computations\n",
915              Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
916              Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
917    }
918    mdd_free(modelInitialStates);
919    mdd_free(fairStates);
920    Ctlp_FormulaFree(ctlFormula);
921
922    if ((McOptionsReadReduceFsm(options)) &&
923        (reducedFsm != NIL(Fsm_Fsm_t))) {
924      /*
925      ** We need to free the reducedFsm only if it was created under "-r"
926      ** option and was non-NIL.
927      */
928      Fsm_FsmFree(reducedFsm);
929      reducedFsm = NIL(Fsm_Fsm_t);
930      modelFsm = NIL(Fsm_Fsm_t);
931      if (modelCareStates) {
932        mdd_array_free(modelCareStatesArray);
933        modelCareStates = NIL(mdd_t);
934        modelCareStatesArray = NIL(array_t);
935      } else if (modelCareStatesArray) {
936        modelCareStatesArray = NIL(array_t);
937      }
938    }
939  }/* for all formulae */
940
941  if (verbosity > McVerbosityNone_c) {
942    finalTime = util_cpu_time();
943    fprintf(vis_stdout, "-- total mc time = %10g\n",
944      (double)(finalTime - totalInitialTime) / 1000.0);
945    fprintf(vis_stdout,
946            "-- total %d image computations and %d preimage computations\n",
947            Img_GetNumberOfImageComputation(Img_Forward_c),
948            Img_GetNumberOfImageComputation(Img_Backward_c));
949    /* Print tfm options if we have a global fsm. */
950    if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) {
951      imageInfo = Fsm_FsmReadImageInfo(modelFsm);
952      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
953          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
954        Img_TfmPrintStatistics(imageInfo, Img_Both_c);
955      }
956    }
957  }
958
959  /* Print results of coverage computation */
960  McPrintCoverageSummary(modelFsm, dcLevel,
961                         options, modelCareStatesArray,
962                         modelCareStates, totalcoveredstates,
963                         signalTypeList, signalList, statesCoveredList,
964                         performCoverageHoskote, performCoverageImproved);
965  mdd_array_free(newCoveredStatesList);
966  mdd_array_free(statesToRemoveList);
967  array_free(signalTypeList);
968  array_free(signalList);
969  mdd_array_free(statesCoveredList);
970  if (totalcoveredstates != NIL(mdd_t))
971    mdd_free(totalcoveredstates);
972
973  if (modelCareStates) {
974    mdd_array_free(modelCareStatesArray);
975  }
976
977  if(hintsArray)
978    Ctlp_FormulaArrayFree(hintsArray);
979
980  if ((McOptionsReadReduceFsm(options) == FALSE) &&
981      (reducedFsm != NIL(Fsm_Fsm_t))) {
982    /* If "-r" was not specified and we did some reduction at top
983       level, we need to free it */
984    Fsm_FsmFree(reducedFsm);
985    reducedFsm = NIL(Fsm_Fsm_t);
986    modelFsm = NIL(Fsm_Fsm_t);
987  }
988
989  if(systemVarBddIdTable)
990    st_free_table(systemVarBddIdTable);
991  array_free(ctlNormalFormulaArray);
992  (void) fprintf(vis_stdout, "\n");
993
994  Ctlp_FormulaArrayFree(ctlArray);
995  McOptionsFree(options);
996  alarm(0);
997  return 0;
998}
Note: See TracBrowser for help on using the repository browser.