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

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

vis2.3
File size: 67.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ltlMinimize.c]
4
5  PackageName [ltl]
6
7  Synopsis    [Buechi automaton minimization.]
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: ltlMinimize.c,v 1.33 2009/04/09 02:21:13 fabio 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 lsList AutomatonPickInputCandidate(graph_t *G, vertex_t *vtx);
48static lsList AutomatonPickOutputCandidate(graph_t *G, vertex_t *vtx);
49static st_table * AutomatonVertexGetPreImg(graph_t *G, vertex_t *vtx);
50static st_table * AutomatonVertexGetImg(graph_t *G, vertex_t *vtx);
51static int AutomatonVertexHasSelfLoop(graph_t *G, vertex_t *vtx);
52static int AutomatonPfairEquivQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate);
53static int AutomatonPfairImplyQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate);
54static char * StTableDelete(st_table *tbl, char *item);
55static st_table * StTableAppend(st_table *tbl1, st_table *tbl2);
56static st_table * StTableRestrict(st_table *tbl1, st_table *tbl2);
57static st_table * StTableSubtract(st_table *tbl1, st_table *tbl2);
58static int StTableIsEqual(st_table *tbl1, st_table *tbl2, st_table *dontcare);
59static int StTableInclude(st_table *large, st_table *small, st_table *dontcare);
60static int StTableIsDisjoint(st_table *tbl1, st_table *tbl2, st_table *dontcare);
61static int StTableIsFair(lsList A_Fair, st_table *Class);
62static int AutomatonPartitionIsClique(graph_t *G, st_table *set);
63static st_table * AutomatonPartitionLabelLUB(st_table *set, array_t *Negate);
64static st_table * AutomatonPartitionLabelGLB(st_table *set, array_t *Negate);
65static st_table * AutomatonQuotientVertexGetClass(vertex_t *vtx);
66/*static int AutomatonVtxGetNodeIdx(vertex_t *v);*/
67
68/**AutomaticEnd***************************************************************/
69
70
71/*---------------------------------------------------------------------------*/
72/* Definition of exported functions                                          */
73/*---------------------------------------------------------------------------*/
74
75
76/**Function********************************************************************
77
78  Synopsis    [Minimize the Automaton using I/O Compatiblility and Dominance.]
79
80  Description [These minimizations are based on the structural information,
81  and are less effective than simulation-based techniques. They are used for
82  pre-processing since they are faster.Also, in some cases they go beyond what
83  simulation based minimization can do.
84
85  Here we consider 3 cases: Input Compatible, Output Compatible and Dominance.]
86
87  SideEffects [The automaton might be changed. In that case return 1.]
88
89  SeeAlso     []
90
91******************************************************************************/
92int
93Ltl_AutomatonMinimizeByIOCompatible(
94  Ltl_Automaton_t *A,
95  int verbosity)
96{
97  int changed = 0;
98  int flag;
99  lsList states, incand, outcand;
100  lsGen lsgen, lsgen2, lsgen3;
101  vertex_t *state, *otherstate, *s;
102  LtlSet_t *set, *set2;
103  st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3, *tbl4;
104  st_generator *stgen;
105
106
107  /* We go through all the states in A->G, and check for Input-Compatible,
108   * Output-Compatible, and Dominance
109   */
110  states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL);
111  lsForEachItem (states, lsgen, state) {
112    int localchanged = 0;
113    /* Compute the Image adn PreImg of 'state' for later use */
114    tbl0 = AutomatonVertexGetPreImg(A->G, state);
115    tbl1 = AutomatonVertexGetImg(A->G, state);
116
117    /* ############################
118     *  Check for Input Compatible
119     * ############################*/
120    incand = AutomatonPickInputCandidate(A->G, state);
121    lsForEachItem (incand, lsgen2, otherstate) {
122      /* p is 'state', q is 'otherstate' */
123      /* p != q */
124      if (state == otherstate) continue;
125      /* L(p) = L(q) */
126      set = LtlAutomatonVertexGetLabels(state);
127      set2 = LtlAutomatonVertexGetLabels(otherstate);
128      if (!LtlSetEqual(set, set2)) continue;
129      /* p \in Q0  <-> q \in Q0 */
130      if (st_is_member(A->Init, state) !=
131          st_is_member(A->Init, otherstate))
132        continue;
133      /* p \in F   <-> q \in F */
134      if (!AutomatonPfairEquivQfair(A, state, otherstate))  continue;
135      /* preImg(p) - {p,q} == preImg(q) - {p,q} */
136      tbl2 = AutomatonVertexGetPreImg(A->G, otherstate);
137      tbl3 = st_init_table(st_ptrcmp, st_ptrhash);
138      st_insert(tbl3, state, state);
139      st_insert(tbl3 , otherstate, otherstate);
140      flag = StTableIsEqual(tbl0, tbl2, tbl3);
141      st_free_table(tbl2);
142      st_free_table(tbl3);
143      if (!flag)              continue;
144      /* q \in [delta(p)+delta(q)] <-> p \in [delta(p)+delta(q)] */
145      tbl2 = AutomatonVertexGetImg(A->G, otherstate);
146      if ( (st_is_member(tbl1,state) ||
147            st_is_member(tbl2,state))
148           !=
149           (st_is_member(tbl1,otherstate) ||
150            st_is_member(tbl2,otherstate)) ) {
151              st_free_table(tbl2);
152              continue;
153      }
154
155      /* ######## (state, otherstate) :: input compatible #######
156       * we merge the two state by deleting 'state'
157       * Notice that now we have the following data available:
158       * tbl0 = PreImg(state),
159       * tbl1 = Img(state),
160       * tbl2 = Img(otherstate)
161       */
162
163      /* Update intial states */
164      StTableDelete(A->Init, (char *)state);
165      /* Add edges (otherstate, s), here s is the sucessor of 'state' */
166      st_foreach_item(tbl1, stgen, &s, NIL(char *)) {
167        if (s != state && !st_is_member(tbl2, s))
168          g_add_edge(otherstate, s);
169      }
170      /* Remove 'otherstate' also if state isn't in dontcare */
171      if (!st_is_member(A->dontcare, state))
172        StTableDelete(A->dontcare, (char *)otherstate);
173      /* Remove 'state' from dontcare (if applicable) */
174      StTableDelete(A->dontcare, (char *)state);
175      /* Update fairness conditions */
176      lsForEachItem (A->Fair, lsgen3, FairSet) {
177        StTableDelete(FairSet, (char *)state);
178      }
179      /* Remove 'state' from the automaton */
180      g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
181
182      st_free_table(tbl2);
183      /* terminate iteration on incand list */
184      changed = localchanged = 1;
185
186      lsFinish(lsgen2);
187      break;
188    }
189    lsDestroy(incand, (void (*)(lsGeneric)) 0);
190    if (localchanged) {
191      st_free_table(tbl0);
192      st_free_table(tbl1);
193      continue;
194    }
195
196
197    /* ############################
198     * Check for Output Compatible
199     * ############################
200     */
201    outcand = AutomatonPickOutputCandidate(A->G, state);
202    lsForEachItem (outcand, lsgen2, otherstate) {
203      /* p != q */
204      if (state == otherstate) continue;
205      /* L(p) = L(q) */
206      set = LtlAutomatonVertexGetLabels(state);
207      set2 = LtlAutomatonVertexGetLabels(otherstate);
208      if (!LtlSetEqual(set, set2)) continue;
209      /* p \in F   <-> q \in F */
210      if (!AutomatonPfairEquivQfair(A, state, otherstate)) continue;
211      /* Img(p) - {p,q} == Img(q) - {p,q} */
212      tbl2 = AutomatonVertexGetImg(A->G, otherstate);
213      tbl3 = st_init_table(st_ptrcmp, st_ptrhash);
214      st_insert(tbl3, state, state);
215      st_insert(tbl3, otherstate, otherstate);
216      flag = StTableIsEqual(tbl1, tbl2, tbl3);
217      st_free_table(tbl3);
218      if (!flag) {
219        st_free_table(tbl2);
220        continue;
221      }
222      /* q \in delta(p) + p \in delta(p)] <->
223       * q \in delta(q) + p \in delta(q)]
224       */
225      flag = 0;
226      if ( (st_is_member(tbl1, state) ||
227            st_is_member(tbl1, otherstate))
228           !=
229           (st_is_member(tbl2, state) ||
230            st_is_member(tbl2, otherstate)) ) {
231        st_free_table(tbl2);
232        continue;
233      }
234
235      /* ######## (state, otherstate) :: output compatible #######
236       * Merge the two state by deleting 'state'
237       * Notice that now we have the following data:
238       *     tbl0 = PreImg(state)
239       *     tbl1 = Img(state)
240       *     tbl2 = Img(otherstate)
241       */
242      tbl3 = AutomatonVertexGetPreImg(A->G, otherstate);
243
244      /* Add 'otherstate to Q0 if 'state' is in it */
245      if (st_is_member(A->Init, state)) {
246        st_delete(A->Init, &state, NIL(char *));
247        if(!st_is_member(A->Init, otherstate))
248          st_insert(A->Init, otherstate, otherstate);
249      }
250      /* Add edge (s, otherstate) where 's' is in PreImg(state) */
251      st_foreach_item(tbl0, stgen, &s, NIL(char *)) {
252        if (s != state && s != otherstate &&
253            !st_is_member(tbl3, s))
254          g_add_edge(s, otherstate);
255      }
256      /* Add edge (otherstate, otherstate) if there exist (state, state) or
257       * (state, otherstate)
258       */
259      if (st_is_member(tbl1, otherstate) ||
260          st_is_member(tbl1, state))
261        if (!st_is_member(tbl2, otherstate))
262          g_add_edge(otherstate, otherstate);
263      /* Update don't care conditions. If 'state' isn't in dontcare, also
264       * remove 'otherstate'
265       */
266      if (!st_is_member(A->dontcare, state)) {
267        StTableDelete(A->dontcare, (char *)otherstate);
268      }
269      StTableDelete(A->dontcare, (char *)state);
270      /* Remove 'state' from FairSets */
271      lsForEachItem (A->Fair, lsgen3, FairSet) {
272        StTableDelete(FairSet, (char *)state);
273      }
274      /* Remove 'state' from the automaton */
275      g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
276
277      st_free_table(tbl2);
278      st_free_table(tbl3);
279      /* terminate iteration on incand list */
280      changed = localchanged = 1;
281
282      lsFinish(lsgen2);
283      break;
284    }
285    if (localchanged) {
286      lsDestroy(outcand, (void (*)(lsGeneric)) 0);
287      st_free_table(tbl0);
288      st_free_table(tbl1);
289      continue;
290    }
291
292
293    /* ############################
294     * Check for Dominance
295     * ############################
296     * We already have the lsList 'outcand'
297     */
298    lsForEachItem (outcand, lsgen2, otherstate) {
299      /* p != q */
300      if (state == otherstate) continue;
301      /* L(p) \leq L(q) (set(Lp) > set(Lq) */
302      set = LtlAutomatonVertexGetLabels(state);
303      set2 = LtlAutomatonVertexGetLabels(otherstate);
304      if (!LtlSetInclude(set, set2)) continue;
305      /* p \in Q0 -> q \in Q0 */
306      if (st_is_member(A->Init, state) &&
307          !st_is_member(A->Init, otherstate))
308        continue;
309      /* p \in F   -> q \in F */
310      if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue;
311      /* Img(p) is less than Img(q) */
312      tbl2 = AutomatonVertexGetImg(A->G, otherstate);
313      flag = StTableInclude(tbl2, tbl1, NIL(st_table));
314      /* p is in Img(p)  ->  q is in Img(q) */
315      if (flag) {
316        flag = (!st_is_member(tbl1, state) ||
317                st_is_member(tbl2, otherstate));
318      }
319      st_free_table(tbl2);
320      if (!flag)       continue;
321      /* PreImg(p)-{p} \leq PreImg(q)-{p} */
322      tbl3 =  AutomatonVertexGetPreImg(A->G, otherstate);
323      tbl4 = st_init_table(st_ptrcmp, st_ptrhash);
324      st_insert(tbl4, state, state);
325      flag = StTableInclude(tbl3, tbl0, tbl4);
326      st_free_table(tbl4);
327      st_free_table(tbl3);
328      if (!flag)       continue;
329
330      /* ######## otherstate dominates state #######
331       * Remove 'state'
332       * Notice that now we have the following data:
333       *     tbl0 = PreImg(state)
334       *     tbl1 = Img(state)
335       */
336      /* Remove 'state' from Initial states */
337      StTableDelete(A->Init, (char *)state);
338      /* Remove 'otherstate' if 'state' isn't in dontcare */
339      if (!st_is_member(A->dontcare, state)) {
340        StTableDelete(A->dontcare, (char *)otherstate);
341      }
342      StTableDelete(A->dontcare, (char *)state);
343      /* Remove 'state' from FairSets */
344      lsForEachItem (A->Fair, lsgen3, FairSet) {
345        StTableDelete(FairSet, (char *)state);
346      }
347      /* Remove 'state' from the automaton */
348      g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
349
350      /* terminate iteration on incand list */
351      changed = localchanged = 1;
352
353      lsFinish(lsgen2);
354      break;
355    }
356    lsDestroy(outcand, (void (*)(lsGeneric)) 0);
357
358
359    st_free_table(tbl0);
360    st_free_table(tbl1);
361
362  }
363  lsDestroy(states, (void (*)(lsGeneric)) 0);
364
365
366  return changed;
367}
368
369/**Function********************************************************************
370
371  Synopsis    [Minimize the Automaton using Direct Simulation.]
372
373  Description [Compute direct-simulation relation, and minimize the automaton
374  according to the following two cases:
375  1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa)
376  2) Remove edges from their common predecessors to p if p is direct
377  simulated by q.]
378
379  SideEffects [The automaton might be changed. if so, return 1.]
380
381  SeeAlso     []
382
383******************************************************************************/
384int
385Ltl_AutomatonMinimizeByDirectSimulation(
386  Ltl_Automaton_t *A,
387  int verbosity)
388{
389  int changed = 0;
390  int flag = 0;
391
392  lsList states, otherstates, list, queue;
393  lsGen lsgen, lsgen1;
394
395  edge_t *e;
396  vertex_t *state, *otherstate;
397  vertex_t *p, *q, *s, *t, *u, *v;
398  LtlSet_t *set, *set2;
399
400  st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3;
401  st_table *simul, *enqueued;
402  st_generator *stgen, *stgen1, *stgen2;
403
404  LtlPair_t *pair, *pair2;
405
406
407  /* store the simulation-relation in hash tables and queue list */
408  simul = st_init_table(LtlPairCompare, LtlPairHash);
409  enqueued = st_init_table(LtlPairCompare, LtlPairHash);
410  queue = lsCreate();
411
412  /*######################################
413   * Initialize sim rln to all pairs (p,q)
414   *######################################
415   */
416  states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL);
417  otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL);
418  lsForEachItem (states, lsgen, state) {
419    lsForEachItem (otherstates, lsgen1, otherstate) {
420      /* p != q */
421      if (state == otherstate) continue;
422      /* L(p) \leq L(q) (set(Lp) > set(Lq) */
423      set = LtlAutomatonVertexGetLabels(state);
424      set2 = LtlAutomatonVertexGetLabels(otherstate);
425      if (!LtlSetInclude(set, set2)) continue;
426      /* p \in F   -> q \in F */
427      if (!AutomatonPfairImplyQfair(A, state, otherstate))   continue;
428
429      /* put (state, otherstate) into simul-relation (candidate) */
430      pair = LtlPairNew((char *)state, (char *)otherstate);
431      st_insert(simul, pair, pair);
432      st_insert(enqueued, pair, pair);
433      lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
434    }
435  }
436  lsDestroy(states, (void (*)(lsGeneric)) NULL);
437  lsDestroy(otherstates, (void (*)(lsGeneric)) NULL);
438
439
440  /*######################################
441   * Compute the "Greatest Fixpoint"
442   *######################################
443   */
444  while (lsDelBegin(queue, &pair) != LS_NOMORE) {
445    st_delete(enqueued, &pair, NIL(char *));
446    p = (vertex_t *)pair->First;
447    q = (vertex_t *)pair->Second;
448
449    /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such
450     * that (s, t) is in simulation relation candidate list
451     */
452    tbl0 = AutomatonVertexGetImg(A->G, p);
453    tbl1 = AutomatonVertexGetImg(A->G, q);
454    st_foreach_item(tbl0, stgen, &s, NIL(char *)) {
455      flag = 0;
456      st_foreach_item(tbl1, stgen1, &t, NIL(char *)) {
457        flag = (s==t);
458        if (flag) {
459          st_free_gen(stgen1);
460          break;
461        }
462        pair2 = LtlPairNew((char *)s, (char *)t);
463        flag = st_is_member(simul, pair2);
464        LtlPairFree(pair2);
465        if (flag) {
466          st_free_gen(stgen1);
467          break;
468        }
469      }
470      if (!flag)  {
471        st_free_gen(stgen);
472        break;
473      }
474    }
475    st_free_table(tbl0);
476    st_free_table(tbl1);
477    if (flag) continue;
478
479    /*  (p, q) is not a simulation relation */
480    st_delete(simul, &pair, &pair);
481    LtlPairFree(pair);
482
483    /* Enqueue perturbed pairs */
484    tbl2 = AutomatonVertexGetPreImg(A->G, p);
485    tbl3 = AutomatonVertexGetPreImg(A->G, q);
486    st_foreach_item(tbl2, stgen1, &u, NIL(char *)) {
487      st_foreach_item(tbl3, stgen2, &v, NIL(char *)) {
488        pair2 = LtlPairNew((char *)u, (char *)v);
489        if (st_lookup(simul, pair2, &pair)) {
490          if (!st_is_member(enqueued, pair2)) {
491            st_insert(enqueued, pair, pair);
492            lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
493          }
494        }
495        LtlPairFree(pair2);
496      }
497    }
498    st_free_table(tbl2);
499    st_free_table(tbl3);
500
501  }
502  lsDestroy(queue, (void (*)(lsGeneric))0);
503  st_free_table(enqueued);
504
505
506  /*######################################
507   * Simplify by Bi-Sim equivalent states
508   *######################################
509   */
510  /* to store removed states */
511  tbl1 = st_init_table(st_ptrcmp, st_ptrhash);
512  /* so that we can modify 'simul' within for loop */
513  tbl0 = st_copy(simul);
514  st_foreach_item (tbl0, stgen, &pair, NIL(char *)) {
515    p = (vertex_t *)pair->First;
516    q = (vertex_t *)pair->Second;
517    /* make sure neither has been removed */
518    if (st_is_member(tbl1, p) || st_is_member(tbl1, q))
519      continue;
520    /* make sure it is Bi-simulation by testing the other direction */
521    pair2 = LtlPairNew((char *)q, (char *)p);
522    flag = st_lookup(simul, pair2, &pair);
523    LtlPairFree(pair2);
524    if (!flag) continue;
525
526    /*#### Direct BI-SIMULATION equivalent states####*/
527    /* Theorem applies */
528    /* remove its swap: (q, p) from simul-rln */
529    st_delete(simul, &pair, &pair);
530    LtlPairFree(pair);
531    /* Remove p, and connect its predecessors to q */
532    tbl2 = AutomatonVertexGetPreImg(A->G, p);
533    tbl3 = AutomatonVertexGetPreImg(A->G, q);
534    st_foreach_item(tbl2, stgen1, &s, NIL(char *)) {
535      if (s == p) continue;
536      if (!st_is_member(tbl3, (char *)s))
537        g_add_edge(s, q);
538    }
539    st_free_table(tbl2);
540    st_free_table(tbl3);
541    /* Update the fair sets */
542    lsForEachItem (A->Fair, lsgen, FairSet) {
543      StTableDelete(FairSet, (char *)p);
544    }
545    /* If 'p' is in Q0, Remove 'p' and put 'q' in Q0 */
546    if (st_is_member(A->Init, p)) {
547      st_delete(A->Init, &p, NIL(char *));
548      if (!st_is_member(A->Init, q))
549        st_insert(A->Init, q, q);
550    }
551    /* Remove 'p' from dontcare (if it's in it ) */
552    StTableDelete(A->dontcare, (char *)p);
553
554    /* Remove 'p' from the automaton */
555    st_insert(tbl1, p, p);
556    g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
557    changed = 1;
558  }
559  st_free_table(tbl0);
560
561
562  /*######################################
563   * Remove arcs to direct-simulated states
564   *######################################
565   */
566  /* so that we can modify simul with the for loop */
567  tbl0 = st_copy(simul);
568  st_foreach_item (tbl0, stgen, &pair, NIL(char *)) {
569    /* 'p' is simulated by 'q' */
570    p = (vertex_t *)pair->First;
571    q = (vertex_t *)pair->Second;
572    /* Make sure neither hasn't been removed yet */
573    if (st_is_member(tbl1, p) || st_is_member(tbl1, q))
574      continue;
575
576    /*#### p is direct-simulated by q####*/
577    /* Theorem applies */
578    /* Drop arcs from their common predecessors to p */
579    tbl3 = AutomatonVertexGetPreImg(A->G, q);
580    list = lsCopy(g_get_in_edges(p), (lsGeneric (*)(lsGeneric)) NULL);
581    lsForEachItem (list, lsgen,  e) {
582      if (!st_is_member(tbl3, g_e_source(e)))  continue;
583      g_delete_edge(e, (void (*)(gGeneric))0);
584      changed = 1;
585    }
586    lsDestroy(list, (void (*)(lsGeneric)) 0);
587    st_free_table(tbl3);
588    /* Remove 'p' from Q0 if 'q' is in Q0 */
589    if (st_is_member(A->Init, q)) {
590      StTableDelete(A->Init, (char *)p);
591      changed = 1;
592    }
593
594  }
595  st_free_table (tbl0);
596
597  st_free_table (tbl1);
598
599  st_foreach_item(simul, stgen, &pair, NIL(char *)) {
600    LtlPairFree(pair);
601  }
602  st_free_table (simul);
603
604  return changed;
605}
606
607
608/**Function********************************************************************
609
610  Synopsis    [Mark trivial SCCs as Fair states]
611
612  Description [Mark trivial SCCs as Fair states]
613
614  SideEffects []
615
616  SeeAlso     []
617
618******************************************************************************/
619void
620Ltl_AutomatonAddFairStates(
621  Ltl_Automaton_t *A)
622{
623
624  long isFair;
625
626  lsGen lsgen1;
627
628  st_generator *stgen, *stgen2;
629  st_table *FairSet, *Class;
630
631  Ltl_AutomatonComputeSCC(A, 1);
632  if (A->Q) {
633    Ltl_AutomatonFree((gGeneric) A->Q);
634    A->Q = NIL(Ltl_Automaton_t);
635  }
636  A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC);
637  /*
638    Mark trivial SCCs as Fair states
639   */
640  st_foreach_item(A->SCC, stgen, &Class, &isFair) {
641    vertex_t *state;
642
643    if (isFair == 2) { /* trivial SCC */
644      lsForEachItem (A->Fair, lsgen1, FairSet) {
645        st_foreach_item(Class, stgen2, &state, NIL(char *)) {
646          if (!st_is_member(FairSet, state)) {
647            if (st_is_member(A->dontcare, state)){
648              StTableDelete(A->dontcare, (char *)state);
649            }
650            st_insert(FairSet, state, state);
651          }
652        }
653      }
654    }
655  }
656}
657
658
659/**Function********************************************************************
660
661  Synopsis    [Maximize the Automaton using Direct Simulation.]
662
663  Description [Compute direct-simulation relation, and minimize the automaton
664  according to the following two cases:
665  1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa)
666  2) Remove edges from their common predecessors to p if p is direct
667  simulated by q.]
668
669  SideEffects [The automaton might be changed. if so, return 1.]
670
671  SeeAlso     []
672
673******************************************************************************/
674int
675Ltl_AutomatonMaximizeByDirectSimulation(
676  Ltl_Automaton_t *A,
677  int verbosity)
678{
679  int changed = 0;
680  int flag = 0;
681
682  lsList states, otherstates, queue;
683  lsGen lsgen, lsgen1;
684
685  vertex_t *state, *otherstate;
686  vertex_t *p, *q, *s, *t, *u, *v;
687  LtlSet_t *set, *set2;
688
689  st_table *tbl0, *tbl1, *tbl2, *tbl3;
690  st_table *simul, *enqueued;
691  st_generator *stgen, *stgen1, *stgen2;
692
693  LtlPair_t *pair, *pair2;
694
695  /*
696    Ltl_AutomatonAddFairStates(A);
697  */
698  /* store the simulation-relation in hash tables and queue list */
699  simul = st_init_table(LtlPairCompare, LtlPairHash);
700  enqueued = st_init_table(LtlPairCompare, LtlPairHash);
701  queue = lsCreate();
702
703  /*######################################
704   * Initialize sim rln to all pairs (p,q)
705   *######################################
706   */
707  states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL);
708  otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL);
709  lsForEachItem (states, lsgen, state) {
710    lsForEachItem (otherstates, lsgen1, otherstate) {
711      /* p != q */
712      if (state == otherstate) continue;
713      /* L(p) \leq L(q) (set(Lp) > set(Lq) */
714      set = LtlAutomatonVertexGetLabels(state);
715      set2 = LtlAutomatonVertexGetLabels(otherstate);
716      if (!LtlSetInclude(set, set2)) continue;
717      /* p \in F   -> q \in F */
718      if (!AutomatonPfairImplyQfair(A, state, otherstate))   continue;
719
720      /* put (state, otherstate) into simul-relation (candidate) */
721      pair = LtlPairNew((char *)state, (char *)otherstate);
722      st_insert(simul, pair, pair);
723      st_insert(enqueued, pair, pair);
724      lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
725    }
726  }
727  lsDestroy(states, (void (*)(lsGeneric)) NULL);
728  lsDestroy(otherstates, (void (*)(lsGeneric)) NULL);
729
730
731  /*######################################
732   * Compute the "Greatest Fixpoint"
733   *######################################
734   */
735  while (lsDelBegin(queue, &pair) != LS_NOMORE) {
736    st_delete(enqueued, &pair, NIL(char *));
737    p = (vertex_t *)pair->First;
738    q = (vertex_t *)pair->Second;
739
740    /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such
741     * that (s, t) is in simulation relation candidate list
742     */
743    tbl0 = AutomatonVertexGetImg(A->G, p);
744    tbl1 = AutomatonVertexGetImg(A->G, q);
745    st_foreach_item(tbl0, stgen, &s, NIL(char *)) {
746      flag = 0;
747      st_foreach_item(tbl1, stgen1, &t, NIL(char *)) {
748        flag = (s==t);
749        if (flag) {
750          st_free_gen(stgen1);
751          break;
752        }
753        pair2 = LtlPairNew((char *)s, (char *)t);
754        flag = st_is_member(simul, pair2);
755        LtlPairFree(pair2);
756        if (flag) {
757          st_free_gen(stgen1);
758          break;
759        }
760      }
761      if (!flag)  {
762        st_free_gen(stgen);
763        break;
764      }
765    }
766    st_free_table(tbl0);
767    st_free_table(tbl1);
768    if (flag) continue;
769
770    /*  (p, q) is not a simulation relation */
771    st_delete(simul, &pair, &pair);
772    LtlPairFree(pair);
773
774    /* Enqueue perturbed pairs */
775    tbl2 = AutomatonVertexGetPreImg(A->G, p);
776    tbl3 = AutomatonVertexGetPreImg(A->G, q);
777    st_foreach_item(tbl2, stgen1, &u, NIL(char *)) {
778      st_foreach_item(tbl3, stgen2, &v, NIL(char *)) {
779        pair2 = LtlPairNew((char *)u, (char *)v);
780        if (st_lookup(simul, pair2, &pair)) {
781          if (!st_is_member(enqueued, pair2)) {
782            st_insert(enqueued, pair, pair);
783            lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
784          }
785        }
786        LtlPairFree(pair2);
787      }
788    }
789    st_free_table(tbl2);
790    st_free_table(tbl3);
791
792  }
793  lsDestroy(queue, (void (*)(lsGeneric))0);
794  st_free_table(enqueued);
795
796
797  /*######################################
798   * Add arcs to direct-simulated states
799   *######################################
800   */
801
802  /* so that we can modify simul with the for-loop */
803  tbl0 = st_copy(simul);
804  st_foreach_item (tbl0, stgen, &pair, NIL(char *)) {
805    /* 'p' is simulated by 'q' */
806    p = (vertex_t *)pair->First;
807    q = (vertex_t *)pair->Second;
808    /*
809      Add arcs from the predecessors of q to p
810     */
811    tbl2 = AutomatonVertexGetPreImg(A->G, p);
812    tbl3 = AutomatonVertexGetPreImg(A->G, q);
813    st_foreach_item(tbl3, stgen1, &s, NIL(char *)) {
814      if (!st_is_member(tbl2, s)){
815        g_add_edge(s, p);
816        changed = 1;
817      }
818    }
819    st_free_table(tbl2);
820    st_free_table(tbl3);
821  }
822  st_free_table (tbl0);
823
824  st_foreach_item(simul, stgen, &pair, NIL(char *)) {
825    LtlPairFree(pair);
826  }
827  st_free_table (simul);
828
829  return changed;
830}
831
832
833/**Function********************************************************************
834
835  Synopsis    [Minimize the Automaton using Reverse Simulation.]
836
837  Description [Compute Reverse-Simulation relation, and minimize the automaton
838  according to the following 2 cases:
839  1) remove p if (p,q) is a Bi-Simulation relation
840  2) remove edges from p to their common sucessors if p is reverse simulated
841  by q.]
842
843  SideEffects [The automaton might be changed. if so, return 1.]
844
845  SeeAlso     []
846
847******************************************************************************/
848int
849Ltl_AutomatonMinimizeByReverseSimulation(
850  Ltl_Automaton_t *A,
851  int verbosity)
852{
853  int changed = 0;
854  int flag = 0;
855
856  lsList states, otherstates, list, queue;
857  lsGen lsgen, lsgen1;
858
859  edge_t *e;
860  vertex_t *state, *otherstate;
861  vertex_t *p, *q, *s, *t, *u, *v;
862  LtlSet_t *set, *set2;
863
864  st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3;
865  st_table *simul, *enqueued;
866  st_generator *stgen, *stgen1, *stgen2;
867
868  LtlPair_t *pair, *pair2;
869
870
871  /* store the simulation-relation in hash tables and queue list */
872  simul = st_init_table(LtlPairCompare, LtlPairHash);
873  enqueued = st_init_table(LtlPairCompare, LtlPairHash);
874  queue = lsCreate();
875
876  /*######################################
877   * Initialize sim rln to all pairs (p,q)
878   *######################################
879   */
880  states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL);
881  otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL);
882  lsForEachItem (states, lsgen, state) {
883    lsForEachItem (otherstates, lsgen1, otherstate) {
884      /* p != q */
885      if (state == otherstate) continue;
886      /* L(p) <= L(q), in other words, (set(Lp) >= set(Lq) */
887      set = LtlAutomatonVertexGetLabels(state);
888      set2 = LtlAutomatonVertexGetLabels(otherstate);
889      if (!LtlSetInclude(set, set2))  continue;
890      /* p is in Q0  ->  q is in Q0 */
891      if (st_is_member(A->Init, state) &&
892          !st_is_member(A->Init, otherstate))
893        continue;
894      /* p is in F   ->  q is in F */
895      if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue;
896
897      /* put (state, otherstate) into simul-relation */
898      pair = LtlPairNew((char *)state, (char *)otherstate);
899      st_insert(simul, pair, pair);
900      st_insert(enqueued, pair, pair);
901      lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
902    }
903  }
904  lsDestroy(states, (void (*)(lsGeneric)) NULL);
905  lsDestroy(otherstates, (void (*)(lsGeneric)) NULL);
906
907
908  /*######################################
909   * Compute the "Greatest Fixpoint"
910   *######################################
911   */
912  while (lsDelBegin(queue, &pair) != LS_NOMORE) {
913    st_delete(enqueued, &pair, NIL(char *));
914    p = (vertex_t *)pair->First;
915    q = (vertex_t *)pair->Second;
916
917    /* For each 's' in Img(p), there must exists a 't' Img(q) such that
918     * (s, t) is also a reverse simulation pair
919     */
920    tbl0 = AutomatonVertexGetPreImg(A->G, p);
921    tbl1 = AutomatonVertexGetPreImg(A->G, q);
922    st_foreach_item(tbl0, stgen, &s, NIL(char *)) {
923      flag = 0;
924      st_foreach_item(tbl1, stgen1, &t, NIL(char *)) {
925        flag = (s==t);
926        if (flag) {
927          st_free_gen(stgen1);
928          break;
929        }
930        pair2 = LtlPairNew((char *)s, (char *)t);
931        flag = st_is_member(simul, pair2);
932        LtlPairFree(pair2);
933        if (flag) {
934          st_free_gen(stgen1);
935          break;
936        }
937      }
938      if (!flag) {
939        st_free_gen(stgen);
940        break;
941      }
942    }
943    st_free_table(tbl0);
944    st_free_table(tbl1);
945
946    if (flag) continue;
947
948    /* (p, q) is not a simulation relation */
949    st_delete(simul, &pair, &pair);
950    LtlPairFree(pair);
951
952    /* Enqueue perturbed pairs */
953    tbl2 = AutomatonVertexGetImg(A->G, p);
954    tbl3 = AutomatonVertexGetImg(A->G, q);
955    st_foreach_item(tbl2, stgen1, &u, NIL(char *)) {
956      st_foreach_item(tbl3, stgen2, &v, NIL(char *)) {
957        pair2 = LtlPairNew((char *)u, (char *)v);
958        if (st_lookup(simul, pair2, &pair))
959          if(!st_is_member(enqueued, pair2)) {
960            st_insert(enqueued, pair, pair);
961            lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle));
962          }
963        LtlPairFree(pair2);
964      }
965    }
966    st_free_table(tbl2);
967    st_free_table(tbl3);
968  }
969  lsDestroy(queue, (void (*)(lsGeneric))0);
970  st_free_table(enqueued);
971
972
973  /*######################################
974   * Simplify by Bi-Sim equivalent states
975   *######################################
976   */
977  /* to store removed states */
978  tbl1 = st_init_table(st_ptrcmp, st_ptrhash);
979  /* so that we can modify simul with the for loop */
980  tbl0 = st_copy(simul);
981  st_foreach_item (tbl0, stgen, &pair, NIL(char *)) {
982    p = (vertex_t *)pair->First;
983    q = (vertex_t *)pair->Second;
984    /* Make sure neither has been removed */
985    if (st_is_member(tbl1, p) || st_is_member(tbl1, q))
986      continue;
987    /* Make sure it is Bi-simulation by checking the other direction*/
988    pair2 = LtlPairNew((char *)q, (char *)p);
989    flag = st_lookup(simul, pair2, &pair);
990    LtlPairFree(pair2);
991    if (!flag) continue;
992
993    /*#### Direct BI-SIMULATION equivalent states####*/
994    /* Theorem applies */
995    /* Remove its swap: (q, p) from simul-rln */
996    st_delete(simul, &pair, &pair);
997    LtlPairFree(pair);
998    /* Remove 'p' and connect 'q' to all its successors */
999    tbl2 = AutomatonVertexGetImg(A->G, p);
1000    tbl3 = AutomatonVertexGetImg(A->G, q);
1001    st_foreach_item(tbl2, stgen1, &s, NIL(char *)) {
1002      if (s == p) continue;
1003      if (!st_is_member(tbl3, s))
1004        g_add_edge(q, s);
1005    }
1006    st_free_table(tbl2);
1007    st_free_table(tbl3);
1008    /* Update the fairsets (remove 'p') */
1009    lsForEachItem (A->Fair, lsgen, FairSet) {
1010      StTableDelete(FairSet, (char *)p);
1011    }
1012    /* Remove 'p' from Q0 */
1013    StTableDelete(A->Init, (char *)p);
1014    /* Remove 'p' form dontcare if it's in it */
1015    StTableDelete(A->dontcare, (char *)p);
1016
1017    /* Remove 'p' from the automaton */
1018    st_insert(tbl1, p, p);
1019    g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
1020    changed = 1;
1021  }
1022  st_free_table(tbl0);
1023
1024
1025  /*######################################
1026   * Remove arcs from Reverse-simulated states
1027   *#####################################*/
1028  /* so that we can modify simul with the for loop */
1029  tbl0 = st_copy(simul);
1030  st_foreach_item (tbl0, stgen, &pair, NIL(char *)) {
1031    /* 'p' is simulated by 'q' */
1032    p = (vertex_t *)pair->First;
1033    q = (vertex_t *)pair->Second;
1034    /* Make sure that neither has been removed */
1035    if (st_is_member(tbl1, p) || st_is_member(tbl1, q))
1036      continue;
1037
1038    /*#### p is reverse-simulated by q####*/
1039    /* Theorem applies */
1040    /* Drop arcs from 'p' to their common successors */
1041    tbl3 = AutomatonVertexGetImg(A->G, q);
1042    list = lsCopy(g_get_out_edges(p), (lsGeneric (*)(lsGeneric)) NULL);
1043    lsForEachItem (list, lsgen,  e) {
1044      if (!st_is_member(tbl3, g_e_dest(e)))  continue;
1045      g_delete_edge(e, (void (*)(gGeneric))0);
1046      changed = 1;
1047    }
1048    lsDestroy(list, (void (*)(lsGeneric)) 0);
1049    st_free_table(tbl3);
1050  }
1051  st_free_table (tbl0);
1052
1053  st_free_table (tbl1);
1054
1055  st_foreach_item(simul, stgen, &pair, NIL(char *)) {
1056    LtlPairFree(pair);
1057  }
1058  st_free_table (simul);
1059
1060  return changed;
1061}
1062
1063
1064/**Function********************************************************************
1065
1066  Synopsis    [Remove states that cannot reach any fair SCC and perform other
1067  simplifications (simplify fair sets).]
1068
1069  Description [We consider the following cases concerning fair SCCs:
1070  1. Remove redundant transitions from predecessors of universal states (a
1071  state with TRUE label and a self-loop, and it belongs to all fair sets.)
1072  2. Remove all states that can not reach any fair SCC
1073  3. Remove duplicate fair set and Shrink the fair sets
1074  ]
1075
1076  SideEffects [The automaton might be changed, in which case return 1. Also,
1077  the A->SCC and A->Q are RE-computed.]
1078
1079  SeeAlso     []
1080
1081******************************************************************************/
1082int
1083Ltl_AutomatonMinimizeByPrune(
1084  Ltl_Automaton_t *A,
1085  int verbosity)
1086{
1087  st_generator *stgen, *stgen1, *stgen2;
1088  st_table *FairSet, *otherset, *Class, *scc, *rest;
1089  st_table *tbl, *tbl1, *tbl2;
1090  lsList states, list;
1091  lsGen lsgen, lsgen1;
1092  vertex_t *state, *s, *greatest, *qstate;
1093  edge_t *e;
1094  long isFair;
1095  int flag, totalnum, procnum;
1096
1097  /* Eliminate redundant edges  from the predecessors of universal states.
1098   * (A universal state is a state labeled 'TRUE' with a self-loop, and it
1099   * should belong to all FairSets)
1100   */
1101  states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL);
1102  lsForEachItem (states, lsgen, state) {
1103    /* label = TRUE */
1104    if (LtlSetCardinality(LtlAutomatonVertexGetLabels(state)) != 0)
1105      continue;
1106    /* self-loop */
1107    if (!AutomatonVertexHasSelfLoop(A->G, state)) continue;
1108    /* blongs to all fairSet */
1109    flag = 1;
1110    lsForEachItem (A->Fair, lsgen1, FairSet) {
1111      if (!st_is_member(FairSet, state)) {
1112        flag = 0;
1113        lsFinish(lsgen1);
1114        break;
1115      }
1116    }
1117    if (!flag)  continue;
1118    /* We can apply the theorem: Remove edges from its predecessors to
1119     * other siblings
1120     */
1121    tbl = AutomatonVertexGetPreImg(A->G, state);
1122    st_foreach_item(tbl, stgen, &s, NIL(char *)) {
1123      if (s == state) continue;
1124      list = lsCopy(g_get_out_edges(s), (lsGeneric (*)(lsGeneric))0);
1125      lsForEachItem(list, lsgen1, e) {
1126        if (g_e_dest(e) != state)
1127          g_delete_edge(e, (void (*)(gGeneric))0);
1128      }
1129      lsDestroy(list, (void (*)(lsGeneric))0);
1130    }
1131    st_free_table(tbl);
1132  }
1133
1134
1135  /*2) Compute all the SCCs, and build the SCC-quotient graph
1136   * every time before pruning, we need to re-compute the SCC graph
1137   */
1138  Ltl_AutomatonComputeSCC(A, 1);
1139  if (A->Q) {
1140    Ltl_AutomatonFree((gGeneric) A->Q);
1141    A->Q = NIL(Ltl_Automaton_t);
1142  }
1143  A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC);
1144
1145  /* Mark those states without loop going through as "don't care states" */
1146  st_foreach_item(A->SCC, stgen, &Class, &isFair) {
1147    if (isFair == 2)
1148      StTableAppend(A->dontcare, Class);
1149  }
1150
1151  /* Restrict automaton to those states that can reach a fair SCC
1152   * There are two cases: (a) with fairness    (b) without fairness
1153   */
1154  lsFirstItem(A->Q->Fair, &FairSet, NIL(lsHandle));
1155  if (lsLength(A->Fair) > 0) {
1156    /* (a) */
1157    tbl = st_init_table(st_ptrcmp, st_ptrhash);
1158    /* Find states that are on fair cycles */
1159    st_foreach_item(FairSet, stgen, &qstate, NIL(char *)) {
1160      Class = AutomatonQuotientVertexGetClass(qstate);
1161      StTableAppend(tbl, Class);
1162    }
1163    /* Shrink fair sets in A->Fair */
1164    lsForEachItem (A->Fair, lsgen, FairSet) {
1165      StTableRestrict(FairSet, tbl);
1166    }
1167    /* Find states that can reach fair cycles */
1168    tbl1 = tbl;
1169    tbl = g_EF(A->G, tbl);
1170    st_free_table(tbl1);
1171    /* Remove the rest part of A->G  */
1172    StTableRestrict(A->Init, tbl);
1173    StTableRestrict(A->dontcare, tbl);
1174    lsForEachItem (states, lsgen, state) {
1175      if (!st_is_member(tbl, state))
1176        g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
1177    }
1178  }else {
1179    /* (b) */
1180    /* Find all the reachable state */
1181    tbl = g_reachable(A->G, A->Init);
1182    /* Remove the rest part of A->G  */
1183    StTableRestrict(A->Init, tbl);
1184    StTableRestrict(A->dontcare, tbl);
1185    lsForEachItem (states, lsgen, state) {
1186      if (!st_is_member(tbl, state))
1187        g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0);
1188    }
1189  }
1190  /* Clean up the Quotient graph */
1191  st_foreach_item(A->SCC, stgen, &Class, &isFair) {
1192    StTableRestrict(Class, tbl);
1193  }
1194  st_free_table(tbl);
1195
1196
1197  /* 3. Remove duplicate FairSet */
1198  /* Discard duplicate fair sets and fair sets including all states. Here we
1199   * also restrict fair sets by analyzing each SCC. If within an SCC, one fair
1200   * set dominates another, it can be restricted to the dominated one. As a
1201   * special case: if an SCC does not intersect all fair sets, its states are
1202   * removed from all fair sets.
1203   */
1204  totalnum = lsLength(A->Fair);
1205  procnum = 0;
1206  while(lsDelBegin(A->Fair, &FairSet) != LS_NOMORE) {
1207    /* Remove this FairSet if it includes all states in the SCC */
1208    if (st_count(FairSet) == lsLength(g_get_vertices(A->G))) {
1209      st_free_table(FairSet);
1210      totalnum--;
1211    }else {
1212      /* After restricted to the SCC: if fair set2 is contained in set1,
1213       * shrink set1 to set2 (remove (set1-set2) from set1
1214       */
1215      st_foreach_item(A->SCC, stgen, &scc, &isFair) {
1216        lsForEachItem(A->Fair, lsgen, otherset) {
1217          tbl1 = st_copy(scc);
1218          tbl2 = st_copy(scc);
1219          StTableRestrict(tbl1, FairSet);
1220          StTableRestrict(tbl2, otherset);
1221          if (StTableInclude(tbl1, tbl2, NIL(st_table))) {
1222            /* tbl1 <= (tbl1 - tbl2) */
1223            StTableSubtract(tbl1, tbl2);
1224            StTableSubtract(FairSet, tbl1);
1225          }
1226          st_free_table(tbl1);
1227          st_free_table(tbl2);
1228        }
1229      }
1230      /* Remove the fair set if another fair set is contained in it */
1231      flag = 1;
1232      lsForEachItem(A->Fair, lsgen, otherset) {
1233        if (StTableInclude(FairSet,otherset,NIL(st_table))) {
1234          flag = 0;
1235          lsFinish(lsgen);
1236          break;
1237        }
1238      }
1239      if (!flag) {
1240        st_free_table(FairSet);
1241        totalnum--;
1242      }else
1243        lsNewEnd(A->Fair, (lsGeneric) FairSet, NIL(lsHandle));
1244    }
1245    procnum++;
1246    if (procnum > totalnum)  break;
1247  }
1248
1249  /* 4. GLB reduction */
1250  /* If an SCC is a clique, and there is a state 's' whose label exactly matches
1251   * the GLB of all the labels of the clique, we can remove 's' from every fair
1252   * set such that it contains at least another state of the SCC besides 's'
1253   */
1254  st_foreach_item(A->SCC, stgen, &Class, &isFair) {
1255    /* 1-state SCC won't work */
1256    if (st_count(Class) <= 1) continue;
1257    /* must be a clique */
1258    if (!AutomatonPartitionIsClique(A->G, Class)) continue;
1259    tbl = AutomatonPartitionLabelGLB(Class, A->labelTableNegate);
1260    if (!tbl) continue;
1261    rest = st_copy(Class);
1262    StTableSubtract(rest, tbl);
1263    lsForEachItem(A->Fair, lsgen, FairSet) {
1264      if (StTableInclude(FairSet, tbl, NIL(st_table)) &&
1265          !StTableIsDisjoint(FairSet, rest, NIL(st_table)))
1266        /* we apply the theorem here */
1267        StTableSubtract(FairSet, tbl);
1268    }
1269    st_free_table(rest);
1270    st_free_table(tbl);
1271  }
1272
1273  /* 5. LUB reduction */
1274  /* If an SCC contains a state 's' that simulates all the other states in the
1275   * same SCC (both forward and backward), then all states of the SCC except
1276   * 's' can be removed from all fair sets. The following code checks for a
1277   * special case of this theorem
1278   */
1279  st_foreach_item(A->SCC, stgen, &Class, &isFair) {
1280    vertex_t *qstate;
1281    st_lookup(A->Q->SCC, Class, &qstate);
1282    /* 1-state SCC won't work */
1283    if (st_count(Class) <= 1)   continue;
1284    tbl = AutomatonPartitionLabelLUB(Class, A->labelTableNegate);
1285    if (!tbl)   continue;
1286    st_foreach_item(tbl, stgen1, &greatest, NIL(char *)) {
1287      /* that state should have a self-loop */
1288      if (!AutomatonVertexHasSelfLoop(A->G, greatest)) continue;
1289      /* that state should be initial if the SCC contains initial states */
1290      if (st_is_member(A->Q->Init, qstate) &&
1291          !st_is_member(A->Init, greatest))
1292        continue;
1293      /* that state should belong to FairSet if the SCC intersect it */
1294      flag = 1;
1295      lsForEachItem(A->Fair, lsgen, FairSet) {
1296        if (!st_is_member(FairSet, greatest) &&
1297            !StTableIsDisjoint(FairSet,Class,NIL(st_table))){
1298          flag = 0;
1299          lsFinish(lsgen);
1300          break;
1301        }
1302      }
1303      if (!flag)  continue;
1304      /* Every state outside of the SCC with a transition into the SCC
1305       * should also have a transition to that state
1306       */
1307      tbl1 = st_init_table(st_ptrcmp, st_ptrhash);
1308      st_foreach_item(Class, stgen2, &state, NIL(char *)) {
1309        tbl2 = AutomatonVertexGetPreImg(A->G, state);
1310        StTableAppend(tbl1, tbl2);
1311        st_free_table(tbl2);
1312      }
1313      tbl2 = AutomatonVertexGetPreImg(A->G, greatest);
1314      flag = StTableInclude(tbl2, tbl1, Class);
1315      st_free_table(tbl2);
1316      st_free_table(tbl1);
1317      if (!flag) continue;
1318
1319      /* we now apply the theorem */
1320      tbl1 = st_copy(Class);
1321      if (st_is_member(tbl1, greatest))
1322        st_delete(tbl1, &greatest, NIL(char *));
1323      lsForEachItem(A->Fair, lsgen, FairSet) {
1324        StTableSubtract(FairSet, tbl1);
1325      }
1326      st_free_table(tbl1);
1327    }
1328    st_free_table(tbl);
1329  }
1330
1331
1332  lsDestroy(states, (void (*)(lsGeneric))0);
1333
1334  return 1;
1335}
1336
1337
1338
1339
1340/**Function********************************************************************
1341
1342  Synopsis    [Compute the SCCs of the Automaton.]
1343
1344  Description [Traverse the entire reachable graph of the automaton, and
1345  put all the SCCs in a hash table.
1346
1347  If force=1, the existing partition (A->SCC) is freed and the new partition
1348  is computed.
1349  If force=0, the partition is computed only if A->SCC=null.]
1350
1351  SideEffects [A->SCC is assigned the new partition.]
1352
1353  SeeAlso     []
1354
1355******************************************************************************/
1356void
1357Ltl_AutomatonComputeSCC(
1358  Ltl_Automaton_t *A,
1359  int force)
1360{
1361  st_generator *stgen;
1362  st_table *component;
1363
1364  /* compute A->SCC if not exist */
1365  if (!force && A->SCC)
1366    return;
1367
1368  if (force && A->SCC) {
1369    st_foreach_item(A->SCC, stgen, &component, NIL(char *)) {
1370      st_free_table(component);
1371    }
1372    st_free_table(A->SCC);
1373  }
1374
1375  A->SCC = g_SCC(A->G, A->Init);
1376
1377  return;
1378}
1379
1380/**Function********************************************************************
1381
1382  Synopsis    [Return 1 if if the automaton is 'WEAK']
1383
1384  Description [The definition of WEAK: For each fair SCC in the automaton,
1385  every fairset F contains all its states.
1386
1387  A special case: If there is no fairness constraint at all, it's WEAK.]
1388
1389  SideEffects [Compute the SCCs and Quotient graph(A->SCC,A->Q) if not exist.]
1390
1391  SeeAlso     []
1392
1393******************************************************************************/
1394int
1395Ltl_AutomatonIsWeak(
1396  Ltl_Automaton_t *A)
1397{
1398  int weak;
1399  long isFair;
1400  st_generator *stgen;
1401  st_table *scc, *FairSet;
1402  lsGen lsgen;
1403
1404  /* A SCC without fairness constraint is WEAK */
1405  if (lsLength(A->Fair) == 0)
1406    return 1;
1407
1408  /* compute the partition(A->SCC) and Quotient graph(A->Q) if not exist */
1409  if (!A->SCC)
1410    Ltl_AutomatonComputeSCC(A,0);
1411  if (!A->Q)
1412    A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC);
1413
1414  /* weak: for each SCC,
1415   * either it's included in all FairSets
1416   * or it intersects none of them
1417   */
1418  weak = 1;
1419  st_foreach_item(A->SCC, stgen, &scc, &isFair) {
1420    int flag = 0;
1421    /* intersect none of them ? */
1422    lsForEachItem (A->Fair, lsgen, FairSet) {
1423      if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) {
1424        lsFinish(lsgen);
1425        flag = 1;
1426        break;
1427      }
1428    }
1429    if (!flag) continue;
1430
1431    /* included in all of them ? */
1432    lsForEachItem (A->Fair, lsgen, FairSet) {
1433      if (!StTableInclude(FairSet, scc, NIL(st_table))) {
1434        weak = 0;
1435        lsFinish(lsgen);
1436        break;
1437      }
1438    }
1439
1440    if (!weak) {
1441      st_free_gen(stgen);
1442      break;
1443    }
1444  }
1445
1446  return weak;
1447}
1448
1449/**Function********************************************************************
1450
1451  Synopsis    [Return the strength of the automaton.]
1452
1453  Description [0 -terminal  1 -weak  2 -strong.]
1454
1455  SideEffects [Compute the parition and quotient graph if not exist.]
1456
1457  SeeAlso     []
1458
1459******************************************************************************/
1460Mc_AutStrength_t
1461Ltl_AutomatonGetStrength(
1462  Ltl_Automaton_t *A)
1463{
1464  Mc_AutStrength_t result;
1465  vertex_t *qstate, *state, *state2;
1466  st_generator *stgen, *stgen1, *stgen2;
1467  st_table *tbl, *FairSet, *scc;
1468  lsList cover;
1469  lsGen lsgen;
1470
1471  /* Every time we need to re-compute the partition(A->SCC) and
1472   * the Quotient graph(A->Q)
1473   */
1474  Ltl_AutomatonComputeSCC(A, 1);
1475  if (A->Q) {
1476    Ltl_AutomatonFree((gGeneric) A->Q);
1477    A->Q = NIL(Ltl_Automaton_t);
1478  }
1479  A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC);
1480
1481  /* is it strong ? */
1482  if (!Ltl_AutomatonIsWeak(A))
1483    return Mc_Aut_Strong_c /*2*/;
1484
1485  /* it's terminal (0) if all the weak SCCs are COMPLETE and FINAL.*/
1486  result = Mc_Aut_Terminal_c;
1487  st_foreach_item(A->SCC, stgen, &scc, NIL(char *)) {
1488    int disjoint_flag = 1;
1489    int final_flag = 1;
1490    int complete_flag = 1;
1491
1492    /* if it does not intersect any fair set, we don't care about it */
1493    if (lsLength(A->Fair) == 0)
1494      disjoint_flag = 0;
1495    else {
1496      lsForEachItem(A->Fair, lsgen, FairSet) {
1497        if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) {
1498          disjoint_flag = 0;
1499          lsFinish(lsgen);
1500          break;
1501        }
1502      }
1503    }
1504    if (disjoint_flag) continue;
1505
1506    /* FINAL:
1507     * it shouldn't be trivial, and shouldn't have edge to other sccs
1508     */
1509    st_lookup(A->Q->SCC, scc, &qstate);
1510    tbl = AutomatonVertexGetImg(A->Q->G, qstate);
1511    final_flag = (st_count(tbl) == 1 && st_is_member(tbl, qstate));
1512    st_free_table(tbl);
1513    if (!final_flag) {
1514      st_free_gen(stgen);
1515      result = Mc_Aut_Weak_c;  /* weak */
1516      break;
1517    }
1518
1519    /* COMPLETE:
1520     * for each state in the SCC: the union of the labels in all
1521     * its successors is tautology
1522     */
1523    st_foreach_item(scc, stgen1, &state, NIL(char *)) {
1524      tbl = AutomatonVertexGetImg(A->G, state);
1525      cover = lsCreate();
1526      st_foreach_item(tbl, stgen2, &state2, NIL(char *)) {
1527        lsNewEnd(cover, (lsGeneric)LtlAutomatonVertexGetLabels(state2),
1528                 NIL(lsHandle));
1529      }
1530      st_free_table(tbl);
1531      complete_flag = LtlCoverIsTautology(cover, A->labelTableNegate);
1532      lsDestroy(cover, (void (*)(lsGeneric))0);
1533      if (!complete_flag) {
1534        st_free_gen(stgen1);
1535        break;
1536      }
1537    }
1538    if (!complete_flag) {
1539      st_free_gen(stgen);
1540      result = Mc_Aut_Weak_c;  /* weak */
1541      break;
1542    }
1543  }
1544
1545  /* Weak = 1;  Terminal = 0 */
1546  return result;
1547}
1548
1549/**Function********************************************************************
1550
1551  Synopsis    [Return the Quotient graph for the given partition.]
1552
1553  Description [The Quotient graph is represented as an automaton Q:
1554
1555  Q->SCC : partition component  TO  vertex in Q graph hash table
1556  Q->Init: initial vertices in Q graph
1557  Q->Fair: only 1 FairSet in it, which contains the Q vertices corresponding
1558           to the fair components
1559  Q->G   : The actual graph_t
1560
1561  Each Q vertex is associated with an automaton node:
1562  node->index:  the index # of the Q vertex
1563  node->Class:  the partition component associated with this vertex.
1564
1565  NOTICE: the Quotient graph is NOT a DAG, non-trivial SCCs have self-loops.]
1566
1567
1568  SideEffects [A->SCC is updated with the following information:
1569  if (key) is a trivial SCC (obviously non-fair), (value)=2;
1570  if (key) is a non-trivial non-fair SCC, (value) = 0;
1571  if (key) is a fair SCC, (value)=1;
1572  otherwise, (value)=1;
1573  The result should be freed by the caller.]
1574
1575  SeeAlso     []
1576
1577******************************************************************************/
1578Ltl_Automaton_t *
1579Ltl_AutomatonCreateQuotient(
1580  Ltl_Automaton_t *A,
1581  st_table *partition)
1582{
1583  long isFair;
1584  int flag;
1585  st_generator *stgen, *stgen1;
1586  st_table *Class, *FairSet;
1587  lsGen lsgen;
1588
1589  st_table *Avtx2Qvtx, *Class2Qvtx, *EdgeUtable;
1590  Ltl_Automaton_t *Q;
1591  Ltl_AutomatonNode_t *node;
1592  vertex_t *q, *p;
1593  edge_t *e;
1594  LtlPair_t *pair;
1595
1596  /* create the Q graph as a Automaton */
1597  Q = Ltl_AutomatonCreate();
1598  Q->isQuotientGraph = 1;
1599
1600  /*### for each class, add vtx in Q->G ###*/
1601  /* hash tables : (vtx in A, vtx in Q), (class_st_table, vtx in Q) */
1602  Avtx2Qvtx = st_init_table(st_ptrcmp, st_ptrhash);
1603  Class2Qvtx = st_init_table(st_ptrcmp, st_ptrhash);
1604  st_foreach_item(partition, stgen, &Class, NIL(char *)) {
1605    /* add 'q' in Q->G */
1606    q = g_add_vertex(Q->G);
1607    node = Ltl_AutomatonNodeCreate(Q);
1608    node->Class = Class;
1609    q->user_data = (gGeneric) node;
1610    st_insert(Class2Qvtx, Class, q);
1611    /* hash table (A_vtx -> Q_vtx) */
1612    flag = 0;
1613    st_foreach_item(Class, stgen1, &p, NIL(char *)) {
1614      st_insert(Avtx2Qvtx, p, q);
1615      if (st_is_member(A->Init, p))
1616        flag = 1;
1617    }
1618    /* if any state in class is in A->Init, put class into Q->Init */
1619    if (flag)
1620      st_insert(Q->Init, q, q);
1621  }
1622
1623
1624  /*### for each (class, class2), add edges ###*/
1625  /* edge unique table in Q graph, key = (class, class2) */
1626  EdgeUtable = st_init_table(LtlPairCompare, LtlPairHash);
1627  pair = LtlPairNew(0,0);
1628  foreach_edge(A->G, lsgen, e) {
1629    if (!st_lookup(Avtx2Qvtx, g_e_source(e), &pair->First))
1630      continue;
1631    if (!st_lookup(Avtx2Qvtx, g_e_dest(e),   &pair->Second))
1632      continue;
1633    /* only consider reachable states in A->G */
1634    if (!st_is_member(EdgeUtable, pair)) {
1635      LtlPair_t *tmpPair = LtlPairNew(pair->First, pair->Second);
1636      st_insert(EdgeUtable, tmpPair, tmpPair);
1637      g_add_edge((vertex_t *)pair->First, (vertex_t *)pair->Second);
1638    }
1639  }
1640
1641  /*### put fair sccs into the only FairSet ###*/
1642  /* isFair = 1 (fair SCC); isFair = 0 (non-trivial non-fair SCC);
1643   * isFair = 2 (dontcare: trivial SCC, obviously non-fair)*/
1644  FairSet = st_init_table(st_ptrcmp, st_ptrhash);
1645  st_foreach_item(partition, stgen, &Class, &isFair) {
1646    st_insert(partition, Class, (char *)0);
1647
1648    /* it should be a nontrivial scc (size >1 or have self-loop) */
1649    if (st_count(Class)==1) {
1650      st_lookup(Class2Qvtx, Class, &pair->First);
1651      st_lookup(Class2Qvtx, Class, &pair->Second);
1652      if (!st_is_member(EdgeUtable, pair)) {
1653        /*trivial scc (1 state without self-loop) */
1654        st_insert(partition, Class, (char *)2);
1655        continue;
1656      }
1657    }
1658    /* for non trivial SCC, check if it intersect all FairSets */
1659    if (!StTableIsFair(A->Fair, Class)) continue;
1660    /* it's a "fair SCC" */
1661    st_insert(partition, Class, (char *)1);
1662
1663    st_lookup(Class2Qvtx, Class, &pair->First);
1664    st_insert(FairSet, pair->First, pair->First);
1665  }
1666  lsNewEnd(Q->Fair, (lsGeneric) FairSet, (lsHandle *) 0);
1667
1668  /* free */
1669  LtlPairFree(pair);
1670  st_foreach_item(EdgeUtable, stgen, &pair, NIL(char *)) {
1671    LtlPairFree(pair);
1672  }
1673  st_free_table(EdgeUtable);
1674
1675  st_free_table(Avtx2Qvtx);
1676  /*  st_free_table(Class2Qvtx); */
1677  Q->SCC = Class2Qvtx;
1678
1679  return Q;
1680}
1681
1682/**Function********************************************************************
1683
1684  Synopsis [Return the node index associated with the given vertex.]
1685
1686  SideEffects []
1687
1688******************************************************************************/
1689int
1690Ltl_AutomatonVtxGetNodeIdx(
1691  vertex_t *v)
1692{
1693  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data;
1694  return node->index;
1695}
1696
1697/**Function********************************************************************
1698
1699  Synopsis [Return the automaton node label set associated with the vertex.]
1700
1701  SideEffects [The result is owned by the node, and should not be freed.]
1702
1703******************************************************************************/
1704LtlSet_t *
1705LtlAutomatonVertexGetLabels(
1706  vertex_t *vtx)
1707{
1708  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) vtx->user_data;
1709  return node->Labels;
1710}
1711
1712
1713/*---------------------------------------------------------------------------*/
1714/* Definition of static functions                                            */
1715/*---------------------------------------------------------------------------*/
1716
1717/**Function********************************************************************
1718
1719  Synopsis [Return the input-compatible candidates.]
1720
1721  SideEffects [Result should be freed by the caller.]
1722
1723******************************************************************************/
1724static lsList
1725AutomatonPickInputCandidate(
1726  graph_t *G,
1727  vertex_t *vtx)
1728{
1729  st_table *uTable;
1730  lsList candi, preImg;
1731  lsGen lsgen, lsgen2;
1732  edge_t *e, *e2;
1733  vertex_t *s, *t;
1734  int size;
1735
1736  preImg = g_get_in_edges(vtx); /* shouldn't be freed */
1737  size = lsLength(preImg);
1738
1739  /* No predecessor */
1740  if (size == 0) {
1741    return  lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL);
1742  }
1743  /* The only predecessor is itself */
1744  if (size == 1) {
1745    lsFirstItem(preImg, &e, NIL(lsHandle));
1746    if (g_e_source(e) == vtx) {          /* all the vertices in G */
1747      return  lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL);
1748    }
1749  }
1750  /* Has predecessor(s) other than itself */
1751  uTable = st_init_table(st_ptrcmp, st_ptrhash);
1752  candi = lsCreate();
1753  lsForEachItem (preImg, lsgen,  e) {
1754    s = g_e_source(e);
1755    foreach_out_edge(s, lsgen2, e2) {
1756      t = g_e_dest(e2);
1757      if (t != vtx) {
1758        if(!st_insert(uTable,  t,  t))
1759          lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle));
1760      }
1761    }
1762    if (size == 1) {
1763      if (!st_insert(uTable, s, s))
1764        lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle));
1765    }
1766  }
1767  st_free_table(uTable);
1768
1769  return candi;
1770}
1771
1772/**Function********************************************************************
1773
1774  Synopsis [Return the output-compatible candidates.]
1775
1776  SideEffects [Result should be freed by the caller.]
1777
1778******************************************************************************/
1779static lsList
1780AutomatonPickOutputCandidate(
1781  graph_t *G,
1782  vertex_t *vtx)
1783{
1784  st_table *uTable;
1785  lsList candi, Img;
1786  lsGen lsgen, lsgen2;
1787  edge_t *e, *e2;
1788  vertex_t *s, *t;
1789  int size;
1790
1791  Img = g_get_out_edges(vtx);
1792  size = lsLength(Img);
1793
1794  /* No successor */
1795  if (size == 0) {
1796    return  lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL);
1797  }
1798  /* The only successor is itself */
1799  if (size == 1) {
1800    lsFirstItem(Img, &e, NIL(lsHandle));
1801    if (g_e_dest(e) == vtx) {
1802      return  lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL);
1803    }
1804  }
1805  /* Has successor(s) other than itself */
1806  uTable = st_init_table(st_ptrcmp, st_ptrhash);
1807  candi = lsCreate();
1808  lsForEachItem(Img, lsgen, e) {
1809    s = g_e_dest(e);
1810    foreach_in_edge(s, lsgen2, e2) {
1811      t = g_e_source(e2);
1812      if (t != vtx) {
1813        if(!st_insert(uTable,  t,  t))
1814          lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle));
1815      }
1816    }
1817    if (size == 1) {
1818      if(!st_insert(uTable, s, s))
1819        lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle));
1820    }
1821  }
1822  st_free_table(uTable);
1823
1824  return candi;
1825}
1826
1827
1828/**Function********************************************************************
1829
1830  Synopsis [Return the pre-image of the given vertex in the hash table.]
1831
1832  SideEffects [Result should be freed by the caller.]
1833
1834******************************************************************************/
1835static st_table *
1836AutomatonVertexGetPreImg(
1837  graph_t *G,
1838  vertex_t *vtx)
1839{
1840  lsList preImg;
1841  lsGen lsgen;
1842  edge_t *e;
1843  vertex_t *s;
1844  st_table *uTable;
1845
1846  preImg = g_get_in_edges(vtx);
1847
1848  uTable = st_init_table(st_ptrcmp, st_ptrhash);
1849  lsForEachItem(preImg, lsgen,  e) {
1850    s = g_e_source(e);
1851    st_insert(uTable,  s,  s);
1852  }
1853
1854  return uTable;
1855}
1856
1857/**Function********************************************************************
1858
1859  Synopsis [Return the image of the given vertex in the hash table.]
1860
1861  SideEffects [Result should be freed by the caller.]
1862
1863******************************************************************************/
1864static st_table *
1865AutomatonVertexGetImg(
1866  graph_t *G,
1867  vertex_t *vtx)
1868{
1869  lsList Img;
1870  lsGen lsgen;
1871  edge_t *e;
1872  vertex_t *s;
1873  st_table *uTable;
1874
1875  Img = g_get_out_edges(vtx);
1876
1877  uTable = st_init_table(st_ptrcmp, st_ptrhash);
1878  lsForEachItem(Img, lsgen, e) {
1879    s = g_e_dest(e);
1880    st_insert(uTable,  s,  s);
1881  }
1882
1883  return uTable;
1884}
1885
1886/**Function********************************************************************
1887
1888  Synopsis [Return 1 iff the given vertex has a self-loop.]
1889
1890  SideEffects []
1891
1892******************************************************************************/
1893static int
1894AutomatonVertexHasSelfLoop(
1895  graph_t *G,
1896  vertex_t *vtx)
1897{
1898  lsList Img;
1899  lsGen lsgen;
1900  edge_t *e;
1901  int flag = 0;
1902
1903  Img = g_get_out_edges(vtx);
1904
1905  lsForEachItem(Img, lsgen, e) {
1906    if (g_e_dest(e) == vtx) {
1907      flag = 1;
1908      lsFinish(lsgen);
1909      break;
1910    }
1911  }
1912
1913  return flag;
1914}
1915
1916/**Function********************************************************************
1917
1918  Synopsis [Return 1 iff the following statement in the automaton holds:
1919  For each fair set,  both states are in it or none of them]
1920
1921  SideEffects []
1922
1923******************************************************************************/
1924static int
1925AutomatonPfairEquivQfair(
1926  Ltl_Automaton_t *A,
1927  vertex_t *state,
1928  vertex_t *otherstate)
1929{
1930  int  flag = 1;
1931  st_table *FairSet;
1932  lsGen lsgen;
1933
1934  lsForEachItem (A->Fair, lsgen, FairSet) {
1935    if (st_is_member(FairSet, state) !=
1936        st_is_member(FairSet, otherstate)) {
1937      flag = 0;
1938      lsFinish(lsgen);
1939      break;
1940    }
1941  }
1942
1943  return flag;
1944}
1945
1946/**Function********************************************************************
1947
1948  Synopsis [Return 1 iff the following statement in the automaton holds:
1949  For each fair set,  if 'state' is in it, 'otherstate' must also in it.]
1950
1951  SideEffects []
1952
1953******************************************************************************/
1954static int
1955AutomatonPfairImplyQfair(
1956  Ltl_Automaton_t *A,
1957  vertex_t *state,
1958  vertex_t *otherstate)
1959{
1960  int  flag = 1;
1961  st_table *FairSet;
1962  lsGen lsgen;
1963
1964  lsForEachItem (A->Fair, lsgen, FairSet) {
1965    if (st_is_member(FairSet, state) &&
1966        !st_is_member(FairSet, otherstate)) {
1967      flag = 0;
1968      lsFinish(lsgen);
1969      break;
1970    }
1971  }
1972
1973  return flag;
1974}
1975
1976/**Function********************************************************************
1977
1978  Synopsis [If 'item' is in the hash table, Delete it and return the real key;
1979  Otherwise, return  0.]
1980
1981  SideEffects ['item' will not be modified.]
1982
1983******************************************************************************/
1984static char *
1985StTableDelete(
1986  st_table *tbl,
1987  char *item)
1988{
1989  char *key = item;
1990
1991  if (st_is_member(tbl, key)) {
1992    st_delete(tbl, &key, NIL(char *));
1993    return key;
1994  }else
1995    return NIL(char);
1996}
1997
1998/**Function********************************************************************
1999
2000  Synopsis [Append the tbl2 to tbl1 and return tbl1.]
2001
2002  SideEffects [tbl1 is permenently changed.]
2003
2004******************************************************************************/
2005static st_table *
2006StTableAppend(
2007  st_table *tbl1,
2008  st_table *tbl2)
2009{
2010  char *key, *value;
2011  st_generator *stgen;
2012
2013  st_foreach_item(tbl2, stgen, &key, &value) {
2014    if (!st_is_member(tbl1, key))
2015      st_insert(tbl1, key, value);
2016  }
2017
2018  return tbl1;
2019}
2020
2021/**Function********************************************************************
2022
2023  Synopsis [Remove from tbl1 all the items that are not in tbl2.]
2024
2025  SideEffects [tbl1 is changed and returned.]
2026
2027******************************************************************************/
2028static st_table *
2029StTableRestrict(
2030  st_table *tbl1,
2031  st_table *tbl2)
2032{
2033  char *key, *value;
2034  st_table *tbl = st_copy(tbl1);
2035  st_generator *stgen;
2036
2037  st_foreach_item(tbl, stgen, &key, &value) {
2038    if (!st_is_member(tbl2, key))
2039      st_delete(tbl1, &key, &value);
2040  }
2041  st_free_table(tbl);
2042
2043  return tbl1;
2044}
2045
2046/**Function********************************************************************
2047
2048  Synopsis [Remove from tbl1 all the items that are in tbl2.]
2049
2050  SideEffects [tbl1 is changed and returned.]
2051
2052******************************************************************************/
2053static st_table *
2054StTableSubtract(
2055  st_table *tbl1,
2056  st_table *tbl2)
2057{
2058  char *key, *value;
2059  st_generator *stgen;
2060
2061  st_foreach_item(tbl2, stgen, &key, &value) {
2062    if (st_is_member(tbl1, key))
2063      st_delete(tbl1, &key, &value);
2064  }
2065
2066  return tbl1;
2067}
2068
2069/**Function********************************************************************
2070
2071  Synopsis [Return 1 if tbl1 and tbl2 have the same items except those also
2072  in 'dontcare'. 'dontcare' can be a null pointer.]
2073
2074  SideEffects []
2075
2076******************************************************************************/
2077static int
2078StTableIsEqual(
2079  st_table *tbl1,
2080  st_table *tbl2,
2081  st_table *dontcare)
2082{
2083  int flag = 1;
2084  st_generator *stgen;
2085  vertex_t *vtx;
2086
2087  flag = 1;
2088  st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) {
2089    if (dontcare) {
2090      if (st_is_member(dontcare,vtx)) continue;
2091    }
2092    if (!st_is_member(tbl2,vtx)) {
2093      flag = 0;
2094      st_free_gen(stgen);
2095      break;
2096    }
2097  }
2098  if (!flag) return 0;
2099
2100  st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) {
2101    if (dontcare) {
2102      if (st_is_member(dontcare,vtx)) continue;
2103    }
2104    if (!st_is_member(tbl1, vtx)) {
2105      flag = 0;
2106      st_free_gen(stgen);
2107      break;
2108    }
2109  }
2110  return flag;
2111}
2112
2113/**Function********************************************************************
2114
2115  Synopsis [Return 1 if 'larger' include every items in 'small' except those
2116  also in 'dontcare'. Notice that 'dontcare' can be a null pointer.]
2117
2118  SideEffects []
2119
2120******************************************************************************/
2121static int
2122StTableInclude(
2123  st_table *large,
2124  st_table *small,
2125  st_table *dontcare)
2126{
2127  int flag = 1;
2128  st_generator *stgen;
2129  vertex_t *vtx;
2130
2131  flag = 1;
2132  st_foreach_item(small, stgen, &vtx, NIL(char *)) {
2133    if (dontcare) {
2134      if (st_is_member(dontcare, vtx)) continue;
2135    }
2136    if (!st_is_member(large,vtx)) {
2137      flag = 0;
2138      st_free_gen(stgen);
2139      break;
2140    }
2141  }
2142
2143  return flag;
2144}
2145
2146
2147/**Function********************************************************************
2148
2149  Synopsis [Return 1 if the two tables shares nothing except those items also
2150  in 'dontcare'. Notice that 'dontcare' can be a null pointer.]
2151
2152  SideEffects []
2153
2154******************************************************************************/
2155static int
2156StTableIsDisjoint(
2157  st_table *tbl1,
2158  st_table *tbl2,
2159  st_table *dontcare)
2160{
2161  int flag = 1;
2162  st_generator *stgen;
2163  vertex_t *vtx;
2164
2165  flag = 1;
2166  st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) {
2167    if (dontcare) {
2168      if (st_is_member(dontcare, vtx))     continue;
2169    }
2170    if (st_is_member(tbl2,vtx)) {
2171      flag = 0;
2172      st_free_gen(stgen);
2173      break;
2174    }
2175  }
2176  if (!flag)  return 0;
2177
2178  st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) {
2179    if (dontcare) {
2180      if (st_is_member(dontcare, vtx)) continue;
2181    }
2182    if (st_is_member(tbl1,vtx)) {
2183      flag = 0;
2184      st_free_gen(stgen);
2185      break;
2186    }
2187  }
2188  return flag;
2189}
2190
2191/**Function********************************************************************
2192
2193  Synopsis [Return 1 if the given tables intersect every tables in the list.]
2194
2195  SideEffects []
2196
2197******************************************************************************/
2198static int
2199StTableIsFair(
2200  lsList A_Fair,
2201  st_table *Class)
2202{
2203  int flag;
2204  st_table *FairSet;
2205  lsGen lsgen;
2206
2207  flag = 1;
2208  lsForEachItem (A_Fair, lsgen, FairSet) {
2209    if (StTableIsDisjoint(FairSet,Class,NIL(st_table))) {
2210      flag = 0;
2211      lsFinish(lsgen);
2212      break;
2213    }
2214  }
2215
2216  return flag;
2217}
2218
2219/**Function********************************************************************
2220
2221  Synopsis [Return 1 if the given table forms a clique (for each state, there
2222  are edges to all the states in the set).]
2223
2224  SideEffects []
2225
2226******************************************************************************/
2227static int
2228AutomatonPartitionIsClique(
2229  graph_t *G,
2230  st_table *set)
2231{
2232  int flag = 1;
2233  st_table *Img;
2234  st_generator *stgen;
2235  vertex_t *state;
2236
2237  st_foreach_item(set, stgen, &state, NIL(char *)) {
2238    Img = AutomatonVertexGetImg(G, state);
2239    flag = StTableInclude(Img, set, NIL(st_table));
2240    st_free_table(Img);
2241    if (!flag) {
2242      st_free_gen(stgen);
2243      break;
2244    }
2245  }
2246
2247  return flag;
2248}
2249
2250/**Function********************************************************************
2251
2252  Synopsis [Find the Least Upper Bound of the labels of a set of states, and
2253  Return a hash table of states that satisfy this 'LUB'. Return null if the
2254  hash table is empty.]
2255
2256  SideEffects [The result should be freed by the caller.]
2257
2258******************************************************************************/
2259static st_table *
2260AutomatonPartitionLabelLUB(
2261  st_table *set,
2262  array_t *Negate)
2263{
2264  vertex_t *state;
2265  st_table *greatest = NIL(st_table);
2266  st_generator *stgen;
2267  LtlSet_t *lub = NIL(LtlSet_t);
2268  LtlSet_t *label;
2269
2270  st_foreach_item(set, stgen, &state, NIL(char *)) {
2271    label = LtlAutomatonVertexGetLabels(state);
2272    if (greatest) {
2273      if (LtlSetEqual(label, lub))
2274        st_insert(greatest, state, state);
2275      else if (LtlSetInclude(lub, label)) {
2276        LtlSetAssign(lub, label);
2277        st_free_table(greatest);
2278        greatest = st_init_table(st_ptrcmp, st_ptrhash);
2279        st_insert(greatest, state, state);
2280      }else if (!LtlSetInclude(label, lub)) {
2281        st_free_table(greatest);
2282        greatest = NIL(st_table);
2283        st_free_gen(stgen);
2284        break;
2285      }
2286    }else {
2287      lub = LtlSetCopy(label);
2288      greatest = st_init_table(st_ptrcmp, st_ptrhash);
2289      st_insert(greatest, state, state);
2290    }
2291  }
2292
2293  if (lub)
2294    LtlSetFree(lub);
2295
2296  return greatest;
2297}
2298
2299/**Function********************************************************************
2300
2301  Synopsis [Find the Greatest Lower Bound of the labels of a set of states, and
2302  Return a hash table of A state that satisfy this 'GLB'. Return null if the
2303  hash table is empty.]
2304
2305  SideEffects [The result should be freed by the caller.]
2306
2307******************************************************************************/
2308static st_table *
2309AutomatonPartitionLabelGLB(
2310  st_table *set,
2311  array_t *Negate)
2312{
2313  vertex_t *state, *least;
2314  LtlSet_t *glb, *label;
2315  st_table *tbl;
2316  st_generator *stgen;
2317
2318  least = NIL(vertex_t);
2319  glb = NIL(LtlSet_t);
2320  st_foreach_item(set, stgen, &state, NIL(char *)) {
2321    label = LtlAutomatonVertexGetLabels(state);
2322    if (!glb)
2323      glb = LtlSetCopy(label);
2324    else
2325      LtlSetOR(glb, glb, label);
2326
2327    if (LtlSetIsContradictory(glb, Negate)) {
2328      least = NIL(vertex_t);
2329      st_free_gen(stgen);
2330      break;
2331    }else if (!least) {
2332      if (LtlSetEqual(glb, label))
2333        least = state;
2334    }else if (!LtlSetEqual(glb, LtlAutomatonVertexGetLabels(least))) {
2335      if (LtlSetEqual(glb, label))
2336        least = state;
2337      else
2338        least = NIL(vertex_t);
2339    }
2340  }
2341
2342  if (glb)
2343    LtlSetFree(glb);
2344
2345  if (least) {
2346    tbl = st_init_table(st_ptrcmp, st_ptrhash);
2347    st_insert(tbl, least, least);
2348  }else
2349    tbl = NIL(st_table);
2350
2351  return tbl;
2352}
2353
2354/**Function********************************************************************
2355
2356  Synopsis [Return the partition component (a st_table) associated with the
2357  given vertex in the Quotient graph.]
2358
2359  SideEffects [The result is owned by the node, and should NOT be freed.]
2360
2361******************************************************************************/
2362static st_table *
2363AutomatonQuotientVertexGetClass(
2364  vertex_t *vtx)
2365{
2366  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *)vtx->user_data;
2367  return node->Class;
2368}
2369
2370/**Function********************************************************************
2371
2372  Synopsis [Return the node index associated with the given vertex.]
2373
2374  SideEffects []
2375
2376******************************************************************************/
2377/*static int
2378AutomatonVtxGetNodeIdx(
2379  vertex_t *v)
2380{
2381  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data;
2382  return node->index;
2383}*/
Note: See TracBrowser for help on using the repository browser.