source: vis_dev/vis-2.3/src/abs/absCmd.c @ 14

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

vis2.3
File size: 26.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [absCmd.c]
4
5  PackageName [abs]
6
7  Synopsis    [Encapsulation for the incremental_ctl_verification command.]
8
9  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "absInt.h"
18
19static char rcsid[] UNUSED = "$Id: absCmd.c,v 1.37 2002/09/08 22:13:50 fabio Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Type declarations                                                         */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Structure declarations                                                    */
27/*---------------------------------------------------------------------------*/
28
29/*---------------------------------------------------------------------------*/
30/* Macro declarations                                                        */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Variable declarations                                                     */
35/*---------------------------------------------------------------------------*/
36static jmp_buf timeOutEnv;
37static int absTimeOut;
38static long alarmLap;
39
40/**AutomaticStart*************************************************************/
41
42/*---------------------------------------------------------------------------*/
43/* Static function prototypes                                                */
44/*---------------------------------------------------------------------------*/
45
46static int CommandAbsCtl(Hrc_Manager_t **hmgr, int argc, char **argv);
47static AbsOptions_t * ParseAbsCtlOptions(int argc, char **argv);
48static void TimeOutHandle(int sigType);
49
50/**AutomaticEnd***************************************************************/
51
52
53/*---------------------------------------------------------------------------*/
54/* Definition of exported functions                                          */
55/*---------------------------------------------------------------------------*/
56
57
58/**Function********************************************************************
59
60  Synopsis [Initialize abs package]
61
62  SideEffects []
63
64******************************************************************************/
65void
66Abs_Init(void)
67{
68  Cmd_CommandAdd("incremental_ctl_verification", CommandAbsCtl, 0);
69}
70
71
72/**Function********************************************************************
73
74  Synopsis [End abs package]
75
76  SideEffects []
77
78******************************************************************************/
79void
80Abs_End(void)
81{
82}
83
84
85/*---------------------------------------------------------------------------*/
86/* Definition of internal functions                                          */
87/*---------------------------------------------------------------------------*/
88
89/*---------------------------------------------------------------------------*/
90/* Definition of static functions                                            */
91/*---------------------------------------------------------------------------*/
92/**Function********************************************************************
93
94  Synopsis [Encapsulation of the incremental_ctl_verification command.]
95
96  Description [The function starts by parsing the options. After that it checks
97  for the network structure. The ctl formulas are read and check for
98  correctness. Once the formulas have been read, they need to be translated
99  from the CTL representation to the operational graph representation required
100  for the incremental algorithm. The function AbsCtlFormulaArrayTranslate
101  performs this task. After all these points have been cleared, the timeout is
102  programmed and the verification process starts.
103 
104  Once the result has been obtained, the function prints the result as well as
105  some execution statistics, de-allocates all the required data structures and
106  returns.]
107
108  SideEffects        []
109
110  CommandName        [incremental_ctl_verification]       
111
112  CommandSynopsis [Verify a set of CTL formulas by means of an incremental
113  model checking algorithm.]
114
115  CommandArguments [\[-D &lt;number&gt;\] \[-e\] \[-h\]  \[-n\] \
116  \[-s\] \[-t &lt;seconds&gt;\] \[-v &lt;number&gt;\] \[-V &lt;number&gt;\]
117  \[-x\] &lt;ctlfile&gt;]]
118
119  CommandDescription [
120  Like model_check, incremental_ctl_verification verifies a set of CTL
121  formulas.  It uses a system of abstraction and incremental
122  refinement
123  that works for all of (fair)CTL, using over and underapproximations as
124  appropriate. See \[1,2\] for details.
125 
126  <p> Incremental_ctl_verification (also known as Abs or Trasgo)
127  works especially well on large systems on which mc is too slow or
128  runs out of memory. 
129  Unlike amc, it can handle full CTL, not just the universal or
130  existential subsets of it. Also, fairness is supported with this
131  command, although it tends to be inefficient. 
132  Support for the mu-calculus is not yet implemented.
133
134  <p>Before using incremental_ctl_verification, a flattened hierarchy
135  should be present. See `help init`. Using dynamic variable reordering
136  may be beneficial on large systems. See `help
137  dynamic_var_ordering`.
138
139  <p>Fairness constraints can be applied using
140  `read_fairness', as with mc.  When using incremental verification
141  with fairness, there is no check for unfair initial states. Please
142  be aware that if there are no fair initial states, all formulas
143  starting with "A" will be trivially true. Mc will tell you whether
144  you have fair initial states.
145
146  <p>A typical use would be
147  <br>incremental_ctl_verification -D2 &lt;ctl_file&gt;
148
149  <p>For every formula, incremental verification will report whether
150  it is valid or invalid, or it returns an inconclusive result. A formula is
151  valid iff it holds for all initial states. An error trace is not provided.
152
153  For the people who are used to mc: The -r option is not supported,
154  incremental verification always reduces the fsm with respect to
155  individual formulas. The -c option is not supported either. There is
156  no sharing of subformulas between different formulas.
157
158  <p>Command options:<p>
159
160  <dl>
161
162  <dt> -D &lt;number&gt;
163  <dd> Specify extent to which don't cares are used to simplify the
164  MDDs.
165  <ul>
166  <li>0: No Don't Cares used.
167  <li>1: Use reachability information to compute the don't-care
168     set. Reachability is performed by formula. This is different from
169     mc, where reachability is performed only once.
170  <li>2: Use reachability information, and minimize the transition relation
171     with respect to the `frontier set' (aggresive minimization).
172  </ul>
173  The equivalent of mc -D3 is not implemented.
174
175  <dt> -e
176  <dd>Compute the set of fair states (those satisfying the formula EGfair TRUE)
177  before the verification process and use the result as care set. In certain
178  cases this will speed up computation when fairness constraints are
179  present. In other cases it will slow it down.
180
181  <dt> -h
182  <dd> Print the command usage.
183
184  <dt> -n
185  <dd> Try to prove the negation of every formula. In some cases it
186  may be easier to prove the negation of a formula than the formula
187  itself. For systems with only one initial state, a formula is true
188  iff its negation is false. Note that for systems with multiple
189  initial states a formula and its negation can both be false.
190
191  <dt> -s
192  <dd> Print a summary of statistics after the verification.
193
194  <dt> -t &lt;secs&gt;
195  <dd> Time in seconds allowed to spend in the verification.  The default is
196  infinity.
197
198  <dt> -v &lt;number&gt;
199  <dd>Specify verbosity level. Use 0 for no feedback (default), 1
200  for more and 2 for maximum feedback. This option can not be used in
201  conjunction with -V.
202
203  <dt> -V &lt;number&gt;
204  <dd> Mask specifying type of information to be printed out while
205  verifying the formulas. This allows for a finer control than -v. -V
206  and -v cannot be used simultaneously.
207  The mask is given as a binary number, by taking the
208  logical or of the following binary values. One does not have to
209  convert these numbers to decimal.<p>
210 
211                        1  number of primary inputs and flip-flops <p>
212                       10  labeled operational graph of the formulas <p>
213                      100  cpu-time for the computation in each vertex <p>
214                     1000  cubes of the function sat for each vertex <p>
215                    10000  cubes of the function goalSet for each vertex <p>
216                   100000  vertex data structure contents after evaluation <p>
217                  1000000  cubes in the care set for every evaluation <p>
218                 10000000  size of care set for every evaluation <p>
219                100000000  number of states that satisfy every sub-formula <p>
220               1000000000  number of overall reachable states <p>
221              10000000000  cubes for every iteration of a fixed point <p>
222             100000000000  size of the BDD in each iteration in a fix-point <p>
223            1000000000000  labeled operational graph in dot format <p>
224           10000000000000  number of envelope states <p>
225          100000000000000  number of states to be refined <p>
226         1000000000000000  size of the refinement operands <p>
227        10000000000000000  cubes of the refinement operands <p>
228       100000000000000000  Number of latches before and after simplification <p>
229      1000000000000000000  report partial progress (i.e. reach, EG(true),...)<p>
230     10000000000000000000  Begin/End refinement process <p>
231    100000000000000000000  Size of goal set <p>
232   1000000000000000000000  cubes of the goal set <p>
233  10000000000000000000000  Contents of vertex after refinement <p>
234
235  <dt> -x
236  <dd> Perform the verification exactly. No approximation is done.
237
238  <dt> &lt;ctlfile&gt;
239  <dd> File containing the CTL formulas to be verified.
240
241  <dt> Related "set" options: <p>
242  <dt> ctl_change_bracket &lt;yes/no&gt;
243  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
244  therefore CTL parser does the same thing. However, in some cases a user
245  does not want to change node names in CTL parsing. Then, use this set
246  option by giving "no". Default is "yes".
247  <p>
248
249  <dt> See also commands : model_check, incremental_ctl_verification <p>
250
251  </dl>
252
253  <p>1. A. Pardo and G. Hachtel. Automatic abstraction techniques for
254  propositional mu-calculus model checking. In <I>9th Conference on
255  Computer Aided Verification (CAV'97)</I>. Springer-Verlag. Pages
256  12-23, 1997.
257  <p>2. A. Pardo and G. Hachtel. Incremental CTL model checking using BDD
258  subsetting.  In <I>35th Design Automation Conference
259  (DAC'98)</I>. pages 457-462, 1998.   
260  ]
261
262******************************************************************************/
263static int
264CommandAbsCtl(
265  Hrc_Manager_t **hmgr,
266  int argc,
267  char **argv)
268{
269  AbsVerificationResult_t formulaResult;
270  Abs_VerificationInfo_t  *absInfo;
271  AbsVertexInfo_t         *formulaPtr;
272  Ctlp_Formula_t          *ctlFormula;
273  AbsOptions_t            *options;
274  Ntk_Network_t           *network;
275  array_t                 *ctlArray;
276  array_t                 *existCtlArray;
277  array_t                 *fairArray;
278  array_t                 *existFairArray;
279  array_t                 *graphArray;
280  array_t                 *resultArray;
281  FILE                    *formulaFile;
282  boolean                 correctSemantics;
283  Fsm_Fsm_t               *fsm;
284  Fsm_Fairness_t          *fairness;
285  long                    cpuTime;
286  int                     status;
287  int                     i;
288  int                     numConjuncts;
289
290  /* Initialize some variables */
291  graphArray = NIL(array_t);
292  resultArray = NIL(array_t);
293  options = NIL(AbsOptions_t);
294  ctlArray = NIL(array_t);
295  existCtlArray = NIL(array_t);
296  fairArray = NIL(array_t);
297  existFairArray = NIL(array_t);
298  absInfo = NIL(Abs_VerificationInfo_t);
299
300  if (bdd_get_package_name() != CUDD) {
301    fprintf(vis_stderr, "** abs error : incremental_ctl_verification ");
302    fprintf(vis_stderr, "is currently supported by only CUDD.\n");
303    status = 1;
304    goto cleanup;
305  }
306
307  error_init();
308
309  /* Parse the options */
310  options = ParseAbsCtlOptions(argc, argv);
311
312  /* Check if there has been any error parsing the options */
313  if (!options) {
314    status = 1;
315    goto cleanup;
316  }
317
318  /* Obtain the network */
319  network = Ntk_HrcManagerReadCurrentNetwork( *hmgr );
320  if ( network == NIL( Ntk_Network_t)) {
321    (void) fprintf(vis_stdout, "%s\n", error_string());
322    error_init();
323    status = 1;
324    goto cleanup;
325  }
326
327  /* Open the file with the ctl formulas */
328  formulaFile = Cmd_FileOpen(AbsOptionsReadFileName(options), "r", 
329                             NIL(char *), 0);
330  if (formulaFile == NIL(FILE)) {
331    status = 1;
332    goto cleanup;
333  }
334
335  /* Parse the formulas and close the file */
336  ctlArray = Ctlp_FileParseFormulaArray(formulaFile);
337  fclose(formulaFile);
338
339  if (ctlArray == NIL(array_t)) {
340    (void) fprintf(vis_stderr, 
341                   "** abs error: Error while parsing CTL formulas\n");
342    status = 1;
343    goto cleanup;
344  }
345
346  /* Read the fairness constraints */
347  fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
348  if (fsm != NIL(Fsm_Fsm_t)){
349    fairness = Fsm_FsmReadFairnessConstraint(fsm);
350    if (fairness != NIL(Fsm_Fairness_t)){
351      fairArray = array_alloc(Ctlp_Formula_t *,0);
352      numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(fairness, 0);
353      for (i = 0; i < numConjuncts; i++) {
354        ctlFormula = Fsm_FairnessReadFinallyInfFormula(fairness, 0, i);
355        if ((Ctlp_FormulaReadType(ctlFormula) != Ctlp_TRUE_c) &&
356            (Ctlp_FormulaReadType(ctlFormula) != Ctlp_FALSE_c)){
357          array_insert_last(Ctlp_Formula_t *, fairArray, 
358                            Ctlp_FormulaDup(ctlFormula));
359        }
360      }
361      if (array_n(fairArray) == 0){
362        array_free(fairArray);
363        fairArray = NIL(array_t);
364      }
365    }
366  }
367
368  /* Verify that the formulas are semantically correct */
369  correctSemantics = TRUE;
370
371  /* Check the semantics of the temporal formulas */
372  arrayForEachItem(Ctlp_Formula_t *, ctlArray, i, ctlFormula) {
373    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
374      (void) fprintf(vis_stdout, 
375                 "** abs error: Inconsistency detected in formula number %d.\n",
376                     i);
377      (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
378      error_init();
379      correctSemantics = FALSE;
380    }
381  }
382
383  /* Check the fairness constraints */
384  if (fairArray != NIL(array_t)) {
385    arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlFormula) {
386      if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
387        (void) fprintf(vis_stdout, 
388                       "** abs error: Inconsistency detected in fairness ");
389        (void) fprintf(vis_stdout, "constraint number %d.\n", i);
390        (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
391        error_init();
392        correctSemantics = FALSE;
393      }
394    }
395  }
396
397  /* If there is any inconsistency, do not execute the command */
398  if (!correctSemantics) {
399    status = 1;
400    goto cleanup;
401  }
402
403  /* Replace XORs and EQs with equivalent subtrees. We insist on having
404   * only monotonic operators. */
405  Ctlp_FormulaArrayMakeMonotonic(ctlArray);
406  Ctlp_FormulaArrayMakeMonotonic(fairArray);
407
408  /* Translate the ctl formulas and fairness constraints to existential form */
409  existCtlArray = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
410  if (fairArray != NIL(array_t)) {
411    existFairArray = Ctlp_FormulaArrayConvertToExistentialFormTree(fairArray);
412  }
413
414  /* Compute the information related to the system being verified */
415  absInfo = Abs_VerificationComputeInfo(network);
416  if (absInfo == NIL(Abs_VerificationInfo_t)) {
417    (void) fprintf(vis_stdout, "** abs error: Error computing the information required ");
418    (void) fprintf(vis_stdout, "for verification.\n");
419    status = 1;
420    goto cleanup;
421  }
422
423  /* Store the options */
424  AbsVerificationInfoSetOptions(absInfo, options);
425
426  /* Translate the array of CTL formulas to operational graphs */
427  graphArray = AbsCtlFormulaArrayTranslate(absInfo, existCtlArray, 
428                                           existFairArray);
429
430  if (graphArray == NIL(array_t)) {
431    (void) fprintf(vis_stderr, 
432                   "** abs error: Error translating CTL formulas.\n");
433    (void) fprintf(vis_stderr, "** abs error: Aborting command.\n");
434    status = 1;
435    goto cleanup;
436  }
437
438  /* Program the timeOut if pertinent */
439  if (AbsOptionsReadTimeOut(options) > 0) {
440    /* Set the static variables */
441    absTimeOut = AbsOptionsReadTimeOut(options);
442    alarmLap = util_cpu_time();
443
444    /* Set the handler */
445    (void) signal(SIGALRM, TimeOutHandle);
446    (void) alarm(AbsOptionsReadTimeOut(options));
447   
448    /* Set the jump for the timeout */
449    if (setjmp(timeOutEnv) > 0) {
450      (void) fprintf(vis_stdout,
451                     "# ABS: Timeout occurred after %7.1f CPU seconds\n",
452                     (util_cpu_time() - alarmLap)/1000.0);
453      (void) fprintf(vis_stdout, "# ABS: data may be corrupted.\n");
454      alarm(0);
455      return 1;
456    }
457  }
458
459  /* Print the graph in DOT format */
460  if (AbsOptionsReadVerbosity(options) & ABS_VB_PRDOT) {
461      AbsVertexPrintDot(vis_stdout, graphArray);
462  }
463
464  /* Set the cpu-time lap */
465  cpuTime = util_cpu_time();
466
467  /* Verify every formula */
468  resultArray = AbsFormulaArrayVerify(absInfo, graphArray);
469
470  /* Print out the execution time*/
471  (void) fprintf(vis_stdout, "ABS: Total Verification Time: %7.1f secs\n",
472                 (util_cpu_time() - cpuTime)/1000.0);
473 
474  /* Print out the results */
475  /* RB changed this to take into account multiple initial states in negtd
476     formulas */
477  arrayForEachItem(AbsVerificationResult_t, resultArray, i, formulaResult) {
478    (void) fprintf(vis_stdout, "# ABS: formula ");
479    switch (formulaResult) {
480    case trueVerification_c:
481      (void) fprintf(vis_stdout, "passed --- ");
482      break;
483    case falseVerification_c:
484      (void) fprintf(vis_stdout, "failed --- ");
485      break;
486    case inconclusiveVerification_c:
487      (void) fprintf(vis_stdout, "undecided --- ");
488    }
489    if (AbsOptionsReadNegateFormula(options))
490      fprintf(vis_stdout, "NOT[ ");
491    Ctlp_FormulaPrint(vis_stdout, 
492                      array_fetch(Ctlp_Formula_t *, ctlArray, i));
493    if (AbsOptionsReadNegateFormula(options))
494      fprintf(vis_stdout, " ]\n");
495    else
496      fprintf(vis_stdout, "\n");
497  }
498 
499  /* Print the stats if selected by command line option */
500  if (AbsOptionsReadPrintStats(options)) {
501    int i;
502   
503    AbsStatsPrintReport(vis_stdout, AbsVerificationInfoReadStats(absInfo));
504   
505    (void) fprintf(vis_stdout, "# ABS: -- Command Line Options --\n");
506    (void) fprintf(vis_stdout, "# ABS: ");
507    for (i=0; i<argc; i++) {
508      (void) fprintf(vis_stdout, "%s ", argv[i]);
509    }
510    (void) fprintf(vis_stdout, "\n");
511  }
512 
513  /* Disconnect the alarm */
514  alarm(0);
515 
516  status = 0;
517 
518  /* Clean up the memory and return */
519  cleanup:
520  if (graphArray != NIL(array_t)) {
521    arrayForEachItem(AbsVertexInfo_t *, graphArray, i, formulaPtr) {
522      AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), formulaPtr,
523                    NIL(AbsVertexInfo_t));
524    }
525    array_free(graphArray);
526  }
527  if (resultArray != NIL(array_t)) {
528    array_free(resultArray);
529  }
530  if (options != NIL(AbsOptions_t)) {
531    AbsOptionsFree(options);
532  }
533  if (ctlArray != NIL(array_t)) {
534    Ctlp_FormulaArrayFree(ctlArray);
535  }
536  if (existCtlArray != NIL(array_t)) {
537    Ctlp_FormulaArrayFree(existCtlArray);
538  }
539  if (fairArray != NIL(array_t)) {
540    Ctlp_FormulaArrayFree(fairArray);
541  }
542  if (existFairArray != NIL(array_t)) {
543    Ctlp_FormulaArrayFree(existFairArray);
544  }
545  if (absInfo != NIL(Abs_VerificationInfo_t)) {
546    AbsVerificationInfoFree(absInfo);
547  }
548 
549  return status;
550} /* End of CommandAbsCtl */
551
552/**Function********************************************************************
553
554  Synopsis [Parses the options given to the incremental_ctl_verification command
555  and stores them into a structure.]
556
557  SideEffects        []
558
559  SeeAlso            [CommandAbsCtl]
560
561******************************************************************************/
562static AbsOptions_t *
563ParseAbsCtlOptions(
564  int argc,
565  char **argv)
566{
567  AbsOptions_t *result;
568  char *fileName;
569  boolean reachability;
570  boolean envelope;
571  boolean exact;
572  boolean printStats;
573  boolean minimizeIterate;
574  boolean negateFormula;
575  boolean partApprox;
576  boolean DFlag, eFlag, nFlag, pFlag, sFlag, tFlag, vFlag, xFlag;
577  long verbosity;
578  int intVerbosity;
579  int timeOut;
580  int dcValue;
581  int c;
582  unsigned int i;
583
584  /* Default Options */
585  DFlag = eFlag = nFlag = pFlag = sFlag = tFlag = FALSE;
586  vFlag = xFlag = FALSE;
587  reachability = FALSE;
588  envelope = FALSE;
589  exact = FALSE;
590  printStats = FALSE;
591  minimizeIterate = FALSE;
592  negateFormula = FALSE;
593  partApprox = FALSE;
594  verbosity = 0;
595  intVerbosity = 0;
596  timeOut = -1;
597  dcValue = 0;
598
599  util_getopt_reset();
600  while ((c = util_getopt(argc, argv, "D:ehnpst:v:V:x")) != EOF) {
601    switch(c) {
602      case 'D':
603        dcValue = atoi(util_optarg);
604        if (DFlag || (dcValue < 0) || (dcValue > 2)) {
605          goto usage;
606        }
607        if (dcValue > 0) {
608          reachability = TRUE;
609        }
610        if (dcValue > 1) {
611          minimizeIterate = TRUE;
612        }
613        DFlag = TRUE;
614        break;
615      case 'e':
616        if (eFlag) {
617          goto usage;
618        }
619        envelope = TRUE;
620        eFlag = TRUE;
621        break;
622      case 'h':
623        goto usage;
624      case 'n':
625        if (nFlag) {
626          goto usage;
627        }
628        negateFormula = TRUE;
629        nFlag = TRUE;
630        break;
631      case 'p':
632        if (pFlag) {
633          goto usage;
634        }
635        partApprox = TRUE;
636        pFlag = TRUE;
637        break;
638      case 's':
639        if (sFlag) {
640          goto usage;
641        }
642        printStats = TRUE;
643        sFlag = TRUE;
644        break;
645      case 't':
646        if (tFlag) {
647          goto usage;
648        }
649        timeOut = atoi(util_optarg);
650        tFlag = TRUE;
651        break;
652      case 'v':
653        if (vFlag) {
654          goto usage;
655        }
656        intVerbosity =  atoi(util_optarg);
657        if (intVerbosity == 1){
658          verbosity = 131849;
659        }else if (intVerbosity == 2){
660          verbosity = 8388607;
661        }else{
662          verbosity = 0;
663        }
664        vFlag = TRUE;
665        break;
666      case 'V':
667        if (vFlag) {
668          goto usage;
669        }
670        for(i=0;i<strlen(util_optarg)-1;i++){
671          if (util_optarg[i] != '0' && util_optarg[i] != '1'){
672             goto usage;
673          }
674        }
675        verbosity =  strtol(util_optarg, NIL(char *), 2);
676        vFlag = TRUE;
677        break;
678      case 'x':
679        if (xFlag) {
680          goto usage;
681        }
682        exact = TRUE;
683        xFlag = TRUE;
684        break;
685      default:
686        goto usage;
687    }
688  }
689
690  /* Check if there is still one parameter left */
691  if (argc - util_optind != 1) {
692    goto usage;
693  }
694
695  /* Obtain the filename from the end of the command line */
696  fileName = util_strsav(argv[util_optind]);
697 
698  /* Store the options  */
699  result = AbsOptionsInitialize();
700 
701  AbsOptionsSetVerbosity(result, verbosity);
702  AbsOptionsSetTimeOut(result, timeOut);
703  AbsOptionsSetReachability(result, reachability);
704  AbsOptionsSetEnvelope(result, envelope);
705  AbsOptionsSetFileName(result, fileName);
706  AbsOptionsSetExact(result, exact);
707  AbsOptionsSetPrintStats(result, printStats);
708  AbsOptionsSetMinimizeIterate(result, minimizeIterate);
709  AbsOptionsSetNegateFormula(result, negateFormula);
710  AbsOptionsSetPartApprox(result, partApprox);
711
712  return result;
713
714 usage:
715  fprintf(vis_stderr,"usage: incremental_ctl_verification [-D <number>] [-e] [-h] [-n] [-s]\n");
716  fprintf(vis_stderr,"[-t <seconds>] [-v <number>] [-V <number>] [-x] <ctlfile>\n");
717  fprintf(vis_stderr,"\n");
718  fprintf(vis_stderr,"Command options:\n");
719  fprintf(vis_stderr,"-D <number>\n");
720  fprintf(vis_stderr,"   Specify extent to which don't cares are used to simplify\n");
721  fprintf(vis_stderr,"   the MDDs.\n");
722  fprintf(vis_stderr,"   0: No Don't Cares used.\n");
723  fprintf(vis_stderr,"   1: Use reachability information to compute the don't-care\n");
724  fprintf(vis_stderr,"     set. Reachability is performed by formula. This is different from\n");
725  fprintf(vis_stderr,"     mc, where reachability is performed only once.\n");
726  fprintf(vis_stderr,"   2: Use reachability information, and minimize the transition relation\n");
727  fprintf(vis_stderr,"     with respect to the `frontier set' (aggresive minimization).\n");
728  fprintf(vis_stderr,"-e\n");
729  fprintf(vis_stderr,"   Compute the set of fair states (those satisfying the formula\n");
730  fprintf(vis_stderr,"   EGfair TRUE) before the verification process and use the result\n");
731  fprintf(vis_stderr,"   as care set.\n");
732  fprintf(vis_stderr,"-h\n");
733  fprintf(vis_stderr,"   Print the command usage.\n");
734  fprintf(vis_stderr,"-n\n");
735  fprintf(vis_stderr,"   Try to prove the negation of every formula\n");
736  fprintf(vis_stderr,"-s\n");
737  fprintf(vis_stderr,"   Print a summary of statistics after the verification.\n");
738  fprintf(vis_stderr,"-t <secs>\n");
739  fprintf(vis_stderr,"   Time in seconds allowed to spend in the verification.\n");
740  fprintf(vis_stderr,"-v <number>\n");
741  fprintf(vis_stderr,"   Specify verbosity level. Use 0 for no feedback (default), 1 for\n");
742  fprintf(vis_stderr,"   more and 2 for maximum feedback. This option can not be used\n");
743  fprintf(vis_stderr,"   in conjunction with -V.\n");
744  fprintf(vis_stderr,"-V <number>\n");
745  fprintf(vis_stderr,"   Mask specifying type of information to be printed out while\n");
746  fprintf(vis_stderr,"   verifying the formulas. See the help page.\n");
747  fprintf(vis_stderr,"-x\n");
748  fprintf(vis_stderr,"   Perform the verification exactly. No approximation is done.\n");
749  fprintf(vis_stderr,"<ctlfile>\n");
750  fprintf(vis_stderr,"   File containing the CTL formulas to be verified.\n");
751  return NIL(AbsOptions_t);
752} /* End of ParseAbsCtlOptions */
753
754/**Function********************************************************************
755
756  Synopsis    [Handle function for timeout.]
757
758  Description [This function is called when the process receives a signal of
759  type alarm. Since alarm is set with elapsed time, this function checks if the
760  CPU time corresponds to the timeout of the command. If not, it reprograms the
761  alarm to fire later and check if the CPU limit has been reached.]
762
763  SideEffects []
764
765******************************************************************************/
766static void
767TimeOutHandle(
768  int sigType)
769{
770  long seconds;
771
772  seconds = (util_cpu_time() - alarmLap) / 1000;
773 
774  if (seconds < absTimeOut) {
775    unsigned slack;
776
777    slack = absTimeOut - seconds;
778    (void) signal(SIGALRM, TimeOutHandle);
779    (void) alarm(slack);
780  }
781  else {
782    longjmp(timeOutEnv, 1);
783  }
784} /* End of TimeOutHandle */
Note: See TracBrowser for help on using the repository browser.