source: vis_dev/vis-2.3/src/ltl/ltl.c @ 101

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

vis2.3
File size: 69.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltl.c]
4
5  PackageName [ltl]
6
7  Synopsis    [LTL model checking.]
8
9  Author      [Chao Wang <chao.wang@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 "ltlInt.h"
18#include <errno.h>
19
20static char rcsid[] UNUSED = "$Id: ltl.c,v 1.74 2009/04/11 01:41:30 fabio Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Structure declarations                                                    */
28/*---------------------------------------------------------------------------*/
29
30/*---------------------------------------------------------------------------*/
31/* Type declarations                                                         */
32/*---------------------------------------------------------------------------*/
33
34/*---------------------------------------------------------------------------*/
35/* Variable declarations                                                     */
36/*---------------------------------------------------------------------------*/
37static jmp_buf timeOutEnv;
38
39
40/*---------------------------------------------------------------------------*/
41/* Macro declarations                                                        */
42/*---------------------------------------------------------------------------*/
43
44/**AutomaticStart*************************************************************/
45
46/*---------------------------------------------------------------------------*/
47/* Static function prototypes                                                */
48/*---------------------------------------------------------------------------*/
49
50static int CommandLtlMc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
51static int CommandLtl2Aut(Hrc_Manager_t ** hmgr, int argc, char ** argv);
52static LtlMcOption_t * ParseLtlMcOptions(int argc, char **argv);
53static LtlMcOption_t * ParseLtlTestOptions(int argc, char **argv);
54static boolean LtlMcAtomicFormulaCheckSemantics(Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
55static void TimeOutHandle(void);
56static void ShuffleMddIdsToTop(mdd_manager *mddManager, array_t *mddIdArray);
57
58/**AutomaticEnd***************************************************************/
59
60
61/*---------------------------------------------------------------------------*/
62/* Definition of exported functions                                          */
63/*---------------------------------------------------------------------------*/
64
65/**Function********************************************************************
66
67  Synopsis    [Initializes the Ltl package.]
68
69  SideEffects []
70
71  SeeAlso     [Ltl_End]
72
73******************************************************************************/
74void
75Ltl_Init(void)
76{
77  /* LTL model checking. Before using this command, the design must be read
78   * and 'init_verify' has been executed.
79   */
80  Cmd_CommandAdd("ltl_model_check", CommandLtlMc,  0);
81
82  /* Test the LTL->Buechi Automaton Translator, may or may not need to read
83   * the design. But If the design is read, the semantic of the formula
84   * will be checked on the model before translation
85   */
86  Cmd_CommandAdd("ltl_to_aut", CommandLtl2Aut, 0);
87}
88
89
90/**Function********************************************************************
91
92  Synopsis    [Ends the Ltl package.]
93
94  SideEffects []
95
96  SeeAlso     [Ltl_Init]
97
98******************************************************************************/
99void
100Ltl_End(void)
101{
102}
103
104
105/**Function********************************************************************
106
107   Synopsis    [Translate the LTL formula into a Buechi automaton.]
108
109   Description [The wrapper of LtlMcFormulaToAutomaton.]
110
111   SideEffects [The returned automaton should be freed by the caller.]
112
113   SeeAlso     [LtlMcFormulaToAutomaton]
114
115******************************************************************************/
116Ltl_Automaton_t *
117Ltl_McFormulaToAutomaton(
118  Ntk_Network_t *network,
119  Ctlsp_Formula_t *Formula,
120  int options_algorithm,
121  int options_rewriting,
122  int options_prunefair,
123  int options_iocompatible,
124  int options_directsim,
125  int options_reversesim,
126  int options_directsimMaximize,
127  int options_verbosity,
128  int checkSemantics
129  )
130{
131  LtlMcOption_t *options = LtlMcOptionAlloc();
132  Ltl_Automaton_t *aut;
133
134  options->algorithm = (Ltl2AutAlgorithm) options_algorithm;
135  if (options_algorithm == Ltl2Aut_WRING_c) {
136    options->rewriting = 1;
137    options->prunefair = 1;
138    options->iocompatible = 1;
139    options->directsim = 1;
140    options->reversesim = 1;
141  }else {
142    options->rewriting = options_rewriting;
143    options->prunefair = options_prunefair;
144    options->iocompatible = options_iocompatible;
145    options->directsim = options_directsim;
146    options->reversesim = options_reversesim;
147  }
148  options->directsimMaximize = options_directsimMaximize;
149  options->verbosity = (Mc_VerbosityLevel) options_verbosity;
150
151  aut = LtlMcFormulaToAutomaton(network, Formula, options, checkSemantics);
152
153  LtlMcOptionFree(options);
154
155  return aut;
156}
157
158
159/**Function********************************************************************
160
161   Synopsis    [Translate the Buechi automaton into a network.]
162
163   Description [A new Hrc_Manager_t is created, in which the network will
164   be stored. The translation goes as the following:
165
166   1) translate the Buechi automaton into a temp file (in blifmv format);
167   2) read in the temp file (into the new hrcMgr) by default blifmv parser
168   3) flatten_hierarchy to get the network   ]
169
170   SideEffects [The returned Hrc_Manager_t should be freed by the caller.]
171
172   SeeAlso     []
173
174******************************************************************************/
175Hrc_Manager_t *
176Ltl_McAutomatonToNetwork(
177  Ntk_Network_t *designNetwork,
178  Ltl_Automaton_t *automaton,
179  int verbosity)
180{
181  FILE *fp;
182  Hrc_Manager_t *buechiHrcMgr;
183  Hrc_Node_t    *buechiHrcNode;
184  Ntk_Network_t *buechiNetwork;
185  int flag;
186
187  /* 1) translate the automaton to a temporary blif_mv file */
188  fp = tmpfile();
189  if (fp == NIL(FILE)) {
190    fail("Aut->Ntk: can't open temp file");
191  }
192#ifdef DEBUG_LTLMC
193  if (verbosity >= 2) {
194    fprintf(vis_stdout, "\nPrint the automaton Blif_Mv file:\n");
195    flag = Ltl_AutomatonToBlifMv(vis_stdout, designNetwork, automaton);
196    fprintf(vis_stdout, "\n");
197    fflush(vis_stdout);
198  }
199#endif
200  flag = Ltl_AutomatonToBlifMv(fp, designNetwork, automaton);
201  if (!flag) {
202    return NIL(Hrc_Manager_t);
203  }
204
205  /* 2) read and parse the tmp blifmv file */
206  rewind(fp);
207  error_init();
208  buechiHrcMgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), 0, 0, 0);
209  fclose(fp);
210  if (buechiHrcMgr == NIL(Hrc_Manager_t))
211    fail(error_string());
212
213  /* 3) flatten_hierarchy */
214  buechiHrcNode = Hrc_ManagerReadCurrentNode(buechiHrcMgr);
215  buechiNetwork = Ntk_HrcNodeConvertToNetwork(buechiHrcNode, TRUE, (lsList)0);
216  Hrc_NodeAddApplInfo(buechiHrcNode, NTK_HRC_NODE_APPL_KEY,
217                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
218                      (Hrc_ApplInfoChangeFn) NULL,
219                      (void *) buechiNetwork);
220
221  /* 4) static_order (!!! using the default mddManager) */
222  Ntk_NetworkSetMddManager(buechiNetwork,
223                           Ntk_NetworkReadMddManager(designNetwork));
224  Ord_NetworkOrderVariables(buechiNetwork,
225                            Ord_RootsByDefault_c,
226                            Ord_NodesByDefault_c,
227                            FALSE,
228                            Ord_InputAndLatch_c,
229                            Ord_Unassigned_c,
230                            (lsList)NULL,
231                            0);
232
233  return buechiHrcMgr;
234}
235
236/**Function********************************************************************
237
238  Synopsis [Perform static semantic check of ltl formula on network.]
239
240  Description [Perform static semantic check of ltl formula on network.
241  Specifically, given an atomic formula of the form LHS=RHS, check that the LHS
242  is the name of a latch/wire in the network, and that RHS is of appropriate
243  type (enum/integer) and is lies in the range of the latch/wire values. If LHS
244  is a wire, and inputsAllowed is false, check to see that the algebraic
245  support of the wire consists of only latches and constants.]
246
247  SideEffects []
248
249******************************************************************************/
250boolean
251Ltl_FormulaStaticSemanticCheckOnNetwork(
252  Ctlsp_Formula_t *formula,
253  Ntk_Network_t *network,
254  boolean inputsAllowed
255  )
256{
257  boolean lCheck;
258  boolean rCheck;
259  Ctlsp_Formula_t *leftChild;
260  Ctlsp_Formula_t *rightChild;
261
262  if(formula == NIL(Ctlsp_Formula_t)){
263    return TRUE;
264  }
265
266  if(Ctlsp_FormulaReadType(formula) == Ctlsp_ID_c){
267    return LtlMcAtomicFormulaCheckSemantics(formula, network, inputsAllowed);
268  }
269
270  leftChild = Ctlsp_FormulaReadLeftChild(formula);
271  rightChild = Ctlsp_FormulaReadRightChild(formula);
272
273  lCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
274                                                   inputsAllowed);
275  if(!lCheck)
276    return FALSE;
277
278  rCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
279                                                   inputsAllowed);
280  if (!rCheck)
281    return FALSE;
282
283  return TRUE;
284}
285
286
287/*---------------------------------------------------------------------------*/
288/* Definition of internal functions                                          */
289/*---------------------------------------------------------------------------*/
290
291/**Function********************************************************************
292
293   Synopsis    [Translate the LTL formula to a Buechi automaton.]
294
295   Description [State-of-the-art Optiomization/Minimization is used to shrink
296   the size of the automaton:
297   1) Rewriting the Formula  (before translation)
298   2) Boolean Minimization   (during translation)
299   3) Automaton Minimization (after translation)
300         - prune fair states
301         - simulation-based minimization (io/direct/reverse)
302
303   For more information, refer to: Fabio Somenzi and Roderick Bloem,"Efficient
304   Buechi Automaton from LTL Formula," CAV'00.
305
306   Before translation, the sementics of the formula is checked on the model.
307   In the case it fails, a NIL pointer will be returned.]
308
309   SideEffects [The returned automaton should be freed by the caller.]
310
311   SeeAlso     []
312
313******************************************************************************/
314Ltl_Automaton_t *
315LtlMcFormulaToAutomaton(
316  Ntk_Network_t *network,
317  Ctlsp_Formula_t *Formula,
318  LtlMcOption_t *options,
319  int checkSemantics)
320{
321
322  char *tmpString;
323  Ctlsp_Formula_t *ltlFormula, *negFormula;
324  LtlTableau_t *tableau;
325  Ltl_Automaton_t *automaton;
326
327  /* check the semantic of the formula on the given network */
328  if (checkSemantics && network != NIL(Ntk_Network_t)) {
329    if (!network) {
330      fprintf(vis_stderr,
331              "ltl_mc error: empty network. use flatten_hierarchy\n");
332      return NIL(Ltl_Automaton_t);
333    }
334    error_init();
335    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(Formula, network, 1)) {
336      fprintf(vis_stderr,
337              "ltl_mc error: formula semantic check on design fails:\n%s\n",
338              error_string());
339      return NIL(Ltl_Automaton_t);
340    }
341  }
342
343  /* print out the given LTL formula */
344  fprintf(vis_stdout, "Formula: ");
345  Ctlsp_FormulaPrint(vis_stdout, Formula);
346  fprintf(vis_stdout, "\n");
347
348  /* Negate Formula and Expand the abbreaviations */
349  negFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, Formula, NIL(Ctlsp_Formula_t));
350  ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negFormula);
351  tmpString = Ctlsp_FormulaConvertToString(negFormula);
352  FREE(negFormula);
353#ifdef DEBUG_LTLMC
354  if (options->verbosity)
355    fprintf(vis_stdout, "\nNegation Print: %s\n", tmpString);
356#endif
357
358  /* 1) Simplify the formula by 'Rewriting' */
359  if (options->rewriting) {
360    Ctlsp_Formula_t *tmpF = ltlFormula;
361    ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
362    Ctlsp_FormulaFree(tmpF);
363  }
364
365  /* create the alph_beta table */
366  tableau = LtlTableauGenerateTableau(ltlFormula);
367  tableau->verbosity = options->verbosity;
368  tableau->algorithm = options->algorithm;
369  tableau->booleanmin = options->booleanmin;
370#ifdef DEBUG_LTLMC
371  /* print out the tableau rules */
372  if (options->verbosity > 1)
373    LtlTableauPrint(vis_stdout, tableau);
374#endif
375
376  /* we dont' need this formula any more */
377  Ctlsp_FormulaFree(ltlFormula);
378
379
380  /* 2) create the automaton */
381  automaton = LtlAutomatonGeneration(tableau);
382  automaton->name = tmpString;
383
384  /* 3-1) minimize the automaton by Pruning fairness */
385  if (options->prunefair) {
386#ifdef DEBUG_LTLMC
387    if (options->verbosity >= McVerbosityMax_c) {
388      Ltl_AutomatonPrint(automaton, options->verbosity);
389      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
390    }
391#endif
392    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
393  }
394
395  /* 3-2) minimize the automaton by I/O compatible and dominance */
396  if (options->iocompatible) {
397#ifdef DEBUG_LTLMC
398    if (options->verbosity >= McVerbosityMax_c) {
399      Ltl_AutomatonPrint(automaton, options->verbosity);
400      fprintf(vis_stdout, "\nIOC-Minimization:\n");
401    }
402#endif
403    while(Ltl_AutomatonMinimizeByIOCompatible(automaton,options->verbosity));
404  }
405
406  /* 3-3) minimize the automaton by Direct Simulation */
407  if (options->directsim) {
408#ifdef DEBUG_LTLMC
409    if (options->verbosity >= McVerbosityMax_c) {
410      Ltl_AutomatonPrint(automaton, options->verbosity);
411      fprintf(vis_stdout, "\nDirSim-Minimization:\n");
412    }
413#endif
414    Ltl_AutomatonMinimizeByDirectSimulation(automaton, options->verbosity);
415  }
416
417  /* 3-4) minimize the automaton by Direct Simulation */
418  if (options->reversesim) {
419#ifdef DEBUG_LTLMC
420    if (options->verbosity >= McVerbosityMax_c) {
421      Ltl_AutomatonPrint(automaton, options->verbosity);
422      fprintf(vis_stdout, "\nRevSim-Minimization:\n");
423    }
424#endif
425    Ltl_AutomatonMinimizeByReverseSimulation(automaton, options->verbosity);
426  }
427
428  /* 3-5) minimize the automaton by Pruning fairness */
429  if (options->prunefair) {
430#ifdef DEBUG_LTLMC
431    if (options->verbosity >= McVerbosityMax_c) {
432      Ltl_AutomatonPrint(automaton, options->verbosity);
433      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
434    }
435#endif
436    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
437  }
438  /* print out the Buechi automaton */
439  if (options->verbosity) {
440    Ltl_AutomatonPrint(automaton, options->verbosity);
441  }
442
443  return automaton;
444}
445
446/**Function********************************************************************
447
448  Synopsis [Load the Fairness Constraint for the compFsm.]
449
450  Description [The fairness constraint comes from two places:
451      1) the fairness constraints on the model (designFairness);
452      2) the fairsets from the Buechi automaton (the LTL formula).
453  *AutomatonStrength is unchanged unless there are external fairness and the
454  automaton is terminal (in which case the strength is assumed to be "1-weak".]
455
456  SideEffects [*AutomatonStrength might be changed.]
457
458******************************************************************************/
459void
460LtlFsmLoadFairness(
461  Fsm_Fsm_t *compFsm,
462  Fsm_Fairness_t *designFairness,
463  int NumberOfFairSets,
464  int *AutomatonStrength)
465{
466  array_t *fairformulaArray;
467  Ctlp_Formula_t *F;
468  int j;
469
470  /* The fairness constraint on the model (before ltl_model_check is invoked)
471   * should be Buechi fairness
472   */
473  if (!Fsm_FairnessTestIsBuchi(designFairness)) {
474    fprintf(vis_stderr, "ltl_mc error: Can not handle non-Buchi Fairness \n");
475    assert(0);
476  }
477
478  /* store the new fairness constraint (for compFsm) */
479  fairformulaArray = array_alloc(Ctlp_Formula_t *, 0);
480
481  /* copy the fairness constraints from the automaton */
482  if (*AutomatonStrength == Mc_Aut_Strong_c/*2*/) {
483    if (NumberOfFairSets > 0) {
484      for (j=0; j<NumberOfFairSets; j++) {
485        char tmpstr[30];
486        sprintf(tmpstr, "fair%d$AUT$NTK2", j+1);
487        F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav(tmpstr),
488                               (void *)util_strsav("1"));
489        array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
490      }
491    }else {
492      F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav("fair1$AUT$NTK2"),
493                             (void *)util_strsav("1"));
494      array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
495    }
496  }
497
498  /* copy the fairness constraints on the model */
499  for (j=0; j<Fsm_FairnessReadNumConjunctsOfDisjunct(designFairness, 0); j++) {
500    F = Fsm_FairnessReadFinallyInfFormula(designFairness, 0, j);
501    if (array_n(fairformulaArray) && Ctlp_FormulaReadType(F) == Ctlp_TRUE_c)
502      continue;
503    array_insert_last(Ctlp_Formula_t *,fairformulaArray, Ctlp_FormulaDup(F));
504  }
505
506  /* this is a conservative conclusion ! */
507  if (*AutomatonStrength == Mc_Aut_Terminal_c /*0*/) {
508    F = array_fetch(Ctlp_Formula_t *, fairformulaArray, 0);
509    if (array_n(fairformulaArray) > 1 ||
510        Ctlp_FormulaReadType(F) != Ctlp_TRUE_c) {
511      *AutomatonStrength = Mc_Aut_Weak_c /*1*/;
512    }
513  }
514
515  /* update the fairness constraints on 'compFsm' */
516  Fsm_FsmFairnessUpdate(compFsm, fairformulaArray);
517
518  array_free(fairformulaArray);
519}
520
521/**Function********************************************************************
522
523  Synopsis [Alloc Memory for LtlMcOption_t.]
524
525  SideEffects []
526
527  SeeAlso []
528******************************************************************************/
529LtlMcOption_t *
530LtlMcOptionAlloc(void)
531{
532  LtlMcOption_t *result = ALLOC(LtlMcOption_t, 1);
533  if (result == NIL(LtlMcOption_t))
534    return NIL(LtlMcOption_t);
535  memset(result, 0, sizeof(LtlMcOption_t));
536
537  result->algorithm = Ltl2Aut_WRING_c;
538  result->schedule = McGSH_EL_c;
539  result->lockstep = MC_LOCKSTEP_OFF;
540  result->outputformat = Aut2File_ALL_c;
541
542  return result;
543}
544
545/**Function********************************************************************
546
547  Synopsis [Free LtlMcOption_t, and close the ltl formula file.]
548
549  SideEffects []
550
551  SeeAlso []
552******************************************************************************/
553void
554LtlMcOptionFree(
555  LtlMcOption_t *result)
556{
557  if (result->ltlFile)
558    fclose(result->ltlFile);
559
560  if (result->debugFile)
561    fclose(result->debugFile);
562
563  if (result->outputfilename)
564    FREE(result->outputfilename);
565
566  FREE(result);
567}
568
569
570/*---------------------------------------------------------------------------*/
571/* Definition of static functions                                            */
572/*---------------------------------------------------------------------------*/
573
574/**Function********************************************************************
575
576  Synopsis [Check LTL formulae given in file are modeled by flattened network]
577
578  CommandName [ltl_model_check]
579
580  CommandSynopsis [perform LTL model checking on a flattened network]
581
582  CommandArguments [ \[-a &lt;ltl2aut_algorithm&gt;\] \[-b\]
583  \[-d &lt;dbg_level&gt;\] \[-f &lt;dbg_file&gt;\] \[-h\] \[-i\] \[-m\] \[-s\]
584  \[-t &lt;time_out_period&gt;\]\[-v &lt;verbosity_level&gt;\]
585  \[-A &lt;le_method&gt;\]
586  \[-D &lt;dc_level&gt;\] \[-L &lt;lockstep_mode&gt;\] \[-S &lt;schedule&gt;\]
587  \[-F\] \[-X\] \[-Y\] \[-M\] &lt;ltl_file&gt;] \[-Z\]
588
589
590  CommandDescription [Performs LTL model checking on a flattened
591  network.  Before calling this command, the user should have
592  initialized the design by calling the command <A
593  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
594  Regardless of the options, no 'false positives' or 'false negatives'
595  will occur: the result is correct for the given circuit.  <p>
596
597  Properties to be verified should be provided as LTL formulae in the
598  file <code>ltl_file</code>.  Note that the support of any wire
599  referred to in a formula should consist only of latches.  For the
600  precise syntax of LTL formulas, see the <A
601  HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>.
602  <p>
603
604  A formula passes iff it is true for all initial states of the
605  system.  Therefore, in the presence of multiple initial states, if a
606  formula fails, the negation of the formula may also fail.<p>
607
608  If a formula does not pass, a (potentially partial) proof of failure
609  (referred to as a debug trace) is demonstrated. Fair paths are
610  represented by a finite sequence of states (the stem) leading to a
611  fair cycle, i.e. a cycle on which there is a state from each
612  fairness condition. Whether demostrate the proof or not can be
613  specified (see option <code>-d</code>).  <p>
614
615
616  Command options:
617  <p>
618
619  <dl>
620
621  <dt> -a <code> &lt;ltl2aut_algorithm&gt; </code> <dd> Specify the algorithm
622  used in LTL formula -> Buechi automaton translation.
623  <p> <dd> <code> ltl2aut_algorithm</code> must be one  of the following:
624
625  <p><code>0</code>: GPVW.
626
627  <p><code>1</code>: GPVW+.
628
629  <p><code>2</code>: LTL2AUT.
630
631  <p><code>3</code>: WRING (default).
632
633  <p>
634
635  <dt> -b
636  <dd> Use boolean minimization during the LTL to Automaton translation.
637  <p>
638
639  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify whether to demonstrate
640  a counter-example when the system fails a formula being checked.
641
642  <p> <dd> <code> dbg_level</code> must be one of the following:
643
644  <p><code>0</code>: No debugging performed.
645  <code>dbg_level</code>=<code>0</code> is the default.
646
647  <p><code>1</code>: Generate a counter-example (a path to a fair cycle).
648  <p>
649
650  <dt> -f &lt;<code>dbg_file</code>&gt;
651  <dd> Write the debugger output to <code>dbg_file</code>.
652  <p>
653
654
655  <dt> -h
656  <dd> Print the command usage.
657  <p>
658
659  <dt> -i
660  <dd> Print input values causing transitions between states during debugging.
661  Both primary and pseudo inputs are printed.
662  <p>
663
664  <dt> -m
665  <dd> Pipe debugger output through the UNIX utility  more.
666  <p>
667
668  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
669  <dd> Specify the time out period (in seconds) after which the command aborts.
670  By default this option is set to infinity.
671  <p>
672
673  <dt> -s
674  <dd> Print debug output in the format accepted by the
675       <A HREF="simulateCmd.html"><code>simulate</code></A> command.
676  <p>
677
678
679  <dt> -v  <code>&lt;verbosity_level&gt;</code>
680  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage
681  and code status.
682
683  <br><code>verbosity_level</code>  must be one of the following:<p>
684
685  <code>0</code>: No feedback provided. This is the default.<p>
686
687  <code>1</code>: Feedback on code location.<p>
688
689  <code>2</code>: Feedback on code location and CPU usage.<p>
690
691  <p>
692
693  <dt> -A <code> &lt;le_method&gt; </code>
694  <dd>
695  Specify whether the compositional SCC analysis algorithm, Divide and
696  Compose (DnC), is enabled for language emptiness checking.
697  The DnC algorithm first enumerates fair SCCs in an over-approximated
698  abstract model, and then successively refines them in the more
699  concrete models.
700  Since non-fair SCCs can be ignored in the more concrete models, a
701  potentially large part of the state space are pruned away early on
702  when the computations are cheap.
703  <p>
704
705  <dd>
706  <code> le_method </code> must be one of the following:
707  <p>
708
709  <code> 0 </code>: no use of Divide and Compose (Default). <p>
710  <code> 1 </code>: use Divide and Compose. <p>
711
712  <dt> -D <code> &lt;dc_level&gt; </code>
713
714  <dd> Specify extent to which don't cares are used to simplify MDDs in model
715  checking.  Don't cares are minterms on which the value taken by functions
716  does not affect the computation; potentially, these minterms can be used to
717  simplify MDDs and reduce the time taken to perform model checking.
718
719  <br>
720  <code> dc_level </code> must be one of the following:
721  <p>
722
723  <code> 0 </code>: No don't cares are used.
724
725  <p> <code> 1 </code>: Use unreachable states as don't cares. This is the
726  default.
727
728  <p> <code> 2 </code>: Use unreachable states as don't cares and in the EU
729  computation, use 'frontiers' for image computation.<p>
730
731  <code> 3 </code>: First compute an overapproximation of the reachable states
732  (ARDC), and use that as the cares set.  Use `frontiers' for image
733  computation.  For help on controlling options for ARDC, look up help on the
734  command: <A HREF="print_ardc_optionsCmd.html">print_ardc_options</A>. Refer
735  to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares
736  for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD
737  December 1996: one is for State Space Decomposition and the other is for
738  Approximate FSM Traversal.<p>
739
740  <dt> -S <code> &lt;schedule&gt; </code>
741
742  <dd> Specify schedule for GSH algorithm, which generalizes the
743  Emerson-Lei algorithm and is used to compute greatest fixpoints.
744  The choice of schedule affects the sequence in which EX and EU
745  operators are applied.  It makes a difference only when fairness
746  constraints are specified.
747
748  <br>
749  <code> &lt;schedule&gt; </code> must be one of the following:
750
751  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
752  is the default.
753
754  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.
755
756  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
757  all EUs.
758
759  <p> <code> budget </code>: a hybrid of EL and EL2
760
761  <p> <code> random </code>: enabled operators are applied in
762  (pseudo-)random order.
763
764  <p> <code> off </code>: GSH is disabled, and the old algorithm is
765  used instead.  The old algorithm uses the <code> EL </code>, but the
766  termination checks are less sophisticated than in GSH.
767  <p>
768
769  <dt> -F
770
771  <dd> Use forward analysis in the computation of the greatest fixpoint.
772  This option is incompatible with -d 1 or higher and can only be used
773  with -D 1.
774
775  <dt> -L <code> &lt;lockstep_mode&gt; </code>
776
777  <dd> Use the lockstep algorithm, which is based on fair SCC enumeration.
778
779  <br>
780  <code> &lt;lockstep_mode&gt; </code> must be one of the following:
781
782  <p> <code> off </code>: Lockstep is disabled.  This is the default.
783  Language emptiness is checked by computing a hull of the fair SCCs.
784
785  <p> <code> on </code>: Lockstep is enabled.
786
787  <p> <code> all </code>: Lockstep is enabled; all fair SCCs are
788  enumerated instead of terminating as soon as one is found.  This can
789  be used to study the SCCs of a graph, but it is slower than the
790  default option.
791
792  <p> <code> n </code>: (n is a positive integer).  Lockstep is
793  enabled and up to <code> n </code> fair SCCs are enumerated.  This
794  is less expensive than <code> all </code>, but still less efficient
795  than <code> on </code>, even when <code> n = 1 </code>.
796
797  <dt> -X
798  <dd> Disable strength reduction (use different decision procedures for
799  strong, weak, and terminal automaton). Strength reduction is the default.
800  Refer to Bloem, Ravi, Somenzi, "Efficient Decision Procedures for LTL Model
801  Checking," CAV99.
802  <p>
803
804  <dt> -Y
805  <dd> Disable incremental construction of the partition for (MxA). Instead,
806  build a new partition from the scratch. Incremental construction of the
807  partition is the default.
808  <p>
809
810  <dt> -Z
811  <dd> Add arcs into the Buechi automaton by direct simulation relation, to
812  heuristically reduce the length of shortest counter-example in model
813  checking. Refer to Awedh and Somenze, "Proving More Properties with
814  Bounded Model Checking," CAV04.
815  <p>
816
817  <dt> -M
818  <dd> Maximize (adding arcs to) Buechi automaton using Direct Simulation.
819
820  <dt> <code> &lt;ltl_file&gt; </code>
821
822  <dd> File containing LTL formulas to be model checked.
823  </dl>
824
825  Related "set" options:
826  <dl>
827  <dt> ltl_change_bracket &lt;yes/no&gt;
828  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
829  therefore CTL* parser does the same thing. However, in some cases a user
830  does not want to change node names in CTL* parsing. Then, use this set
831  option by giving "no". Default is "yes".
832  <p>
833
834  See also commands : model_check, approximate_model_check,
835  incremental_ctl_verification ]
836
837  Description [First, the LTL formula is parsed and translated into a
838  Buechi automaton (minimization techniques can by applied during the process).
839
840  Then, the Buechi Automaton is translated into a Hrc_Node in a newly created
841  Hrc_Manager. flatten_hierarchy/static_order are used to obtain the automaton
842  Network. In this process the same mddManager (as that of the design network)
843  is used.
844
845  Now we need to compose the (M x A). We choose to append the automaton network
846  to the design network. Partition is updated (or regenerated) for the composed
847  network.
848
849  A new FSM is created and the fairness are loaded in it. The fairness
850  constraints comes from both the design network and the automaton network.
851  Finally we use Mc_FsmCheckLanguageEmptiness() to do the language emptiness
852  checking. "Strength Reduction Technique" -- using different decision
853  procedures for strong, weak, and terminal automaon -- is used.
854
855  After the model check, we free everything we created in this command:
856  partition for (MxA), the new FSM, newly-created network nodes, the
857  automaton network as well as the automaton Hrc_Manager.
858
859  If necessary, the result mdd (which is the bad state -- a state that leads
860  to a fair path) can be saved. (for example, in the CTL*  model checker).]
861
862  SideEffects []
863
864******************************************************************************/
865static int
866CommandLtlMc(
867  Hrc_Manager_t ** hmgr,
868  int  argc,
869  char ** argv)
870{
871  array_t *ltlArray;
872  LtlMcOption_t *options;
873  Ctlsp_Formula_t *ltlFormula;
874  Ltl_Automaton_t *automaton;
875  LtlTableau_t *tableau;
876  Hrc_Manager_t *buechiHrcMgr;
877  Hrc_Node_t *designNode;
878  Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
879  Fsm_Fsm_t *compFsm = NIL(Fsm_Fsm_t);
880  Ntk_Network_t *designNetwork,*buechiNetwork = NIL(Ntk_Network_t);
881  Ntk_Node_t *node1, *node2;
882  array_t *modelCareStatesArray;
883  lsGen lsgen2;
884  lsList nodeList;
885  graph_t *partition, *save_partition;
886  mdd_t *fairInitStates, *modelCareStates, *mddOne;
887  char *designModelName, *name1;
888  int i;
889  long startLtlMcTime, endLtlMcTime;
890  static int timeOutPeriod = 0;
891
892  Img_ResetNumberOfImageComputation(Img_Both_c);
893
894  if (!(options = ParseLtlMcOptions(argc, argv))) {
895    return 1;
896  }
897  timeOutPeriod = options->timeOutPeriod;
898
899  if (options->dbgLevel != 0 && options->direction == McFwd_c) {
900    (void) fprintf(vis_stderr, "** ltl_mc error: -d is incompatible with -F\n");
901    LtlMcOptionFree(options);
902    return 1;
903  }
904  if (options->dcLevel !=  McDcLevelRch_c && options->direction == McFwd_c) {
905    (void) fprintf(vis_stderr, "** ltl_mc error: -F can only be used with -D1\n");
906    LtlMcOptionFree(options);
907    return 1;
908  }
909
910  /* 'designFsm' and 'designNetwork' are for the model */
911  designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
912  if (designFsm == NIL(Fsm_Fsm_t)) {
913    return 1;
914  }
915  designNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
916
917  /* Parse LTL formulae */
918  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
919  if (ltlArray != NIL(array_t)) {
920    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
921    Ctlsp_FormulaArrayFree(ltlArray);
922    ltlArray = tmpArray;
923  }
924  if (ltlArray == NIL(array_t)) {
925    (void) fprintf(vis_stderr,
926                   "** ltl_mc error: error in parsing formulas from file\n");
927    LtlMcOptionFree(options);
928    return 1;
929  }
930  /* Semantic Check of the Ltl formula array on the network */
931  arrayForEachItem(Ctlsp_Formula_t *, ltlArray, i, ltlFormula) {
932    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(ltlFormula,
933                                                 designNetwork, 1)) {
934      fprintf(vis_stderr,
935              "ltl_mc error: formula semantic check on design fails:\n%s\n",
936              error_string());
937      Ctlsp_FormulaArrayFree(ltlArray);
938      LtlMcOptionFree(options);
939      return 1;
940    }
941  }
942
943  /* Set time out processing (if timeOutPeriod is set) */
944  if (timeOutPeriod > 0) {
945    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
946    (void) alarm(timeOutPeriod);
947    if (setjmp(timeOutEnv) > 0) {
948      (void) fprintf(vis_stdout, "# LTL_MC: Ltl modelchecking - timeout occurred after %d seconds.\n", timeOutPeriod);
949      (void) fprintf(vis_stdout, "# LTL_MC: data may be corrupted.\n");
950      if (options->verbosity > McVerbosityNone_c) {
951        (void) fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c), Img_GetNumberOfImageComputation(Img_Backward_c));
952      }
953      alarm(0);
954      return 1;
955    }
956  }
957  startLtlMcTime = util_cpu_time();
958
959  mddOne = mdd_one(Ntk_NetworkReadMddManager(designNetwork));
960
961  /* Start LTL model checking for each formula */
962  for (i=0; i<array_n(ltlArray); i++) {
963    st_table *tbl;
964    array_t *mddIds;
965    lsList rootList;
966    int NumberOfFairSet, AutomatonStrength;
967    long initialTime, finalTime; /* for checking each formula */
968    int nImgComps, nPreComps;
969
970    /* stats */
971    if (options->verbosity > McVerbosityNone_c) {
972      initialTime = util_cpu_time();
973      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
974      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
975    } else {
976      /* to remove uninitialized variable warning */
977      initialTime = 0;
978      nImgComps = 0;
979      nPreComps = 0;
980    }
981    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);
982
983    /*---------------------------------------------------------------------
984     * 1) create the Buechi Automaton/Network/Mdd_Order/Partition in a new
985     * Hrc_Manager. It shares nothing with the Design but the mddManager.
986     *--------------------------------------------------------------------*/
987    automaton = LtlMcFormulaToAutomaton(designNetwork, ltlFormula, options, 1);
988    assert(automaton != NIL(Ltl_Automaton_t));
989
990    if (options->noStrengthReduction)
991      AutomatonStrength = Mc_Aut_Strong_c /*2*/;
992    else
993      AutomatonStrength = Ltl_AutomatonGetStrength(automaton);
994
995    /* add arcs by Direct Simulation, to reduce the counter-example length */
996    if (options->directsimMaximize) {
997#ifdef DEBUG_LTLMC
998      if (options->verbosity >= McVerbosityMax_c) {
999        Ltl_AutomatonPrint(automaton, options->verbosity);
1000        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
1001      }
1002#endif
1003      Ltl_AutomatonMaximizeByDirectSimulation(automaton, options->verbosity);
1004    }
1005    NumberOfFairSet = lsLength(automaton->Fair);
1006    buechiHrcMgr = Ltl_McAutomatonToNetwork(designNetwork, automaton,
1007                                            options->verbosity);
1008    assert(buechiHrcMgr != NIL(Hrc_Manager_t));
1009    tableau = automaton->tableau;
1010    Ltl_AutomatonFree((gGeneric) automaton);
1011    LtlTableauFree(tableau);
1012    buechiNetwork =  Ntk_HrcManagerReadCurrentNetwork(buechiHrcMgr);
1013
1014    /*---------------------------------------------------------------------
1015     * 2) build (M x A) by attaching buechiNetwork(A) to designNetwork(M).
1016     * The result network M x A (designNetwork) shares some data with the
1017     * buechiNetwork (Variables, and Tables). The newly created nodes in
1018     * designNetwork retain their MddId in buechiNetwork
1019     *--------------------------------------------------------------------*/
1020    /* 2-a) Retrieve the Model (in the default hrc_manager) */
1021    designNode = Hrc_ManagerReadCurrentNode(*hmgr);
1022    designModelName = Hrc_NodeReadModelName(designNode);
1023    /* 2-b) Attach buechiNetwork to designNetwork */
1024    tbl = st_init_table(strcmp, st_strhash);
1025    Ntk_NetworkAppendNetwork(designNetwork, buechiNetwork, tbl);
1026    st_free_table(tbl);
1027
1028    /* Here we have the choice of incrementally build the partition,
1029     * or build it from scratch. In both cases, the original partition
1030     * will be saved (and restored later)
1031     */
1032    if (!options->noIncrementalPartition) {
1033      rootList = lsCreate();
1034      mddIds = array_alloc(int, 2);
1035      /* 2-c) Assign MddId to the newly-created nodes */
1036      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
1037        if (!Ntk_NodeTestIsPrimaryInput(node2)) {
1038          name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
1039          node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
1040          Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
1041          if (!strcmp(name1, "state$AUT$NTK2"))
1042            array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
1043          else if (!strcmp(name1, "state$AUT$NS$NTK2"))
1044            array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
1045          else if (!strcmp(name1, "selector$AUT$NTK2"))
1046            array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
1047          FREE(name1);
1048          if (Ntk_NodeTestIsCombOutput(node1))
1049            lsNewEnd(rootList, (lsGeneric)node1, (lsHandle *)0);
1050        }
1051      }
1052      /* move the automaton variables to the top most -- this is believed
1053       * to be an optimal ordering */
1054      if (!options->noShuffleToTop)
1055        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
1056      array_free(mddIds);
1057
1058      /* 2-d) Create the Partition information for (M x A) */
1059      save_partition = Part_NetworkReadPartition(designNetwork);
1060      partition = Part_PartitionDuplicate(save_partition);
1061      Part_UpdatePartitionFrontier(designNetwork, partition, rootList,
1062                                   (lsList)0, mddOne);
1063      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
1064                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1065                             (void *)partition);
1066      lsDestroy(rootList, (void (*)(lsGeneric))0);
1067
1068    }else {
1069      mddIds = array_alloc(int, 2);
1070      /* 2-c) Assign MddId to the newly-created nodes */
1071      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
1072        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
1073        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
1074        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
1075        Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
1076        if (!strcmp(name1, "state$AUT$NTK2"))
1077          array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
1078        else if (!strcmp(name1, "state$AUT$NS$NTK2"))
1079          array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
1080        else if (!strcmp(name1, "selector$AUT$NTK2"))
1081          array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
1082        FREE(name1);
1083      }
1084      /* move the automaton variables to the top most. This might be the
1085       * best BDD variable ordering for (M x A)! */
1086      if (!options->noShuffleToTop)
1087        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
1088      array_free(mddIds);
1089
1090      /* 2-d) Create the Partition information for (M x A) */
1091      nodeList = lsCreate();
1092      partition = Part_NetworkCreatePartition(designNetwork,
1093                                              designNode,
1094                                              designModelName,
1095                                              (lsList)0,
1096                                              (lsList)0,
1097                                              NIL(mdd_t),
1098                                              Part_Default_c,
1099                                              nodeList,
1100                                              FALSE, 0, 0);
1101      save_partition = Part_NetworkReadPartition(designNetwork);
1102      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
1103                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1104                             (void *)partition);
1105
1106      lsDestroy(nodeList, (void (*)(lsGeneric))0);
1107    }
1108
1109    /*---------------------------------------------------------------------
1110     * 3) Create the FSM for (M x A) and load Fairness constraints
1111     *--------------------------------------------------------------------*/
1112    /* try to get a reduced Fsm (w.r.t. each individual property) first */
1113    {
1114      array_t *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
1115      Ctlp_Formula_t *ctlF = Ctlp_FormulaCreate(Ctlp_ID_c,
1116                                                util_strsav("state$AUT$NTK2"),
1117                                                util_strsav("Trap"));
1118      array_insert(Ctlp_Formula_t *, ctlArray, 0, ctlF);
1119      compFsm = Mc_ConstructReducedFsm(designNetwork, ctlArray);
1120      Ctlp_FormulaFree(ctlF);
1121      array_free(ctlArray);
1122      if (compFsm == NIL(Fsm_Fsm_t))
1123        compFsm = Fsm_FsmCreateFromNetworkWithPartition(designNetwork,
1124                                                        NIL(graph_t));
1125    }
1126    /* merge fairnesses from outside and those from the automaton ... */
1127    LtlFsmLoadFairness(compFsm, Fsm_FsmReadFairnessConstraint(designFsm),
1128                       NumberOfFairSet, &AutomatonStrength);
1129
1130
1131    /*---------------------------------------------------------------------
1132     * 4) Language emptiness checking (store result if necessary)
1133     *--------------------------------------------------------------------*/
1134    if (options->dcLevel == McDcLevelArdc_c) {
1135      Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
1136      array_t *tmpArray;
1137      long startRchTime;
1138      Fsm_ArdcGetDefaultOptions(ardcOptions);
1139      startRchTime = util_cpu_time();
1140      tmpArray =
1141        Fsm_ArdcComputeOverApproximateReachableStates(compFsm, 0,
1142                                                      options->verbosity,
1143                                                      0, 0, 0, 0, 0, 0,
1144                                                      ardcOptions);
1145      modelCareStatesArray = mdd_array_duplicate(tmpArray);
1146      FREE(ardcOptions);
1147      if (options->verbosity > McVerbosityNone_c)
1148        Fsm_ArdcPrintReachabilityResults(compFsm,
1149                                         util_cpu_time() - startRchTime);
1150    }else if (options->dcLevel >= McDcLevelRch_c) {
1151      long startRchTime;
1152      startRchTime = util_cpu_time();
1153      modelCareStates =
1154        Fsm_FsmComputeReachableStates(compFsm, 0, options->verbosity, 0, 0,
1155                                      (options->lockstep != MC_LOCKSTEP_OFF),
1156                                      0, 0, Fsm_Rch_Default_c, 0, 0,
1157                                      NIL(array_t), FALSE, NIL(array_t));
1158      if (options->verbosity > McVerbosityNone_c) {
1159        Fsm_FsmReachabilityPrintResults(compFsm,
1160                                        util_cpu_time() - startRchTime,
1161                                        Fsm_Rch_Default_c);
1162      }
1163      modelCareStatesArray = array_alloc(mdd_t *, 0);
1164      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
1165    } else {
1166      modelCareStates = mdd_one(Fsm_FsmReadMddManager(compFsm));
1167      modelCareStatesArray = array_alloc(mdd_t *, 0);
1168      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
1169    }
1170    /*
1171    Fsm_MinimizeTransitionRelationWithReachabilityInfo(compFsm,
1172                                                       Img_Backward_c,
1173                                                       options->verbosity > 1);
1174    */
1175
1176    /* language emptiness checking */
1177    fairInitStates = Mc_FsmCheckLanguageEmptiness(compFsm,
1178                                                  modelCareStatesArray,
1179                                                  (Mc_AutStrength_t) AutomatonStrength,
1180                                                  options->leMethod,
1181                                                  options->dcLevel,
1182                                                  options->dbgLevel,
1183                                                  options->printInputs,
1184                                                  options->verbosity,
1185                                                  options->schedule,
1186                                                  options->direction,
1187                                                  options->lockstep,
1188                                                  options->debugFile,
1189                                                  options->useMore,
1190                                                  options->simValue,
1191                                                  "LTL_MC");
1192    mdd_array_free(modelCareStatesArray);
1193
1194    if (fairInitStates)
1195      mdd_free(fairInitStates);
1196
1197    /*---------------------------------------------------------------------
1198     * 5) Remove 'A' from designNetwork (M x A), which contains 3 steps:
1199     * a) free compFsm/partition
1200     * b) remove newly-created nodes from designNetwork;
1201     * c) destory buechiHrcMgr (buechiNetwork)
1202     *--------------------------------------------------------------------*/
1203    Ntk_NetworkAddApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
1204                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1205                           (void *)save_partition);
1206    Fsm_FsmFree(compFsm);
1207    {
1208      int tmpi, tmpj;
1209      Ntk_Node_t *node3, *node4;
1210      /* first, remove the newly-added A nodes ('xxxlabel$AUT$NTK2') from the
1211       * fanout list of the M nodes */
1212      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
1213        if (strstr(Ntk_NodeReadName(node2), "label$AUT") == NULL)
1214          continue;
1215        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
1216        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
1217        FREE(name1);
1218        assert(node1);
1219        Ntk_NodeForEachFanin(node1, tmpi, node3) {
1220          array_t *oldFanouts = Ntk_NodeReadFanouts(node3);
1221          array_t *newFanouts;
1222          if (oldFanouts != NIL(array_t)) {
1223            newFanouts = array_alloc(Ntk_Node_t *, 0);
1224            arrayForEachItem(Ntk_Node_t *, oldFanouts, tmpj, node4) {
1225              if (node4 != node1)
1226                array_insert_last(Ntk_Node_t *, newFanouts, node4);
1227            }
1228            Ntk_NodeSetFanouts(node3, newFanouts);
1229          }
1230        }
1231      }
1232      /* Now we can safely remove all the newly-added A nodes */
1233      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
1234        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
1235        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
1236        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
1237        FREE(name1);
1238        Ntk_NodeRemoveFromNetwork(designNetwork, node1, 1, 1, 0);
1239        Ntk_NodeFree(node1);
1240      }
1241    }
1242    Ntk_NetworkSetMddManager(buechiNetwork, (mdd_manager *)0);
1243    Hrc_ManagerFree(buechiHrcMgr);
1244
1245    if (options->verbosity > McVerbosityNone_c) {
1246      finalTime = util_cpu_time();
1247      fprintf(vis_stdout, "-- ltl_mc time = %10g\n",
1248        (double)(finalTime - initialTime) / 1000.0);
1249      fprintf(vis_stdout,
1250              "-- %d image computations and %d preimage computations\n",
1251              Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
1252              Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
1253    }
1254  }
1255
1256  /* Print stats if verbose. */
1257  endLtlMcTime = util_cpu_time();
1258  if (options->verbosity > McVerbosityNone_c) {
1259    fprintf(vis_stdout, "-- total ltl_mc time: %10g\n",
1260            (double)(endLtlMcTime-startLtlMcTime)/1000.0);
1261    fprintf(vis_stdout,
1262            "-- total %d image computations and %d preimage computations\n",
1263            Img_GetNumberOfImageComputation(Img_Forward_c),
1264            Img_GetNumberOfImageComputation(Img_Backward_c));
1265  }
1266
1267  /* Clean-ups */
1268  Ctlsp_FormulaArrayFree(ltlArray);
1269  LtlMcOptionFree(options);
1270  mdd_free(mddOne);
1271
1272  alarm(0);
1273  return 0;             /* normal exit */
1274}
1275
1276/**Function********************************************************************
1277
1278  Synopsis    [Translate LTL formulae given in file into Buechi automata]
1279
1280  CommandName [ltl_to_aut]
1281
1282  CommandSynopsis [translate LTL formulae into Buechi automata]
1283
1284  CommandArguments [ \[-f &lt;ltl_file&gt;\] \[-m &lt;algorithm&gt;\] \[-o &lt;output_file&gt;\] \[-t &lt;output_format&gt;\] \[-w\] \[-b\] \[-p\] \[-d\] \[-r\] \[-i\] \[-M\] \[-v &lt;verbosity&gt;\] \[-h\] ]
1285
1286  CommandDescription [Translate the given LTL formulae into Buechi automata,
1287  and output the automaton into a file. <p>
1288
1289  The translation algorithms are the same as the one used in <A
1290  HREF="ltl_model_checkCmd.html"> <code> ltl_model_check </code></A>. However,
1291  more flexible combination of the options can be used with this command. <p>
1292
1293  The automaton can be displayed on the screen and written into a file. The
1294  format of the output can be dot, blifmv, verilog and smv. <p>
1295
1296
1297  Command options:
1298  <p>
1299
1300  <dl>
1301
1302  <dt> -f <code> &lt;ltl_file&gt; </code>
1303  <dd> The input file containing LTL formulae.
1304
1305  <dt> -m <code> &lt;algorithm&gt; </code>
1306  <dd> Specify the algorithm used in LTL formula -> Buechi automaton
1307  translation algorithm.
1308  <p> <dd> <code>algorithm</code> must be one  of the following:
1309  <p><code>0</code>: GPVW.
1310  <p><code>1</code>: GPVW+.
1311  <p><code>2</code>: LTL2AUT.
1312  <p><code>3</code>: WRING (default).
1313
1314  <dt> -o <code> &lt;output_file&gt; </code>
1315  <dd> Write the automata into this file.
1316
1317  <dt> -t <code> &lt;output_format&gt; </code>
1318  <dd> Specify the output format of the automata.
1319  <p> <dd> <code>output_format</code> must be one of the following:
1320  <p><code>0</code>: dot.
1321  <p><code>1</code>: blif_mv.
1322  <p><code>2</code>: verilog.
1323  <p><code>3</code>: all of the formats above (default).
1324  <p>
1325
1326
1327  <dt> -w
1328  <dd> Rewriting the formula before translation.
1329
1330  <dt> -b
1331  <dd> Boolean minimization during the translation.
1332
1333  <dt> -p
1334  <dd> Pruning the fair states in the Buechi automaton.
1335
1336  <dt> -d
1337  <dd> Direct-simulation minimization of the Buechi automaton.
1338
1339  <dt> -r
1340  <dd> Reverse-simulation minimization of the Buechi automaton.
1341
1342  <dt> -i
1343  <dd> Minimization based ont the I/O structural information.
1344
1345  <dt> -M
1346  <dd> Maximize (adding arcs to) Buechi automaton using Direct Simulation.
1347
1348  <dt> -v <code>&lt;verbosity_level&gt;</code>
1349  <dd> Specify verbosity level. It must be one of the following: 0,1,2,3.
1350
1351  <dt> -h
1352  <dd> Print the command usage.
1353
1354  </dl>
1355  ]
1356
1357  SideEffects []
1358
1359******************************************************************************/
1360static int
1361CommandLtl2Aut(
1362  Hrc_Manager_t ** hmgr,
1363  int  argc,
1364  char ** argv)
1365{
1366  array_t        *ltlArray;
1367  Ctlsp_Formula_t        *ltlFormula;
1368  LtlTableau_t           *tableau;
1369  Ltl_Automaton_t        *automaton;
1370  int            i;
1371  LtlMcOption_t *options;
1372  int            verbosity = 0;   /* verbosity level */
1373  int            algorithm = 0;   /* translation algorithm */
1374  int            rewriting = 0;   /* simplify Formula by rewriting */
1375  int            booleanmin = 0;  /* boolean minimization */
1376  int            prunefair = 0;   /* prune fairness */
1377  int            iocompatible = 0;/* simplify by io-compatible */
1378  int            directsim = 0;   /* simplify by Direct simulation */
1379  int            reversesim = 0;  /* simplify by reverse simulation */
1380  int            directsimMaximize = 0;   /* simplify by Direct simulation */
1381  Ntk_Network_t  *network;
1382  char  *tmpString;
1383  long           beginTime, finalTime;
1384
1385
1386  if (!(options = ParseLtlTestOptions(argc, argv))) {
1387    return 1;
1388  }
1389  rewriting = options->rewriting;
1390  verbosity = options->verbosity;
1391  algorithm = options->algorithm;
1392  booleanmin = options->booleanmin;
1393  prunefair = options->prunefair;
1394  iocompatible = options->iocompatible;
1395  directsim = options->directsim;
1396  reversesim = options->reversesim;
1397  directsimMaximize = options->directsimMaximize;
1398
1399  beginTime = util_cpu_time();
1400  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1401
1402  /* Parse the LTL Formulae */
1403  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
1404  if (ltlArray != NIL(array_t)) {
1405    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
1406    Ctlsp_FormulaArrayFree(ltlArray);
1407    ltlArray = tmpArray;
1408  }
1409  if (ltlArray == NIL(array_t)) {
1410    (void) fprintf(vis_stderr,
1411                   "** ltl_to_aut error: error in parsing formulas file\n");
1412    LtlMcOptionFree(options);
1413    return 1;
1414  }
1415
1416  /* For each LTL formula, build a Buechi automaton ... */
1417  for (i=0; i<array_n(ltlArray); i++) {
1418    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);
1419    tmpString = Ctlsp_FormulaConvertToString(ltlFormula);
1420
1421    /* expand the abbreaviations */
1422    ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(ltlFormula);
1423    fprintf(vis_stdout, "\nFormula: %s\n", tmpString);
1424
1425    /* 1) Simplify the formula by 'Rewriting' */
1426    if (rewriting) {
1427      Ctlsp_Formula_t *tmpF = ltlFormula;
1428      ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
1429      tmpString = Ctlsp_FormulaConvertToString(ltlFormula);
1430      Ctlsp_FormulaFree(tmpF);
1431    }
1432
1433    /* create the alph_beta table */
1434    tableau = LtlTableauGenerateTableau(ltlFormula);
1435    tableau->verbosity = verbosity;
1436    tableau->algorithm = algorithm;
1437    tableau->booleanmin = booleanmin;
1438    /* print out the tableau rules */
1439    if (verbosity >= McVerbosityMax_c)
1440      LtlTableauPrint(vis_stdout, tableau);
1441
1442    /* 2) create the automaton */
1443    automaton = LtlAutomatonGeneration(tableau);
1444    automaton->name = tmpString;
1445
1446    /* 3) minimize the automaton by Pruning fairness */
1447    if (prunefair) {
1448      if (verbosity >= McVerbosityMax_c) {
1449        Ltl_AutomatonPrint(automaton, verbosity);
1450        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
1451      }
1452      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
1453    }
1454
1455    /* 4) minimize the automaton by I/O compatible and dominance */
1456    if (iocompatible) {
1457      if (verbosity >= McVerbosityMax_c) {
1458        Ltl_AutomatonPrint(automaton, verbosity);
1459        fprintf(vis_stdout, "\nIOC-Minimization:\n");
1460      }
1461      while(Ltl_AutomatonMinimizeByIOCompatible(automaton, verbosity));
1462    }
1463
1464    /* 5) minimize the automaton by Direct Simulation */
1465    if (directsim) {
1466      if (verbosity >= McVerbosityMax_c) {
1467        Ltl_AutomatonPrint(automaton, verbosity);
1468        fprintf(vis_stdout, "\nDirSim-Minimization:\n");
1469      }
1470      Ltl_AutomatonMinimizeByDirectSimulation(automaton, verbosity);
1471    }
1472
1473    /* 6) minimize the automaton by Reverse Simulation */
1474    if (reversesim) {
1475      if (verbosity >= McVerbosityMax_c) {
1476        Ltl_AutomatonPrint(automaton, verbosity);
1477        fprintf(vis_stdout, "\nRevSim-Minimization:\n");
1478      }
1479      Ltl_AutomatonMinimizeByReverseSimulation(automaton, verbosity);
1480    }
1481
1482    /* 7/3) minimize the automaton by Pruning fairness */
1483    if (prunefair) {
1484      if (verbosity >= McVerbosityMax_c) {
1485        Ltl_AutomatonPrint(automaton, verbosity);
1486        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
1487      }
1488      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
1489    }
1490
1491    /* 8) add arcs by Direct Simulation, to reduce counter-example length */
1492    if (directsimMaximize) {
1493      if (verbosity >= McVerbosityMax_c) {
1494        Ltl_AutomatonPrint(automaton, verbosity);
1495        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
1496      }
1497      Ltl_AutomatonMaximizeByDirectSimulation(automaton, verbosity);
1498    }
1499
1500    /* print out the Buechi automaton */
1501    Ltl_AutomatonPrint(automaton, verbosity+1);
1502
1503    /* write the automaton in a file in the proper format */
1504    if (options->outputfilename) {
1505      FILE *fp;
1506      fp = Cmd_FileOpen( options->outputfilename, (char *)((i==0)?"w":"a"),
1507                         NIL(char *), 0);
1508      if (options->outputformat == Aut2File_DOT_c)
1509        Ltl_AutomatonToDot(fp, automaton, 0);
1510      else if (options->outputformat == Aut2File_BLIFMV_c)
1511        Ltl_AutomatonToBlifMv(fp, network, automaton);
1512      else if (options->outputformat == Aut2File_VERILOG_c)
1513        Ltl_AutomatonToVerilog(fp, network, automaton);
1514      else {
1515        Ltl_AutomatonToDot(fp, automaton, 0);
1516        Ltl_AutomatonToBlifMv(fp, network, automaton);
1517        Ltl_AutomatonToVerilog(fp, network, automaton);
1518      }
1519      fclose(fp);
1520    }
1521
1522    /* Clean-ups: the current formula*/
1523    Ltl_AutomatonFree((gGeneric) automaton);
1524    LtlTableauFree(tableau);
1525    Ctlsp_FormulaFree(ltlFormula);
1526  }
1527
1528  /* Clean-ups */
1529  Ctlsp_FormulaArrayFree(ltlArray);
1530  LtlMcOptionFree(options);
1531
1532  finalTime = util_cpu_time();
1533  fprintf(vis_stdout, "# LTL_TO_AUT time: %10g\n",
1534          (double)(finalTime-beginTime)/1000.0);
1535
1536  return 0;             /* normal exit */
1537}
1538
1539
1540/**Function********************************************************************
1541
1542  Synopsis [Parse the user input for command "ltl_model_check."]
1543
1544  Description []
1545
1546  SideEffects []
1547
1548******************************************************************************/
1549static LtlMcOption_t *
1550ParseLtlMcOptions(
1551  int argc,
1552  char **argv)
1553{
1554  LtlMcOption_t *options = LtlMcOptionAlloc();
1555  char *ltlFileName = (char *)0;
1556  char *debugOutName = (char *)0;
1557  Mc_GSHScheduleType schedule = McGSH_EL_c;
1558  Mc_FwdBwdAnalysis direction = McBwd_c;
1559  int lockstep = MC_LOCKSTEP_OFF;
1560  int c;
1561
1562  if (options == NIL(LtlMcOption_t))
1563    return NIL(LtlMcOption_t);
1564  options->leMethod = Mc_Le_Default_c;
1565  options->dcLevel = McDcLevelRch_c;
1566  options->noStrengthReduction = 0;
1567  options->noIncrementalPartition = 0;
1568
1569  /* Parse command line options.
1570   */
1571  util_getopt_reset();
1572  while ((c = util_getopt(argc, argv, "a:bd:f:t:A:D:v:S:L:FhimsXYM")) != EOF) {
1573    switch(c) {
1574    case 'a':
1575      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
1576      if (options->algorithm < 0 || options->algorithm > 3)
1577        goto usage;
1578      break;
1579    case 'b':
1580      options->booleanmin = 1;
1581      break;
1582    case 'd':
1583      options->dbgLevel = (LtlMcDbgLevel) atoi(util_optarg);
1584      break;
1585    case 'f':
1586      debugOutName = util_strsav(util_optarg);
1587      break;
1588    case 't':
1589      options->timeOutPeriod = atoi(util_optarg);
1590      break;
1591    case 'A':
1592      options->leMethod = (Mc_LeMethod_t) atoi(util_optarg);
1593      break;
1594    case 'D':
1595      options->dcLevel = (Mc_DcLevel) atoi(util_optarg);
1596      break;
1597    case 'v':
1598      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
1599      break;
1600    case 'S' :
1601      schedule = Mc_StringConvertToScheduleType(util_optarg);
1602      break;
1603    case 'L' :
1604      lockstep = Mc_StringConvertToLockstepMode(util_optarg);
1605      break;
1606    case 'F' :
1607      direction = McFwd_c;
1608      break;
1609    case 'i':
1610      options->printInputs = 1;
1611      break;
1612    case 'm':
1613      options->useMore = TRUE;
1614      break;
1615    case 's' :
1616      options->simValue = TRUE;
1617      break;
1618    case 'X':
1619      options->noStrengthReduction = 1;
1620      break;
1621    case 'Y':
1622      options->noIncrementalPartition = 1;
1623      break;
1624    case 'Z':
1625      options->noShuffleToTop = 1;
1626      break;
1627    case 'M':
1628      options->directsimMaximize = 1;
1629      break;
1630    case 'h':
1631      goto usage;
1632    default:
1633      goto usage;
1634    }
1635  }
1636  if (options->algorithm == Ltl2Aut_WRING_c) {
1637    options->rewriting =    TRUE;
1638    options->prunefair =    TRUE;
1639    options->directsim =    TRUE;
1640    options->reversesim =   TRUE;
1641    options->iocompatible = TRUE;
1642  }
1643
1644  if (schedule == McGSH_Unassigned_c) {
1645    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
1646    goto usage;
1647  } else {
1648    options->schedule = schedule;
1649  }
1650  if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
1651    (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
1652    goto usage;
1653  } else {
1654    options->lockstep = lockstep;
1655  }
1656  options->direction = direction;
1657
1658  /* Open the ltl file.
1659   */
1660  if (argc - util_optind == 0) {
1661    (void) fprintf(vis_stderr, "** ltl_mc error: file containing ltl formulae not provided\n");
1662    goto usage;
1663  }
1664  else if (argc - util_optind > 1) {
1665    (void) fprintf(vis_stderr, "** ltl_mc error: too many arguments\n");
1666    goto usage;
1667  }
1668  ltlFileName = util_strsav(argv[util_optind]);
1669
1670  /* Read LTL Formulae */
1671  if (!ltlFileName)
1672    goto usage;
1673  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
1674  if (options->ltlFile == NIL(FILE)) {
1675    (void) fprintf(vis_stdout,  "** ltl_mc error: error in opening file %s\n", ltlFileName);
1676    FREE(ltlFileName);
1677    LtlMcOptionFree(options);
1678    return NIL(LtlMcOption_t);
1679  }
1680  FREE(ltlFileName);
1681
1682  if (debugOutName != NIL(char)) {
1683    options->debugFile = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
1684    if (options->debugFile == NIL(FILE)) {
1685      (void) fprintf(vis_stdout,"** ltl_mc error: error in opening file %s\n", debugOutName);
1686      FREE(debugOutName);
1687      LtlMcOptionFree(options);
1688      return NIL(LtlMcOption_t);
1689    }
1690    FREE(debugOutName);
1691  }
1692
1693  return options;
1694
1695 usage:
1696  (void) fprintf(vis_stderr, "usage: ltl_model_check [-a ltl2aut_algorithm][-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A le_method][-D dc_level][-L lockstep_mode][-S schedule][-F][-X][-Y][-M] <ltl_file>\n");
1697  (void) fprintf(vis_stderr, "    -a <ltl2aut_algorithm>\n");
1698  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 0 => GPVW\n");
1699  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 1 => GPVW+\n");
1700  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 2 => LTL2AUT\n");
1701  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 3 => WRING (Default)\n");
1702  (void) fprintf(vis_stderr, "    -b \tUse boolean minimization in automaton generation\n");
1703  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
1704  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
1705  (void) fprintf(vis_stderr, "        debug_level = 1 => automatic debugging\n");
1706  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
1707  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
1708  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
1709  (void) fprintf(vis_stderr, "    -m \tPipe debugger output through the UNIX utility more.\n");
1710  (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
1711  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
1712  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
1713  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
1714  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
1715  (void) fprintf(vis_stderr, "    -t <period> time out period\n");
1716  (void) fprintf(vis_stderr, "    -A <le_method>\n");
1717  (void) fprintf(vis_stderr, "        le_method = 0 => no use of Divide and Compose (Default)\n");
1718  (void) fprintf(vis_stderr, "        le_method = 1 => use Divide and Compose\n");
1719  (void) fprintf(vis_stderr, "    -D <dc_level>\n");
1720  (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
1721  (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
1722  (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");
1723
1724  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
1725  (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
1726  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
1727  (void) fprintf(vis_stderr, "    -L <lockstep_mode>\n");
1728  (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");
1729  (void) fprintf(vis_stderr, "    -S <schedule>\n");
1730  (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
1731  (void) fprintf(vis_stderr, "    -F \tUse forward analysis in fixpoint computation.\n");
1732  (void) fprintf(vis_stderr, "    -X \tDisable strength reduction (using different decision procedure \n");
1733  (void) fprintf(vis_stderr, "       \tfor strong, weak, terminal automaton).\n");
1734  (void) fprintf(vis_stderr, "    -Y \tDisable incremental partition of the composed system (M x A).\n");
1735  (void) fprintf(vis_stderr, "    -Z \tAdd arcs into the Buechi automaton by direct simulation relation.\n");
1736
1737  (void) fprintf(vis_stderr, "    -M \tAdd arcs to the automaton to reduce counter-example length.\n");
1738  (void) fprintf(vis_stderr, "    <ltl_file> The input file containing LTL formulae to be checked.\n");
1739  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
1740
1741  LtlMcOptionFree(options);
1742  return NIL(LtlMcOption_t);
1743}
1744
1745/**Function********************************************************************
1746
1747  Synopsis [Parse the user input for command "ltl_to_aut".]
1748
1749  Description []
1750
1751  SideEffects []
1752
1753******************************************************************************/
1754static LtlMcOption_t *
1755ParseLtlTestOptions(
1756  int argc,
1757  char **argv)
1758{
1759  LtlMcOption_t *options = LtlMcOptionAlloc();
1760  char *ltlFileName = (char *)0;
1761  int c;
1762
1763  if (options == NIL(LtlMcOption_t))
1764    return NIL(LtlMcOption_t);
1765
1766  /*
1767   * Parse command line options.
1768   */
1769  util_getopt_reset();
1770  while ((c = util_getopt(argc, argv, "wbpdMrif:m:v:o:t:h")) != EOF) {
1771    switch(c) {
1772    case 'w':
1773      options->rewriting = 1;
1774      break;
1775    case 'b':
1776      options->booleanmin = 1;
1777      break;
1778    case 'p':
1779      options->prunefair = 1;
1780      break;
1781    case 'd':
1782      options->directsim = 1;
1783      break;
1784    case 'M':
1785      options->directsimMaximize = 1;
1786      break;
1787    case 'r':
1788      options->reversesim = 1;
1789      break;
1790    case 'i':
1791      options->iocompatible = 1;
1792      break;
1793    case 'f':
1794      ltlFileName = util_strsav(util_optarg);
1795      break;
1796    case 'm':
1797      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
1798      break;
1799    case 'v':
1800      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
1801      break;
1802    case 'o':
1803      options->outputfilename = util_strsav(util_optarg);
1804      break;
1805    case 't':
1806      options->outputformat = (Aut2FileType) atoi(util_optarg);
1807      break;
1808    case 'h':
1809      goto usage;
1810    default:
1811      goto usage;
1812    }
1813  }
1814
1815  /* 'Wring' is equivalent to
1816  *    LTL2AUT +
1817  *    rewriting +
1818  *    prunefair + directsim + reversesim + iocompatible
1819  */
1820  if (options->algorithm ==3) {
1821    options->rewriting = 1;
1822    options->prunefair = 1;
1823    options->directsim = 1;
1824    options->reversesim = 1;
1825    options->iocompatible = 1;
1826  }
1827
1828  /* Read LTL Formulae */
1829  if (!ltlFileName)
1830    goto usage;
1831
1832  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
1833  FREE(ltlFileName);
1834  if (options->ltlFile == NIL(FILE)) {
1835    (void) fprintf(vis_stdout,  "** ltl_to_aut error: error in opening file %s\n", ltlFileName);
1836    LtlMcOptionFree(options);
1837    return NIL(LtlMcOption_t);
1838  }
1839
1840  return options;
1841
1842  usage:
1843  (void) fprintf(vis_stderr, "usage: ltl_to_aut <-f ltl_file> [-m algorithm] [-o output_file] [-t output_format] [-w] [-b] [-p] [-d] [-r] [-i] [-M] [-v verbosity_level] [-h]\n");
1844  (void) fprintf(vis_stderr, "    -f <ltl_file>\n");
1845  (void) fprintf(vis_stderr, "       The input file containing LTL formulae\n");
1846  (void) fprintf(vis_stderr, "    -m <algorithm>\n");
1847  (void) fprintf(vis_stderr, "        algorithm = 0 => GPVW\n");
1848  (void) fprintf(vis_stderr, "        algorithm = 1 => GPVW+\n");
1849  (void) fprintf(vis_stderr, "        algorithm = 2 => LTL2AUT\n");
1850  (void) fprintf(vis_stderr, "        algorithm = 3 => Wring (default)\n");
1851  (void) fprintf(vis_stderr, "    -o <output_file>\n");
1852  (void) fprintf(vis_stderr, "       Write the automata to output_file\n");
1853  (void) fprintf(vis_stderr, "    -t <output_format>\n");
1854  (void) fprintf(vis_stderr, "        output_format = 0 => dot\n");
1855  (void) fprintf(vis_stderr, "        output_format = 1 => blif_mv\n");
1856  (void) fprintf(vis_stderr, "        output_format = 2 => verilog\n");
1857  (void) fprintf(vis_stderr, "        output_format = 3 => all (default)\n");
1858  (void) fprintf(vis_stderr, "    -w \tRewriting the formula\n");
1859  (void) fprintf(vis_stderr, "    -b \tBoolean minimization \n");
1860  (void) fprintf(vis_stderr, "    -p \tPruning the fairness\n");
1861  (void) fprintf(vis_stderr, "    -d \tDirect-simulation minimization\n");
1862  (void) fprintf(vis_stderr, "    -r \tReverse-simulation minimization\n");
1863  (void) fprintf(vis_stderr, "    -i \tI/O compatible minimization\n");
1864  (void) fprintf(vis_stderr, "    -M \tAdd arcs by direct-simulation to reduce the counter-example length\n");
1865  (void) fprintf(vis_stderr, "    -v <verbosity>\n");
1866  (void) fprintf(vis_stderr, "       \tVerbosity can be 0,1,2,3\n");
1867  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
1868
1869  LtlMcOptionFree(options);
1870  return NIL(LtlMcOption_t);
1871}
1872
1873
1874/**Function********************************************************************
1875
1876  Synopsis [Perform simple static semantic checks on formula.]
1877
1878  SideEffects []
1879
1880  SeeAlso [Ltl_FormulaStaticSemanticCheckOnNetwork]
1881******************************************************************************/
1882static boolean
1883LtlMcAtomicFormulaCheckSemantics(
1884  Ctlsp_Formula_t *formula,
1885  Ntk_Network_t *network,
1886  boolean inputsAllowed)
1887{
1888  char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
1889  char *nodeValueString = Ctlsp_FormulaReadValueName( formula );
1890  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );
1891
1892  Var_Variable_t *nodeVar;
1893  int nodeValue;
1894
1895  if ( !node ) {
1896    error_append("Could not find node corresponding to the name\n\t- ");
1897    error_append( nodeNameString );
1898    return FALSE;
1899  }
1900
1901  nodeVar = Ntk_NodeReadVariable( node );
1902  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
1903    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
1904    if ( nodeValue == -1 ) {
1905      error_append("Value specified in RHS is not in domain of variable\n");
1906      error_append( Ctlsp_FormulaReadVariableName( formula ) );
1907      error_append("=");
1908      error_append( Ctlsp_FormulaReadValueName( formula ) );
1909      return FALSE;
1910    }
1911  }
1912  else {
1913    int check;
1914
1915    check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
1916    if( check==0 ) {
1917      error_append("Value in the RHS is illegal\n");
1918      error_append( Ctlsp_FormulaReadVariableName( formula ) );
1919      error_append("=");
1920      error_append( Ctlsp_FormulaReadValueName( formula ) );
1921      return FALSE;
1922    }
1923    if( check==1 ) {
1924      error_append("Value in the RHS is out of range of int\n");
1925      error_append( Ctlsp_FormulaReadVariableName( formula ) );
1926      error_append("=");
1927      error_append( Ctlsp_FormulaReadValueName( formula ) );
1928      return FALSE;
1929    }
1930    if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
1931      error_append("Value specified in RHS is not in domain of variable\n");
1932      error_append( Ctlsp_FormulaReadVariableName( formula ) );
1933      error_append("=");
1934      error_append( Ctlsp_FormulaReadValueName( formula ) );
1935      return FALSE;
1936    }
1937  }
1938
1939  if(!inputsAllowed){
1940    boolean coverSupport;
1941    lsGen tmpGen;
1942    Ntk_Node_t *tmpNode;
1943    st_table *supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
1944    array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);
1945
1946    array_insert_last( Ntk_Node_t *, thisNodeArray, node );
1947    Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
1948      if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
1949        st_insert(supportNodes,  tmpNode, NIL(char));
1950      }
1951    }
1952
1953    coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
1954                                                            thisNodeArray,
1955                                                            supportNodes);
1956    array_free(thisNodeArray);
1957    st_free_table(supportNodes);
1958
1959    if ( coverSupport == FALSE ) {
1960      char *tmpString =
1961        util_strcat3( "\nNode ", nodeNameString,
1962                      " is not driven only by latches and constants.\n");
1963      error_append(tmpString);
1964      return FALSE;
1965    }
1966  }
1967
1968  return TRUE;
1969}
1970
1971/**Function********************************************************************
1972
1973  Synopsis    [Handle function for timeout.]
1974
1975  Description [This function is called when the process receives a signal of
1976  type alarm. Since alarm is set with elapsed time, this function checks if the
1977  CPU time corresponds to the timeout of the command. If not, it reprograms the
1978  alarm to fire later and check if the CPU limit has been reached.]
1979
1980  SideEffects []
1981
1982******************************************************************************/
1983static void
1984TimeOutHandle(void)
1985{
1986  longjmp(timeOutEnv, 1);
1987}
1988
1989/**Function********************************************************************
1990
1991  Synopsis    [Move the mdd variables to the top most.]
1992
1993  Description [This function is called to move the automaton variables to the
1994  top most. This is believed to be the best variable ordering for the composed
1995  system (M x A). The variable corresponding to the first item in mddIdArray
1996  will be the top most.]
1997
1998  SideEffects []
1999
2000******************************************************************************/
2001static void
2002ShuffleMddIdsToTop(mdd_manager *mddManager, array_t *mddIdArray)
2003{
2004  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
2005  int *invPermArray = ALLOC(int, bdd_num_vars(mddManager));
2006  int invPermIndex, i, j, bvarId, mddId, result;
2007  st_table *stored = st_init_table(st_ptrcmp, st_ptrhash);
2008  mvar_type mvar;
2009
2010  /* put mddId on the top most */
2011  invPermIndex = 0;
2012  arrayForEachItem(int, mddIdArray, j, mddId) {
2013    if (mddId == 0) continue;
2014    mvar = array_fetch(mvar_type, mvar_list, mddId);
2015    for (i = 0; i<mvar.encode_length; i++) {
2016      bvarId = mdd_ret_bvar_id(&mvar, i);
2017      invPermArray[invPermIndex++] = bvarId;
2018      st_insert(stored, (char *) (long) bvarId, (char *)0);
2019    }
2020  }
2021  /* shift every one else down */
2022  for (i = 0; (unsigned) i< bdd_num_vars(mddManager); i++) {
2023    bvarId = bdd_get_id_from_level(mddManager, i);
2024    if (!st_is_member(stored, (char *) (long) bvarId)) {
2025      invPermArray[invPermIndex++] = bvarId;
2026    }
2027  }
2028  /* call bdd_shuffle */
2029  result = bdd_shuffle_heap(mddManager, invPermArray);
2030#ifdef DEBUG_LTLMC
2031  if (result)
2032    fprintf(vis_stdout, "\nShuffle automaton vars to the top: success!\n");
2033  else
2034    fprintf(vis_stdout, "\nShuffle automaton vars to the top: failure!\n");
2035#endif
2036
2037  /* Clean up */
2038  st_free_table(stored);
2039  FREE(invPermArray);
2040}
Note: See TracBrowser for help on using the repository browser.