source: vis_dev/vis-2.3/src/mc/mcCmd.c @ 93

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

vis2.3

File size: 115.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [mcCmd.c]
4
5  PackageName [mc]
6
7  Synopsis    [Functions for CTL model checking commands.]
8
9  Description [This file contains the functions implementing the CTL
10  model checking commands.]
11
12  SeeAlso     []
13
14  Author      [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon,
15  Roderick Bloem, and others]
16
17  Copyright   [Copyright (c) 2002-2005, Regents of the University of Colorado
18
19  All rights reserved.
20
21  Redistribution and use in source and binary forms, with or without
22  modification, are permitted provided that the following conditions
23  are met:
24
25  Redistributions of source code must retain the above copyright
26  notice, this list of conditions and the following disclaimer.
27
28  Redistributions in binary form must reproduce the above copyright
29  notice, this list of conditions and the following disclaimer in the
30  documentation and/or other materials provided with the distribution.
31
32  Neither the name of the University of Colorado nor the names of its
33  contributors may be used to endorse or promote products derived from
34  this software without specific prior written permission.
35
36  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
37  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
38  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
39  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
40  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
41  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
42  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
43  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
44  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
45  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
46  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
47  POSSIBILITY OF SUCH DAMAGE.]
48
49******************************************************************************/
50
51#include "ctlpInt.h"
52#include "grab.h"
53#include "puresat.h"
54#include "mcInt.h"
55
56
57/*---------------------------------------------------------------------------*/
58/* Constant declarations                                                     */
59/*---------------------------------------------------------------------------*/
60
61/*---------------------------------------------------------------------------*/
62/* Stucture declarations                                                     */
63/*---------------------------------------------------------------------------*/
64
65/*---------------------------------------------------------------------------*/
66/* Type declarations                                                         */
67/*---------------------------------------------------------------------------*/
68
69/*---------------------------------------------------------------------------*/
70/* Variable declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73#ifndef lint
74static char rcsid[] UNUSED = "$Id: mcCmd.c,v 1.27 2009/04/11 01:43:30 fabio Exp $";
75#endif
76
77/*---------------------------------------------------------------------------*/
78/* Macro declarations                                                        */
79/*---------------------------------------------------------------------------*/
80
81/*---------------------------------------------------------------------------*/
82/* Variable declarations                                                     */
83/*---------------------------------------------------------------------------*/
84
85static jmp_buf timeOutEnv;
86static int mcTimeOut;           /* timeout value */
87static long alarmLapTime;       /* starting CPU time for timeout */
88
89/**AutomaticStart*************************************************************/
90
91/*---------------------------------------------------------------------------*/
92/* Static function prototypes                                                */
93/*---------------------------------------------------------------------------*/
94
95static int CommandMc(Hrc_Manager_t **hmgr, int argc, char **argv);
96static McOptions_t * ParseMcOptions(int argc, char **argv);
97static int CommandLe(Hrc_Manager_t **hmgr, int argc, char **argv);
98static McOptions_t * ParseLeOptions(int argc, char **argv);
99static int CommandInv(Hrc_Manager_t **hmgr, int argc, char **argv);
100static McOptions_t * ParseInvarOptions(int argc, char **argv);
101static void TimeOutHandle(void);
102static int UpdateResultArray(mdd_t *reachableStates, array_t *invarStatesArray, int *resultArray);
103static void PrintInvPassFail(array_t *invarFormulaArray, int *resultArray);
104
105/**AutomaticEnd***************************************************************/
106
107/*---------------------------------------------------------------------------*/
108/* Definition of exported functions                                          */
109/*---------------------------------------------------------------------------*/
110
111
112/**Function********************************************************************
113
114  Synopsis [Initialize mc package]
115
116  SideEffects []
117
118******************************************************************************/
119void
120Mc_Init(void)
121{
122  Cmd_CommandAdd("model_check", CommandMc, /* doesn't changes_network */ 0);
123  Cmd_CommandAdd("check_invariant", CommandInv, /* doesn't changes_network */ 0);
124  Cmd_CommandAdd("lang_empty", CommandLe, /* doesn't changes_network */ 0);
125  Cmd_CommandAdd("_init_state_formula", McCommandInitState, /* doesn't changes_network */ 0);
126}
127
128
129/**Function********************************************************************
130
131  Synopsis [End mc package]
132
133  SideEffects []
134
135******************************************************************************/
136void
137Mc_End(void)
138{
139}
140
141/*---------------------------------------------------------------------------*/
142/* Definition of internal functions                                          */
143/*---------------------------------------------------------------------------*/
144
145
146/*---------------------------------------------------------------------------*/
147/* Definition of static functions                                            */
148/*---------------------------------------------------------------------------*/
149
150
151/**Function********************************************************************
152
153  Synopsis [Check CTL formulas given in file are modeled by flattened network]
154
155  CommandName [model_check]
156
157  CommandSynopsis [perform fair CTL model checking on a flattened network]
158
159  CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\]
160  \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\]
161  \[-t <time_out_period>\]\[-v <verbosity_level>\]
162  \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\]
163  \[-C\] \[-w  <node_file>\] \[-W\] \[-G\] <ctl_file>]
164
165  CommandDescription [Performs fair CTL model checking on a flattened
166  network.  Before calling this command, the user should have
167  initialized the design by calling the command <A
168  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
169  Regardless of the options, no 'false positives' or 'false negatives'
170  will occur: the result is correct for the given circuit.  <p>
171
172  Properties to be verified should be provided as CTL formulas in the
173  file <code>ctl_file</code>.  Note that the support of any wire
174  referred to in a formula should consist only of latches.  For the
175  precise syntax of CTL formulas, see the <A
176  HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>.  <p>
177
178  Properties of the form <code> AG f</code>, where  <code>f</code> is a formula not
179  involving path quantifiers are referred to as invariants; for such properties
180  it may be substantially faster to use the <A HREF="check_invariantCmd.html">
181  <code> check_invariant</code></A> command.
182  <p>
183
184  A fairness constraint can be specified by invoking the
185  <A HREF="read_fairnessCmd.html"><code>read_fairness</code></A> command;
186  if none is specified, all paths are taken to be fair.
187  If some initial states
188  do not lie on a fair path, the model checker prints a message to this effect.
189  <p>
190
191  A formula passes iff it is true for all initial states of the
192  system.  Therefore, in the presence of multiple initial states, if a
193  formula fails, the negation of the formula may also fail.<p>
194
195  If a formula does not pass, a (potentially partial) proof of failure
196  (referred to as a debug trace) is demonstrated. Fair paths are
197  represented by a finite sequence of states (the stem) leading to a
198  fair cycle, i.e. a cycle on which there is a state from each
199  fairness condition. The level of detail of the proof can be
200  specified (see option <code>-d</code>). <p>
201
202  Both backward (future tense CTL formulas) and forward (past tense CTL
203  formulas) model checking can be performed. Forward model checking is
204  based on Iwashita's ICCAD96 paper. Future tense CTL formulas are
205  automatically converted to past tense ones as much as possible in
206  forward model checking. <p>
207
208  Command options:
209  <p>
210
211  <dl>
212
213  <dt> -b
214  <dd> Use backward analysis when performing debugging; the default is
215  to use forward analysis. This should be tried when the debugger spends a
216  large amount of time when creating a path to a fair cycle. This option is not
217  compatible with forward model checking option (-F).</dd><p>
218
219  <dt> -c
220  <dd> Use the formula tree so that there is no sharing of sub-formulae among
221  the formulae in the input file. This option is useful in the following
222  scenario - formulae A, B and C are being checked in order and there is
223  sub-formula sharing between A and C. If the BDDs corresponding to the shared
224  sub-formula is huge then computation for B might not be able to finish
225  without using this option.
226  </dd><p>
227
228  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify the amount of
229  debugging performed when the system fails a formula being checked.
230  Note that it may not always be possible to give a simple
231  counter-example to show that a formula is false, since this may
232  require enumerating all paths from a state.  In such a case the
233  model checker will print a message to this effect.  This option is
234  incompatible with -F.</dd>  <p>
235  <dd> <code> dbg_level</code> must be one of the following:
236
237  <p><code>0</code>: No debugging performed.
238  <code>dbg_level</code>=<code>0</code> is the default.
239
240  <p><code>1</code>: Debugging with minimal output: generate counter-examples
241  for universal formulas (formulas of the form <code>AX|AF|AU|AG</code>) and
242  witnesses for existential formulas (formulas of the form
243  <code>EX|EF|EU|EG</code>).  States on a path are not further analyzed.
244
245  <p><code>2</code>: Same as <code>dbg_level</code>=<code>1</code>, but more
246  verbose. (The subformulas are printed, too.)
247
248  <p><code>3</code>: Maximal automatic debugging: as for level <code>1</code>,
249  except that states occurring on paths will be recursively analyzed.
250
251  <p><code>4</code>: Manual debugging: at each state, the user is queried if
252  more feedback is desired.
253  </dd>
254
255  <p>
256
257  <dt> -f &lt;<code>dbg_file</code>&gt;
258  <dd> Write the debugger output to <code>dbg_file</code>.
259  This option is incompatible with -F.
260  Notes: when you use -d4 (interactive mode), -f is not recommended, since you
261  can't see the output of vis on stdout.</dd>
262
263  <dt> -g &lt;<code>hints_file</code>&gt; <dd> Use guided search.  The file
264  <code>hints_file</code> contains a series of hints.  A hint is a formula that
265  does not contain any temporal operators, so <code>hints_file</code> has the
266  same syntax as a file of invariants used for check_invariant.  The hints are
267  used in the order given to change the transition relation.  In the case of
268  least fixpoints (EF, EU), the transition relation is conjoined with the hint,
269  whereas for greatest fixpoints the transition relation is disjoined with the
270  negation of the hint.  If the hints are cleverly chosen, this may speed up
271  the computation considerably, because a search with the changed transition
272  relation may be much simpler than one with the original transition relation,
273  and results obtained can be reused, so that we may never have to do a
274  complicated search with the original relation.  Note: hints in terms of
275  primary inputs are not useful for greatest fixpoints.  See also: Ravi and
276  Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
277  Somenzi, Efficient Decision Procedures for Model Checking of Linear Time
278  Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search
279  for CTL Model Checking, DAC'00.
280
281  <p>For formulae that contain both least and greatest fixpoints, the
282  behavior depends on the flag <code>guided_search_hint_type</code>.
283  If it is set to local (default) then every subformula is evaluated
284  to completion, using all hints in order, before the next subformula
285  is started.  For pure ACTL or pure ECTL formulae, we can also set
286  guided_search_hint_type to global, in which case the entire formula
287  is evaluated for one hint before moving on to the next hint, using
288  underapproximations.  The description of the options for guided
289  search can be found in the help page for
290  print_guided_search_options.
291
292  <p>model_check will call reachability without any guided search, even
293  if -g is used.  If you want to perform reachability with guided
294  search, call rch directly.
295
296  <p>Incompatible with -F.</dd>
297
298  <dt> -h
299  <dd> Print the command usage.</dd>
300  <p>
301
302  <dt> -i
303  <dd> Print input values causing transitions between states during debugging.
304  Both primary and pseudo inputs are printed.
305  This option is incompatible with -F.</dd>
306  <p>
307
308  <dt> -m
309  <dd> Pipe debugger output through the UNIX utility  more.
310  This option is incompatible with -F.</dd>
311  <p>
312
313  <dt> -r
314  <dd> Reduce the FSM derived from the flattened network with respect to each
315  formula being checked. By default, the FSM is reduced with respect to the
316  conjunction of the formulae in the input file. If this option is used and
317  don't cares are being used for simplification, then subformula sharing is
318  disabled (result might be incorrect otherwise).</dd>
319  <p>
320
321  <dd> The truth of  a formula may be independent of parts of the network
322  (such as when wires have been abstracted; see
323  <A HREF="flatten_hierarchyCmd.html"><code>flatten_hierarchy</code></A>).
324  These parts are effectively removed when this option is invoked; this may
325  result in more efficient model checking.</dd>
326  <p>
327
328  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
329  <dd> Specify the time out period (in seconds) after which the command
330  aborts. By default this option is set to infinity.</dd>
331  <p>
332
333  <dt> -v  <code>&lt;verbosity_level&gt;</code>
334  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage
335  and code status.
336
337  <br><code>verbosity_level</code>  must be one of the following:<p>
338
339  <code>0</code>: No feedback provided. This is the default.<p>
340
341  <code>1</code>: Feedback on code location.<p>
342
343  <code>2</code>: Feedback on code location and CPU usage.</dd><p>
344
345  <dt> -B
346  <dd> Check for vacuously passing formulae using the algorithm of Beer et al.
347  (CAV97).  The algorithm applies to a subset of ACTL (w-ACTL) and replaces
348  the smallest important subformula of a passing property with either FALSE
349  or TRUE depending on its negation parity.  It then applies model checking
350  to the resulting witness formula.  If the witness formula also passes, then
351  the original formula is deemed to pass vacuously.  If the witness formula
352  fails, a counterexample to it provides an interesting witness to the
353  original passing formula.  See the CAV97 paper for the definitions of
354  w-ACTL, important subformula, and interesting witness.  In short, one of the
355  operands of a binary operator in a w-ACTL formula must be a propositional
356  formula.  See also the -V option.
357  </dd><p>
358
359  <dt> -C
360  <dd> Compute coverage of all observable signals in a set of CTL formulae
361  using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity
362  level (-v option) is equal to 0, only the coverage stats are printed. If
363  verbosity level is greater than zero, then detailed information of the
364  computation at each step of the algorithm is also provided.
365  Debug information is provided in the form of states not covered for each
366  observable signal if the dbg_level (-d option) is greater than 0. The number
367  of states printed is set by the vis environment variable
368  'nr_uncoveredstates'. By default the number of states printed is 1.
369  The value of nr_uncoveredstates can be set using the set command.
370  See also the -I option.</dd>
371  <p>
372
373  <dt> -D <code> &lt;dc_level&gt; </code>
374
375  <dd> Specify extent to which don't cares are used to simplify MDDs in model
376  checking.  Don't cares are minterms on which the values taken by functions
377  do not affect the computation; potentially, these minterms can be used to
378  simplify MDDs and reduce the time taken to perform model checking.  The -g
379  flag for guided search does not affect the way in which the don't-care
380  conditions are computed.
381
382  <br>
383  <code> dc_level </code> must be one of the following:
384  <p>
385
386  <code> 0 </code>: No don't cares are used.
387
388  <p> <code> 1 </code>: Use unreachable states as don't cares. This is the
389  default.
390
391  <p> <code> 2 </code>: Use unreachable states as don't cares and in the EU
392  computation, use 'frontiers' for image computation.<p>
393
394  <code> 3 </code>: First compute an overapproximation of the reachable states
395  (ARDC), and use that as the cares set.  Use `frontiers' for image
396  computation.  For help on controlling options for ARDC, look up help on the
397  command: <A HREF="print_ardc_optionsCmd.html">print_ardc_options</A>. Refer
398  to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares
399  for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD
400  December 1996: one is for State Space Decomposition and the other is for
401  Approximate FSM Traversal.</dd>
402  <p>
403
404  <dt> -F
405  <dd> Use forward model checking based on Iwashita's method in ICCAD96.
406  Future tense CTL formulas are automatically converted to past tense
407  ones as much as possible. Converted forward formulas are printed when
408  verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m)
409  are ignored with this option. We have seen that forward model checking
410  was much faster than backward in many cases, also forward was much slower
411  than backward in many cases.</dd>
412  <p>
413
414  <dt> -I
415  <dd> Compute coverage of all observable signals in a set of CTL formulae
416  using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If
417  the verbosity level (-v option) is equal to 0, only the coverage stats are
418  printed. If verbosity level is greater than zero, then detailed information
419  of the computation at each step of the algorithm is also provided.
420  Debug information is provided in the form of states not covered for each
421  observable signal if the dbg_level (-d option) is greater than 0. The number
422  of states printed is set by the vis environment variable
423  'nr_uncoveredstates'. By default the number of states printed is 1.
424  The value of nr_uncoveredstates can be set using the set command.
425  Compared to the -C option, this one produces more accurate results and deals
426  with a larger subset of CTL.</dd>
427  <p>
428
429  <dt> -S <code> &lt;schedule&gt; </code>
430
431  <dd> Specify schedule for GSH algorithm, which generalizes the
432  Emerson-Lei algorithm and is used to compute greatest fixpoints.
433  The choice of schedule affects the sequence in which EX and EU
434  operators are applied.  It makes a difference only when fairness
435  constraints are specified.
436
437  <br>
438  <code> &lt;schedule&gt; </code> must be one of the following:
439
440  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
441  is the default.
442
443  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.
444
445  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
446  all EUs.
447
448  <p> <code> budget </code>: a hybrid of EL and EL2.
449
450  <p> <code> random </code>: enabled operators are applied in
451  (pseudo-)random order.
452
453  <p> <code> off </code>: GSH is disabled, and the old algorithm is
454  used instead.  The old algorithm uses the <code> EL </code> schedule, but
455  the termination checks are less sophisticated than in GSH.</dd>
456  <p>
457
458  <dt> -V
459  <dd> Check for vacuously passing formulae with the algorithm
460  of Purandare and Somenzi (CAV2002).  The algorithm applies to all of
461  CTL, and to both passing and failing properties.  It says whether a
462  passing formula may be strengthened and still pass, and whether a
463  failing formula may be weakened and still fail.  It considers all
464  leaves of a formula that are under one negation parity (e.g., not
465  descendants of a XOR or EQ node) for replacement by either TRUE or
466  FALSE.  See also the -B option.
467  </dd><p>
468
469
470  <dt> -w  &lt;<code>node_file</code>&gt;
471
472  This option invoked the algorithm to generate an error trace divided
473  into fated and free segements. Fate represents the inevitability and
474  free is asserted when there is no inevitability. This can be formulated
475  as a two-player concurrent reachability game. The two players are
476  the environment and the system. The node_file is given to specify the
477  variables the are controlled by the system.
478
479  <dt> -W <dt>
480
481  This option represents the case that all input variables are controlled
482  by system.
483
484  <dt> -G <dt>
485
486  We proposed two algorithm to generate segemented counter example.
487  They are general and restrcited algorithm. Bu default we use restricted
488  algorithm. We can invoke general algorithm with -G option.
489
490  For more information, please check the STTT'04
491  paper of Jin et al., "Fate and Free Will in Error Traces" <p>
492
493  <dt> <code> &lt;ctl_file&gt; </code>
494
495  <dd> File containing CTL formulas to be model checked.
496  </dl>
497
498  Related "set" options:
499  <dl>
500  <dt> ctl_change_bracket &lt;yes/no&gt;
501  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
502  therefore CTL parser does the same thing. However, in some cases a user
503  does not want to change node names in CTL parsing. Then, use this set
504  option by giving "no". Default is "yes".
505  <p>
506  <dt>guided_search_hint_type</dt> <dd>Switches between local and
507  global hints (see the -g option, or the help page for set).
508  </dl>
509
510  See also commands : approximate_model_check, incremental_ctl_verification
511  ]
512
513  Description [First argument is a file containing a set of CTL formulas - see
514  ctlp package for grammar. Second argument is an FSM that we will check the
515  formulas on. Formulas are checked by calling the recursive function
516  Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.]
517
518  Comment [Ctlp creates duplicate formulas when converting to
519  existential form; e.g.  when converting AaUb. We aren't using this
520  fact, which leads to some performance degradation.
521
522  A system satisfies a formula if all its initial states are in the satisfying
523  set of the formula.  Hence, we do not need to continue the computation if we
524  know that all initial states are in the satisfying set, or if there are
525  initial states that we are sure are not in the satisfying set.  This is what
526  early termination does: it supplies an extra termination condition for the
527  fixpoints that kicks in when we can decide the truth of the formula.  Note
528  that this leads to some nasty consequences in storing the satisfying sets.
529  A computation that has terminated early does not yield the exact satisfying
530  set, and hence we can not always reuse this result when there is subformula
531  sharing.]
532
533  SideEffects []
534
535  SeeAlso [CommandInv]
536
537******************************************************************************/
538static int
539CommandMc(
540  Hrc_Manager_t **hmgr,
541  int argc,
542  char **argv)
543{
544 /* options */
545  McOptions_t         *options;
546  Mc_VerbosityLevel   verbosity;
547  Mc_DcLevel          dcLevel;
548  FILE                *ctlFile;
549  int                 timeOutPeriod     = 0;
550  Mc_FwdBwdAnalysis   traversalDirection;
551  int                 buildOnionRings   = 0;
552  FILE                *guideFile;
553  FILE                *systemFile;
554  Mc_GuidedSearch_t   guidedSearchType  = Mc_None_c;
555  Ctlp_FormulaArray_t *hintsArray       = NIL(Fsm_HintsArray_t);
556  array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
557  st_table            *systemVarBddIdTable;
558  boolean             noShare           = 0;
559  Mc_GSHScheduleType  GSHschedule;
560  boolean             checkVacuity;
561  boolean             performCoverageHoskote;
562  boolean             performCoverageImproved;
563
564  /* CTL formulae */
565  array_t *ctlArray;
566  array_t *ctlNormalFormulaArray;
567  int i;
568  int numFormulae;
569  /* FSM, network and image */
570  Fsm_Fsm_t       *totalFsm = NIL(Fsm_Fsm_t);
571  Fsm_Fsm_t       *modelFsm = NIL(Fsm_Fsm_t);
572  Fsm_Fsm_t       *reducedFsm = NIL(Fsm_Fsm_t);
573  Ntk_Network_t   *network;
574  mdd_t           *modelCareStates = NIL(mdd_t);
575  array_t         *modelCareStatesArray = NIL(array_t);
576  mdd_t           *modelInitialStates;
577  mdd_t           *fairStates;
578  Fsm_Fairness_t  *fairCond;
579  mdd_manager     *mddMgr;
580  array_t         *bddIdArray;
581  Img_ImageInfo_t *imageInfo;
582  Mc_EarlyTermination_t *earlyTermination;
583  /* Coverage estimation */
584  mdd_t           *totalcoveredstates = NIL(mdd_t);
585  array_t         *signalTypeList = array_alloc(int,0);
586  array_t         *signalList = array_alloc(char *,0);
587  array_t         *statesCoveredList = array_alloc(mdd_t *,0);
588  array_t         *newCoveredStatesList = array_alloc(mdd_t *,0);
589  array_t         *statesToRemoveList = array_alloc(mdd_t *,0);
590
591  /* Early termination is only partially implemented right now.  It needs
592     distribution over all operators, including limited cases of temporal
593     operators.  That should be relatively easy to implement. */
594
595  /* time keeping */
596  long totalInitialTime; /* for model checking */
597  long initialTime, finalTime; /* for model checking */
598
599  error_init();
600  Img_ResetNumberOfImageComputation(Img_Both_c);
601
602  /* read options */
603  if (!(options = ParseMcOptions(argc, argv))) {
604    return 1;
605  }
606  verbosity = McOptionsReadVerbosityLevel(options);
607  dcLevel = McOptionsReadDcLevel(options);
608  ctlFile = McOptionsReadCtlFile(options);
609  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
610  traversalDirection = McOptionsReadTraversalDirection(options);
611  buildOnionRings =
612    (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
613  noShare = McOptionsReadUseFormulaTree(options);
614  GSHschedule = McOptionsReadSchedule(options);
615  checkVacuity = McOptionsReadVacuityDetect(options);
616   /* for the command mc -C foo.ctl */
617  performCoverageHoskote = McOptionsReadCoverageHoskote(options);
618  /* for the command mc -I foo.ctl */
619  performCoverageImproved = McOptionsReadCoverageImproved(options);
620
621  /* Check for incompatible options and do some option-specific
622   * intializations.
623   */
624
625  if (traversalDirection == McFwd_c) {
626    if (checkVacuity) {
627      fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n");
628      McOptionsFree(options);
629      return 1;
630    }
631    if (performCoverageHoskote || performCoverageImproved) {
632      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n");
633      McOptionsFree(options);
634      return 1;
635    }
636  }
637
638  if (checkVacuity) {
639    if (performCoverageHoskote || performCoverageImproved) {
640      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n");
641      McOptionsFree(options);
642      return 1;
643    }
644  }
645
646  guideFile =  McOptionsReadGuideFile(options);
647
648  if(guideFile != NIL(FILE) ){
649    guidedSearchType = Mc_ReadGuidedSearchType();
650    if(guidedSearchType == Mc_None_c){  /* illegal setting */
651      fprintf(vis_stderr, "** mc error: Unknown  hint type\n");
652      fclose(guideFile);
653      McOptionsFree(options);
654      return 1;
655    }
656
657    if(traversalDirection == McFwd_c){  /* illegal combination */
658      fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n");
659      fclose(guideFile);
660      McOptionsFree(options);
661      return 1;
662    }
663
664    if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
665       Img_UserSpecifiedMethod() != Img_Monolithic_c &&
666       Img_UserSpecifiedMethod() != Img_Mlp_c){
667      fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n");
668      fclose(guideFile);
669      McOptionsFree(options);
670      return 1;
671    }
672
673    hintsArray = Mc_ReadHints(guideFile);
674    fclose(guideFile); guideFile = NIL(FILE);
675    if( hintsArray == NIL(array_t) ){
676      McOptionsFree(options);
677      return 1;
678    }
679
680  } /* if guided search */
681
682  /* If don't-cares are used, -r implies -c.  Note that the satisfying
683     sets of a subformula are only in terms of propositions therein
684     and their cone of influence.  Hence, we can share satisfying sets
685     among formulae.  I don't quite understand what the problem with
686     don't-cares is (RB) */
687  if (McOptionsReadReduceFsm(options))
688    if (dcLevel != McDcLevelNone_c)
689      McOptionsSetUseFormulaTree(options, TRUE);
690
691  if (traversalDirection == McFwd_c &&
692      McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
693    McOptionsSetDbgLevel(options, McDbgLevelNone_c);
694    (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n");
695  }
696
697  /* Read CTL formulae */
698  ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile);
699  fclose(ctlFile); ctlFile = NIL(FILE);
700  if (ctlArray == NIL(array_t)) {
701    (void) fprintf(vis_stderr,
702                   "** mc error: error in parsing formulas from file\n");
703    McOptionsFree(options);
704    return 1;
705  }
706
707  /* read network */
708  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
709  if (network == NIL(Ntk_Network_t)) {
710    fprintf(vis_stdout, "%s\n", error_string());
711    error_init();
712    Ctlp_FormulaArrayFree(ctlArray);
713    McOptionsFree(options);
714    return 1;
715  }
716
717  /* read fsm */
718  totalFsm = Fsm_NetworkReadOrCreateFsm(network);
719  if (totalFsm == NIL(Fsm_Fsm_t)) {
720    fprintf(vis_stdout, "%s\n", error_string());
721    error_init();
722    Ctlp_FormulaArrayFree(ctlArray);
723    McOptionsFree(options);
724    return 1;
725  }
726
727  /* Assign variables to system if doing FAFW */
728  systemVarBddIdTable = NIL(st_table);
729  systemFile = McOptionsReadSystemFile(options);
730  if (systemFile != NIL(FILE)) {
731    systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
732    fclose(systemFile); systemFile = NIL(FILE);
733    if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */
734      Ctlp_FormulaArrayFree(ctlArray);
735      McOptionsFree(options);
736      return 1;
737    }
738  } /* if FAFW */
739
740  if(options->FAFWFlag && systemVarBddIdTable == 0) {
741    systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
742  }
743
744  if (verbosity > McVerbosityNone_c)
745    totalInitialTime = util_cpu_time();
746  else /* to remove uninitialized variable warning */
747    totalInitialTime = 0;
748
749  if(traversalDirection == McFwd_c){
750    mdd_t *totalInitialStates;
751    double nInitialStates;
752
753    totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm);
754    nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm),
755                                     totalInitialStates,
756                                     Fsm_FsmReadPresentStateVars(totalFsm));
757    mdd_free(totalInitialStates);
758
759    /* If the number of initial states is only one, we can use both
760     * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE),
761     * however, if we have multiple initial states, we should use
762     * p0 ^ !f == FALSE.
763     */
764    ctlNormalFormulaArray =
765      Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0),
766                                        noShare);
767    /* end conversion for forward traversal */
768  } else if (noShare) { /* conversion for backward, no sharing */
769    ctlNormalFormulaArray =
770      Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
771  }else{ /* conversion for backward, with sharing */
772    /* Note that converting to DAG after converting to existential form would
773       lead to more sharing, but it cannot be done since equal subformula that
774       are converted from different formulae need different pointers back to
775       their originals */
776    if (checkVacuity) {
777      ctlNormalFormulaArray =
778        Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
779    }
780    else {
781      array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray );
782      array_free( ctlArray );
783      ctlArray = temp;
784      ctlNormalFormulaArray =
785        Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray);
786    }
787  }
788  /* At this point, ctlNormalFormulaArray contains the formulas that are
789     actually going to be checked, and ctlArray contains the formulas from
790     which the conversion has been done.  Both need to be kept around until the
791     end, for debugging purposes. */
792
793  numFormulae = array_n(ctlNormalFormulaArray);
794
795  /* time out */
796  if (timeOutPeriod > 0) {
797    /* Set the static variables used by the signal handler. */
798    mcTimeOut = timeOutPeriod;
799    alarmLapTime = util_cpu_ctime();
800    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
801    (void) alarm(timeOutPeriod);
802    if (setjmp(timeOutEnv) > 0) {
803      (void) fprintf(vis_stdout,
804                "# MC: timeout occurred after %d seconds.\n", timeOutPeriod);
805      (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n");
806      if (verbosity > McVerbosityNone_c) {
807        fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n",
808                Img_GetNumberOfImageComputation(Img_Forward_c),
809                Img_GetNumberOfImageComputation(Img_Backward_c));
810      }
811      alarm(0);
812      return 1;
813    }
814  }
815
816  /* Create reduced fsm, if necessary */
817  if (!McOptionsReadReduceFsm(options)){
818    /* We want to minimize only when "-r" option is not specified */
819    /* reduceFsm would be NIL, if there is no reduction observed */
820    assert (reducedFsm == NIL(Fsm_Fsm_t));
821    reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
822    if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) {
823      mddMgr = Fsm_FsmReadMddManager(reducedFsm);
824      bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
825                   Fsm_FsmReadPresentStateVars(reducedFsm));
826      (void)fprintf(vis_stdout,"Local system includes ");
827      (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
828                    array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
829                    array_n(bddIdArray));
830      array_free(bddIdArray);
831    }
832  }
833
834  /************** for all formulae **********************************/
835  for(i = 0; i < numFormulae; i++) {
836    int nImgComps, nPreComps;
837    boolean result;
838    Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
839                                             ctlNormalFormulaArray, i);
840
841    modelFsm = NIL(Fsm_Fsm_t);
842
843    /* do a check */
844    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
845      (void) fprintf(vis_stdout,
846                     "** mc error: error in parsing Atomic Formula:\n%s\n",
847                     error_string());
848      error_init();
849      Ctlp_FormulaFree(ctlFormula);
850      continue;
851    }
852
853    /* Create reduced fsm */
854    if (McOptionsReadReduceFsm(options)) {
855      /* We have not done top level reduction. */
856      /* Using the same variable reducedFsm here   */
857      array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1);
858
859      assert(reducedFsm == NIL(Fsm_Fsm_t));
860      array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula);
861      reducedFsm = McConstructReducedFsm(network, oneFormulaArray);
862      array_free(oneFormulaArray);
863
864      if (reducedFsm && verbosity != McVerbosityNone_c) {
865        mddMgr = Fsm_FsmReadMddManager(reducedFsm);
866        bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
867                       Fsm_FsmReadPresentStateVars(reducedFsm));
868        (void)fprintf(vis_stdout,"Local system includes ");
869        (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
870                      array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
871                      array_n(bddIdArray));
872        array_free(bddIdArray);
873      }
874    }/* if readreducefsm */
875
876    /* Let us see if we got any reduction via top level or via "-r" */
877    if (reducedFsm == NIL(Fsm_Fsm_t))
878      modelFsm = totalFsm; /* no reduction */
879    else
880      modelFsm = reducedFsm; /* some reduction at some point */
881
882    /* compute initial states */
883    modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
884    if (modelInitialStates == NIL(mdd_t)) {
885      int j;
886      (void) fprintf(vis_stdout,
887      "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n",
888                     error_string());
889      if (modelFsm != totalFsm)
890        Fsm_FsmFree(reducedFsm);
891
892      alarm(0);
893
894      for(j = i; j < numFormulae; j++)
895        Ctlp_FormulaFree(
896          array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
897      array_free( ctlNormalFormulaArray );
898
899      Ctlp_FormulaArrayFree( ctlArray );
900
901      McOptionsFree(options);
902
903      return 1;
904    }
905
906    earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);
907
908    if(hintsArray != NIL(Ctlp_FormulaArray_t)) {
909      hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
910      if( hintsStatesArray == NIL(array_t) ||
911          (guidedSearchType == Mc_Global_c &&
912           Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) {
913        int j;
914
915        if( guidedSearchType == Mc_Global_c &&
916            Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)
917          fprintf(vis_stderr, "** mc error: global hints incompatible with "
918                  "mixed formulae\n");
919
920        Mc_EarlyTerminationFree(earlyTermination);
921        mdd_free(modelInitialStates);
922        if (modelFsm != totalFsm)
923          Fsm_FsmFree(reducedFsm);
924        alarm(0);
925        for(j = i; j < numFormulae; j++)
926          Ctlp_FormulaFree(
927            array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
928        array_free( ctlNormalFormulaArray );
929        Ctlp_FormulaArrayFree( ctlArray );
930        McOptionsFree(options);
931        return 1;
932      } /* problem with hints */
933    } /* hints exist */
934
935    /* stats */
936    if (verbosity > McVerbosityNone_c) {
937      initialTime = util_cpu_time();
938      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
939      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
940    } else { /* to remove uninitialized variable warnings */
941      initialTime = 0;
942      nImgComps = 0;
943      nPreComps = 0;
944    }
945    mddMgr = Fsm_FsmReadMddManager(modelFsm);
946
947    /* compute don't cares. */
948    if (modelCareStatesArray == NIL(array_t)) {
949      long iTime; /* starting time for reachability analysis */
950      if (verbosity > McVerbosityNone_c && i == 0)
951        iTime = util_cpu_time();
952      else /* to remove uninitialized variable warnings */
953        iTime = 0;
954
955      /* ardc */
956      if (dcLevel == McDcLevelArdc_c) {
957        Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options);
958
959        modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates(
960          modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
961        if (verbosity > McVerbosityNone_c && i == 0)
962          Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime);
963
964      /* rch dc */
965      } else if (dcLevel >= McDcLevelRch_c) {
966        modelCareStates =
967          Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0,
968                                        Fsm_Rch_Default_c, 0, 0,
969                                        NIL(array_t), FALSE, NIL(array_t));
970        if (verbosity > McVerbosityNone_c && i == 0) {
971          Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime,
972                                          Fsm_Rch_Default_c);
973        }
974
975        modelCareStatesArray = array_alloc(mdd_t *, 0);
976        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
977      } else {
978        modelCareStates = mdd_one(mddMgr);
979        modelCareStatesArray = array_alloc(mdd_t *, 0);
980        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
981      }
982    }
983
984    Fsm_MinimizeTransitionRelationWithReachabilityInfo(
985      modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c,
986      verbosity > 1);
987
988    /* fairness conditions */
989    fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
990                                          verbosity, dcLevel, GSHschedule,
991                                          McBwd_c, FALSE);
992    fairCond = Fsm_FsmReadFairnessConstraint(modelFsm);
993
994    if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) {
995      (void)fprintf(vis_stdout,
996                    "** mc warning: There are no fair initial states\n");
997    }
998    else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) {
999      (void)fprintf(vis_stdout,
1000                    "** mc warning: Some initial states are not fair\n");
1001    }
1002
1003    /* some user feedback */
1004    if (verbosity != McVerbosityNone_c) {
1005      (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1);
1006      Ctlp_FormulaPrint(vis_stdout,
1007                        Ctlp_FormulaReadOriginalFormula(ctlFormula));
1008      (void)fprintf (vis_stdout, "\n");
1009      if (traversalDirection == McFwd_c) {
1010        (void)fprintf(vis_stdout, "Forward formula : ");
1011        Ctlp_FormulaPrint(vis_stdout, ctlFormula);
1012        (void)fprintf(vis_stdout, "\n");
1013      }
1014    }
1015
1016    /************** the actual computation **********************************/
1017    if (checkVacuity) {
1018      McVacuityDetection(modelFsm, ctlFormula, i,
1019                         fairStates, fairCond, modelCareStatesArray,
1020                         earlyTermination, hintsStatesArray,
1021                         guidedSearchType, modelInitialStates,
1022                         options);
1023    }
1024    else { /* Normal Model Checking */
1025      mdd_t *ctlFormulaStates =
1026        Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
1027                              fairCond, modelCareStatesArray,
1028                              earlyTermination, hintsStatesArray,
1029                              guidedSearchType, verbosity, dcLevel,
1030                              buildOnionRings, GSHschedule);
1031
1032      McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond,
1033                         modelCareStatesArray, earlyTermination,
1034                         hintsStatesArray, guidedSearchType, verbosity,
1035                         dcLevel, buildOnionRings, GSHschedule,
1036                         traversalDirection, modelInitialStates,
1037                         ctlFormulaStates, &totalcoveredstates,
1038                         signalTypeList, signalList, statesCoveredList,
1039                         newCoveredStatesList, statesToRemoveList,
1040                         performCoverageHoskote, performCoverageImproved);
1041
1042      Mc_EarlyTerminationFree(earlyTermination);
1043      if(hintsStatesArray != NIL(array_t))
1044        mdd_array_free(hintsStatesArray);
1045      /* Set up things for possible FAFW analysis of counterexample. */
1046      Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
1047      Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
1048      /* user feedback on succes/fail */
1049      result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
1050                               ctlFormula, ctlFormulaStates,
1051                               modelInitialStates, modelCareStatesArray,
1052                               options, verbosity);
1053      Fsm_FsmSetFAFWFlag(modelFsm, 0);
1054      Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL);
1055      mdd_free(ctlFormulaStates);
1056    }
1057
1058    if (verbosity > McVerbosityNone_c) {
1059      finalTime = util_cpu_time();
1060      fprintf(vis_stdout, "-- mc time = %10g\n",
1061        (double)(finalTime - initialTime) / 1000.0);
1062      fprintf(vis_stdout,
1063              "-- %d image computations and %d preimage computations\n",
1064              Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
1065              Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
1066    }
1067    mdd_free(modelInitialStates);
1068    mdd_free(fairStates);
1069    Ctlp_FormulaFree(ctlFormula);
1070
1071    if ((McOptionsReadReduceFsm(options)) &&
1072        (reducedFsm != NIL(Fsm_Fsm_t))) {
1073      /*
1074      ** We need to free the reducedFsm only if it was created under "-r"
1075      ** option and was non-NIL.
1076      */
1077      Fsm_FsmFree(reducedFsm);
1078      reducedFsm = NIL(Fsm_Fsm_t);
1079      modelFsm = NIL(Fsm_Fsm_t);
1080      if (modelCareStates) {
1081        mdd_array_free(modelCareStatesArray);
1082        modelCareStates = NIL(mdd_t);
1083        modelCareStatesArray = NIL(array_t);
1084      } else if (modelCareStatesArray) {
1085        modelCareStatesArray = NIL(array_t);
1086      }
1087    }
1088  }/* for all formulae */
1089
1090  if (verbosity > McVerbosityNone_c) {
1091    finalTime = util_cpu_time();
1092    fprintf(vis_stdout, "-- total mc time = %10g\n",
1093      (double)(finalTime - totalInitialTime) / 1000.0);
1094    fprintf(vis_stdout,
1095            "-- total %d image computations and %d preimage computations\n",
1096            Img_GetNumberOfImageComputation(Img_Forward_c),
1097            Img_GetNumberOfImageComputation(Img_Backward_c));
1098    /* Print tfm options if we have a global fsm. */
1099    if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) {
1100      imageInfo = Fsm_FsmReadImageInfo(modelFsm);
1101      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
1102          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
1103        Img_TfmPrintStatistics(imageInfo, Img_Both_c);
1104      }
1105    }
1106  }
1107
1108  /* Print results of coverage computation */
1109  McPrintCoverageSummary(modelFsm, dcLevel,
1110                         options, modelCareStatesArray,
1111                         modelCareStates, totalcoveredstates,
1112                         signalTypeList, signalList, statesCoveredList,
1113                         performCoverageHoskote, performCoverageImproved);
1114  mdd_array_free(newCoveredStatesList);
1115  mdd_array_free(statesToRemoveList);
1116  array_free(signalTypeList);
1117  array_free(signalList);
1118  mdd_array_free(statesCoveredList);
1119  if (totalcoveredstates != NIL(mdd_t))
1120    mdd_free(totalcoveredstates);
1121
1122  if (modelCareStates) {
1123    mdd_array_free(modelCareStatesArray);
1124  }
1125
1126  if(hintsArray)
1127    Ctlp_FormulaArrayFree(hintsArray);
1128
1129  if ((McOptionsReadReduceFsm(options) == FALSE) &&
1130      (reducedFsm != NIL(Fsm_Fsm_t))) {
1131    /* If "-r" was not specified and we did some reduction at top
1132       level, we need to free it */
1133    Fsm_FsmFree(reducedFsm);
1134    reducedFsm = NIL(Fsm_Fsm_t);
1135    modelFsm = NIL(Fsm_Fsm_t);
1136  }
1137
1138  if(systemVarBddIdTable)
1139    st_free_table(systemVarBddIdTable);
1140  array_free(ctlNormalFormulaArray);
1141  (void) fprintf(vis_stdout, "\n");
1142
1143  Ctlp_FormulaArrayFree(ctlArray);
1144  McOptionsFree(options);
1145  alarm(0);
1146  return 0;
1147}
1148
1149
1150/**Function********************************************************************
1151
1152  Synopsis    [Parse command line options for mc.]
1153
1154  SideEffects []
1155
1156******************************************************************************/
1157static McOptions_t *
1158ParseMcOptions(
1159  int argc,
1160  char **argv)
1161{
1162  unsigned int i;
1163  int c;
1164  char *guideFileName = NIL(char);
1165  char *variablesForSystem = NIL(char);
1166  FILE *guideFile = NIL(FILE);
1167  FILE *systemFile = NIL(FILE);
1168  boolean doCoverageHoskote = FALSE;
1169  boolean doCoverageImproved = FALSE;
1170  boolean useMore = FALSE;
1171  boolean reduceFsm = FALSE;
1172  boolean printInputs = FALSE;
1173  boolean useFormulaTree = FALSE;
1174  boolean vd = FALSE;
1175  boolean beer = FALSE;
1176  boolean FAFWFlag = FALSE;
1177  boolean GFAFWFlag = FALSE;
1178  FILE *inputFp=NIL(FILE);
1179  FILE *debugOut=NIL(FILE);
1180  char *debugOutName=NIL(char);
1181  Mc_DcLevel dcLevel = McDcLevelRch_c;
1182  McDbgLevel dbgLevel = McDbgLevelNone_c;
1183  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
1184  Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
1185  McOptions_t *options = McOptionsAlloc();
1186  int timeOutPeriod = 0;
1187  Mc_FwdBwdAnalysis traversalDirection = McBwd_c;
1188  Fsm_ArdcOptions_t *ardcOptions;
1189  Mc_GSHScheduleType schedule = McGSH_EL_c;
1190
1191  /*
1192   * Parse command line options.
1193   */
1194
1195  util_getopt_reset();
1196  while ((c = util_getopt(argc, argv, "bcirmg:hv:d:D:VBf:t:CIFR:S:GWw:")) != EOF) {
1197    switch(c) {
1198    case 'g':
1199      guideFileName = util_strsav(util_optarg);
1200      break;
1201    case 'h':
1202      goto usage;
1203    case 'v':
1204      for (i = 0; i < strlen(util_optarg); i++) {
1205        if (!isdigit((int)util_optarg[i])) {
1206          goto usage;
1207        }
1208      }
1209      verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
1210      break;
1211    case 'd':
1212      for (i = 0; i < strlen(util_optarg); i++) {
1213        if (!isdigit((int)util_optarg[i])) {
1214          goto usage;
1215        }
1216      }
1217      dbgLevel = (McDbgLevel) atoi(util_optarg);
1218      break;
1219    case 'D':
1220      for (i = 0; i < strlen(util_optarg); i++) {
1221        if (!isdigit((int)util_optarg[i])) {
1222          goto usage;
1223        }
1224      }
1225      dcLevel = (Mc_DcLevel) atoi(util_optarg);
1226      break;
1227    case 'b':
1228      fwdBwd = McBwd_c;
1229      break;
1230    case 'V':         /*Vacuity detection option*/
1231      vd = TRUE;
1232      break;
1233    case 'B':         /*Vacuity detection Beer et al method option*/
1234      vd = TRUE;
1235      beer = TRUE;
1236      break;
1237    case 'f':
1238      debugOutName = util_strsav(util_optarg);
1239      break;
1240    case 'm':
1241      useMore = TRUE;
1242      break;
1243    case 'r' :
1244      reduceFsm = TRUE;
1245      break;
1246    case 'c':
1247      useFormulaTree = TRUE;
1248      break;
1249    case 't' :
1250      timeOutPeriod  = atoi(util_optarg);
1251      break;
1252    case 'i' :
1253      printInputs = TRUE;
1254      break;
1255    case 'F' :
1256      traversalDirection = McFwd_c;
1257      break;
1258    case 'S' :
1259      schedule = McStringConvertToScheduleType(util_optarg);
1260      break;
1261    case 'w':
1262      variablesForSystem = util_strsav(util_optarg);
1263    case 'W':
1264      FAFWFlag = 1;
1265      break;
1266    case 'G':
1267      GFAFWFlag = 1;
1268      break;
1269    case 'C' :
1270      doCoverageHoskote = TRUE;
1271      break;
1272    case 'I' :
1273      doCoverageImproved = TRUE;
1274      break;
1275    default:
1276      goto usage;
1277    }
1278  }
1279
1280  /*
1281   * Open the ctl file.
1282   */
1283  if (argc - util_optind == 0) {
1284    (void) fprintf(vis_stderr, "** mc error: file containing ctl formulas not provided\n");
1285    goto usage;
1286  }
1287  else if (argc - util_optind > 1) {
1288    (void) fprintf(vis_stderr, "** mc error: too many arguments\n");
1289    goto usage;
1290  }
1291
1292  McOptionsSetFwdBwd(options, fwdBwd);
1293  McOptionsSetUseMore(options, useMore);
1294  McOptionsSetReduceFsm(options, reduceFsm);
1295  McOptionsSetVacuityDetect(options, vd);
1296  McOptionsSetBeerMethod(options, beer);
1297  McOptionsSetUseFormulaTree(options, useFormulaTree);
1298  McOptionsSetPrintInputs(options, printInputs);
1299  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
1300  McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
1301  McOptionsSetCoverageHoskote(options, doCoverageHoskote);
1302  McOptionsSetCoverageImproved(options, doCoverageImproved);
1303
1304  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
1305    fprintf(vis_stderr, "** mc warning : -w and -W options are ignored without -d option\n");
1306  }
1307
1308  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
1309    fprintf(vis_stderr, "** mc warning : -i is recommended with -w or -W option\n");
1310  }
1311  if(FAFWFlag) {
1312    if (bdd_get_package_name() != CUDD) {
1313      fprintf(vis_stderr, "** mc warning : -w and -W option is only available with CUDD\n");
1314      FAFWFlag = 0;
1315      FREE(variablesForSystem);
1316      variablesForSystem = NIL(char);
1317    }
1318  }
1319
1320
1321  if (schedule == McGSH_Unassigned_c) {
1322    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
1323    goto usage;
1324  } else {
1325    McOptionsSetSchedule(options, schedule);
1326  }
1327  inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
1328  if (inputFp == NIL(FILE)) {
1329    McOptionsFree(options);
1330    if (guideFileName != NIL(char)) FREE(guideFileName);
1331    return NIL(McOptions_t);
1332  }
1333  McOptionsSetCtlFile(options, inputFp);
1334
1335  if (debugOutName != NIL(char)) {
1336    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
1337    FREE(debugOutName);
1338    if (debugOut == NIL(FILE)) {
1339      McOptionsFree(options);
1340      if (guideFileName != NIL(char)) FREE(guideFileName);
1341      return NIL(McOptions_t);
1342    }
1343  }
1344  McOptionsSetDebugFile(options, debugOut);
1345
1346
1347  if (guideFileName != NIL(char)) {
1348    guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
1349    if (guideFile == NIL(FILE)) {
1350      fprintf(vis_stderr, "** mc error: cannot open guided search file %s.\n",
1351              guideFileName);
1352      FREE(guideFileName);
1353      guideFileName = NIL(char);
1354      McOptionsFree(options);
1355      return NIL(McOptions_t);
1356    }
1357    FREE(guideFileName);
1358    guideFileName = NIL(char);
1359  }
1360  McOptionsSetGuideFile(options, guideFile);
1361
1362  if (variablesForSystem != NIL(char)) {
1363    systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
1364    if (systemFile == NIL(FILE)) {
1365      fprintf(vis_stderr, "** mc error: cannot open system variables file for FAFW %s.\n",
1366              variablesForSystem);
1367      FREE(variablesForSystem);
1368      variablesForSystem = NIL(char);
1369      McOptionsFree(options);
1370      return NIL(McOptions_t);
1371    }
1372    FREE(variablesForSystem);
1373    variablesForSystem = NIL(char);
1374  }
1375  McOptionsSetVariablesForSystem(options, systemFile);
1376
1377  if ((verbosityLevel != McVerbosityNone_c) &&
1378       (verbosityLevel != McVerbosityLittle_c) &&
1379       (verbosityLevel != McVerbositySome_c) &&
1380       (verbosityLevel != McVerbosityMax_c)) {
1381    goto usage;
1382  }
1383  else {
1384    McOptionsSetVerbosityLevel(options, verbosityLevel);
1385  }
1386
1387  if ((dbgLevel != McDbgLevelNone_c) &&
1388       (dbgLevel != McDbgLevelMin_c) &&
1389       (dbgLevel != McDbgLevelMinVerbose_c) &&
1390       (dbgLevel != McDbgLevelMax_c) &&
1391       (dbgLevel != McDbgLevelInteractive_c)) {
1392    goto usage;
1393  }
1394  else {
1395    McOptionsSetDbgLevel(options, dbgLevel);
1396  }
1397
1398  if ((dcLevel != McDcLevelNone_c) &&
1399       (dcLevel != McDcLevelRch_c ) &&
1400       (dcLevel != McDcLevelRchFrontier_c ) &&
1401       (dcLevel != McDcLevelArdc_c )) {
1402    goto usage;
1403  }
1404  else {
1405    McOptionsSetDcLevel(options, dcLevel);
1406  }
1407
1408  McOptionsSetTraversalDirection(options, traversalDirection);
1409  if (dcLevel == McDcLevelArdc_c) {
1410    ardcOptions = Fsm_ArdcAllocOptionsStruct();
1411    Fsm_ArdcGetDefaultOptions(ardcOptions);
1412  } else
1413    ardcOptions = NIL(Fsm_ArdcOptions_t);
1414  McOptionsSetArdcOptions(options, ardcOptions);
1415
1416  return options;
1417
1418  usage:
1419  (void) fprintf(vis_stderr, "usage: model_check [-b][-c][-d dbg_level][-f dbg_file][-g <hintfile>][-h][-i][-m][-r][-V][-B][-t period][-C][-I][-P][-v verbosity_level][-D dc_level][-F][-S <schedule>] <ctl_file>\n");
1420  (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\n");
1421  (void) fprintf(vis_stderr, "    -c \tNo sharing of CTL parse tree. This option does not matter for vacuity detection.\n");
1422  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
1423  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
1424  (void) fprintf(vis_stderr, "        debug_level = 1 => automatic minimal debugging\n");
1425  (void) fprintf(vis_stderr, "        debug_level = 2 => automatic minimal debugging with extra verbosity\n");
1426  (void) fprintf(vis_stderr, "        debug_level = 3 => automatic maximal debugging\n");
1427  (void) fprintf(vis_stderr, "        debug_level = 4 => interactive debugging\n");
1428  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
1429  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
1430  (void) fprintf(vis_stderr, "    -g <hint_file> \tSpecify file for guided search.\n");
1431  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
1432  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
1433  (void) fprintf(vis_stderr, "    -m \tPipe debug output through more.\n");
1434  (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to formula being verified\n");
1435  (void) fprintf(vis_stderr, "    -t <period> time out period\n");
1436  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
1437  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
1438  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
1439  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
1440  (void) fprintf(vis_stderr, "    -w <node file> \tSpecify variables controlled by system.\n");
1441  (void) fprintf(vis_stderr, "    -B  vacuity detection for w-ACTL formulae using method of Beer et al \n");
1442  (void) fprintf(vis_stderr, "    -C Compute coverage of all observable signals using Hoskote et.al's implementation\n");
1443  (void) fprintf(vis_stderr, "    -D <dc_level>\n");
1444  (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
1445  (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
1446  (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");
1447
1448  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
1449  (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
1450  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
1451  (void) fprintf(vis_stderr, "    -F \tUse forward model checking.\n");
1452  (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
1453  (void) fprintf(vis_stderr, "    -I Compute coverage of all observable signals using improved coverage implementation\n");
1454  (void) fprintf(vis_stderr, "    -S <schedule>\n");
1455  (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
1456  (void) fprintf(vis_stderr, "    -V  thorough vacuity detection\n");
1457  (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
1458  (void) fprintf(vis_stderr, "    <ctl_file> The input file containing CTL formula to be checked.\n");
1459
1460  if (guideFileName != NIL(char)) FREE(guideFileName);
1461  McOptionsFree(options);
1462
1463  return NIL(McOptions_t);
1464}
1465
1466
1467/**Function********************************************************************
1468
1469  Synopsis [Check whether language of FSM is empty.]
1470
1471  CommandName [lang_empty]
1472
1473  CommandSynopsis [perform language emptiness check on a flattened network]
1474
1475  CommandArguments [ \[-b\] \[-d &lt;dbg_level&gt;\] \[-f &lt;dbg_file&gt;\]
1476  \[-h\] \[-i\] \[-s\] \[-t &lt;time_out_period&gt;\]
1477  \[-v &lt;verbosity_level&gt;\]
1478  \[-A &lt;le_method&gt;\] \[-D &lt;dc_level&gt;\]
1479  \[-S &lt;schedule&gt;\] \[-L &lt;lockstep_mode&gt;\] ]
1480
1481  CommandDescription [
1482  Performs language emptiness check on a flattened network.  The
1483  language is not empty when there is a fair path starting at an
1484  initial state.  Before calling this command, the user should have
1485  initialized the design by calling the command <A
1486  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.  <p>
1487
1488  A fairness constraint can be read in by calling the
1489  <A HREF="read_fairnessCmd.html"><code>read_fairness</code></A> command;
1490  if none is specified, all paths are taken to be fair.
1491  <p>
1492
1493  The system is reduced automatically with respect to the set of
1494  fairness constraints.  If the language is not empty, a proof of this
1495  fact is generated.  A proof is a fair path starting at an initial
1496  state.  This is represented by a finite sequence of states starting
1497  at an initial state (the stem) leading to a fair cycle, i.e., a
1498  cycle on which there lies a state from each fairness condition.
1499  <p>
1500
1501  Command options:
1502  <p>
1503
1504  <dl>
1505
1506  <dt> -b
1507  <dd> Use backward analysis when performing debugging; the default is to use forward
1508           analysis. This should be tried when the debugger spends a large amount of time when
1509           creating a path to a fair cycle.
1510  <p>
1511
1512  <dt> -d <code> &lt;dbg_level&gt; </code>
1513  <dd> Specify whether to demonstrate a proof of the language non-emptiness
1514  <p>
1515  <dd>
1516  <code> dbg_level</code> must be one of the following:
1517  <p>
1518
1519  <code> 0 </code>: No debugging  performed. This is the default.
1520  <p>
1521
1522  <code> 1 </code>: Generate a path to a fair cycle.
1523  <p>
1524
1525  <dt> -f &lt;<code>dbg_file</code>&gt;
1526  <dd> Write the debugger output to <code>dbg_file</code>.
1527  <p>
1528
1529  <dt> -h
1530  <dd> Print the command usage.
1531  <p>
1532
1533  <dt> -m
1534  <dd> Pipe debugger output through the UNIX utility more.
1535  <p>
1536
1537  <dt> -i
1538  <dd> Print input values causing transitions between states during debugging.
1539  Both primary and pseudo inputs are printed.
1540  <p>
1541
1542  <dt> -s
1543  <dd> Print debug output in the format accepted by the
1544       <A HREF="simulateCmd.html"><code>simulate</code></A> command.
1545  <p>
1546
1547  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
1548  <dd> Specify the time out period (in seconds) after which the command
1549  aborts.  By default this option is set to infinity.
1550  <p>
1551
1552  <dt> -v  <code>&lt;verbosity_level&gt;</code>
1553  <dd> Specify verbosity level. This sets the amount of feedback on CPU
1554  usage and code status.
1555  <p>
1556
1557  <dd>
1558  <code>verbosity_level</code> must be one of the following:
1559  <p>
1560
1561  <code> 0 </code>: No feedback provided. This is the default.<p>
1562
1563  <code> 1 </code>: Feedback on code location.<p>
1564
1565  <code> 2 </code>: Feedback on code location and CPU usage.<p>
1566
1567  <dt> -A <code> &lt;le_method&gt; </code>
1568  <dd>
1569  Specify whether the compositional SCC analysis algorithm, Divide and
1570  Compose (DnC), is enabled for language emptiness checking.
1571  The DnC algorithm first enumerates fair SCCs in an over-approximated
1572  abstract model, and then successively refines them in the more
1573  concrete models.
1574  Since non-fair SCCs can be ignored in the more concrete models, a
1575  potentially large part of the state space are pruned away early on
1576  when the computations are cheap.
1577  <p>
1578
1579  <dd>
1580  <code> le_method </code> must be one of the following:
1581  <p>
1582
1583  <code> 0 </code>: no use of Divide and Compose (Default). <p>
1584  <code> 1 </code>: use Divide and Compose. <p>
1585
1586  <dt> -D <code> &lt;dc_level&gt; </code>
1587  <dd> Specify extent to which don't cares are used to simplify MDDs.
1588  Don't cares are minterms on which the value taken by functions does not affect the computation;
1589  potentially, these minterms can be used to simplify MDDs and reduce time taken to perform
1590  MDD computations.
1591  <p>
1592
1593  <dd>
1594  <code> dc_level </code> must be one of the following:
1595  <p>
1596
1597  <code> 0 </code>: No don't cares are used. <p>
1598  <code> 1 </code>: Use unreachable states as don't cares.  This is the
1599  default. <p>
1600
1601  <dt> -S <code> &lt;schedule&gt; </code>
1602
1603  <dd> Specify schedule for GSH algorithm, which generalizes the
1604  Emerson-Lei algorithm and is used to compute greatest fixpoints.
1605  The choice of schedule affects the sequence in which EX and EU
1606  operators are applied.  It makes a difference only when fairness
1607  constraints are specified.
1608
1609  <br>
1610  <code> &lt;schedule&gt; </code> must be one of the following:
1611
1612  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
1613  is the default.
1614
1615  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.
1616
1617  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
1618  all EUs.
1619
1620  <p> <code> budget </code>: a hybrid of EL and EL2.
1621
1622  <p> <code> random </code>: enabled operators are applied in
1623  (pseudo-)random order.
1624
1625  <p> <code> off </code>: GSH is disabled, and the old algorithm is
1626  used instead.  The old algorithm uses the <code> EL </code>, but the
1627  termination checks are less sophisticated than in GSH.
1628  <p>
1629
1630  <dt> -F
1631
1632  <dd> Use forward analysis in the computation of the greatest fixpoint.
1633  This option is incompatible with -d 1 or higher and can only be used
1634  with -D 1.
1635
1636  <dt> -L <code> &lt;lockstep_mode&gt; </code>
1637
1638  <dd> Use the lockstep algorithm, which is based on fair SCC enumeration.
1639
1640  <br>
1641  <code> &lt;lockstep_mode&gt; </code> must be one of the following:
1642
1643  <p> <code> off </code>: Lockstep is disabled.  This is the default.
1644  Language emptiness is checked by computing a hull of the fair SCCs.
1645
1646  <p> <code> on </code>: Lockstep is enabled.
1647
1648  <p> <code> all </code>: Lockstep is enabled; all fair SCCs are
1649  enumerated instead of terminating as soon as one is found.  This can
1650  be used to study the SCCs of a graph, but it is slower than the
1651  default option.
1652
1653  <p> <code> n </code>: (n is a positive integer).  Lockstep is
1654  enabled and up to <code> n </code> fair SCCs are enumerated.  This
1655  is less expensive than <code> all </code>, but still less efficient
1656  than <code> on </code>, even when <code> n = 1 </code>.
1657
1658  </dl>
1659
1660  ]
1661
1662  SideEffects []
1663
1664  SeeAlso []
1665
1666******************************************************************************/
1667static int
1668CommandLe(
1669  Hrc_Manager_t **hmgr,
1670  int argc,
1671  char **argv)
1672{
1673  McOptions_t *options;
1674  Mc_VerbosityLevel verbosity;
1675  Mc_LeMethod_t leMethod;
1676  Mc_DcLevel dcLevel;
1677  McDbgLevel dbgLevel;
1678  FILE *dbgFile= NIL(FILE);
1679  boolean printInputs = FALSE;
1680  int timeOutPeriod = 0;
1681  Mc_GSHScheduleType GSHschedule;
1682  Mc_FwdBwdAnalysis GSHdirection;
1683  int lockstep;
1684  int useMore;
1685  int simValue;
1686  int reduceFsm_flag = 1;
1687  long startRchTime;
1688  mdd_t *modelCareStates;
1689  Fsm_Fsm_t *totalFsm;
1690  Fsm_Fsm_t *modelFsm, *reducedFsm = NIL(Fsm_Fsm_t);
1691  mdd_t *fairInitStates;
1692  array_t *modelCareStatesArray;
1693  long initialTime, finalTime; /* for lang_empty checking */
1694
1695  Img_ResetNumberOfImageComputation(Img_Both_c);
1696
1697  /* Read options and set timeout if requested. */
1698  if (!(options = ParseLeOptions(argc, argv))) {
1699    return 1;
1700  }
1701
1702  totalFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
1703  if (totalFsm == NIL(Fsm_Fsm_t)) {
1704    (void) fprintf(vis_stdout, "%s\n", error_string());
1705    error_init();
1706    McOptionsFree(options);
1707    return 1;
1708  }
1709
1710  initialTime = util_cpu_time();
1711
1712  verbosity     = McOptionsReadVerbosityLevel(options);
1713  leMethod      = McOptionsReadLeMethod(options);
1714  dcLevel       = McOptionsReadDcLevel(options);
1715  dbgLevel      = McOptionsReadDbgLevel(options);
1716  printInputs   = McOptionsReadPrintInputs(options);
1717  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
1718  GSHschedule   = McOptionsReadSchedule(options);
1719  GSHdirection  = McOptionsReadTraversalDirection(options);
1720  lockstep      = McOptionsReadLockstep(options);
1721  dbgFile       = McOptionsReadDebugFile(options);
1722  useMore       = McOptionsReadUseMore(options);
1723  simValue      = McOptionsReadSimValue(options);
1724
1725  if (dbgLevel != McDbgLevelNone_c && GSHdirection == McFwd_c) {
1726    (void) fprintf(vis_stderr, "** le error: -d is incompatible with -F\n");
1727    McOptionsFree(options);
1728    return 1;
1729  }
1730  if (dcLevel !=  McDcLevelRch_c && GSHdirection == McFwd_c) {
1731    (void) fprintf(vis_stderr, "** le error: -F can only be used with -D1\n");
1732    McOptionsFree(options);
1733    return 1;
1734  }
1735
1736  if (timeOutPeriod > 0) {
1737    /* Set the static variables used by the signal handler. */
1738    mcTimeOut = timeOutPeriod;
1739    alarmLapTime  = util_cpu_ctime();
1740    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
1741    (void) alarm(timeOutPeriod);
1742    if (setjmp(timeOutEnv) > 0) {
1743      (void) fprintf(vis_stdout,
1744                     "# LE: language emptiness - timeout occurred after %d seconds.\n",
1745                     timeOutPeriod);
1746      (void) fprintf(vis_stdout, "# LE: data may be corrupted.\n");
1747      if (verbosity > McVerbosityNone_c) {
1748        (void) fprintf(vis_stdout,
1749                       "-- total %d image computations and %d preimage computations\n",
1750                       Img_GetNumberOfImageComputation(Img_Forward_c),
1751                       Img_GetNumberOfImageComputation(Img_Backward_c));
1752      }
1753      alarm(0);
1754      return 1;
1755    }
1756  }
1757
1758  /* Reduce FSM to cone of influence of fairness constraints. */
1759  if (reduceFsm_flag) {
1760    Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
1761    array_t *ctlNormalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
1762    reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
1763    array_free(ctlNormalFormulaArray);
1764  }
1765
1766  if (reducedFsm == NIL(Fsm_Fsm_t)) {
1767    modelFsm = totalFsm;
1768  }else {
1769    modelFsm = reducedFsm;
1770  }
1771
1772  /* Find care states and put them in an array */
1773  if (dcLevel == McDcLevelArdc_c) { /* aRDC */
1774    Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
1775    array_t *tmpArray;
1776    Fsm_ArdcGetDefaultOptions(ardcOptions);
1777
1778    if (verbosity > 0)
1779      startRchTime = util_cpu_time();
1780    else /* to remove uninitialized variable warning */
1781      startRchTime = 0;
1782    tmpArray = Fsm_ArdcComputeOverApproximateReachableStates(
1783      modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
1784    modelCareStatesArray = mdd_array_duplicate(tmpArray);
1785
1786    FREE(ardcOptions);
1787
1788    if (verbosity > 0 )
1789      Fsm_ArdcPrintReachabilityResults(modelFsm,
1790                                       util_cpu_time() - startRchTime);
1791
1792  }else if (dcLevel >= McDcLevelRch_c) { /*RDC*/
1793    if (verbosity > 0)
1794      startRchTime = util_cpu_time();
1795    else /* to remove uninitialized variable warning */
1796      startRchTime = 0;
1797    modelCareStates =
1798      Fsm_FsmComputeReachableStates(modelFsm, 0, verbosity, 0, 0,
1799                                    (lockstep != MC_LOCKSTEP_OFF), 0, 0,
1800                                    Fsm_Rch_Default_c, 0, 0,
1801                                    NIL(array_t), FALSE, NIL(array_t));
1802    if (verbosity > 0) {
1803      Fsm_FsmReachabilityPrintResults(modelFsm,
1804                                      util_cpu_time() - startRchTime,
1805                                      Fsm_Rch_Default_c);
1806    }
1807    modelCareStatesArray = array_alloc(mdd_t *, 0);
1808    array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
1809
1810  } else {  /* mdd_one */
1811    modelCareStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
1812    modelCareStatesArray = array_alloc(mdd_t *, 0);
1813    array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
1814  }
1815
1816
1817  fairInitStates = Mc_FsmCheckLanguageEmptiness(modelFsm,
1818                                                modelCareStatesArray,
1819                                                Mc_Aut_Strong_c,
1820                                                leMethod,
1821                                                dcLevel,
1822                                                dbgLevel,
1823                                                printInputs,
1824                                                verbosity,
1825                                                GSHschedule,
1826                                                GSHdirection,
1827                                                lockstep,
1828                                                dbgFile,
1829                                                useMore,
1830                                                simValue,
1831                                                "LE");
1832
1833  if (verbosity > McVerbosityNone_c) {
1834    finalTime = util_cpu_time();
1835    fprintf(vis_stdout, "-- total le time = %10g\n",
1836            (double)(finalTime - initialTime) / 1000.0);
1837    fprintf(vis_stdout,
1838            "-- total %d image computations and %d preimage computations\n",
1839            Img_GetNumberOfImageComputation(Img_Forward_c),
1840            Img_GetNumberOfImageComputation(Img_Backward_c));
1841  }
1842
1843  /* Clean up. */
1844  if (fairInitStates) {
1845    mdd_free(fairInitStates);
1846  }
1847  mdd_array_free(modelCareStatesArray);
1848  McOptionsFree(options);
1849  if (reducedFsm) {
1850    Fsm_FsmFree(reducedFsm);
1851  }
1852
1853  alarm(0);
1854  return 0;
1855
1856} /* CommandLe */
1857
1858
1859/**Function********************************************************************
1860
1861  Synopsis    [Parse command line options for lang_empty.]
1862
1863  SideEffects []
1864
1865******************************************************************************/
1866static McOptions_t *
1867ParseLeOptions(
1868  int argc,
1869  char **argv)
1870{
1871  unsigned int i;
1872  int c;
1873  boolean useSimFormat = FALSE;
1874  FILE *debugOut=NIL(FILE);
1875  char *debugOutName=NIL(char);
1876  Mc_DcLevel dcLevel = McDcLevelRch_c;
1877  Mc_LeMethod_t leMethod = Mc_Le_Default_c;
1878  McDbgLevel dbgLevel = McDbgLevelNone_c;
1879  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
1880  Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
1881  McOptions_t *options = McOptionsAlloc();
1882  boolean printInputs = FALSE;
1883  boolean useMore = FALSE;
1884  int timeOutPeriod = 0;
1885  Mc_GSHScheduleType schedule = McGSH_EL_c;
1886  Mc_FwdBwdAnalysis direction = McBwd_c;
1887  int lockstep = MC_LOCKSTEP_OFF;
1888  Fsm_ArdcOptions_t *ardcOptions;
1889
1890  /*
1891   * Parse command line options.
1892   */
1893
1894  util_getopt_reset();
1895  while ((c = util_getopt(argc, argv, "bihmt:v:d:A:D:f:sS:L:F")) != EOF) {
1896    switch(c) {
1897    case 'h':
1898      goto usage;
1899    case 'v':
1900      for (i = 0; i < strlen(util_optarg); i++) {
1901        if (!isdigit((int)util_optarg[i])) {
1902          goto usage;
1903        }
1904      }
1905      verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
1906      break;
1907    case 'd':
1908      for (i = 0; i < strlen(util_optarg); i++) {
1909        if (!isdigit((int)util_optarg[i])) {
1910          goto usage;
1911        }
1912      }
1913      dbgLevel = (McDbgLevel) atoi(util_optarg);
1914      break;
1915    case 'A':
1916      for (i = 0; i < strlen(util_optarg); i++) {
1917        if (!isdigit((int)util_optarg[i])) {
1918          goto usage;
1919        }
1920      }
1921      leMethod = (Mc_LeMethod_t) atoi(util_optarg);
1922      break;
1923    case 'D':
1924      for (i = 0; i < strlen(util_optarg); i++) {
1925        if (!isdigit((int)util_optarg[i])) {
1926          goto usage;
1927        }
1928      }
1929      dcLevel = (Mc_DcLevel) atoi(util_optarg);
1930      break;
1931    case 'f':
1932      debugOutName = util_strsav(util_optarg);
1933      break;
1934    case 's':
1935      useSimFormat = TRUE;
1936      break;
1937    case 't':
1938      timeOutPeriod = atoi(util_optarg);
1939      break;
1940    case 'i':
1941      printInputs = TRUE;
1942      break;
1943    case 'm':
1944      useMore = TRUE;
1945      break;
1946    case 'b':
1947      fwdBwd = McBwd_c;
1948      break;
1949    case 'S' :
1950      schedule = McStringConvertToScheduleType(util_optarg);
1951      break;
1952    case 'L' :
1953      lockstep = McStringConvertToLockstepMode(util_optarg);
1954      break;
1955    case 'F' :
1956      direction = McFwd_c;
1957      break;
1958    default:
1959      goto usage;
1960    }
1961  }
1962
1963  if (schedule == McGSH_Unassigned_c) {
1964    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
1965    goto usage;
1966  } else {
1967    McOptionsSetSchedule(options, schedule);
1968  }
1969  McOptionsSetTraversalDirection(options, direction);
1970  if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
1971    (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
1972    goto usage;
1973  } else {
1974    McOptionsSetLockstep(options, lockstep);
1975  }
1976  if ((verbosityLevel != McVerbosityNone_c) &&
1977       (verbosityLevel != McVerbosityLittle_c) &&
1978       (verbosityLevel != McVerbositySome_c) &&
1979       (verbosityLevel != McVerbosityMax_c)) {
1980    goto usage;
1981  }
1982  else {
1983    McOptionsSetVerbosityLevel(options, verbosityLevel);
1984  }
1985
1986  if (debugOutName != NIL(char)) {
1987    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
1988    if (debugOut == NIL(FILE)) {
1989      McOptionsFree(options);
1990      return NIL(McOptions_t);
1991    }
1992  }
1993  McOptionsSetDebugFile(options, debugOut);
1994
1995  if ((dbgLevel != McDbgLevelNone_c) &&
1996       (dbgLevel != McDbgLevelMin_c)) {
1997    goto usage;
1998  }
1999  else {
2000    McOptionsSetDbgLevel(options, dbgLevel);
2001  }
2002
2003  if ((dcLevel != McDcLevelNone_c)  &&
2004       (dcLevel != McDcLevelRch_c )  &&
2005       (dcLevel != McDcLevelRchFrontier_c )  &&
2006       (dcLevel != McDcLevelArdc_c )) {
2007    goto usage;
2008  }
2009  else {
2010    McOptionsSetDcLevel(options, dcLevel);
2011  }
2012
2013  if ((leMethod != Mc_Le_Default_c) &&
2014      (leMethod != Mc_Le_Dnc_c)) {
2015    goto usage;
2016  }
2017  else {
2018    McOptionsSetLeMethod(options, leMethod);
2019  }
2020
2021  /* set Ardc options for le : C.W. */
2022  if (dcLevel == McDcLevelArdc_c) {
2023      ardcOptions = Fsm_ArdcAllocOptionsStruct();
2024      Fsm_ArdcGetDefaultOptions(ardcOptions);
2025  } else
2026      ardcOptions = NIL(Fsm_ArdcOptions_t);
2027  McOptionsSetArdcOptions(options, ardcOptions);
2028
2029  McOptionsSetFwdBwd(options, fwdBwd);
2030  McOptionsSetSimValue(options, useSimFormat);
2031  McOptionsSetUseMore(options, useMore);
2032  McOptionsSetPrintInputs(options, printInputs);
2033  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
2034  return options;
2035
2036  usage:
2037  (void) fprintf(vis_stderr, "usage: lang_empty [-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A <le_method>][-D <dc_level>][-S <schedule>][-F][-L <lockstep_mode>]\n");
2038  (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\n");
2039  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
2040  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
2041  (void) fprintf(vis_stderr, "        debug_level = 1 => automatic debugging\n");
2042  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
2043  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
2044  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
2045  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
2046  (void) fprintf(vis_stderr, "    -m \tPipe debug output through more\n");
2047  (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
2048  (void) fprintf(vis_stderr, "    -t <period> time out period\n");
2049  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
2050  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
2051  (void) fprintf(vis_stderr, "        verbosity_level = 1 => feedback\n");
2052  (void) fprintf(vis_stderr, "        verbosity_level = 2 => feedback and CPU usage profile\n");
2053  (void) fprintf(vis_stderr, "    -A <le_method>\n");
2054  (void) fprintf(vis_stderr, "        le_method = 0 => no use of Divide and Compose (Default)\n");
2055  (void) fprintf(vis_stderr, "        le_method = 1 => use Divide and Compose\n");
2056  (void) fprintf(vis_stderr, "    -D <dc_level>\n");
2057  (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
2058  (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
2059  (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");
2060
2061  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
2062  (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
2063  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
2064  (void) fprintf(vis_stderr, "    -S <schedule>\n");
2065  (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
2066  (void) fprintf(vis_stderr, "    -F \tUse forward analysis in fixpoint computation.\n");
2067  (void) fprintf(vis_stderr, "    -L <lockstep_mode>\n");
2068  (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");
2069
2070  McOptionsFree(options);
2071
2072  return NIL(McOptions_t);
2073}
2074
2075
2076/**Function********************************************************************
2077
2078  Synopsis [checks that all reachable states in flattened network satisfy invariants]
2079
2080  CommandName [check_invariant]
2081
2082  CommandSynopsis [check all states reachable in flattened network satisfy specified invariants]
2083
2084  CommandArguments [ \[-c\] \[-d &lt;dbg_level&gt;\] \[-g
2085  &lt;<code>hints_file</code>&gt;\] \[-f\] \[-h\] \[-i\] \[-m\] \[-r\]
2086  \[-t &lt;time_out_period&gt;\] \[-v &lt;verbosity_level&gt;\] \[-A &lt;reachability_analysis_type&gt;\] \[-D\] &lt;invar_file&gt;]
2087
2088  CommandDescription [Performs invariant checking on a flattened
2089  network.  Before calling this command, the user should have
2090  initialized the design by calling the command <A
2091  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
2092  <p>
2093
2094  If the option -A3 (abstraction refinement method GRAB) is used, the command
2095  <A
2096  HREF="build_partition_maigsCmd.html"><code>build_partition_maigs</code></A>
2097  should also have been executed. However, in this case, the default BDD
2098  manager and network partition are not mandatory, though they will be used if
2099  available. (In other words, the user must run the commands <A
2100  HREF="flatten_hierarchyCmd.html"><code> flatten_hierarchy</code></A> and <A
2101  HREF="build_partition_maigsCmd.html"><code>build_partition_maigs</code></A>, but
2102  doesn't have to run the commands <A
2103  HREF="static_orderCmd.html"><code>static_order</code></A> and <A
2104  HREF="build_partition_mddsCmd.html"><code>build_partition_mdds</code></A> before
2105  calling this command.) For extremely large networks, it is actually favorable
2106  not to build them for the entire concrete model, but let this procedure
2107  assign bdd ids and construct the partition incrementally.
2108
2109  <p>
2110
2111  Option -A4 means abstraction refinement approach using puresat algorithm,
2112  which is entirely based on SAT solver.
2113  <p>
2114
2115  An invariant is a set of states.
2116  Checking the invariant is the process of determining that all states reachable
2117  from the initial states lie in the invariant.
2118  <p>
2119
2120
2121  One way of defining an invariant is through a CTL formula which has no path operators.
2122  Such formulas should be specified in the file <code>invar_file</code>.
2123  Note that the support  of any wire referred to in a formula should consist only
2124  of latches.
2125  For the precise syntax of CTL formulas,
2126  see the <A HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>.
2127  <p>
2128
2129  <code>check_invariant</code> ignores all fairness conditions associated with the FSM.
2130  <p>
2131
2132  <code>check_invariant<code> involves reachability analysis where at
2133   every step of the reachability computation all the specified
2134   invariants are checked in the reachable states computed thus
2135   far. If some invariant does not hold, a proof of failure is
2136   demonstrated. This consists of a path starting from an initial
2137   state to a state lying outside the invariant. This path is made as
2138   short as possible. For the -A 0 option or default -A option, it is
2139   the shortest path leading to a state outside the invariant. If a
2140   set of invariants is specified, the failed formulas are reported as
2141   soon as they are detected. The check is continued with the
2142   remaining invariants.<p>
2143
2144  Command options:
2145  <p>
2146
2147  <dl>
2148
2149  <dt> -d <code> &lt;dbg_level&gt; </code>
2150  <dd> Specify the amount of debugging performed when the system fails a formula being checked.
2151  <p>
2152  <dd>
2153  <code> dbg_level</code> must be one of the following:
2154  <p>
2155
2156  <code> 0 </code>: No debugging  performed. This is the default.
2157  <p>
2158
2159  <code> 1 </code>: Generate a path from an initial state to a state
2160  lying outside the invariant. This option stores the onion rings just
2161  as specifying -f would have. Therefore, it may take more time and
2162  memory if the formula passes. This option is incompatible with -A 2
2163  option. <p>
2164
2165  <dt> -f
2166  <dd> Store the set of new states (onion rings) reached at each step of
2167  invariant. This option is likely to use more memory but possibly
2168  faster results for invariants that fail. Therefore, the debug
2169  information for a failed invariant, if requested, may be provided
2170  faster. This option is not compatible with -A 2 options.<p>
2171
2172  <dt> -g &lt;<code>hints_file</code>&gt;</dt>
2173
2174  <dd> Use guided search.  The file <code>hints_file</code> contains a
2175  series of hints.  A hint is a formula that does not contain any
2176  temporal operators, so <code>hints_file</code> has the same syntax
2177  as a file of invariants used for check_invariant.  The hints are
2178  used in the order given to change the transition relation.  The
2179  transition relation is conjoined with the hint to yield an
2180  underapproximation of the transition relation.  If the hints are
2181  cleverly chosen, this may speed up the computation considerably,
2182  because a search with the changed transition relation may be much
2183  simpler than one with the original transition relation, and results
2184  obtained can be reused, so that we may never have to do an expensive
2185  search with the original relation.  See also: Ravi and Somenzi,
2186  Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
2187  Somenzi, Efficient Decision Procedures for Model Checking of Linear
2188  Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic
2189  Guided Search for CTL Model Checking, DAC'00. This option is not
2190  compatible with -A 2 option. The description of some options for
2191  guided search can be found in the help page for
2192  print_guided_search_options. <p>
2193
2194  <dt> -h
2195  <dd> Print the command usage.
2196  <p>
2197
2198  <dt> -c
2199  <dd> Use the formula tree so that subformulae are not shared among the CTL
2200  formulae in the input file. This option is useful in the following
2201  scenario - formulae A, B and C are being checked in order and there is
2202  sub-formula sharing between A and C. If the BDDs corresponding to the shared
2203  sub-formula is huge then computation for B might not be able to finish
2204  without using this option.
2205  <p>
2206
2207  <dt> -i
2208  <dd> Print input values causing transitions between states during
2209  debugging. Both primary and pseudo inputs are printed.  <p>
2210
2211  <dt> -m
2212  <dd> Pipe debugger output through the UNIX utility  more.
2213  <p>
2214
2215  <dt> -r
2216  <dd> Reduce the FSM derived from the flattened network with respect to each
2217  of the invariants in the input file. By default, the FSM is reduced with
2218  respect to the conjunction of the invariants in the input file. If this
2219  option is used and don't cares are being used for simplification, then
2220  subformula sharing is disabled (result might be incorrect otherwise).
2221  <p>
2222
2223  <dd> The truth of  an invariant  may be independant  of  parts of the network (such as when wires have
2224  been abstracted; see <A HREF="flatten_hierarchyCmd.html"><code>flatten_hierarchy</code></A>).
2225  These parts are effectively removed when this option is invoked; this may result in
2226  more efficient invariant checking.
2227  <p>
2228
2229  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
2230  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
2231  <p>
2232  <dt> -v  <code>&lt;verbosity_level&gt;</code>
2233  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.
2234  <p>
2235
2236  <dd>
2237  <code>verbosity_level</code>  must be one of the following:
2238  <p>
2239
2240  <code> 0 </code>: No feedback provided. This is the default.<p>
2241
2242  <code> 1 </code>: Feedback on code location.<p>
2243
2244  <code> 2 </code>: Feedback on code location and CPU usage.<p>
2245
2246  <dt> -A &lt;reachability_analysis_type&gt;
2247  <dd> This option allows specification of the type of reachability computation. <p>
2248
2249  0:  (default) Breadth First Search. No approximate reachability computation. <p>
2250
2251  1: High Density Reachability Analysis (HD). Computes reachable states in a
2252  manner that keeps BDD sizes under control. May be faster than BFS in some
2253  cases. For larger circuits, this option could compute more reachable states
2254  than the -A 0 option for the same memory constraints, consequently may prove
2255  more invariants false. For help on controlling options for HD, look up help
2256  on the command: print_hd_options <A HREF="print_hd_optionsCmd.html"> <code>
2257  print_hd_options</code></A>. Refer Ravi & Somenzi, ICCAD95.  The path
2258  generated for a failed invariant using this method may not be the shortest
2259  path. This option is available only when compiled with the CUDD package. <p>
2260
2261  2. Approximate Reachability Don't Cares(ARDC). Computes over-approximated
2262  reachable states in the reachability analysis step. This may be faster than
2263  the -A 0 option . The invariants are checked in the over-approximation. This
2264  may produce false negatives, but these are resolved internally using the
2265  exact reachable states. The final results produced are the same as those for
2266  exact reachable states. For help on controlling options for ARDC, look up
2267  help on the command: print_ardc_options. <A
2268  HREF="print_ardc_optionsCmd.html"><code> print_ardc_options</code></A> Refer
2269  2 papers in TCAD96 Dec. Cho et al, one is for State Space Decomposition and
2270  the other is for Approximate FSM Traversal. This option is incompatible with
2271  -d 1 and -g options.<p>
2272
2273  3. The GRAB Abstraction Refinement Method. Conducts the reachability
2274  analysis on an abstract model. If the invariants are true in the
2275  abstract model, they are also true in the original model. If the
2276  invariants are false, the abstract counter-examples are used to
2277  refine the abstract model (since it is still inconclusive). This
2278  procedure iterates until a conclusive result is reached.  Note that,
2279  with this option, "build_partitioned_mdds" and "static_order" does
2280  not have to be executed before calling "check_invariants," though
2281  the default BDD partition and order will be reused if available.
2282  (When checking extremely large models, skipping either or both
2283  "static_order" and "build_partitioned_mdds" can often make the
2284  verification much faster.)  The grainularity of abstraction
2285  refinement also depends on the parameter "partition_threshold",
2286  which by default is 5000; one can use the VIS command "set
2287  partition_threshold 1000" to change its value. For experienced users
2288  who want to fine-tune the different parameters of GRAB, please try
2289  the test command "_grab_test" ("_grab_test -h" prints out its usage
2290  information).  Refer to Wang et al., ICCAD2003 and ICCD2004 for more
2291  information about the GRAB algorithm. Note that this option is
2292  incompatible with the "-d 1" and "-g" options.  <p>
2293
2294  4. Abstraction refinement approach using puresat algorithm, which is
2295  entirely based on SAT solver. It has several parts:
2296
2297  * Localization base Abstraction
2298  * K-induction to prove the truth of a property
2299  * Bounded Model Checking to find bugs
2300  * Incremental concretization based methods to verify abstract bugs
2301  * UNSAT proof based method to obtain refinement
2302  * Refinement minization to guarrantee a minimal refinement
2303
2304  For more information, please check the BMC'03 and STTT'05
2305  paper of Li et al., "A satisfiability-based appraoch to abstraction
2306  refinement in model checking", and " Abstraction in symbolic model checking
2307  using satisfiability as the only decision procedure" <p>
2308
2309  <dt> -D</dt>
2310
2311  <dd>First compute an overapproximation to the reachable states.  Minimize the
2312  transition relation using this approximation, and then compute the set of
2313  reachable states exactly. This may accelerate reachability analysis. Refer to
2314  the paper by Moon et al, ICCAD98. The BDD minimizing method can be chosen by
2315  using "set image_minimize_method <method>" <A HREF = "setCmd.html">
2316  <code>set</code></A>.  This option is incompatible with -g.  <p>
2317
2318  <dt> -F &lt;<code>dbg_file</code>&gt;
2319  <dd> Write the debugger output to <code>dbg_file</code>.
2320  <p>
2321
2322  <dt> -w  &lt;<code>node_file</code>&gt;
2323
2324  This option invokes the algorithm to generate an error trace divided
2325  into fated and free segements. Fate represents the inevitability and
2326  free is asserted when there is no inevitability. This can be formulated
2327  as a two-player concurrent reachability game. The two players are
2328  the environment and the system. The node_file is given to specify the
2329  variables the are controlled by the system.
2330
2331  <dt> -W <dt>
2332
2333  This option represents the case that all input variables are controlled
2334  by system.
2335
2336  <dt> -G <dt>
2337
2338  We proposed two algorithms to generate segmented counterexamples:
2339  general and restricted. By default we use the restricted
2340  algorithm. We can invoke the general algorithm with -G option.
2341
2342  For more information, please read the STTT'04
2343  paper by Jin et al., "Fate and Free Will in Error Traces" <p>
2344
2345  <dt> &lt;invarFile&gt;
2346  <dd> File containing invariants to be checked.
2347  <p>
2348  </dl>
2349
2350  <dt> Related "set" options: <p>
2351  <dt> rch_simulate &lt;#&gt;
2352  <dd> The set option can be used to set this flag rch_simulate to specify the
2353  number of random vectors to be simulated. Default value for this number is 0.
2354  <p>
2355
2356  <dt> ctl_change_bracket &lt;yes/no&gt;
2357  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
2358  therefore CTL parser does the same thing. However, in some cases a user
2359  does not want to change node names in CTL parsing. Then, use this set
2360  option by giving "no". Default is "yes".
2361  <p>
2362
2363  <dt> See also command : compute_reach <p>
2364
2365
2366  ]
2367
2368  SideEffects []
2369
2370  SeeAlso [CommandMc]
2371
2372******************************************************************************/
2373static int
2374CommandInv(
2375  Hrc_Manager_t **hmgr,
2376  int argc,
2377  char **argv)
2378{
2379  int i, j;
2380  mdd_t *tautology;
2381  McOptions_t *options;
2382  FILE *invarFile;
2383  array_t *invarArray, *formulas, *sortedFormulaArray;
2384  static Fsm_Fsm_t *totalFsm, *modelFsm;
2385  mdd_manager *mddMgr;
2386  Ntk_Network_t *network;
2387  Mc_VerbosityLevel verbosity;
2388  Mc_DcLevel dcLevel;
2389  array_t *invarNormalFormulaArray, *invarStatesArray;
2390  int timeOutPeriod = 0;
2391  int debugFlag;
2392  int buildOnionRings;
2393  Fsm_RchType_t approxFlag;
2394  int ardc;
2395  int someLeft;
2396  Ctlp_Formula_t *invarFormula;
2397  mdd_t *invarFormulaStates;
2398  mdd_t *reachableStates;
2399  array_t *fsmArray;
2400  int printStep = 0;
2401  long initTime, finalTime;
2402  array_t *careSetArray;
2403  FILE              *guideFile;
2404  FILE          *systemFile;
2405  st_table      *systemVarBddIdTable;
2406  Ctlp_FormulaArray_t *hintsArray    = NIL(Fsm_HintsArray_t);
2407  array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
2408
2409  error_init();
2410  initTime = util_cpu_time();
2411
2412  /* get command line options */
2413  if (!(options = ParseInvarOptions(argc, argv))) {
2414    return 1;
2415  }
2416  verbosity = McOptionsReadVerbosityLevel(options);
2417  dcLevel = McOptionsReadDcLevel(options);
2418  invarFile = McOptionsReadCtlFile(options);
2419  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
2420  approxFlag = McOptionsReadInvarApproxFlag(options);
2421  buildOnionRings = (int)McOptionsReadInvarOnionRingsFlag(options);
2422
2423  /* read the array of invariants */
2424  invarArray = Ctlp_FileParseFormulaArray(invarFile);
2425  fclose(invarFile);
2426  if (invarArray == NIL(array_t)) {
2427    (void) fprintf(vis_stderr, "** inv error: Error in parsing invariants from file\n");
2428    McOptionsFree(options);
2429    return 1;
2430  }
2431  if (array_n(invarArray) == 0) {
2432    (void) fprintf(vis_stderr, "** inv error: No formula in file\n");
2433    McOptionsFree(options);
2434    return 1;
2435  }
2436
2437  /* read the netwrok */
2438  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
2439  if (network == NIL(Ntk_Network_t)) {
2440    fprintf(vis_stderr, "%s\n", error_string());
2441    error_init();
2442    McOptionsFree(options);
2443    return 1;
2444  }
2445
2446  /**************************************************************************
2447   * if "-A 3" is enabled (using the abstraction refinement method GRAB ),
2448   *    call GRAB.
2449   **************************************************************************/
2450  if (approxFlag == Fsm_Rch_Grab_c) {
2451
2452    if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
2453      McOptionsFree(options);
2454      fprintf(vis_stderr,
2455              "** inv error: To use GRAB, please run build_partition_maigs first\n");
2456      /*McOptionsFree(options);*/
2457      return 1;
2458    }
2459
2460    if (timeOutPeriod > 0) {
2461      /* Set the static variables used by the signal handler. */
2462      mcTimeOut = timeOutPeriod;
2463      alarmLapTime = util_cpu_ctime();
2464      (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
2465      (void) alarm(timeOutPeriod);
2466      if (setjmp(timeOutEnv) > 0) {
2467        (void) fprintf(vis_stdout,
2468           "# INV: Checking Invariant: timeout occurred after %d seconds.\n",
2469                       timeOutPeriod);
2470        (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
2471        alarm(0);
2472        return 1;
2473      }
2474    }
2475
2476    Grab_NetworkCheckInvariants(network,
2477                                invarArray,
2478                                "GRAB", /* refineAlgorithm, */
2479                                TRUE,   /* fineGrainFlag, */
2480                                TRUE,   /* refineMinFlag, */
2481                                FALSE,  /* useArdcFlag, */
2482                                2,      /* cexType = SOR */
2483                                verbosity,
2484                                McOptionsReadDbgLevel(options),
2485                                McOptionsReadPrintInputs(options),
2486                                McOptionsReadDebugFile(options),
2487                                McOptionsReadUseMore(options),
2488                                "INV" /* driverName */
2489                                );
2490    McOptionsFree(options);
2491    return 0;
2492  }
2493
2494  if (approxFlag == Fsm_Rch_PureSat_c) {
2495
2496    if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
2497      McOptionsFree(options);
2498      fprintf(vis_stderr,
2499              "** inv error: Please run build_partition_maigs first\n");
2500      McOptionsFree(options);
2501      return 1;
2502    }
2503
2504    if (timeOutPeriod > 0) {
2505      /* Set the static variables used by the signal handler. */
2506      mcTimeOut = timeOutPeriod;
2507      alarmLapTime = util_cpu_ctime();
2508      (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
2509      (void) alarm(timeOutPeriod);
2510      if (setjmp(timeOutEnv) > 0) {
2511        (void) fprintf(vis_stdout,
2512           "# INV by PURESAT: Checking Invariant using PURESAT: timeout occurred after %d seconds.\n",
2513                       timeOutPeriod);
2514        (void) fprintf(vis_stdout, "# INV by PURESAT: data may be corrupted.\n");
2515        alarm(0);
2516        return 1;
2517      }
2518    }
2519    PureSat_CheckInvariant(network,invarArray,
2520                           (int)options->verbosityLevel,
2521                           options->dbgLevel,McOptionsReadDebugFile(options),
2522                           McOptionsReadPrintInputs(options),options->incre,
2523                           options->sss, options->flatIP, options->IPspeed);
2524    McOptionsFree(options);
2525    return 0;
2526  }
2527  guideFile =  McOptionsReadGuideFile(options);
2528
2529  if(guideFile != NIL(FILE) ){
2530    hintsArray = Mc_ReadHints(guideFile);
2531    fclose(guideFile); guideFile = NIL(FILE);
2532    if( hintsArray == NIL(array_t) ){
2533      McOptionsFree(options);
2534      return 1;
2535    }
2536  } /* if guided search */
2537
2538  if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
2539     Img_UserSpecifiedMethod() != Img_Monolithic_c &&
2540     Img_UserSpecifiedMethod() != Img_Mlp_c &&
2541     guideFile != NIL(FILE)){
2542    fprintf(vis_stdout,
2543 "** inv error: The Tfm and Hybrid image methods are incompatible with -g\n");
2544    McOptionsFree(options);
2545    return 1;
2546  }
2547
2548  if (dcLevel == McDcLevelArdc_c)
2549    ardc = 1;
2550  else
2551    ardc = 0;
2552
2553  /* obtain the fsm and mdd manager */
2554  totalFsm = Fsm_NetworkReadOrCreateFsm(network);
2555  if (totalFsm == NIL(Fsm_Fsm_t)) {
2556    fprintf(vis_stderr, "%s\n", error_string());
2557    error_init();
2558    McOptionsFree(options);
2559    return 1;
2560  }
2561
2562  systemVarBddIdTable = 0;
2563  systemFile = McOptionsReadSystemFile(options);
2564  if(systemFile != NIL(FILE) ){
2565    systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
2566    fclose(systemFile); systemFile = NIL(FILE);
2567    if(systemVarBddIdTable == (st_table *)-1 ){
2568      McOptionsFree(options);
2569      return 1;
2570    }
2571  } /* if FAFW */
2572
2573  if(options->FAFWFlag && systemVarBddIdTable == 0) {
2574    systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
2575  }
2576
2577  mddMgr = Fsm_FsmReadMddManager(totalFsm);
2578  tautology = mdd_one(mddMgr);
2579
2580  /* set time out */
2581  if (timeOutPeriod > 0) {
2582    /* Set the static variables used by the signal handler. */
2583    mcTimeOut = timeOutPeriod;
2584    alarmLapTime = util_cpu_ctime();
2585    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
2586    (void) alarm(timeOutPeriod);
2587    if (setjmp(timeOutEnv) > 0) {
2588      (void) fprintf(vis_stdout, "# INV: Checking Invariant: timeout occurred after %d seconds.\n", timeOutPeriod);
2589      (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
2590      alarm(0);
2591      return 1;
2592    }
2593  }
2594
2595  /* debugFlag = 1 -> need to store/compute onion shells, else not */
2596  debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);
2597
2598  /* use formula tree if reduce option and dont-care level is high */
2599  if ((McOptionsReadReduceFsm(options) == TRUE) &&
2600     (dcLevel != McDcLevelNone_c)) {
2601      McOptionsSetUseFormulaTree(options, TRUE);
2602  }
2603
2604  /* derive the normalized array of invariant formulas */
2605  if (McOptionsReadUseFormulaTree(options) == TRUE) {
2606    invarNormalFormulaArray =
2607      Ctlp_FormulaArrayConvertToExistentialFormTree(invarArray);
2608  } else {
2609    array_t *temp = Ctlp_FormulaArrayConvertToDAG( invarArray );
2610    array_free( invarArray );
2611    invarArray = temp;
2612    invarNormalFormulaArray = Ctlp_FormulaDAGConvertToExistentialFormDAG(
2613      invarArray );
2614  }
2615
2616  if (array_n(invarNormalFormulaArray) == 0) {
2617    array_free(invarNormalFormulaArray);
2618    Ctlp_FormulaArrayFree(invarArray);
2619    mdd_free(tautology);
2620    return 1;
2621  }
2622  fsmArray = array_alloc(Fsm_Fsm_t *, 0);
2623  sortedFormulaArray = SortFormulasByFsm(totalFsm, invarNormalFormulaArray,
2624                                         fsmArray, options);
2625  if (sortedFormulaArray == NIL(array_t)) {
2626    array_free(invarNormalFormulaArray);
2627    Ctlp_FormulaArrayFree(invarArray);
2628    mdd_free(tautology);
2629    return 1;
2630  }
2631  assert(array_n(fsmArray) == array_n(sortedFormulaArray));
2632
2633  careSetArray = array_alloc(mdd_t *, 0);
2634
2635  /* main loop for array of array of formulas. Each of the latter
2636     arrays corresponds to one reduced fsm. */
2637  arrayForEachItem(array_t *, sortedFormulaArray, i, formulas) {
2638    int *resultArray;
2639    int fail;
2640    /* initialize pass, fail array */
2641    resultArray = ALLOC(int, array_n(formulas));
2642    for (j = 0; j < array_n(formulas); j++) {
2643      resultArray[j] = 1;
2644    }
2645    /* get reduced fsm for this set of formulas */
2646    modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, i);
2647
2648    /* evaluate hints for this reduced fsm, stop if the hints contain variables
2649     * outside this model FSM.
2650     */
2651    if (hintsArray != NIL(Ctlp_FormulaArray_t)) {
2652      int k;
2653      hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
2654      if( hintsStatesArray == NIL(array_t)) { /* something wrong, clean up */
2655        int l;
2656        fprintf(vis_stdout, "Hints dont match the reduced FSM for this set of invariants.\n");
2657        fprintf(vis_stdout, "Continuing with the next set of invariants\n");
2658        for (k = i; k < array_n(sortedFormulaArray); k++) {
2659          formulas = array_fetch(array_t *, sortedFormulaArray, k);
2660          arrayForEachItem(Ctlp_Formula_t *, formulas, l, invarFormula) {
2661            Ctlp_FormulaFree(invarFormula);
2662          }
2663          array_free(formulas);
2664          /* get reduced fsm for this set of formulas */
2665          modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, k);
2666          /* free the Fsm if it was reduced here */
2667          if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
2668        }
2669        array_free(careSetArray);
2670        array_free(fsmArray);
2671        array_free(sortedFormulaArray);
2672        array_free(invarNormalFormulaArray);
2673        (void) fprintf(vis_stdout, "\n");
2674
2675        Ctlp_FormulaArrayFree(invarArray);
2676        McOptionsFree(options);
2677        mdd_free(tautology);
2678        return 1;
2679      }
2680    }/* hints exist */
2681
2682    if(options->FAFWFlag > 1) {
2683      reachableStates = Fsm_FsmComputeReachableStates(
2684          modelFsm, 0, verbosity , 0, 0, 1, 0, 0,
2685          approxFlag, ardc, 0, 0, (verbosity > 1),
2686          hintsStatesArray);
2687      mdd_free(reachableStates);
2688    }
2689
2690
2691    invarStatesArray = array_alloc(mdd_t *, 0);
2692    array_insert(mdd_t *, careSetArray, 0, tautology);
2693    arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
2694      /* compute the set of states represented by the invariant. */
2695      invarFormulaStates =
2696        Mc_FsmEvaluateFormula(modelFsm, invarFormula, tautology,
2697                              NIL(Fsm_Fairness_t), careSetArray,
2698                              MC_NO_EARLY_TERMINATION,
2699                              NIL(Fsm_HintsArray_t), Mc_None_c,
2700                              verbosity, dcLevel, buildOnionRings,
2701                              McGSH_EL_c);
2702
2703      array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
2704    }
2705
2706    printStep = (verbosity == McVerbosityMax_c) && (totalFsm == modelFsm);
2707    /* main loop to check a set of invariants. */
2708    do {
2709      boolean compute = FALSE;
2710      /* check if the computed reachable set in the total FSM already violates an invariant. */
2711      compute = TestInvariantsInTotalFsm(totalFsm, invarStatesArray, (debugFlag ||
2712                                                         buildOnionRings));
2713
2714      /* compute reachable set or until early failure */
2715      if (compute)
2716        reachableStates = Fsm_FsmComputeReachableStates(
2717          modelFsm, 0, verbosity , 0, 0, (debugFlag || buildOnionRings), 0, 0,
2718          approxFlag, ardc, 0, invarStatesArray, (verbosity > 1),
2719          hintsStatesArray);
2720      else if (debugFlag || buildOnionRings) {
2721        (void)Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
2722      } else {
2723        reachableStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(totalFsm));
2724      }
2725
2726      ardc = 0; /* once ardc is applied, we don't need it again. */
2727      /* updates result array and sets fail if any formula failed.*/
2728      fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
2729      mdd_free(reachableStates);
2730      someLeft = 0;
2731      if (fail) {
2732        /* some invariant failed */
2733        if (debugFlag) {
2734          assert (approxFlag != Fsm_Rch_Oa_c);
2735          Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
2736          Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
2737          InvarPrintDebugInformation(modelFsm, formulas, invarStatesArray,
2738                                     resultArray, options, hintsStatesArray);
2739          Fsm_FsmSetFAFWFlag(modelFsm, 0);
2740          Fsm_FsmSetSystemVariableFAFW(modelFsm, 0);
2741        } else if (approxFlag == Fsm_Rch_Oa_c) {
2742          assert(!buildOnionRings);
2743          /* May be a false negative */
2744          /* undo failed results in the result array, report passed formulae */
2745          arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
2746            if (invarFormulaStates == NIL(mdd_t)) continue;
2747            /* print all formulae that are known to have passed */
2748            if (resultArray[j] == 1) {
2749              mdd_free(invarFormulaStates);
2750              array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
2751              (void) fprintf(vis_stdout, "# INV: Early detection - formula passed --- ");
2752              invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
2753              Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
2754              fprintf(vis_stdout, "\n");
2755            } else resultArray[j] = 1;
2756          }
2757          fprintf(vis_stdout, "# INV: Invariant violated by over-approximated reachable states\n");
2758          fprintf(vis_stdout, "# INV: Switching to BFS (exact computation) to resolve false negatives\n");
2759          /* compute reachable set or until early failure */
2760          reachableStates = Fsm_FsmComputeReachableStates(
2761            modelFsm, 0, verbosity , 0, 0, 0, 0, 0, Fsm_Rch_Bfs_c, ardc, 0,
2762            invarStatesArray, (verbosity > 1), hintsStatesArray);
2763          /* either invariant has failed or all reachable states are computed */
2764          /* updates result array */
2765          fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
2766          mdd_free(reachableStates);
2767        }
2768        /* remove the failed invariants from the invariant list. */
2769        if (fail) {
2770          arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
2771            if (invarFormulaStates == NIL(mdd_t)) continue;
2772            /* free the failed invariant mdds */
2773            if (resultArray[j] == 0) {
2774              mdd_free(invarFormulaStates);
2775              array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
2776              if (!debugFlag) {
2777                (void) fprintf(vis_stdout, "# INV: Early detection - formula failed --- ");
2778                invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
2779                Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
2780                fprintf(vis_stdout, "\n");
2781              }
2782            } else {
2783              someLeft = 1;
2784            }
2785          }
2786        }
2787      } /* end of recomputation dur to over approximate computation */
2788    } while (someLeft);
2789
2790    arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
2791      if (invarFormulaStates == NIL(mdd_t)) continue;
2792      /* free the passed invariant mdds */
2793      mdd_free(invarFormulaStates);
2794    }
2795    array_free(invarStatesArray);
2796    if (printStep) {
2797      finalTime = util_cpu_time();
2798      Fsm_FsmReachabilityPrintResults(modelFsm,finalTime-initTime ,approxFlag);
2799    }
2800    /* free the Fsm if it was reduced here */
2801    if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
2802
2803
2804    PrintInvPassFail(formulas, resultArray);
2805
2806
2807    arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
2808      Ctlp_FormulaFree(invarFormula);
2809    }
2810    array_free(formulas);
2811    FREE(resultArray);
2812  } /* end of processing the sorted array of array of invariants */
2813
2814  if(hintsStatesArray != NIL(array_t))
2815    mdd_array_free(hintsStatesArray);
2816  if(hintsArray)
2817    Ctlp_FormulaArrayFree(hintsArray);
2818  array_free(careSetArray);
2819  array_free(fsmArray);
2820  array_free(sortedFormulaArray);
2821  array_free(invarNormalFormulaArray);
2822  (void) fprintf(vis_stdout, "\n");
2823
2824  if (options->FAFWFlag) {
2825    st_free_table(systemVarBddIdTable);
2826  }
2827
2828  Ctlp_FormulaArrayFree(invarArray);
2829  McOptionsFree(options);
2830  mdd_free(tautology);
2831
2832  alarm(0);
2833  return 0;
2834}
2835
2836
2837/**Function********************************************************************
2838
2839  Synopsis    [Parse command line options for invar.]
2840
2841  SideEffects []
2842
2843******************************************************************************/
2844static McOptions_t *
2845ParseInvarOptions(
2846  int argc,
2847  char **argv)
2848{
2849  unsigned int i;
2850  int c;
2851  boolean useMore = FALSE;
2852  boolean reduceFsm = FALSE;
2853  boolean printInputs = FALSE;
2854  boolean useFormulaTree = FALSE;
2855  FILE *inputFp=NIL(FILE);
2856  FILE *debugOut=NIL(FILE);
2857  char *debugOutName=NIL(char);
2858  McDbgLevel dbgLevel = McDbgLevelNone_c;
2859  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
2860  int timeOutPeriod = 0;
2861  McOptions_t *options = McOptionsAlloc();
2862  int approxFlag = 0, ardc = 0, shellFlag = 0;
2863  Fsm_RchType_t rchType;
2864  FILE *guideFile;
2865  FILE *systemFile = NIL(FILE);
2866  boolean FAFWFlag = FALSE;
2867  boolean GFAFWFlag = FALSE;
2868  char *guideFileName = NIL(char);
2869  char *variablesForSystem = NIL(char);
2870  int incre, speed;
2871  /* int sss; */
2872
2873  /*
2874   * Parse command line options.
2875   */
2876
2877  util_getopt_reset();
2878  while ((c = util_getopt(argc, argv, "ifcrt:g:hmv:d:A:DO:Ww:I:SPs:")) != EOF) {
2879    switch(c) {
2880      case 'g':
2881        guideFileName = util_strsav(util_optarg);
2882        break;
2883      case 'h':
2884        goto usage;
2885      case 't':
2886        timeOutPeriod = atoi(util_optarg);
2887        break;
2888      case 'v':
2889        for (i = 0; i < strlen(util_optarg); i++) {
2890          if (!isdigit((int)util_optarg[i])) {
2891            goto usage;
2892          }
2893        }
2894        verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
2895        break;
2896      case 'd':
2897        for (i = 0; i < strlen(util_optarg); i++) {
2898          if (!isdigit((int)util_optarg[i])) {
2899            goto usage;
2900          }
2901        }
2902        dbgLevel = (McDbgLevel) atoi(util_optarg);
2903        break;
2904      case 'f':
2905        shellFlag = 1;
2906        break;
2907      case 'r' :
2908        reduceFsm = TRUE;
2909        break;
2910      case 'm':
2911        useMore = TRUE;
2912        break;
2913      case 'i' :
2914        printInputs = TRUE;
2915        break;
2916      case 'c' :
2917        useFormulaTree = TRUE;
2918        break;
2919      case 'A':
2920        approxFlag = atoi(util_optarg);
2921        if ((approxFlag > 4) || (approxFlag < 0)) {
2922            goto usage;
2923        }
2924        break;
2925      case 'D':
2926        ardc = 1;
2927        break;
2928      case 'O':
2929        debugOutName = util_strsav(util_optarg);
2930        break;
2931      case 'w':
2932        variablesForSystem = util_strsav(util_optarg);
2933      case 'W':
2934        FAFWFlag = 1;
2935        break;
2936      case 'G':
2937        GFAFWFlag = 1;
2938        break;
2939      case 'I':
2940        incre = atoi(util_optarg);
2941        options->incre = (incre==0)? FALSE:TRUE;
2942        break;
2943      case 'S':
2944        /*sss = atoi(util_optarg);*/
2945        /*options->sss = (sss==0)? FALSE:TRUE;*/
2946        options->sss = TRUE;
2947        break;
2948      case 'P':
2949        options->flatIP = TRUE;
2950        break;
2951      case 's':
2952        speed = atoi(util_optarg);
2953        options->IPspeed = speed;
2954        break;
2955      default:
2956        goto usage;
2957    }
2958  }
2959
2960  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
2961    fprintf(vis_stderr, "** inv warning : -w and -W options are ignored without -d option\n");
2962  }
2963
2964  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
2965    fprintf(vis_stderr, "** inv warning : -i is recommended with -w or -W option\n");
2966  }
2967
2968  if(FAFWFlag) {
2969    if (bdd_get_package_name() != CUDD) {
2970      fprintf(vis_stderr, "** inv warning : -w and -W option is only available with CUDD\n");
2971      FAFWFlag = 0;
2972      FREE(variablesForSystem);
2973      variablesForSystem = NIL(char);
2974    }
2975  }
2976
2977
2978  /* translate approx flag */
2979  switch(approxFlag) {
2980  case 0: rchType = Fsm_Rch_Bfs_c; break;
2981  case 1: rchType = Fsm_Rch_Hd_c; break;
2982  case 2: rchType = Fsm_Rch_Oa_c; break;
2983  case 3: rchType = Fsm_Rch_Grab_c; break;
2984  case 4: rchType = Fsm_Rch_PureSat_c; break;
2985  default: rchType = Fsm_Rch_Default_c; break;
2986  }
2987
2988  if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
2989    fprintf(vis_stderr, "** inv error: check_invariant with -A 1 option is currently supported by only CUDD.\n");
2990    return NIL(McOptions_t);
2991  }
2992
2993  if (rchType == Fsm_Rch_Oa_c) {
2994    if (dbgLevel > 0) {
2995      fprintf(vis_stdout, "Over approximation and debug level 1 are incompatible\n");
2996      fprintf(vis_stdout, "Read check_invariant help page\n");
2997      goto usage;
2998    } else if (shellFlag == 1) {
2999      fprintf(vis_stdout, "Over approximation and shell flag are incompatible\n");
3000      fprintf(vis_stdout, "Read check_invariant help page\n");
3001      goto usage;
3002    }
3003  }
3004
3005  if (rchType == Fsm_Rch_Grab_c) {
3006    if (guideFileName != NIL(char)) {
3007      fprintf(vis_stdout, "Abstraction refinement Grab and guided search are incompatible\n");
3008      fprintf(vis_stdout, "Read check_invariant help page\n");
3009      goto usage;
3010    }
3011  }
3012
3013  if (rchType == Fsm_Rch_PureSat_c) {
3014    if (guideFileName != NIL(char)) {
3015      fprintf(vis_stdout, "Abstraction refinement PureSat and guided search are incompatible\n");
3016      fprintf(vis_stdout, "Read check_invariant help page\n");
3017      goto usage;
3018    }
3019  }
3020
3021  if (guideFileName != NIL(char)) {
3022    guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
3023    FREE(guideFileName);
3024    if (guideFile == NIL(FILE)) {
3025      McOptionsFree(options);
3026      return NIL(McOptions_t);
3027    }
3028    McOptionsSetGuideFile(options, guideFile);
3029  }
3030
3031  /*
3032   * Open the ctl file.
3033   */
3034  if (argc - util_optind == 0) {
3035    (void) fprintf(vis_stderr, "** inv error: file containing invariant formulas not provided\n");
3036    goto usage;
3037  }
3038  else if (argc - util_optind > 1) {
3039    (void) fprintf(vis_stderr, "** inv error: too many arguments\n");
3040    goto usage;
3041  }
3042
3043  McOptionsSetUseMore(options, useMore);
3044  McOptionsSetReduceFsm(options, reduceFsm);
3045  McOptionsSetPrintInputs(options, printInputs);
3046  McOptionsSetUseFormulaTree(options, useFormulaTree);
3047  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
3048  McOptionsSetInvarApproxFlag(options, rchType);
3049  if (ardc)
3050    McOptionsSetDcLevel(options, McDcLevelArdc_c);
3051  else
3052    McOptionsSetDcLevel(options, McDcLevelNone_c);
3053  McOptionsSetInvarOnionRingsFlag(options, shellFlag);
3054  McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
3055
3056  inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
3057  if (inputFp == NIL(FILE)) {
3058    McOptionsFree(options);
3059    return NIL(McOptions_t);
3060  }
3061  McOptionsSetCtlFile(options, inputFp);
3062
3063  if (debugOutName != NIL(char)) {
3064    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
3065    if (debugOut == NIL(FILE)) {
3066      McOptionsFree(options);
3067      return NIL(McOptions_t);
3068    }
3069  }
3070  McOptionsSetDebugFile(options, debugOut);
3071
3072  if ((verbosityLevel != McVerbosityNone_c) &&
3073       (verbosityLevel != McVerbosityLittle_c) &&
3074       (verbosityLevel != McVerbositySome_c) &&
3075       (verbosityLevel != McVerbosityMax_c)) {
3076    goto usage;
3077  }
3078  else {
3079    McOptionsSetVerbosityLevel(options, verbosityLevel);
3080  }
3081
3082  if ((dbgLevel != McDbgLevelNone_c) &&
3083       (dbgLevel != McDbgLevelMin_c)) {
3084    if(((rchType == Fsm_Rch_Grab_c) && (dbgLevel == McDbgLevelMinVerbose_c)))
3085    {
3086      McOptionsSetDbgLevel(options, dbgLevel);
3087    }
3088    else
3089    {
3090      if((rchType == Fsm_Rch_PureSat_c) && (options->flatIP == TRUE) && (dbgLevel == McDbgLevelMinVerbose_c))
3091      {
3092        McOptionsSetDbgLevel(options, dbgLevel);
3093      }
3094      else
3095      {
3096        if((rchType == Fsm_Rch_Bfs_c) && (dbgLevel == McDbgLevelMinVerbose_c))
3097        {
3098          McOptionsSetDbgLevel(options, dbgLevel);
3099        }
3100        else
3101        {
3102          goto usage;
3103        }
3104      }
3105    }
3106  }
3107  else {
3108    McOptionsSetDbgLevel(options, dbgLevel);
3109  }
3110
3111  if (variablesForSystem != NIL(char)) {
3112    systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
3113    if (systemFile == NIL(FILE)) {
3114      fprintf(vis_stderr, "** inv error: cannot open system variables file for FAFW %s.\n",
3115              variablesForSystem);
3116      FREE(variablesForSystem);
3117      variablesForSystem = NIL(char);
3118      McOptionsFree(options);
3119      return NIL(McOptions_t);
3120    }
3121    FREE(variablesForSystem);
3122    variablesForSystem = NIL(char);
3123  }
3124  McOptionsSetVariablesForSystem(options, systemFile);
3125
3126
3127  return options;
3128
3129  usage:
3130  (void) fprintf(vis_stderr, "usage: check_invariant [-c][-d dbg_level][-f][-g <hintfile>][-h][-i][-m][-r][-v verbosity_level][-t time_out][-A <number>][-D dc_level] [-O <dbg_out>] <invar_file>\n");
3131  (void) fprintf(vis_stderr, "    -c  avoid sub-formula sharing between formulae\n");
3132  (void) fprintf(vis_stderr, "    -d  <dbg_level>");
3133  (void) fprintf(vis_stderr, "        dbg_level = 0 => no debug output (Default)\n");
3134  (void) fprintf(vis_stderr, "        dbg_level = 1 => print debug trace. (available for all options)\n ");
3135  (void) fprintf(vis_stderr, "        dbg_level = 2 => print debug trace in Aiger format. (available for -A0, -A3, -A4 and -A4 -P)\n");
3136  (void) fprintf(vis_stderr, "    -f \tStore the onion rings at each step.\n");
3137  (void) fprintf(vis_stderr, "    -g <hint_file> \tSpecify file for guided search.\n");
3138  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
3139  (void) fprintf(vis_stderr, "    -m  pipe debugger output through UNIX utility more\n");
3140  (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to invariant being checked\n");
3141  (void) fprintf(vis_stderr, "    -t <period> Time out period.\n");
3142  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
3143  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
3144  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
3145  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
3146  (void) fprintf(vis_stderr, "    -A  <number> Use Different types of reachability analysis\n");
3147  (void) fprintf(vis_stderr, "            0 (default) - BFS method.\n");
3148  (void) fprintf(vis_stderr, "            1 - HD method.\n");
3149  (void) fprintf(vis_stderr, "            2 - Over-approximation.\n");
3150  (void) fprintf(vis_stderr, "            3 - Abstraction refinement GRAB.\n");
3151  (void) fprintf(vis_stderr, "    -D  minimize transition relation with ARDCs\n");
3152  (void) fprintf(vis_stderr, "    -O <dbg_out>\n");
3153  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
3154  (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
3155  (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
3156  (void) fprintf(vis_stderr, "    -w <node file> \tSpecify variables controlled by system.\n");
3157  (void) fprintf(vis_stderr, "    <invar_file> The input file containing invariants to be checked.\n");
3158  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
3159  (void) fprintf(vis_stderr, "    -I \tSwitch for Incremental SAT solver in PureSAT method abstraction refinement\n");
3160  McOptionsFree(options);
3161
3162  return NIL(McOptions_t);
3163}
3164
3165/**Function********************************************************************
3166
3167  Synopsis    [Handle function for timeout.]
3168
3169  Description [This function is called when the time out occurs.
3170  Since alarm is set with an elapsed time, this function checks if the
3171  CPU time corresponds to the timeout of the command.  If not, it
3172  reprograms the alarm to fire again later.]
3173
3174  SideEffects []
3175
3176******************************************************************************/
3177static void
3178TimeOutHandle(void)
3179{
3180  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
3181
3182  if (seconds < mcTimeOut) {
3183    unsigned slack = (unsigned) (mcTimeOut - seconds);
3184    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
3185    (void) alarm(slack);
3186  } else {
3187    longjmp(timeOutEnv, 1);
3188  }
3189} /* TimeOutHandle */
3190
3191
3192/**Function********************************************************************
3193
3194  Synopsis [Check whether the reachable states violate the array of
3195  invariants.]
3196
3197  Description [Check whether the reachable states violate the array of
3198  invariants. Return 1 if any formula failed. Update the result
3199  array. Entry 0 implies fail, 1 implies pass.]
3200
3201  SideEffects []
3202
3203******************************************************************************/
3204static int
3205UpdateResultArray(mdd_t *reachableStates,
3206                  array_t *invarStatesArray,
3207                  int *resultArray)
3208{
3209  int i;
3210  mdd_t *invariant;
3211  int fail = 0;
3212  arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
3213    if (invariant == NIL(mdd_t)) continue;
3214    if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
3215      fail = 1;
3216      resultArray[i] = 0;
3217    }
3218  }
3219  return fail;
3220} /* end of UpdateResultArray */
3221
3222
3223/**Function********************************************************************
3224
3225  Synopsis [Prints whether the set of invariants passed or failed]
3226
3227  Description [Prints whether the set of invariants passed or failed.]
3228
3229  SideEffects []
3230
3231******************************************************************************/
3232static void
3233PrintInvPassFail(array_t *invarFormulaArray,
3234                 int *resultArray)
3235{
3236  int i;
3237  Ctlp_Formula_t *formula;
3238  fprintf(vis_stdout, "\n# INV: Summary of invariant pass/fail\n");
3239  arrayForEachItem(Ctlp_Formula_t *, invarFormulaArray, i, formula) {
3240    if (resultArray[i]) {
3241      (void) fprintf(vis_stdout, "# INV: formula passed --- ");
3242      Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
3243      fprintf(vis_stdout, "\n");
3244    } else {
3245      (void) fprintf(vis_stdout, "# INV: formula failed --- ");
3246      Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
3247      fprintf(vis_stdout, "\n");
3248    }
3249  }
3250  return;
3251} /* end of PrintInvPassFail */
Note: See TracBrowser for help on using the repository browser.