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

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

vis2.3
File size: 26.9 KB
RevLine 
[14]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.