source: vis_dev/vis-2.3/src/bmc/bmcAutUtil.c @ 97

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

vis2.3
File size: 26.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [bmcAutUtil.c]
4
5  PackageName [bmc]
6 
7  Synopsis    [Utility file for BMC_Automaton]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15******************************************************************************/
16
17#include "bmc.h"
18#include "bmcInt.h"
19
20static char rcsid[] UNUSED = "$Id: bmcAutUtil.c,v 1.18 2005/05/18 18:11:52 jinh Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Type declarations                                                         */
28/*---------------------------------------------------------------------------*/
29
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static st_table * AutomatonVertexGetImg(graph_t *G, vertex_t *vtx);
48static st_table * AutomatonVertexGetPreImg(graph_t *G, vertex_t *vtx);
49static int stIntersect(st_table *tbl1, st_table *tbl2);
50static int NoOfBitEncode(int n);
51static bdd_t * encodeOfInteger(mdd_manager *manager, array_t *varArray, int val);
52
53/**AutomaticEnd***************************************************************/
54
55
56/*---------------------------------------------------------------------------*/
57/* Definition of exported functions                                          */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Definition of internal functions                                          */
63/*---------------------------------------------------------------------------*/
64
65/**Function********************************************************************
66
67  Synopsis [Encode the states of the Automaton.]
68
69  Description []
70
71  SideEffects []
72
73  SeeAlso     []
74
75******************************************************************************/
76void
77BmcAutEncodeAutomatonStates(
78  Ntk_Network_t   *network,
79  Ltl_Automaton_t *automaton)
80{
81  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
82  lsGen               lsGen, lsGen1;
83  vertex_t            *vtx;
84  Ltl_AutomatonNode_t *node, *node1;
85  Ctlsp_Formula_t     *F;
86  mdd_t               *label;
87 
88  int                 i;
89
90  /*
91    Build the mdd of the labels of each automaton node
92   */
93  foreach_vertex(automaton->G, lsGen, vtx) {
94    node = (Ltl_AutomatonNode_t *) vtx->user_data;
95    if (node->Labels) {
96      label =  mdd_one(manager);
97      for (i=0; i<array_n(automaton->labelTable); i++) {
98        if (LtlSetGetElt(node->Labels, i)) {
99          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i);
100          label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
101        }
102      }
103      node->Encode = label;
104    }
105  }
106  /*
107    Encode automaton labels
108   */
109  foreach_vertex(automaton->G, lsGen, vtx) {
110    bdd_t *newVar = NULL;
111   
112    node = (Ltl_AutomatonNode_t *) vtx->user_data;
113    foreach_vertex(automaton->G, lsGen1, vtx) {
114      node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
115      if(node != node1){
116        if(newVar == NULL){
117          newVar = bdd_create_variable(manager);
118          node->Encode = bdd_and(node->Encode, newVar, 1, 1);
119        }
120        node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
121      }
122    }
123  }
124} /* BmcAutEncodeAutomatonStates() */
125
126
127/**Function********************************************************************
128
129  Synopsis [Encode the states of the Automaton.]
130
131  Description [The labels of each node in the automaton are
132  propositional and are asserted by state variables in the original
133  model. So, we uses these labels as part of the state encoding of the
134  automaton.  If two nodes cannot be uniquely specified, then we use
135  new variables]
136
137  SideEffects []
138
139  SeeAlso     []
140
141******************************************************************************/
142void
143BmcAutEncodeAutomatonStates2(
144  Ntk_Network_t   *network,
145  Ltl_Automaton_t *automaton)
146{
147  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
148  lsGen               lsGen, lsGen1;
149  vertex_t            *vtx;
150  Ltl_AutomatonNode_t *node, *node1;
151  Ctlsp_Formula_t     *F;
152  mdd_t               *label;
153 
154  int                 i;
155 
156  /*
157    Build the mdd for the labels of each automaton node.
158   */
159  foreach_vertex(automaton->G, lsGen, vtx) {
160    node = (Ltl_AutomatonNode_t *) vtx->user_data;
161    if (node->Labels) {
162      label =  mdd_one(manager);
163      for (i=0; i<array_n(automaton->labelTable); i++) {
164        if (LtlSetGetElt(node->Labels, i)) {
165          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i); 
166          label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
167        }
168      }
169      node->Encode = label;
170    }
171  }
172  /*
173    Three cases:
174      1- node and node1 are both = 1
175      2- node1 = 1
176      3- neither node nor nod1 equal to 1
177   */
178  foreach_vertex(automaton->G, lsGen, vtx) {
179    bdd_t *newVar = NULL;
180    st_table        *preState, *preState1;
181   
182    node = (Ltl_AutomatonNode_t *) vtx->user_data;
183    preState  = AutomatonVertexGetPreImg(automaton->G, vtx);
184
185    foreach_vertex(automaton->G, lsGen1, vtx) { 
186      node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
187      if(node != node1){
188        if (!mdd_is_tautology(mdd_and(node->Encode, node1->Encode, 1,1),0)){
189          preState1 = AutomatonVertexGetPreImg(automaton->G, vtx);
190          if (stIntersect(preState, preState1)){
191            if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
192              node->Encode = bdd_not(node1->Encode);
193            } else
194              if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
195                node1->Encode = bdd_not(node->Encode);
196              } else {
197                if(newVar == NULL){
198                  newVar = bdd_create_variable(manager);
199                }
200                node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
201                node->Encode = bdd_and(node->Encode, bdd_not(node1->Encode), 1, 1);
202              }
203          } else {
204            if(newVar == NULL){
205              newVar = bdd_create_variable(manager);
206              node->Encode = bdd_and(node->Encode, newVar, 1, 1);
207            }
208            node1->Encode = bdd_and(node1->Encode,  bdd_not(newVar), 1, 1);
209          }
210        }
211      }
212    }
213  }
214
215#if 0 
216  /*
217    Encode the automaton labels
218   */
219  foreach_vertex(automaton->G, lsGen, vtx) {
220    bdd_t               *newVar = NULL;
221    st_table            *nextStates;
222    Ltl_AutomatonNode_t *nextState;
223    st_generator        *stGen;
224   
225    node       = (Ltl_AutomatonNode_t *) vtx->user_data;
226    nextStates = AutomatonVertexGetImg(automaton->G, vtx);
227   
228    st_foreach_item(nextStates, stGen, (char **)&vtx, NIL(char *)) {
229      nextState = (Ltl_AutomatonNode_t *) vtx->user_data;
230
231      if(node != nextState){
232        if (!mdd_is_tautology(mdd_and(node->Encode, nextState->Encode, 1,1),0)){
233          printf("n%d intersects n%d\n", node->index, nextState->index);
234          if(newVar == NULL){
235            newVar = bdd_create_variable(manager);
236            /*node->Encode = bdd_and(node->Encode, newVar, 1, 1);*/
237          }
238          nextState->Encode = bdd_and(nextState->Encode, bdd_not(newVar), 1, 1);
239          node->Encode = bdd_and(node->Encode, bdd_not(nextState->Encode), 1, 1);
240        }
241      }
242    }
243  }
244#endif
245 
246} /* BmcAutEncodeAutomatonStates2() */
247
248/**Function********************************************************************
249
250  Synopsis [Encode the states of the Automaton.]
251
252  Description [The labels of each node in the automaton are
253  propositional and are asserted by state variables in the original
254  model. So, we uses these labels as part of the state encoding of the
255  automaton.  If two nodes cannot be uniquely specified, then we use
256  new variables]
257
258  SideEffects []
259
260  SeeAlso     []
261
262******************************************************************************/
263void
264BmcAutEncodeAutomatonStates3(
265  Ntk_Network_t   *network,
266  Ltl_Automaton_t *automaton)
267{
268  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
269  lsGen               lsGen;
270  st_generator        *stGen, *stGen1;
271  vertex_t            *vtx, *vtx1;
272  Ltl_AutomatonNode_t *node, *node1;
273  Ctlsp_Formula_t     *F;
274  bdd_t               *label;
275 
276  int                 i;
277  int                 noOfStates=0;
278  int                 noOfBits;
279  array_t             *varArray = array_alloc(bdd_t*,0);
280
281  /*
282    Build the bdd for the labels of each automaton node.
283   */
284  foreach_vertex(automaton->G, lsGen, vtx) {
285    node = (Ltl_AutomatonNode_t *) vtx->user_data;
286    if (node->Labels) {
287      noOfStates++;
288      label =  bdd_one(manager);
289      for (i=0; i<array_n(automaton->labelTable); i++) {
290        if (LtlSetGetElt(node->Labels, i)) {
291          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i); 
292          label = bdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
293        }
294      }
295      node->Encode = label;
296    }
297  }
298
299  st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
300    node = (Ltl_AutomatonNode_t *) vtx->user_data;
301    st_foreach_item(automaton->Init, stGen1, &vtx1, NULL) {
302      node1 = (Ltl_AutomatonNode_t *) vtx1->user_data;
303      if(node != node1){
304        if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
305              node->Encode = bdd_not(node1->Encode);
306        } else
307          if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
308            node1->Encode = bdd_not(node->Encode);
309          }
310      }
311    }
312  }
313
314  noOfBits = NoOfBitEncode(noOfStates);
315  for(i=0; i< noOfBits; i++){ 
316    array_insert_last(bdd_t*, varArray, bdd_create_variable(manager));
317  }
318  i=0;
319  foreach_vertex(automaton->G, lsGen, vtx) {
320    node = (Ltl_AutomatonNode_t *) vtx->user_data;
321    if (node->Labels) {
322      node->Encode = bdd_and(node->Encode, encodeOfInteger(manager, varArray, i), 1, 1);
323      i++;
324    }
325  }
326} /* BmcAutEncodeAutomatonStates3() */
327
328
329/**Function********************************************************************
330
331  Synopsis [Build BDD of the transition relation of the Automaton.]
332
333  Description []
334
335  SideEffects []
336
337  SeeAlso     []
338
339******************************************************************************/
340void
341BmcAutBuildTransitionRelation(
342  Ntk_Network_t   *network,
343  Ltl_Automaton_t *automaton)
344{
345  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
346  lsGen               lsGen;
347  st_generator        *stGen;
348  vertex_t            *vtx, *vtx1;
349  Ltl_AutomatonNode_t *state, *nextState;
350 
351 
352 
353  bdd_t               *nextStateBdd, *transitionRelation;
354  bdd_t               *initialState, *fairSet, *fairState;
355  int                 i;
356  bdd_t               *bddVar;
357  st_table            *nextStates;
358  var_set_t           *psSupport, *nsSupport;
359  st_table            *FairSet = 0;
360  array_t             *fairSetArray;
361
362  /*
363    psNsTable  (Bdd Id, bdd_t*)
364   */
365  st_table            *psNsTable = st_init_table(st_numcmp, st_numhash);
366  /*
367    nsPsTable  (BDD Id, BDD Id)
368   */
369  st_table            *nsPsTable = st_init_table(st_numcmp, st_numhash);
370
371  boolean             isComplemented;
372  int                 nodeIndex;
373 
374  /*
375    Initialization
376   */
377  transitionRelation = bdd_zero(manager);
378
379  /*
380    Build the transition relation
381   */
382  foreach_vertex(automaton->G, lsGen, vtx) {
383    state = (Ltl_AutomatonNode_t *) vtx->user_data;
384    /*
385      support is the set of the bddId of the bdd node in the support of the bdd function.
386    */
387    psSupport = bdd_get_support(state->Encode);
388    for(i=0; i<psSupport->n_elts; i++) {
389      if (var_set_get_elt(psSupport, i) == 1) {
390        /*
391          i is the bdd Id of the variable in the support of the function.
392        */
393        if (!st_lookup(psNsTable, (char *)(long) i, NULL)){
394          bddVar =  bdd_create_variable(manager);
395          nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
396          st_insert(psNsTable, (char *) (long) i,         (char *) bddVar);
397          st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
398        }
399      }
400    }
401    /*
402      Get the next states.
403     */
404    nextStates = AutomatonVertexGetImg(automaton->G, vtx);
405    st_foreach_item(nextStates, stGen, &vtx1, NULL) {
406      nextState = (Ltl_AutomatonNode_t *) vtx1->user_data;
407
408      nextStateBdd = bdd_dup(nextState->Encode);
409      nsSupport = bdd_get_support(nextStateBdd);
410      for(i=0; i<nsSupport->n_elts; i++) {
411        if (var_set_get_elt(nsSupport, i) == 1) {
412          bdd_t *tmp;
413
414          if (!st_lookup(psNsTable, (char *)(long)i, &bddVar)){
415            bddVar =  bdd_create_variable(manager);
416            nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
417            st_insert(psNsTable, (char *) (long) i,         (char *) bddVar);
418            st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
419          }       
420          tmp = nextStateBdd;
421          nextStateBdd = bdd_compose(nextStateBdd, bdd_get_variable(manager, i), bddVar);
422          bdd_free(tmp);
423        }
424      }
425      transitionRelation = bdd_or(transitionRelation, bdd_and(state->Encode, nextStateBdd,1 ,1) ,1 ,1);
426     
427    } /* for each next states*/
428  } /* for each present state */
429
430  fairSetArray = array_alloc(bdd_t*, 0);
431  fairSet = 0;
432  if (lsLength(automaton->Fair) != 0) {
433    fairSet = bdd_zero(manager);
434    lsForEachItem(automaton->Fair, lsGen, FairSet) {
435      fairState = bdd_zero(manager);
436      st_foreach_item(FairSet, stGen, &vtx, NULL) {
437        state = (Ltl_AutomatonNode_t *) vtx->user_data;
438        fairState = bdd_or(fairState, state->Encode,1,1);
439      }
440      array_insert_last(bdd_t*, fairSetArray, fairState); 
441      fairSet = bdd_or(fairSet, fairState,1,1);
442    }
443  }
444  initialState = bdd_zero(manager);
445  st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
446    state = (Ltl_AutomatonNode_t *) vtx->user_data;
447    initialState = bdd_or(initialState, state->Encode, 1, 1);
448  }
449  automaton->transitionRelation  = transitionRelation;
450  automaton->initialStates       = initialState;
451  automaton->fairSets            = fairSet;
452  automaton->psNsTable           = psNsTable;
453  automaton->nsPsTable           = nsPsTable;
454  automaton->fairSetArray        = fairSetArray;
455 
456} /* BmcAutBuildTransitionRelation() */
457
458
459/**Function********************************************************************
460
461  Synopsis [Build MDD for a propositional formula.]
462
463  Description [Build MDD for a propositional formula. Returns NIL if the conversion
464  fails. The calling application is responsible for freeing the returned MDD.]
465
466  SideEffects []
467
468  SeeAlso     []
469
470******************************************************************************/
471mdd_t *
472BmcAutBuildMddForPropositionalFormula(
473   Ntk_Network_t   *network,
474   Ltl_Automaton_t *automaton,
475   Ctlsp_Formula_t *formula)
476{
477  mdd_manager     *manager = Ntk_NetworkReadMddManager(network);
478  mdd_t           *left, *right, *result;
479 
480
481  if (formula == NIL(Ctlsp_Formula_t)) {
482    return NIL(mdd_t);
483  }
484  if (formula->type == Ctlsp_TRUE_c){
485    return bdd_one(manager);
486  }
487  if (formula->type == Ctlsp_FALSE_c){
488    return  mdd_zero(manager);
489  }
490 
491  if (!Ctlsp_isPropositionalFormula(formula)) {
492    (void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
493    fprintf(vis_stdout, "\nFormula: ");
494    Ctlsp_FormulaPrint(vis_stdout, formula);
495    fprintf(vis_stdout, "\n");
496    return NIL(mdd_t);
497  }
498  /*
499    Atomic proposition.
500   */
501  if (formula->type == Ctlsp_ID_c){
502    int       is_complemented;
503    bdd_node  *funcNode;
504   
505    result   =  BmcModelCheckAtomicFormula(Fsm_NetworkReadOrCreateFsm(network), formula);
506    funcNode = bdd_get_node(result, &is_complemented);
507    if(is_complemented){
508      funcNode = bdd_not_bdd_node(funcNode);
509    }
510    return result;
511  }
512  /*
513    right can be NIL(mdd_t) for unery operators, but left can't be  NIL(mdd_t)
514   */
515  left  = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->left);
516  if (left == NIL(mdd_t)){
517    return NIL(mdd_t);
518  } 
519  right = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->right);
520  /*assert(right !=  NIL(mdd_t)); */
521  switch(formula->type) {
522    case Ctlsp_NOT_c:
523      result = mdd_not(left);
524      break;
525    case Ctlsp_OR_c:
526      result = mdd_or(left, right, 1, 1);
527      break;
528    case Ctlsp_AND_c:
529      result = mdd_and(left, right, 1, 1);
530      break;
531    case Ctlsp_THEN_c:
532      result = mdd_or(left, right, 0, 1); 
533      break;
534    case Ctlsp_EQ_c:
535      result = mdd_xnor(left, right);
536      break;
537    case Ctlsp_XOR_c:
538      result = mdd_xor(left, right);
539      break;
540  default:
541    /*
542      return NIL(mdd_t) if the type is not supported
543     */
544    fail("Unexpected type");
545  }
546  return result;
547}
548
549/**Function********************************************************************
550
551  Synopsis [Generate CNF for a given BDD function.]
552
553  Description [Generate CNF for a BDD function.  This function first
554  negates the BDD function, and then generates the CNF corresponding
555  to the OFF-set of the negated function.  If the BDD node is a next
556  state variable, we use the BDD index of the present state variable
557  corresponding to this variable.  We could do this by searching the
558  nsPSTable.  If trans ==1, this function generates a CNF for a
559  transition from current state to next state, otherwise it generates
560  CNF for NO transition.
561
562  The function calling this function must add a unit clause to set the
563  returned value to positive (for function to be true) or negative
564  (for function to be false).
565
566  ]
567 
568  SideEffects []
569
570  SeeAlso     []
571 
572******************************************************************************/
573int 
574BmcAutGenerateCnfForBddOffSet(
575   bdd_t          *function,
576   int             current,
577   int             next,
578   BmcCnfClauses_t *cnfClauses,
579   st_table        *nsPsTable)
580{
581  bdd_manager *bddManager = bdd_get_manager(function);
582  bdd_node    *node, *funcNode;
583  int         is_complemented;
584  bdd_gen     *gen;
585  int         varIndex; 
586  array_t     *tmpClause;
587  array_t     *cube;
588  int         i, value;
589  int         state = current;
590  bdd_t       *bddFunction;
591  bdd_t       *newVar;
592
593  int         total=0, ndc=0;
594  float       per;
595
596  if (function == NULL){
597    return 0;
598  }
599 
600  funcNode = bdd_get_node(function, &is_complemented);
601 
602  if (bdd_is_constant(funcNode)){
603    if (is_complemented){
604      /* add an empty clause to indicate FALSE (un-satisfiable)*/
605      BmcAddEmptyClause(cnfClauses);
606    }
607    /*bdd_free(bddFunction);
608      bdd_free(newVar);*/
609    return 0;
610  }
611
612  newVar = bdd_create_variable(bddManager);
613  bddFunction = bdd_xnor(newVar, function);
614  bddFunction = bdd_not(bddFunction);
615
616  foreach_bdd_cube(bddFunction, gen, cube){
617    tmpClause = array_alloc(int,0);
618    arrayForEachItem(int, cube, i, value) {
619      total++;
620      if (value != 2){
621        int j;
622
623        ndc++;
624        /*
625          If the BDD varaible is a next state varaible, we use the corresponding
626          current state varaible but with next state index.
627         */
628       
629        if (nsPsTable && st_lookup_int(nsPsTable, (char *)(long)i, &j)){
630          node = bdd_bdd_ith_var(bddManager, j);
631          state = next;
632        } else {
633          node = bdd_bdd_ith_var(bddManager, i);
634          state = current;
635        }
636        varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), state, cnfClauses);
637        if (value == 1){
638          varIndex = -varIndex; 
639        }
640        array_insert_last(int, tmpClause, varIndex);
641      }
642    }
643    BmcCnfInsertClause(cnfClauses, tmpClause);
644    array_free(tmpClause);
645  }/* foreach_bdd_cube() */
646  varIndex  = BmcGetCnfVarIndexForBddNode(bddManager,
647                                       bdd_regular(bdd_get_node(newVar, &is_complemented)),
648                                       current, cnfClauses);
649  per = ((float) ((float)ndc/(float)total))*100; 
650  return (varIndex);
651} /* BmcAutGenerateCnfForBddOffSet() */
652
653
654/**Function********************************************************************
655
656  Synopsis [Alloc Memory for BmcCheckForTermination_t]
657
658  SideEffects []
659
660  SeeAlso []
661******************************************************************************/
662BmcCheckForTermination_t *
663BmcAutTerminationAlloc(
664  Ntk_Network_t   *network,
665  Ctlsp_Formula_t *ltlFormula,
666  array_t         *constraintArray)
667{
668  BmcCheckForTermination_t  *result = ALLOC(BmcCheckForTermination_t, 1);
669  Ltl_Automaton_t           *automaton;
670  LtlMcOption_t             *ltlOptions = LtlMcOptionAlloc();
671 
672  if (!result){
673    return result;
674  }
675  /*
676    Build the Buechi Automaton for the negation of the LTL formula.
677  */
678  ltlOptions->algorithm    = Ltl2Aut_WRING_c;
679  ltlOptions->rewriting    = TRUE;
680  ltlOptions->prunefair    = TRUE;
681  ltlOptions->iocompatible = TRUE;
682  ltlOptions->directsim    = TRUE;
683  ltlOptions->reversesim   = TRUE;
684  ltlOptions->verbosity    = McVerbosityNone_c;
685  ltlOptions->noStrengthReduction = 1;
686 
687  automaton  = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
688  assert(automaton != NIL(Ltl_Automaton_t));
689 
690  /*BmcAutEncodeAutomatonStates(network, automaton); */
691  /*mcAutEncodeAutomatonStates2(network, automaton);*/
692  BmcAutEncodeAutomatonStates3(network, automaton);
693  BmcAutBuildTransitionRelation(network, automaton);
694   
695  LtlMcOptionFree(ltlOptions);
696
697  result->k = 0;
698  result->m = -1;
699  result->n = -1;
700  result->checkLevel = 0;
701  result->action = 0;
702  result->automaton = automaton;
703
704  result->externalConstraints  = NIL(Ctlsp_Formula_t);
705  if(constraintArray != NIL(array_t)){
706    Ctlsp_Formula_t *formula1, *formula2;
707    int              j;
708   
709    formula1 = NIL(Ctlsp_Formula_t);
710    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula2) {
711      formula2 = Ctlsp_FormulaDup(formula2);
712      if(formula1 == NIL(Ctlsp_Formula_t)) {
713        formula1 = formula2;
714      } else {
715        formula1 =  Ctlsp_FormulaCreate(Ctlsp_OR_c, formula1, formula2);
716      }
717    }
718    result->externalConstraints = formula1;
719  }
720  result->internalConstraints = automaton->fairSets;
721  return result;
722}
723
724/**Function********************************************************************
725
726  Synopsis [Convert LTL to Automaton]
727
728  Description []
729  SideEffects []
730
731  SeeAlso []
732******************************************************************************/
733Ltl_Automaton_t *
734BmcAutLtlToAutomaton(
735  Ntk_Network_t   *network,
736  Ctlsp_Formula_t *ltlFormula)
737{
738  Ltl_Automaton_t  *automaton;
739  LtlMcOption_t    *ltlOptions = LtlMcOptionAlloc();
740 
741  /*
742    Build the Buechi Automaton for the negation of the LTL formula.
743  */
744  ltlOptions->algorithm    = Ltl2Aut_WRING_c;
745  ltlOptions->rewriting    = TRUE;
746  ltlOptions->prunefair    = TRUE;
747  ltlOptions->iocompatible = TRUE;
748  ltlOptions->directsim    = TRUE;
749  ltlOptions->reversesim   = TRUE;
750  ltlOptions->verbosity    = McVerbosityNone_c;
751  ltlOptions->noStrengthReduction = 1;
752 
753  automaton  = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
754  assert(automaton != NIL(Ltl_Automaton_t));
755 
756  return automaton;
757}
758
759
760/**Function********************************************************************
761
762  Synopsis [Free BmcCheckForTermination_t.]
763
764  SideEffects []
765
766  SeeAlso []
767******************************************************************************/
768void
769BmcAutTerminationFree(
770  BmcCheckForTermination_t *result)
771{
772  LtlTableau_t    *tableau;
773  Ltl_Automaton_t *automaton = result->automaton;
774   
775  tableau = automaton->tableau; 
776  Ltl_AutomatonFree((gGeneric) automaton);
777  LtlTableauFree(tableau);
778  if(result->externalConstraints  != NIL(Ctlsp_Formula_t)){
779    Ctlsp_FormulaFree(result->externalConstraints);
780  }
781 
782  FREE(result);
783}
784
785
786/*---------------------------------------------------------------------------*/
787/* Definition of static functions                                            */
788/*---------------------------------------------------------------------------*/
789
790/**Function********************************************************************
791
792  Synopsis [Return the image of the given vertex in the hash table.]
793
794  SideEffects [Result should be freed by the caller.]
795
796******************************************************************************/
797static st_table *
798AutomatonVertexGetImg(
799  graph_t *G,
800  vertex_t *vtx)
801{
802  lsList Img;
803  lsGen lsgen;
804  edge_t *e;
805  vertex_t *s;
806  st_table *uTable;
807
808  Img = g_get_out_edges(vtx);
809
810  uTable = st_init_table(st_ptrcmp, st_ptrhash);
811  lsForEachItem(Img, lsgen, e) {
812    s = g_e_dest(e);
813    st_insert(uTable, (char *) s, (char *) s);
814  }
815
816  return uTable;
817}
818
819/**Function********************************************************************
820
821  Synopsis [Return the pre-image of the given vertex in the hash table.]
822
823  SideEffects [Result should be freed by the caller.]
824
825******************************************************************************/
826static st_table *
827AutomatonVertexGetPreImg(
828  graph_t *G,
829  vertex_t *vtx)
830{
831  lsList preImg;
832  lsGen lsgen;
833  edge_t *e;
834  vertex_t *s;
835  st_table *uTable;
836
837  preImg = g_get_in_edges(vtx);
838
839  uTable = st_init_table(st_ptrcmp, st_ptrhash);
840  lsForEachItem(preImg, lsgen,  e) {
841    s = g_e_source(e);
842    st_insert(uTable, (char *) s, (char *) s);
843  }
844 
845  return uTable;
846}
847
848/**Function********************************************************************
849
850  Synopsis [Return 1 if tbl1 and tbl2 two intersects.]
851
852  SideEffects []
853
854******************************************************************************/
855static int
856stIntersect(
857  st_table *tbl1,
858  st_table *tbl2)
859{
860  st_generator *stgen;
861  vertex_t *vtx;
862
863  st_foreach_item(tbl1, stgen, &vtx, NULL) {
864    if (st_is_member(tbl2,(char *)vtx)) {
865      st_free_gen(stgen);
866      return 1;
867    }
868  }
869  return 0;
870}
871
872/**Function********************************************************************
873
874  Synopsis    [Returns no. of Bit encoding needed for n]
875
876  Description []
877
878  SideEffects []
879
880  SeeAlso     []
881
882******************************************************************************/
883static int
884NoOfBitEncode(
885   int n)
886{
887    int i = 0;
888    int j = 1;
889
890    if (n < 2) return 1; /* Takes care of value <= 1 */
891
892    while (j < n) {
893        j = j * 2;
894        i++;
895    }
896    return i;
897}
898
899/**Function********************************************************************
900
901  Synopsis    [Returns no. of Bit encoding needed for n]
902
903  Description []
904
905  SideEffects []
906
907  SeeAlso     []
908
909******************************************************************************/
910static bdd_t *
911encodeOfInteger(
912  mdd_manager *manager,
913  array_t *varArray,
914  int val)
915{
916  int i;
917  bdd_t *returnValue =  mdd_one(manager);
918  int tmp = val;
919  bdd_t  *var;
920
921  for(i=0; i< array_n(varArray); i++){
922    var = array_fetch(bdd_t*, varArray, i);
923    if(tmp%2 == 0){
924      returnValue = bdd_and(returnValue, var, 1, 0); 
925    } else {
926      returnValue = bdd_and(returnValue, var, 1, 1);
927    }
928    tmp = tmp / 2;
929  }
930  return returnValue;
931}
932
Note: See TracBrowser for help on using the repository browser.