source: vis_dev/vis-2.3/src/ltl/ltlAutomaton.c

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

vis2.3
File size: 33.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltlAutomaton.c]
4
5  PackageName [ltl]
6
7  Synopsis    [Translate LTL formula to the Buechi Automaton.]
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: ltlAutomaton.c,v 1.34 2005/04/28 08:47:15 bli Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Structure declarations                                                    */
27/*---------------------------------------------------------------------------*/
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33/*---------------------------------------------------------------------------*/
34/* Variable declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37/*---------------------------------------------------------------------------*/
38/* Macro declarations                                                        */
39/*---------------------------------------------------------------------------*/
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static int HasToBeStored(LtlTableau_t *tableau, int index);
48static int Contradiction(LtlTableau_t *tableau, int index, LtlSet_t *ToCover, LtlSet_t *Current, LtlSet_t *Covered);
49static int Redundant(LtlTableau_t *tableau, int index, LtlSet_t *ToCover, LtlSet_t *Current, LtlSet_t *Covered);
50static int SI(LtlTableau_t *tableau, int index, LtlSet_t *A);
51static void AutomatonComputeFair(LtlTableau_t *tableau, LtlSet_t *r, vertex_t *vtx1);
52static int AutomatonCreateFairList(LtlTableau_t *tableau, Ltl_Automaton_t *aut);
53static void AutomatonAssignNext(LtlTableau_t *tableau, LtlSet_t * toCover, LtlSet_t * s);
54static LtlSet_t * AutomatonSetCreate(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
55static lsList AutomatonBuildCover(LtlTableau_t *tableau, LtlSet_t *ToCover);
56static void AutomatonBuildCover_Aux(LtlTableau_t *tableau, LtlSet_t *pToCover, LtlSet_t *pCurrent, LtlSet_t *pCovered, lsList Cover);
57
58/**AutomaticEnd***************************************************************/
59   
60/*---------------------------------------------------------------------------*/
61/* Definition of exported functions                                          */
62/*---------------------------------------------------------------------------*/
63
64/**Function********************************************************************
65
66  Synopsis    [Allocate the automaton data structure.]
67
68  Description []
69
70  SideEffects []
71
72  SeeAlso     []
73
74******************************************************************************/
75Ltl_Automaton_t *
76Ltl_AutomatonCreate(void)
77{
78  Ltl_Automaton_t *aut = ALLOC(Ltl_Automaton_t, 1); 
79  (void)memset((void *)aut, 0, sizeof(Ltl_Automaton_t));
80 
81  aut->name = 0;
82  aut->SCC = (st_table *)0;
83  aut->G = g_alloc();
84  /* table of the initial states */
85  aut->Init = st_init_table(st_ptrcmp, st_ptrhash); 
86  /* these states can be either in or outside the "FairSet" */
87  aut->dontcare = st_init_table(st_ptrcmp, st_ptrhash); 
88  /* list of FairSets (each FairSet is a table of states) */
89  aut->Fair = lsCreate(); 
90  aut->node_idx = 1;
91 
92  return aut;
93}
94
95/**Function********************************************************************
96
97  Synopsis    [Free the automaton data structure.]
98
99  Description []
100
101  SideEffects []
102
103  SeeAlso     []
104
105******************************************************************************/
106void
107Ltl_AutomatonFree(gGeneric g)
108{
109  st_table *tbl;
110  st_generator *stgen;
111  int i, n;
112  Ltl_Automaton_t *aut = (Ltl_Automaton_t *) g;
113
114  if (aut->name)  FREE(aut->name);
115
116  g_free(aut->G, (void (*)(gGeneric))0, Ltl_AutomatonNodeFree,
117         (void (*)(gGeneric))0);
118
119  st_free_table(aut->Init);
120  st_free_table(aut->dontcare);
121 
122  while (lsDelBegin(aut->Fair, &tbl) != LS_NOMORE) {
123      st_free_table(tbl);
124  }
125  lsDestroy(aut->Fair, (void (*)(lsGeneric)) NULL);
126
127  if (aut->labelTable) {
128      n = array_n(aut->labelTable);
129      for (i=0; i<n; i++) 
130          Ctlsp_FormulaFree(array_fetch(Ctlsp_Formula_t *, 
131                                        aut->labelTable, i));
132      array_free(aut->labelTable);
133      array_free(aut->labelTableNegate);
134  }
135
136  /* free the partition/quotient */
137  if (aut->SCC) {
138    /* for a Buechi automaton, this is a st_table of st_table of vertices;
139     * otherwise, this is a st_table of vertices */
140    if (aut->isQuotientGraph == 0) {
141      st_foreach_item(aut->SCC, stgen, &tbl, NIL(char *)) {
142        st_free_table(tbl);
143      }
144    }
145    st_free_table(aut->SCC);
146  }
147
148  if (aut->Q)
149      Ltl_AutomatonFree((gGeneric) aut->Q);
150
151  FREE(aut);
152}
153       
154/**Function********************************************************************
155
156  Synopsis    [Allocate the automaton node data structure.]
157
158  Description []
159
160  SideEffects []
161
162  SeeAlso     []
163
164******************************************************************************/
165Ltl_AutomatonNode_t *
166Ltl_AutomatonNodeCreate(Ltl_Automaton_t *aut)
167{
168  Ltl_AutomatonNode_t *node = ALLOC(Ltl_AutomatonNode_t, 1);
169  (void)memset((void *)node, 0, sizeof(Ltl_AutomatonNode_t));
170
171  node->index = aut->node_idx++;
172  node->Labels = NIL(LtlSet_t);
173  node->CoverSet = NIL(LtlSet_t);
174  node->Class = (st_table *)0;        /* used in Quotient graph */
175     
176  return node;
177}
178
179/**Function********************************************************************
180
181  Synopsis    [Free the automaton node data structure.]
182
183  Description []
184
185  SideEffects []
186
187  SeeAlso     []
188
189******************************************************************************/
190void
191Ltl_AutomatonNodeFree(gGeneric g)
192{
193  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) g;
194  if (node->Labels)
195    LtlSetFree(node->Labels);
196  if (node->CoverSet)
197    LtlSetFree(node->CoverSet);
198  /*  if (node->Class)
199        st_free_table(node->Class);*/
200 
201  FREE(node);
202}
203
204/**Function********************************************************************
205
206  Synopsis    [Print the automaton node.]
207
208  Description []
209
210  SideEffects []
211
212  SeeAlso     []
213
214******************************************************************************/
215void
216Ltl_AutomatonNodePrint(
217  Ltl_Automaton_t *aut,
218  Ltl_AutomatonNode_t *node)
219{
220  st_generator *stgen;
221  vertex_t *vtx;
222  Ltl_AutomatonNode_t *state;
223  Ctlsp_Formula_t *F;
224  int first, i, n;
225 
226  /* index (required) */
227  fprintf(vis_stdout, "n%d: ", node->index);
228 
229  /* 1. cover (set of formulae) ? */
230  if (aut->tableau && node->CoverSet) 
231    LtlSetPrint(aut->tableau, node->CoverSet);
232 
233  /* 2. label ? */
234  if (node->Labels) {
235    fprintf(vis_stdout, " label: {");
236    first = 1; n = array_n(aut->labelTable);
237    for (i=0; i<n; i++) {
238      if (LtlSetGetElt(node->Labels, i)) {
239        if (!first)       fprintf(vis_stdout, ",");
240        else              first = 0;
241        F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i);
242        Ctlsp_FormulaPrint(vis_stdout, F);
243      }
244    }
245    fprintf(vis_stdout, "}");
246  }
247
248  /* 3. Class ? (for quotient graph node) */
249  if (node->Class) {
250    fprintf(vis_stdout, "scc{");
251    st_foreach_item(node->Class, stgen, &vtx, NIL(char *)) {
252      state = (Ltl_AutomatonNode_t *)vtx->user_data;
253      fprintf(vis_stdout, "n%d ", state->index);
254    }
255    fprintf(vis_stdout, "}");
256  }
257 
258  fprintf(vis_stdout, "\n");
259}
260
261/**Function********************************************************************
262
263  Synopsis    [Print the automaton.]
264
265  Description []
266
267  SideEffects []
268
269  SeeAlso     []
270
271******************************************************************************/
272void
273Ltl_AutomatonPrint(
274  Ltl_Automaton_t *aut,
275  int verbosity)
276{
277  edge_t   *edge;
278  vertex_t *vtx1, *vtx2;           
279  Ltl_AutomatonNode_t *node, *node2;
280  lsGen     gen;
281  lsGeneric data;
282
283  st_table  *tbl;
284  st_generator *stgen;
285
286  int n_states = 0;
287  int n_trans = 0;
288  int n_fairsets = 0;
289  int n_init = 0;
290  int strength;
291 
292  /* name ? */
293  if (verbosity)
294    fprintf(vis_stdout, "Automaton:\n");
295
296  if (verbosity > 1) {
297    fprintf(vis_stdout, "-----------------------------------------------\n");
298    if (aut->name)
299      fprintf(vis_stdout, "Name: %s \n", aut->name);
300    fprintf(vis_stdout, "-----------------------------------------------\n");
301   
302    /* negation normal form ?*/
303    if(aut->tableau)
304      Ctlsp_FormulaPrint(vis_stdout, aut->tableau->F);
305   
306    /* States & Labels */
307    fprintf(vis_stdout, "\nStates: \n");
308    foreach_vertex( aut->G, gen, vtx1) {
309      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
310      Ltl_AutomatonNodePrint(aut, node);
311    }
312   
313    /* Init States ? */
314    fprintf(vis_stdout, "Arcs: \n"); 
315    st_foreach_item(aut->Init, stgen,  &vtx1, NIL(char *)) {
316      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
317      fprintf(vis_stdout, "-> n%d\n", node->index);
318    }
319   
320    /* Edges */
321    foreach_edge(aut->G, gen, edge) {
322      vtx1 = g_e_source(edge);
323      vtx2 = g_e_dest(edge);
324      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
325      node2 = (Ltl_AutomatonNode_t *) vtx2->user_data;
326         
327      if (node)
328        fprintf(vis_stdout, "   n%d -> ", node->index);
329      if (node2)
330        fprintf(vis_stdout, "n%d\n", node2->index);
331    }
332
333    /* Sets of Fair Sets */
334    fprintf(vis_stdout, "Fair Sets: \n"); 
335    lsForEachItem (aut->Fair, gen, data) {
336      tbl = (st_table *) data;
337      fprintf(vis_stdout, "{ ");
338      st_foreach_item(tbl, stgen,  &vtx1, NIL(char *)) {
339        node = (Ltl_AutomatonNode_t *) vtx1->user_data;
340        fprintf(vis_stdout, "n%d ", node->index);
341      }
342      fprintf(vis_stdout, " }\n");
343    }
344   
345#ifdef DEBUG_LTLMC     
346    /* Dontcare states */
347    fprintf(vis_stdout, "Dontcare States: \n{");
348    if (aut->dontcare) {
349      st_foreach_item(aut->dontcare, stgen, &vtx1, NIL(char *)) {
350        node = (Ltl_AutomatonNode_t *) vtx1->user_data;
351        fprintf(vis_stdout, "n%d ", node->index);
352      }
353    }
354    fprintf(vis_stdout, " }\n");
355#endif
356 
357    fprintf(vis_stdout, "End\n");
358  }
359 
360  /* Get the strength (2, 1, 0) */
361  n_states = lsLength(g_get_vertices(aut->G));
362  n_init = st_count(aut->Init);
363  n_trans = lsLength(g_get_edges(aut->G));
364  n_fairsets = lsLength(aut->Fair);
365  strength = Ltl_AutomatonGetStrength(aut);
366
367  if (verbosity) 
368    fprintf(vis_stdout, "Stats: %d states, %d trans, %d fair sets, %d init states, %s\n", n_states, n_trans, n_fairsets, n_init, (strength==2)? "strong":((strength==1)?"weak":"terminal") );
369
370}
371
372
373/*---------------------------------------------------------------------------*/
374/* Definition of internal functions                                          */
375/*---------------------------------------------------------------------------*/
376
377/**Function********************************************************************
378
379  Synopsis    [Generate the Buechi automaton from the formula.]
380
381  Description [Before calling this function, 'tableau' should contains:
382   1) LTL Formula (NNF) and its negation in a DAG (or UniqueTable)
383   2) alpha-beta Table (tableau-rule expansion of each sub-formulae )
384   3) Until formulae list.]
385
386  SideEffects [The returned automaton should be freed by the caller.]
387
388  SeeAlso     []
389
390******************************************************************************/
391Ltl_Automaton_t *
392LtlAutomatonGeneration(
393  LtlTableau_t *tableau)
394{
395  LtlSet_t *toCover, *s, *r, *rprime; /* terms (set) */
396  lsList Cover;                       /* current list of terms (cover) */
397  lsList U = lsCreate();              /* a list of terms <to be processed>*/
398  lsList Q = lsCreate();              /* unique table for terms <processed> */
399  st_table  *Set2Vtx = st_init_table(st_ptrcmp, st_ptrhash);
400  vertex_t *vtx1, *vtx2;              /* vertex in graph, related to node */
401  Ltl_Automaton_t *A = Ltl_AutomatonCreate();
402  Ltl_AutomatonNode_t *node;
403  Ctlsp_Formula_t *F;
404  int i;
405
406  A->tableau = tableau;
407 
408  /* Compute Cover( {F} ), the init states, and U */
409  toCover = AutomatonSetCreate(tableau, tableau->F); 
410  Cover = AutomatonBuildCover(tableau, toCover);     
411  while (lsDelBegin(Cover, &r) != LS_NOMORE) {
412#ifdef DEBUG_LTLMC
413    if (tableau->verbosity >=2) {
414      fprintf(vis_stdout, "**** term: ");
415      LtlSetPrintIndex(tableau->abIndex, r);
416      fprintf(vis_stdout, "**** n%d added! \n", A->node_idx);
417    }
418#endif
419    lsNewEnd(U, (lsGeneric) r, (lsHandle *) 0);
420    lsNewEnd(Q, (lsGeneric) r, (lsHandle *) 0);
421    /* Build the initial states of the Buechi automaton
422     * add a new node in G
423     */
424    node = Ltl_AutomatonNodeCreate(A);
425    node->Labels = LtlSetToLabelSet(tableau, r);
426    node->CoverSet = LtlSetCopy(r); 
427    vtx1 = g_add_vertex(A->G);
428    vtx1->user_data = (gGeneric) node;
429    /* add into A->Init */
430    st_insert(A->Init, vtx1,  vtx1);
431    /* put this node to proper Fair sets */
432    AutomatonComputeFair(tableau, r, vtx1);
433    /* add into the (Set, Vtx) unique table */
434    st_insert(Set2Vtx, r,  vtx1);
435  }
436  lsDestroy(Cover, (void (*)(lsGeneric))0);
437
438  /* Each time, remove one set 's' from the to-be-processed list 'U' */
439  while (lsDelBegin(U, &s) == LS_OK) {
440    /* Put all the next (state) formulae into toCover */
441    AutomatonAssignNext(tableau, toCover, s);
442#ifdef DEBUG_LTLMC
443    if (tableau->verbosity >= 2) {
444      fprintf(vis_stdout, "\n** AssignNext Of:");
445      LtlSetPrintIndex(tableau->abIndex, s);
446      fprintf(vis_stdout, "** ==>           ");
447      LtlSetPrintIndex(tableau->abIndex, toCover);
448    }
449#endif
450    /* Build the cover for next state */
451    Cover = AutomatonBuildCover(tableau, toCover);
452    while (lsDelBegin(Cover, &r) == LS_OK) {
453      /* Get the existing identical copy of r from Q (if exist) */
454      rprime = LtlSetIsInList(r, Q);
455#ifdef DEBUG_LTLMC       
456      if (tableau->verbosity >=2 ) {
457        fprintf(vis_stdout, "** term: ");
458        LtlSetPrintIndex(tableau->abIndex, r);
459      }
460#endif
461      /* If the next state exists, simply add the new edge; Otherwise,
462         create the next state, and add the new edge */
463      if (rprime) {
464        /* both s and r' are already in G */
465        st_lookup(Set2Vtx,  rprime,  &vtx1);
466        assert(vtx1 != NIL(vertex_t));
467        st_lookup(Set2Vtx, s,  &vtx2); 
468        assert(vtx2 != NIL(vertex_t));
469        /* add edge(s, r') */
470        g_add_edge(vtx2, vtx1);       
471        LtlSetFree(r);
472      }else {
473#ifdef DEBUG_LTLMC           
474        if (tableau->verbosity >=2 ) {
475          fprintf(vis_stdout, "** n%d added!\n", A->node_idx);
476        }
477#endif
478        /* add a new state in G */
479        node = Ltl_AutomatonNodeCreate(A);
480        node->Labels = LtlSetToLabelSet(tableau, r);
481        node->CoverSet = LtlSetCopy(r); 
482        vtx1 = g_add_vertex(A->G); 
483        vtx1->user_data = (gGeneric) node;
484        /* add edge(s, r) */
485        st_lookup(Set2Vtx,  s,  &vtx2);
486        assert(vtx2 != NIL(vertex_t));     
487        g_add_edge(vtx2, vtx1); 
488        /* put the new state to the proper Fair Sets */
489        AutomatonComputeFair(tableau, r, vtx1);
490        /* add r in the (Set, Vtx) unique table */
491        st_insert(Set2Vtx,  r,  vtx1);       
492        lsNewEnd(Q, (lsGeneric) r, (lsHandle *) 0);
493        lsNewEnd(U, (lsGeneric) r, (lsHandle *) 0);
494      }
495    }
496     
497    lsDestroy(Cover, (void (*)(lsGeneric))0);
498  }
499
500  /* Convert fair sets of the tableau into fair sets of the automaton:
501   * if there is an empty fairset, create an empty automaton and return;
502   * otherwise, keep going ...
503   */
504  if (AutomatonCreateFairList(tableau, A) == 0) {
505    st_table *tbl;
506    while (lsDelBegin(A->Fair, &tbl) != LS_NOMORE) {
507      st_free_table(tbl);
508    }
509    g_free(A->G, (void (*)(gGeneric))0, Ltl_AutomatonNodeFree,
510           (void (*)(gGeneric))0);
511    A->G = g_alloc();
512    st_free_table(A->Init);
513    A->Init = st_init_table(st_ptrcmp, st_ptrhash);
514  }
515
516  /* Copy the lable table of the tableau into the automaton
517   * Note that the new one shares nothing with the one in the tableau
518   */
519  A->labelTable = array_alloc(Ctlsp_Formula_t *, tableau->labelIndex);
520  for (i=0; i<tableau->labelIndex; i++) {
521    F = Ctlsp_LtlFormulaNegationNormalForm(tableau->labelTable[i]);
522    array_insert(Ctlsp_Formula_t *, A->labelTable, i, F);
523  }
524  A->labelTableNegate = array_dup(tableau->labelTableNegate);
525 
526  /* Free all the sets in the list
527   * toCover/U  should be empty sets, while Q contains all the processed set
528   */
529  LtlSetFree(toCover);         
530  lsDestroy(U, (void (*)(lsGeneric)) 0);   
531  lsDestroy(Q, (void (*)(lsGeneric))LtlSetFree);   
532  st_free_table(Set2Vtx);
533
534#ifdef DEBUG_LTLMC 
535  /* sanity check */
536  g_check(A->G);
537#endif
538 
539  return A;
540}
541
542
543/**Function********************************************************************
544
545  Synopsis    [Return 1 if the given set belongs to a fair set.]
546
547  Description [It is used in Boolean minimization. It might prevent
548  over-simplification.]
549
550  SideEffects []
551
552******************************************************************************/
553int 
554LtlAutomatonSetIsFair(
555  LtlTableau_t *tableau,
556  LtlSet_t *r)
557{
558#if 0
559  st_table *uniqueTable = tableau->untilUniqueTable;
560  char *key, *value;
561  st_generator *gen;
562  int flag = 0;
563#endif
564
565  /* this is the same as "Wring" */
566  return 0; 
567
568#if 0 
569  st_foreach_item(uniqueTable, gen, &key, &value) {
570    Ctlsp_Formula_t *F = (Ctlsp_Formula_t *) key;
571    Ctlsp_Formula_t *right = Ctlsp_FormulaReadRightChild(F);
572    int F_ab_idx = Ctlsp_FormulaReadABIndex(F);
573    int right_ab_idx = Ctlsp_FormulaReadABIndex(right);
574     
575    if ( SI(tableau, right_ab_idx, r) ||
576         !(SI(tableau, F_ab_idx, r)) ) {
577      /* set 'r' belongs to one fair set */
578      flag = 1;
579      st_free_gen(gen);
580      break;
581    }
582  }
583  return flag;
584#endif
585}
586
587
588/*---------------------------------------------------------------------------*/
589/* Definition of exported functions                                          */
590/*---------------------------------------------------------------------------*/
591
592/**Function********************************************************************
593
594  Synopsis    [Return 1 iff the elementary formula need to be stored.]
595
596  Description [The formula is represented by its index in the abTable]
597
598  SideEffects []
599
600******************************************************************************/
601static int
602HasToBeStored(
603  LtlTableau_t *tableau,
604  int index)
605{
606  int result = 1;
607  Ctlsp_Formula_t *F;
608  Ctlsp_FormulaType F_type;
609 
610  F = tableau->abTable[index].F;
611 
612  switch(tableau->algorithm) {
613  case Ltl2Aut_GPVW_c:
614    result = 1;
615    break;
616  case Ltl2Aut_GPVWplus_c:
617    /* T iff 'u' is an until formula or 'u' is the right hand of an until */
618    F_type = Ctlsp_FormulaReadType(F);
619    result = (F_type == Ctlsp_U_c || Ctlsp_FormulaReadRhs(F) == 1);
620    break;
621  case Ltl2Aut_LTL2AUT_c: 
622  case Ltl2Aut_WRING_c:   
623    result = 0;
624    break;
625  }
626#ifdef DEBUG_LTLMC
627  if (tableau->verbosity >2)
628    fprintf(vis_stdout, "...HasToBeStored=%d\n", result);
629#endif
630 
631  return result;
632}
633
634/**Function********************************************************************
635
636  Synopsis    [Return 1 iff there is there is a contradition so far.]
637
638  Description [The formula is represented by its index in the abTable]
639
640  SideEffects []
641
642******************************************************************************/
643static int
644Contradiction(
645  LtlTableau_t *tableau,
646  int index,
647  LtlSet_t *ToCover,
648  LtlSet_t *Current,
649  LtlSet_t *Covered)
650{
651  int result = 0;
652  Ctlsp_Formula_t *F, *notF;
653  LtlSet_t *UC;
654  int notF_ab_idx;
655  Ctlsp_FormulaType F_type;
656 
657  F = tableau->abTable[index].F;
658  F_type = Ctlsp_FormulaReadType(F);
659  notF = tableau->abTable[index].notF;
660  notF_ab_idx = Ctlsp_FormulaReadABIndex(notF);
661
662 
663  switch(tableau->algorithm) {
664  case Ltl2Aut_GPVW_c:
665    /* if 'u' is False, or (!u) exists in Current */
666    result = ( F_type == Ctlsp_FALSE_c ||
667               LtlSetGetElt(Current, notF_ab_idx) );
668    break;
669  case Ltl2Aut_GPVWplus_c:
670    /* if 'u' is False, or !(u) exists in Covered */
671    result = ( F_type == Ctlsp_FALSE_c ||
672               LtlSetGetElt(Covered, notF_ab_idx) );
673    break;
674  case Ltl2Aut_LTL2AUT_c:
675  case Ltl2Aut_WRING_c:
676    UC = LtlSetCopy(ToCover);
677    LtlSetOR(UC, ToCover, Current);
678    /* T iff (!u) \in SI(ToCover U Current) */
679    result = SI(tableau, notF_ab_idx, UC);
680    LtlSetFree(UC);
681    break;
682  }
683#ifdef DEBUG_LTLMC
684  if (tableau->verbosity >2)
685    fprintf(vis_stdout, "...Contradiction=%d\n", result);
686#endif
687 
688  return result;
689}
690
691/**Function********************************************************************
692
693  Synopsis    [Return 1 iff the given formula is redundant.]
694
695  Description [The formula is represented by its index in the abTable]
696
697  SideEffects []
698
699******************************************************************************/
700static int
701Redundant(
702  LtlTableau_t *tableau,
703  int index,
704  LtlSet_t *ToCover,
705  LtlSet_t *Current,
706  LtlSet_t *Covered)
707{
708  int result = 0;
709  Ctlsp_Formula_t *F;
710  LtlSet_t *UC = LtlSetCopy(ToCover);
711  int Fleft_ab_idx , Fright_ab_idx;
712  Ctlsp_FormulaType F_type;
713 
714  LtlSetOR(UC, ToCover, Current);
715 
716  F = tableau->abTable[index].F;
717 
718  F_type = Ctlsp_FormulaReadType(F);
719  if (F_type == Ctlsp_U_c || F_type == Ctlsp_R_c) {
720    Fleft_ab_idx = Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadLeftChild(F));
721    Fright_ab_idx = Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadRightChild(F));
722  } else { /* to remove uninitialized variable warnings */
723    Fleft_ab_idx = 0;
724    Fright_ab_idx = 0;
725  }
726  switch(tableau->algorithm) {
727  case Ltl2Aut_GPVW_c:
728    result = 0;
729    break;
730  case Ltl2Aut_GPVWplus_c:
731    /* T iff  'u' is (n U v) and {v} is in (ToCover U Current),
732     *   or   'u' is (n R v) and {n,v} is in (ToCover U Current)
733     */
734    if (F_type == Ctlsp_U_c) 
735      result = LtlSetGetElt(UC, Fright_ab_idx);
736    else if (F_type == Ctlsp_R_c) 
737      result = ( LtlSetGetElt(UC, Fleft_ab_idx) &&
738                 LtlSetGetElt(UC, Fright_ab_idx) );
739    else
740      result = 0;
741    break;
742  case Ltl2Aut_LTL2AUT_c:
743  case Ltl2Aut_WRING_c:
744    /* T iff the following two cases are both true:
745     *  (1) 'u' is in SI(ToCover U Current)
746     *  (2) if 'u' is (n U v), then 'v' is in (ToCover U Current)
747     */
748    result = SI(tableau, index, UC);
749    if (result && F_type == Ctlsp_U_c) {
750      result = SI(tableau, Fright_ab_idx, UC);
751    }
752    break;
753  }
754  LtlSetFree(UC);
755#ifdef DEBUG_LTLMC 
756  if (tableau->verbosity >2)
757    fprintf(vis_stdout, "...Redundant=%d\n", result);
758#endif
759 
760  return result;
761}
762
763/**Function********************************************************************
764
765  Synopsis    [Test if the given formula is synatically implied by the
766  existing set (product term).]
767
768  Description [Return 1 if the formula is implied. The formula is represented
769  by its index in the abTable]
770
771  SideEffects []
772
773******************************************************************************/
774static int
775SI(
776  LtlTableau_t *tableau,
777  int index,
778  LtlSet_t *A)
779{
780  int result = 0;
781  Ctlsp_Formula_t *XF;
782  Ctlsp_Formula_t *F = tableau->abTable[index].F;
783  Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F);
784  int Fleft_ab_idx, Fright_ab_idx;
785 
786  if (tableau->algorithm == Ltl2Aut_GPVW_c ||
787      tableau->algorithm == Ltl2Aut_GPVWplus_c) {
788    result = LtlSetGetElt(A, index);
789  } else {
790    if (F_type == Ctlsp_AND_c || F_type == Ctlsp_OR_c ||
791        F_type == Ctlsp_U_c || F_type == Ctlsp_R_c) {
792      Fleft_ab_idx =
793        Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadLeftChild(F));
794      Fright_ab_idx =
795        Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadRightChild(F));
796    } else { /* to remove uninitialized variable warnings */
797      Fleft_ab_idx = 0;
798      Fright_ab_idx = 0;
799    }
800   
801    switch(Ctlsp_FormulaReadType(F)) {
802    case Ctlsp_FALSE_c:
803      result = 0;
804      break;
805    case Ctlsp_TRUE_c:
806      result = 1;
807      break;
808    case Ctlsp_X_c:
809    case Ctlsp_NOT_c:
810    case Ctlsp_ID_c:
811      result = LtlSetGetElt(A, index);
812      break;
813    case Ctlsp_AND_c:
814      if (Ctlsp_LtlFormulaIsPropositional(F))
815        result = LtlSetGetElt(A, index);
816      else {
817        result = (SI(tableau, Fleft_ab_idx, A) &&
818                  SI(tableau, Fright_ab_idx, A));
819      }
820      break;
821    case Ctlsp_OR_c:
822      if (Ctlsp_LtlFormulaIsPropositional(F))
823        result = LtlSetGetElt(A, index);
824      else {
825        result = (SI(tableau, Fleft_ab_idx, A) ||
826                  SI(tableau, Fright_ab_idx, A));
827      }
828      break;
829    case Ctlsp_U_c:
830      XF = LtlTableauGetUniqueXFormula(tableau, F);       
831      result = (SI(tableau, Fright_ab_idx, A) ||
832                (SI(tableau, Fleft_ab_idx, A) &&
833                 LtlSetGetElt(A, Ctlsp_FormulaReadABIndex(XF))));
834      break;
835    case Ctlsp_R_c:
836      XF = LtlTableauGetUniqueXFormula(tableau, F);       
837      result = SI(tableau, Fright_ab_idx, A) &&
838        (SI(tableau, Fleft_ab_idx, A) ||
839         LtlSetGetElt(A, Ctlsp_FormulaReadABIndex(XF)));
840      break;
841    default:
842      assert(0);
843    }
844  }
845 
846#ifdef DEBUG_LTLMC
847  if (tableau->verbosity > 3) {
848    fprintf(vis_stdout, "...SI( %d, ", index);
849    LtlSetPrintIndex(tableau->abIndex, A);
850    fprintf(vis_stdout, "     )=%d\n", result);
851  }
852#endif
853 
854  return result;
855}
856
857
858/**Function********************************************************************
859
860  Synopsis    [Put the node into the fairset if it contains a until formula.]
861
862  Description [Each until formula in the 'untilUnqiueTable' corresponds to
863  a fair set (a set of vertices in the automaton, represented by a hash
864  table. A vertex belongs to a fair set iff its cover set contains the until
865  formula.]
866
867  SideEffects []
868
869******************************************************************************/
870static void
871AutomatonComputeFair(
872  LtlTableau_t *tableau,
873  LtlSet_t *r,
874  vertex_t *vtx1)
875{
876  st_table *uniqueTable = tableau->untilUniqueTable;
877  char *key, *value;
878  st_generator *gen;
879
880  /* Notice that each pair in 'uniqueTable' is a (Unitl formula, Fair set) */
881  st_foreach_item(uniqueTable, gen, &key, &value) {
882    Ctlsp_Formula_t *F = (Ctlsp_Formula_t *) key;
883    Ctlsp_Formula_t *right = Ctlsp_FormulaReadRightChild(F);
884    int F_ab_idx = Ctlsp_FormulaReadABIndex(F);
885    int right_ab_idx = Ctlsp_FormulaReadABIndex(right);
886    lsList Fair = (lsList) value;
887     
888    if ( SI(tableau, right_ab_idx, r) || !(SI(tableau, F_ab_idx, r)) ) {
889      lsNewEnd(Fair, (lsGeneric) vtx1, (lsHandle *) 0); 
890    }
891  }
892}
893
894/**Function********************************************************************
895
896  Synopsis    [Convert the fair sets of the tableau into the fair set in the
897  automaton.]
898
899  Description [The fairness in the tableau is "a hash table (Until formula,
900  FairVerticesList)". The fairness in the automaton should be " a list of
901  hash tables" (each hash table corresponds to a fair set, and a vertex is
902  in the hash table iff it's in that fair set).
903
904  Return 0 iff there is an empty fairset (which means the language of the
905  automaton is empty no matter what);  Return 1 otherwise.]
906
907  SideEffects []
908
909******************************************************************************/
910static int
911AutomatonCreateFairList(
912  LtlTableau_t *tableau,
913  Ltl_Automaton_t *aut)
914{
915  lsList FairList = aut->Fair;
916  char *key, *value;
917  st_generator *gen;
918  int noEmptyFairSet = 1;
919
920  st_foreach_item(tableau->untilUniqueTable, gen, &key, &value) {
921    lsList Fair = (lsList) value;
922
923    /* translate a lsList into a st_table */
924    if (lsLength(Fair) > 0) {
925      lsGen lsgen;
926      lsGeneric lsdata;
927      st_table *tbl = st_init_table(st_ptrcmp, st_ptrhash);
928     
929      lsForEachItem (Fair, lsgen, lsdata) {
930        st_insert(tbl, lsdata, lsdata);
931      }
932      lsNewEnd(FairList, (lsGeneric) tbl, (lsHandle *) 0); 
933    }else 
934      noEmptyFairSet = 0;
935
936    lsDestroy(Fair, (void (*)(lsGeneric)) NULL);
937  }
938
939  return noEmptyFairSet;
940}
941
942/**Function********************************************************************
943
944  Synopsis    [Generate the next-formulae set.]
945 
946  Description [toCover = { u: X(u) is in s }. In other words, for each formula
947  of the form X(u) in the set 's', add the subformula u into 'toCover'.]
948
949  SideEffects ['toCover' is changed.]
950
951******************************************************************************/
952static void
953AutomatonAssignNext(
954  LtlTableau_t *tableau,
955  LtlSet_t * toCover,
956  LtlSet_t * s)
957{
958  int i;
959  Ctlsp_FormulaType type;
960  Ctlsp_Formula_t *left;
961  int left_ab_idx;
962     
963  LtlSetClear(toCover);
964 
965  for (i=0; i<tableau->abIndex; i++) {
966    if (LtlSetGetElt(s, i)) {
967      type = Ctlsp_FormulaReadType(tableau->abTable[i].F);
968      if (type == Ctlsp_X_c) {
969        left = Ctlsp_FormulaReadLeftChild(tableau->abTable[i].F);
970        left_ab_idx = Ctlsp_FormulaReadABIndex(left);
971        LtlSetSetElt(toCover, left_ab_idx);
972       
973      }
974    }
975  }
976} 
977
978
979/**Function********************************************************************
980
981  Synopsis    [Create the set representation of the given formula.]
982
983  Description [Its size will be the total number of sub-formulae in the
984  tableau. Only the bit corresponding to the given formula is set.]
985
986  SideEffects [The result should be freed by the caller.]
987
988******************************************************************************/
989static LtlSet_t *
990AutomatonSetCreate(
991  LtlTableau_t *tableau,
992  Ctlsp_Formula_t *F) 
993{
994  LtlSet_t *cs = LtlSetNew(tableau->abIndex);
995
996  if (!F)
997    return cs;
998
999  LtlSetSetElt(cs, Ctlsp_FormulaReadABIndex(F));
1000   
1001  return cs;
1002}
1003
1004/**Function********************************************************************
1005
1006  Synopsis    [Build the cover for a given set 'toCover'.]
1007
1008  Description [The cover is "a list of sets", where the sets are product terms
1009  and the list is in DNF form (union of all its product terms).]
1010
1011  SideEffects [The result should be freed by the caller.]
1012
1013******************************************************************************/
1014static lsList
1015AutomatonBuildCover(
1016  LtlTableau_t *tableau,
1017  LtlSet_t *ToCover)
1018{
1019  LtlSet_t *Current = LtlSetNew(tableau->abIndex);
1020  LtlSet_t *Covered = LtlSetNew(tableau->abIndex);
1021  lsList Cover = lsCreate();
1022
1023  AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered, Cover);
1024  LtlSetFree(Current);
1025  LtlSetFree(Covered);
1026 
1027  /* Boolean Minimization -- heuristics */
1028  if (tableau->booleanmin == 1) {
1029    if (lsLength(Cover)) {
1030      lsList list = Cover;
1031      Cover = LtlCoverPrimeAndIrredundant(tableau, Cover,
1032                                          tableau->abTableNegate);
1033      lsDestroy(list, (void (*)(lsGeneric))LtlSetFree);
1034    }
1035  }
1036  return Cover;
1037}
1038
1039/**Function********************************************************************
1040
1041  Synopsis    [Recursively construct the cover.]
1042
1043  Description [the cover is updated in the parameter 'lsList Cover'. This
1044  function is used in AutomatonBuildCover() only.]
1045
1046  SideEffects []
1047
1048******************************************************************************/
1049static void
1050AutomatonBuildCover_Aux(
1051  LtlTableau_t *tableau,
1052  LtlSet_t *pToCover,
1053  LtlSet_t *pCurrent,
1054  LtlSet_t *pCovered,
1055  lsList Cover)
1056{
1057  LtlSet_t *ToCover = LtlSetCopy(pToCover);
1058  LtlSet_t *Current = LtlSetCopy(pCurrent);
1059  LtlSet_t *Covered = LtlSetCopy(pCovered);
1060  int i;
1061
1062#ifdef DEBUG_LTLMC 
1063  if (tableau->verbosity >2 ) {
1064    fprintf(vis_stdout, "ToCover=");
1065    LtlSetPrintIndex(tableau->abIndex, ToCover);
1066    fprintf(vis_stdout, "Current=");
1067    LtlSetPrintIndex(tableau->abIndex, Current);
1068    fprintf(vis_stdout, "Covered=");
1069    LtlSetPrintIndex(tableau->abIndex, Covered);
1070    fflush(vis_stdout);
1071  }     
1072#endif
1073 
1074  if (LtlSetIsEmpty(ToCover)) {
1075#if 1
1076    /* chao: 7/22/2002 remove identical set in current Cover */
1077    if (!LtlSetIsInList(Current, Cover))
1078#endif
1079      lsNewEnd(Cover, (lsGeneric) LtlSetCopy(Current), (lsHandle *) 0);
1080    /* return */
1081  }else {
1082    /* select 'u' from 'ToCover' */
1083    for (i=0; i<tableau->abIndex; i++) {
1084      if (LtlSetGetElt(ToCover,i))
1085        break;
1086    }
1087    /* remove 'u' from 'ToCover' and add it to 'Covered' */
1088    LtlSetClearElt(ToCover, i);
1089    LtlSetSetElt(Covered, i);
1090   
1091    /* if HAS_TO_BE_STORED(u), store into 'Current' */
1092    if (HasToBeStored(tableau,i)) 
1093      LtlSetSetElt(Current, i);
1094   
1095    /* if CONTRADICTION(u, ToCover, Current, Covered), return 'Cover' */
1096    if (Contradiction(tableau, i, ToCover, Current, Covered)) {
1097      ; /* return */
1098    }else if (Redundant(tableau, i, ToCover, Current, Covered)) {
1099      AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered, Cover);
1100      /* return */
1101    }else {
1102      if (Ctlsp_LtlFormulaIsElementary(tableau->abTable[i].F)) {
1103        LtlSetSetElt(Current, i);
1104        AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
1105                                Cover);
1106        /* return */
1107      }else {
1108        int A0B0 = tableau->abTable[i].A[0].B[0];
1109        int A0B1 = tableau->abTable[i].A[0].B[1];
1110        int A0n = tableau->abTable[i].A[0].n;
1111        int A1B0 = tableau->abTable[i].A[1].B[0];
1112        int A1B1 = tableau->abTable[i].A[1].B[1];
1113        int A1n = tableau->abTable[i].A[1].n;
1114       
1115        /* cover( (ToCover+alph2(u)-Current), Current, Covered, Cover) */
1116        if (A1B0 != -1 || A1B1!= -1 || A1n!= -1) {
1117          LtlSet_t *saveToCover = LtlSetCopy(ToCover);       
1118          if (A1B0 != -1)
1119            if (!LtlSetGetElt(Current, A1B0))
1120              LtlSetSetElt(ToCover, A1B0);
1121          if (A1B1 != -1)
1122            if (!LtlSetGetElt(Current, A1B1))
1123              LtlSetSetElt(ToCover, A1B1);
1124          if (A1n != -1)
1125            if (!LtlSetGetElt(Current, A1n))
1126              LtlSetSetElt(ToCover, A1n);
1127         
1128          AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
1129                                  Cover);
1130         
1131          LtlSetAssign(ToCover, saveToCover);
1132          LtlSetFree(saveToCover);
1133        }
1134       
1135        /* cover( (ToCover+alph1(u)-Current), Current, Covered, Cover) */
1136        if (A0B0 != -1 || A0B1!= -1 || A0n!= -1) {           
1137          if (A0B0 != -1)
1138            if (!LtlSetGetElt(Current, A0B0))
1139              LtlSetSetElt(ToCover, A0B0);
1140          if (A0B1 != -1)
1141            if (!LtlSetGetElt(Current, A0B1))
1142              LtlSetSetElt(ToCover, A0B1);
1143          if (A0n != -1)
1144            if (!LtlSetGetElt(Current, A0n))
1145              LtlSetSetElt(ToCover, A0n);
1146         
1147          AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
1148                                  Cover);
1149        }
1150        /* return */
1151      }
1152    }
1153  }
1154 
1155  /* Clean-Ups */
1156  LtlSetFree(ToCover);
1157  LtlSetFree(Current);
1158  LtlSetFree(Covered);
1159}
1160
1161
1162
1163
1164
Note: See TracBrowser for help on using the repository browser.