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

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

vis2.3
File size: 26.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltlSet.c]
4
5  PackageName [ltl]
6
7  Synopsis    [Set/Pair/Cover Manipulation functions used in the ltl package.]
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
19static char rcsid[] UNUSED = "$Id: ltlSet.c,v 1.25 2005/04/28 08:45:27 bli Exp $";
20
21/* Set manipulation functions.
22 * 
23 * Set is a term -- the conjunction of literals. In the Ltl->Aut process, a
24 * literal can be an propositional formula, a X-formula and its negation.
25 * In order to interpret a Set, we need to corresponding arrays: Table and
26 * Negate. An '1' in the i-th position of the Set means "Table[i] is contained
27 * in the Set", and the negation of "Table[i]" is "Negate[i]".
28 *
29 * Cover is a lsList of terms -- the "union" of all the items (product terms).
30 *
31 * Pair is a data structure to hold a 'ordered pair of items': (First, Second).
32 */
33
34/*---------------------------------------------------------------------------*/
35/* Constant declarations                                                     */
36/*---------------------------------------------------------------------------*/
37
38/*---------------------------------------------------------------------------*/
39/* Structure declarations                                                    */
40/*---------------------------------------------------------------------------*/
41
42/*---------------------------------------------------------------------------*/
43/* Type declarations                                                         */
44/*---------------------------------------------------------------------------*/
45
46/*---------------------------------------------------------------------------*/
47/* Variable declarations                                                     */
48/*---------------------------------------------------------------------------*/
49
50/*---------------------------------------------------------------------------*/
51/* Macro declarations                                                        */
52/*---------------------------------------------------------------------------*/
53
54/**AutomaticStart*************************************************************/
55
56/*---------------------------------------------------------------------------*/
57/* Static function prototypes                                                */
58/*---------------------------------------------------------------------------*/
59
60
61/**AutomaticEnd***************************************************************/
62
63
64/*---------------------------------------------------------------------------*/
65/* Definition of exported functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis    [Allocate the set data structure.]
71
72  Description []
73
74  SideEffects [The result should be freed by the caller.]
75
76******************************************************************************/
77LtlSet_t *
78LtlSetNew(
79  int size)
80{
81  LtlSet_t *set = ALLOC(LtlSet_t, 1);
82   
83  set->e = var_set_new(size);
84
85  return set;
86}
87
88/**Function********************************************************************
89
90  Synopsis    [Free the data structure associated with 'set'.]
91
92  Description []
93
94  SideEffects []
95
96******************************************************************************/
97void
98LtlSetFree(
99  LtlSet_t *set)
100{
101  var_set_free(set->e);
102  FREE(set);
103}
104
105/**Function********************************************************************
106
107  Synopsis    [Allocate the new set and copy the content of the given set.]
108
109  Description []
110
111  SideEffects [The result should be freed by the caller.]
112
113******************************************************************************/
114LtlSet_t *
115LtlSetCopy(
116  LtlSet_t *from)
117{
118  LtlSet_t *set = ALLOC(LtlSet_t, 1);
119 
120  set->e = var_set_copy(from->e);
121 
122  return set;
123}
124
125/**Function********************************************************************
126
127  Synopsis    [Assign the content of 'from' to set 'to'.]
128
129  Description []
130
131  SideEffects [set 'to' is changed.]
132
133******************************************************************************/
134void
135LtlSetAssign(
136  LtlSet_t *to,
137  LtlSet_t *from)
138{
139  var_set_assign(to->e, from->e);
140}
141
142/**Function********************************************************************
143
144  Synopsis    [Return 1 if the two sets have the same content.]
145
146  Description []
147
148  SideEffects []
149
150******************************************************************************/
151int
152LtlSetEqual(
153  LtlSet_t *s1,
154  LtlSet_t *s2)
155{
156  return var_set_equal(s1->e, s2->e);
157}
158
159
160/**Function********************************************************************
161
162  Synopsis    [Return how many bit is set to 1 in the given set.]
163
164  Description []
165
166  SideEffects []
167
168******************************************************************************/
169int
170LtlSetCardinality(
171  LtlSet_t *set)
172{
173  return (var_set_n_elts(set->e));
174}
175
176/**Function********************************************************************
177
178  Synopsis    [Return -1/0/+1 when 's1' has more/equal/less cardinality than
179  's2'.]
180
181  Description []
182
183  SideEffects []
184
185******************************************************************************/
186int
187LtlSetCompareCardinality(
188  const void *p1,
189  const void *p2)
190{
191  LtlSet_t **s1 = (LtlSet_t **) p1;
192  LtlSet_t **s2 = (LtlSet_t **) p2;
193  int c1;
194  int c2;
195 
196  c1 = LtlSetCardinality(*s1);
197  c2 = LtlSetCardinality(*s2);
198 
199  if (c1 < c2)
200    return -1;
201  else if (c1 == c2)
202    return 0;
203  else
204    return +1;
205}
206
207/**Function********************************************************************
208
209  Synopsis    [Return 1 iff the set contains both 'F' and '!F'.]
210
211  Description []
212
213  SideEffects []
214
215******************************************************************************/
216int
217LtlSetIsContradictory(
218  LtlSet_t *set,
219  array_t *Negate)
220{
221  int i, negi;
222  int flag = 0;
223
224  for (i=0; i<array_n(Negate); i++) {
225    if (LtlSetGetElt(set, i)) {
226      negi = array_fetch(int, Negate, i);
227      if (LtlSetGetElt(set, negi)) {
228        flag = 1;
229        break;
230      }
231    }
232  }
233 
234  return flag;
235}
236
237/**Function********************************************************************
238
239  Synopsis    [Return 1 iff 'large' includes 'small'.]
240
241  Description []
242
243  SideEffects []
244
245******************************************************************************/
246int
247LtlSetInclude(
248  LtlSet_t *large,
249  LtlSet_t *small)
250{
251  var_set_t *neg_large = var_set_not(var_set_copy(large->e),large->e);
252  int result = ! var_set_intersect(small->e, neg_large);
253  var_set_free(neg_large);
254 
255  return result;
256}
257
258/**Function********************************************************************
259
260  Synopsis    [Union the two sets 'from1' and 'from2', and assign to set 'to'.]
261
262  Description []
263
264  SideEffects [set 'to' is changed.]
265
266******************************************************************************/
267void
268LtlSetOR(
269  LtlSet_t *to,
270  LtlSet_t *from1,
271  LtlSet_t *from2)
272{
273  var_set_or(to->e, from1->e, from2->e);
274}
275
276/**Function********************************************************************
277
278  Synopsis    [Clear all bits in the set.]
279
280  Description []
281
282  SideEffects [The set is changed.]
283
284******************************************************************************/
285void
286LtlSetClear(
287  LtlSet_t *set)
288{
289  var_set_clear(set->e);
290}
291
292/**Function********************************************************************
293
294  Synopsis    [Set the bit indicated by 'index'.]
295
296  Description []
297
298  SideEffects [The set is changed.]
299
300******************************************************************************/
301void
302LtlSetSetElt(
303  LtlSet_t *set,
304  int index)
305{
306  var_set_set_elt(set->e, index);
307}
308
309/**Function********************************************************************
310
311  Synopsis    [Clear the bit indicated by 'index'.]
312
313  Description []
314
315  SideEffects [The set is changed.]
316
317******************************************************************************/
318void
319LtlSetClearElt(
320  LtlSet_t *set,
321  int index)
322{
323  var_set_clear_elt(set->e, index);
324}
325
326/**Function********************************************************************
327
328  Synopsis    [Return the value of the bit indicated by 'index'.]
329
330  Description []
331
332  SideEffects [The set is changed.]
333
334******************************************************************************/
335int
336LtlSetGetElt(
337  LtlSet_t *set,
338  int index)
339{
340  return var_set_get_elt(set->e,index);
341}
342
343/**Function********************************************************************
344
345  Synopsis    [Return 1 if the set is empty.]
346
347  Description []
348
349  SideEffects []
350
351******************************************************************************/
352int
353LtlSetIsEmpty(
354  LtlSet_t *set)
355{
356  return var_set_is_empty(set->e);
357}
358
359/**Function********************************************************************
360
361  Synopsis    [Return the set in the list that matches the given set.]
362
363  Description [Null will be return if there does not exist a match set.]
364
365  SideEffects []
366
367******************************************************************************/
368LtlSet_t *
369LtlSetIsInList(
370  LtlSet_t *set,
371  lsList list)
372{
373  lsGen gen;
374  lsGeneric data;
375  LtlSet_t *s = NIL(LtlSet_t);
376  int flag = 0;
377 
378  lsForEachItem(list, gen, data) {
379    s = (LtlSet_t *) data;
380    if ( var_set_equal(s->e, set->e) ) {
381      flag = 1;
382      lsFinish(gen);
383      break;
384    }
385  }
386 
387  return flag? s: NIL(LtlSet_t);
388}
389   
390/**Function********************************************************************
391
392  Synopsis    [Transform the given set to the label set and return it.]
393
394  Description [The given set may contain all the 'elementary formulae'. Its
395  table and negation are 'tableau->abTable' and 'tableau->abTableNegate'.
396 
397  The label set contain only the propositional formulae and their
398  negations. Its table and negation array are 'labelTable' and 'labelNegate'.
399
400  The above two table could have been the same, but we choose to implement
401  them differently: Since labelTable might be smaller than abTable, it will
402  make the boolean minimization based on it faster.]
403
404  SideEffects [The result should be freed by the caller.]
405
406******************************************************************************/
407LtlSet_t *
408LtlSetToLabelSet(
409  LtlTableau_t *tableau,
410  LtlSet_t *set)
411{
412  int i;
413  LtlSet_t *vset = LtlSetNew(tableau->labelIndex);
414  Ctlsp_Formula_t *F;
415 
416  for (i=0; i<tableau->abIndex; i++) {
417    if (var_set_get_elt(set->e, i)) {
418      F = tableau->abTable[i].F;
419      if (Ctlsp_LtlFormulaIsPropositional(F)&&
420          Ctlsp_FormulaReadType(F) != Ctlsp_TRUE_c &&
421          Ctlsp_FormulaReadType(F) != Ctlsp_FALSE_c)
422        var_set_set_elt(vset->e, 
423                        Ctlsp_FormulaReadLabelIndex(tableau->abTable[i].F));
424    }
425  }
426 
427  return vset;
428}
429
430/**Function********************************************************************
431
432  Synopsis    [Print all the 'elementary formulae' contained in the set.]
433
434  Description [Assume the set is based on the index table 'tableau->abTable'.]
435
436  SideEffects []
437
438******************************************************************************/
439void
440LtlSetPrint(
441  LtlTableau_t *tableau,
442  LtlSet_t *set)
443{
444  int i;
445 
446  fprintf(vis_stdout, "{ ");
447  for (i=0; i<tableau->abIndex; i++) {
448    if (LtlSetGetElt(set, i)) {
449      Ctlsp_FormulaPrint(vis_stdout, tableau->abTable[i].F);
450      fprintf(vis_stdout, "; ");
451    }
452  }
453  fprintf(vis_stdout, " }");
454}
455
456/**Function********************************************************************
457
458  Synopsis    [Print all index that are set in the set.]
459
460  Description [The length of the set should be provided.]
461 
462  SideEffects []
463
464******************************************************************************/
465void
466LtlSetPrintIndex(
467  int length,
468  LtlSet_t *set)
469{
470  int i;
471 
472  fprintf(vis_stdout, "{ ");
473  for (i=0; i<length; i++) {
474    if (LtlSetGetElt(set, i)) {
475      fprintf(vis_stdout, " %d ", i);
476    }
477  }
478  fprintf(vis_stdout, " }\n");
479}
480
481
482/**Function********************************************************************
483
484  Synopsis    [Allocate the data struture for 'pair'.]
485
486  Description []
487 
488  SideEffects []
489
490******************************************************************************/
491LtlPair_t *
492LtlPairNew(
493  char *First,
494  char *Second)
495{
496  LtlPair_t *pair = ALLOC(LtlPair_t, 1);
497
498  pair->First = First;
499  pair->Second= Second;
500  return pair;
501}
502
503/**Function********************************************************************
504
505  Synopsis    [Free the LtlPair_t data struture.]
506
507  Description []
508 
509  SideEffects []
510
511******************************************************************************/
512void
513LtlPairFree(
514  LtlPair_t *pair)
515{
516  FREE(pair);
517}
518
519/**Function********************************************************************
520
521  Synopsis    [Return a hash key for the given pair.]
522
523  Description [The key is based on the content. Thus two pair with the same
524  content (not necessarily the same pointer) have the same hash key.]
525 
526  SideEffects []
527
528******************************************************************************/
529int
530LtlPairHash(
531  char *key,
532  int modulus)
533{
534  LtlPair_t *pair = (LtlPair_t *) key;
535 
536  return (int) ((((unsigned long) pair->First >>2) +
537                 ((unsigned long) pair->Second>>4)) % modulus);
538}
539
540/**Function********************************************************************
541
542  Synopsis    [Return -1/0/+1 when the key1 is greater/equal/less than key2.]
543
544  Description [For two keys with the same content, they are equal.]
545 
546  SideEffects []
547
548******************************************************************************/
549int 
550LtlPairCompare(
551  const char *key1,
552  const char *key2)
553{
554  LtlPair_t *pair1 = (LtlPair_t *) key1;
555  LtlPair_t *pair2 = (LtlPair_t *) key2;
556 
557  assert(key1 != NIL(char));
558  assert(key2 != NIL(char));
559
560  if ((pair1->First == pair2->First) && (pair1->Second == pair2->Second))
561    return 0;
562  else if (pair1->First >= pair2->First && pair1->Second >= pair2->Second)
563    return 1;
564  else
565    return -1;
566}
567
568/**Function********************************************************************
569
570  Synopsis    [Print the pair as index pair.]
571
572  Description []
573 
574  SideEffects []
575
576******************************************************************************/
577void
578LtlPairPrint(
579  LtlPair_t *pair)
580{
581  vertex_t *first = (vertex_t *) pair->First;
582  vertex_t *second= (vertex_t *) pair->Second;
583  Ltl_AutomatonNode_t *node1 = (Ltl_AutomatonNode_t *) first->user_data;
584  Ltl_AutomatonNode_t *node2 = (Ltl_AutomatonNode_t *) second->user_data;
585
586  fprintf(vis_stdout, " (n%d, n%d) ", node1->index, node2->index);
587}
588
589/**Function********************************************************************
590
591  Synopsis    [Print the cover as a set of index.]
592
593  Description []
594 
595  SideEffects []
596
597******************************************************************************/
598void
599LtlCoverPrintIndex(
600  int length,
601  lsList cover)
602{
603  int first = 1;
604  lsGen gen;
605  LtlSet_t *set;
606
607  fprintf(vis_stdout, "{ ");
608  lsForEachItem(cover, gen, set) {
609    if (first)    first = 0;
610    else                  fprintf(vis_stdout, " + ");
611    LtlSetPrintIndex(length, set);
612  }
613  fprintf(vis_stdout, " }");
614}
615
616
617/**Function********************************************************************
618
619  Synopsis    [Return the 'Complete Sum' of the cover by iterated consensus.]
620
621  Description [The cover is represented by a list of sets (product terms).]
622 
623  SideEffects [The result should be freed by the caller. The given cover is
624  NOT changed.]
625
626******************************************************************************/
627lsList
628LtlCoverCompleteSum(
629  lsList Cover,
630  array_t *Negate)
631{
632  lsList cs = lsCreate();
633  lsGen lsgen;
634  array_t *products = array_alloc(LtlSet_t *, 0);
635  LtlSet_t *term, *term1, *term2, *consensus;
636  long i, j, k, flag;
637  st_table *removed, *consList;  /* removed, and consensus generated */
638 
639  /* Check and remove contraditory terms -- containing both F and !F */
640  lsForEachItem(Cover, lsgen, term) {
641    if (!LtlSetIsContradictory(term, Negate))
642      array_insert_last(LtlSet_t *, products, term);
643  }
644 
645  /* Sort terms by increasing number of literals */
646  array_sort(products, LtlSetCompareCardinality);
647
648  /* Check tautologous term */
649  term = array_fetch(LtlSet_t *, products, 0);
650  if (LtlSetCardinality(term) == 0) {
651    lsNewEnd(cs, (lsGeneric) LtlSetCopy(term), (lsHandle *)0);
652    array_free(products);
653    return cs;
654  }
655
656  /* In the following, we won't change 'products'. Instead, if a term need to
657   * be removed, we will store it (its index number) in the hash table
658   */
659  removed = st_init_table(st_ptrcmp, st_ptrhash);
660  /* In the following, we might generate some new consensus terms, and we will
661   * store them (LtlSet_t) in the list
662   */
663  consList = st_init_table(st_ptrcmp, st_ptrhash);
664 
665  /* Check terms for single-cube containment. Rely on ordering for efficiency.
666   * A term can only be contained by another term with fewer literals
667   */
668  for (i=array_n(products)-1; i>0; i--) {
669    term = array_fetch(LtlSet_t *, products, i);
670    for (j=0; j<i; j++) {
671      term1 = array_fetch(LtlSet_t *, products, j);
672      if (LtlSetCardinality(term1) == LtlSetCardinality(term)) break;
673      if (LtlSetInclude(term, term1)) {
674        /* remember the removed term */
675        st_insert(removed, (char *)i, (char *)i);
676        break;
677      }
678    }
679  }
680 
681  /* Now do iterated consensus */
682  for (i=1; i<array_n(products); i++) {
683    if (st_is_member(removed, (char *)i)) continue;
684    term = array_fetch(LtlSet_t *, products, i);
685     
686    for (j=0; j<i; j++) {
687      if (st_is_member(removed, (char *)j)) continue;     
688      term1 = array_fetch(LtlSet_t *, products, j);
689     
690      consensus = LtlSetConsensus(term, term1, Negate);
691         
692      if (consensus) {
693        /* should store consensus ? */
694        flag = 1; 
695        for(k=0; k<array_n(products); k++) {
696          if (st_is_member(removed, (char *)k)) continue;
697          term2 = array_fetch(LtlSet_t *, products, k);
698         
699          if (LtlSetInclude(consensus, term2)) {
700            /* redudant new term */
701            flag = 0; 
702            break;
703          } 
704          if (LtlSetInclude(term2, consensus)) {
705            /* remember the removed term2 (k)  */
706            st_insert(removed, (char *)k, (char *)k);
707          }
708        }
709        if (flag) {
710          array_insert_last(LtlSet_t *, products, consensus);
711          st_insert(consList, consensus, (char *)0);
712        }else
713          LtlSetFree(consensus);
714      }
715    }
716  }
717
718#if 0
719  if (0) {
720    fprintf(vis_stdout, "\nLtlCompleteSum: products = {  ");
721    for(i=0; i<array_n(products); i++) {
722      term = array_fetch(LtlSet_t *, products, i);
723      LtlSetPrintIndex(array_n(Negate), term);
724    }
725    fprintf(vis_stdout, "}\nLtlCompleteSum: removed = {  ");
726    st_foreach_item(removed, stgen, &i, NIL(char *)) {
727      term = array_fetch(LtlSet_t *, products, i);
728      LtlSetPrintIndex(array_n(Negate), term);
729    }
730    fprintf(vis_stdout, "}\nLtlCompleteSum: consList = {  ");
731    st_foreach_item(consList, stgen, &term, NIL(char *)) {
732      LtlSetPrintIndex(array_n(Negate), term);
733    }
734    fprintf(vis_stdout, "}\n");
735   
736    fflush(vis_stdout);
737  }
738#endif     
739 
740  arrayForEachItem(LtlSet_t *, products, i, term) {
741    if (!st_is_member(removed, (char *)i)) {
742      /* put it into the complete sum list */
743      if (!st_is_member(consList, term))
744        term1 = LtlSetCopy(term);
745      else
746        term1 = term;
747      lsNewEnd(cs, (lsGeneric) term1, NIL(lsHandle));
748    }else {
749      /* it has been removed. If it was allocated locally, free it */
750      if (st_is_member(consList, term))
751        LtlSetFree(term);
752    }
753  }
754
755  array_free(products);
756  st_free_table(removed);
757  st_free_table(consList);
758
759  return cs;
760}
761
762
763/**Function********************************************************************
764
765  Synopsis    [Return the consensus of two given set (product terms).]
766
767  Description [If the consesus does not exist, return a null pointer.]
768 
769  SideEffects [The result should be freed by the caller.]
770
771******************************************************************************/
772LtlSet_t *
773LtlSetConsensus(
774  LtlSet_t *first,
775  LtlSet_t *second,
776  array_t *Negate)
777{
778  LtlSet_t *consensus = LtlSetNew(array_n(Negate));
779  int pivot = -1;
780  int literal, complement;
781 
782  for (literal=0; literal<array_n(Negate); literal++) {
783    if (LtlSetGetElt(first, literal)) {
784      complement = array_fetch(int, Negate, literal);
785      if (LtlSetGetElt(second, complement)) {
786        if (pivot != -1) {
787          LtlSetFree(consensus);
788          return NIL(LtlSet_t);
789        }else {
790          pivot = complement;
791        }
792      }else {
793        LtlSetSetElt(consensus, literal);
794      }
795    }
796  }
797  /* if pivot has never been defined, return NIL */
798  if (pivot == -1) {
799    LtlSetFree(consensus);
800    return NIL(LtlSet_t);
801  }
802
803  for (literal=0; literal<array_n(Negate); literal++) {
804    if (LtlSetGetElt(second, literal)) {
805      if (literal != pivot)
806        LtlSetSetElt(consensus, literal);
807    }
808  }
809
810  return consensus;
811}
812
813/**Function********************************************************************
814
815  Synopsis    [Return the cofactor of the cover with respect to the set.]
816
817  Description [We need the Negate method for each item in the set.]
818 
819  SideEffects [The result need to be freed by the caller. The input is left
820  unchanged.]
821
822******************************************************************************/
823lsList
824LtlCoverCofactor(
825  lsList Cover,
826  LtlSet_t *c,
827  array_t *Negate)
828{
829  lsList cofactor = lsCopy(Cover, (lsGeneric (*)(lsGeneric))LtlSetCopy);
830  lsList list;
831  lsGen  lsgen;
832  st_table *removed = st_init_table(st_ptrcmp, st_ptrhash);
833  int literal, complement;
834  LtlSet_t *term;
835 
836  for (literal=0; literal<array_n(Negate); literal++) {
837    if (!LtlSetGetElt(c, literal))  continue;
838    complement = array_fetch(int, Negate, literal);
839    lsForEachItem(cofactor, lsgen, term) {
840      if (st_is_member(removed, term)) continue;
841      if (LtlSetGetElt(term, complement)) 
842        st_insert(removed, term, term);
843      else if (LtlSetGetElt(term, literal))
844        LtlSetClearElt(term, literal);
845    }
846  }
847
848  list = cofactor;
849  cofactor = lsCreate();
850  lsForEachItem(list, lsgen, term) {
851    if (st_is_member(removed, term)) 
852      LtlSetFree(term);
853    else
854      lsNewEnd(cofactor, (lsGeneric) term, (lsHandle *) 0);
855  }
856  lsDestroy(list, (void (*)(lsGeneric))0);
857
858  st_free_table(removed);
859
860  return cofactor;
861}
862     
863/**Function********************************************************************
864
865  Synopsis    [Return 1 if the given cover is tautology.]
866
867  Description [The test is not fast: the compute sum of the cover should be
868  computed.]
869 
870  SideEffects []
871
872******************************************************************************/
873int
874LtlCoverIsTautology(
875  lsList Cover,
876  array_t *Negate)
877{
878  lsList complete = LtlCoverCompleteSum(Cover, Negate);
879  LtlSet_t *term;
880  int result;
881
882  if (lsLength(complete) !=1)
883    result = 0;
884  else {
885    lsFirstItem(complete, &term, (lsHandle *)0);
886    result = (LtlSetCardinality(term) == 0);
887  }
888
889  lsDestroy(complete, (void (*)(lsGeneric))LtlSetFree);
890  return result;
891}
892
893/**Function********************************************************************
894
895  Synopsis    [Return 1 if the given cover is implied BY the set.]
896
897  Description []
898 
899  SideEffects []
900
901******************************************************************************/
902int
903LtlCoverIsImpliedBy(
904  lsList Cover,
905  LtlSet_t *term,
906  array_t *Negate)
907{
908  lsList cofactor = LtlCoverCofactor(Cover, term, Negate);
909  int result = LtlCoverIsTautology(Cover, Negate);
910  lsDestroy(cofactor, (void (*)(lsGeneric))LtlSetFree);
911 
912  return result;
913}
914   
915
916/**Function********************************************************************
917
918  Synopsis    [Boolean minimization of the given cover.]
919
920  Description [First, compute a prime and irredundant version of the Cover;
921  Then try to drop each item iff it is implied by the remaining items.
922 
923  Notice: there might be a bug in the algorithm. Need to be fixed.
924  Need to talke to Fabio/Roderick
925  ]
926 
927  SideEffects []
928
929******************************************************************************/
930lsList
931LtlCoverPrimeAndIrredundant(
932  LtlTableau_t *tableau,
933  lsList Cover,
934  array_t *Negate)
935{
936  lsList pai = LtlCoverCompleteSum(Cover, Negate);
937  int totalnum;   /* total num of terms in current lsList pai */
938  int procnum;    /* how many are already processed so far ? */
939  LtlSet_t *term;
940 
941  totalnum = lsLength(pai);
942  procnum = 0;
943  /* Try to drop each term in turn */
944  while(lsDelBegin(pai, &term) != LS_NOMORE) {
945    if ( (lsLength(pai) != 0) &&
946         /* !LtlAutomatonSetIsFair(tableau, term) && */
947         LtlCoverIsImpliedBy(pai, term, Negate) ) {
948      LtlSetFree(term);
949      totalnum--;
950    }else 
951      lsNewEnd(pai, (lsGeneric) term, (lsHandle *)0);
952   
953    procnum++;
954    if (procnum >= totalnum)
955      break;
956  }
957 
958  return pai;
959}
960
961
962/**Function********************************************************************
963
964  Synopsis    [Return the supercube of a cover.]
965
966  Description []
967 
968  SideEffects [The result should be freed by the caller.]
969
970******************************************************************************/
971LtlSet_t *
972LtlCoverGetSuperCube(
973  lsList Cover,
974  array_t *Negate)
975{
976  LtlSet_t *unate = LtlSetNew(array_n(Negate));
977  LtlSet_t *binate = LtlSetNew(array_n(Negate));
978  lsGen  lsgen;
979  LtlSet_t *term;
980  int literal, neg;
981
982  lsForEachItem( Cover, lsgen, term ) {
983    for (literal=0; literal<array_n(Negate); literal++) {
984      if (!LtlSetGetElt(term, literal))  continue;
985      if (LtlSetGetElt(binate, literal) || LtlSetGetElt(unate, literal))
986        continue;
987      neg = array_fetch(int, Negate, literal);
988      if (LtlSetGetElt(unate, neg)) {
989        LtlSetClearElt(unate, neg);
990        LtlSetSetElt(binate, literal);
991        LtlSetSetElt(binate, neg);
992      }else
993        LtlSetSetElt(unate, literal);
994    }
995  }
996
997  LtlSetFree(binate);
998 
999  return unate;
1000}
1001
1002
1003
1004/**Function********************************************************************
1005
1006  Synopsis    [Return the supercube of a cover.]
1007
1008  Description []
1009 
1010  SideEffects [The result should be freed by the caller.]
1011
1012******************************************************************************/
1013mdd_t *
1014LtlSetModelCheckFormulae(
1015  LtlSet_t *set,
1016  array_t *labelTable,
1017  Fsm_Fsm_t *fsm)
1018{
1019  mdd_t *minterm, *mdd1, *mdd2;
1020  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
1021  mdd_t *mddOne = mdd_one(mddManager);
1022  array_t *careStatesArray = array_alloc(mdd_t *, 0);
1023  int i;
1024
1025  array_insert(mdd_t *, careStatesArray, 0, mddOne);
1026
1027  minterm = mdd_dup(mddOne);
1028  for (i=0; i<array_n(labelTable); i++) {
1029    if (LtlSetGetElt(set, i)) {
1030      Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, labelTable, i);
1031      Ctlp_Formula_t *ctlF = Ctlsp_PropositionalFormulaToCTL(F);
1032      mdd1 = Mc_FsmEvaluateFormula(fsm, ctlF, mddOne, 
1033                                   NIL(Fsm_Fairness_t),
1034                                   careStatesArray, 
1035                                   MC_NO_EARLY_TERMINATION,
1036                                   NIL(Fsm_HintsArray_t), Mc_None_c,
1037                                   McVerbosityNone_c, McDcLevelNone_c, 0,
1038                                   McGSH_EL_c);
1039      mdd2 = minterm;
1040      minterm = mdd_and(minterm, mdd1, 1, 1);
1041      mdd_free(mdd2);
1042      mdd_free(mdd1);
1043      Ctlp_FormulaFree(ctlF);
1044    }
1045  }
1046
1047  mdd_array_free(careStatesArray);
1048
1049  return minterm;
1050}
Note: See TracBrowser for help on using the repository browser.