/**CFile*********************************************************************** FileName [ltlMinimize.c] PackageName [ltl] Synopsis [Buechi automaton minimization.] Author [Chao Wang] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "ltlInt.h" static char rcsid[] UNUSED = "$Id: ltlMinimize.c,v 1.33 2009/04/09 02:21:13 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static lsList AutomatonPickInputCandidate(graph_t *G, vertex_t *vtx); static lsList AutomatonPickOutputCandidate(graph_t *G, vertex_t *vtx); static st_table * AutomatonVertexGetPreImg(graph_t *G, vertex_t *vtx); static st_table * AutomatonVertexGetImg(graph_t *G, vertex_t *vtx); static int AutomatonVertexHasSelfLoop(graph_t *G, vertex_t *vtx); static int AutomatonPfairEquivQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate); static int AutomatonPfairImplyQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate); static char * StTableDelete(st_table *tbl, char *item); static st_table * StTableAppend(st_table *tbl1, st_table *tbl2); static st_table * StTableRestrict(st_table *tbl1, st_table *tbl2); static st_table * StTableSubtract(st_table *tbl1, st_table *tbl2); static int StTableIsEqual(st_table *tbl1, st_table *tbl2, st_table *dontcare); static int StTableInclude(st_table *large, st_table *small, st_table *dontcare); static int StTableIsDisjoint(st_table *tbl1, st_table *tbl2, st_table *dontcare); static int StTableIsFair(lsList A_Fair, st_table *Class); static int AutomatonPartitionIsClique(graph_t *G, st_table *set); static st_table * AutomatonPartitionLabelLUB(st_table *set, array_t *Negate); static st_table * AutomatonPartitionLabelGLB(st_table *set, array_t *Negate); static st_table * AutomatonQuotientVertexGetClass(vertex_t *vtx); /*static int AutomatonVtxGetNodeIdx(vertex_t *v);*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Minimize the Automaton using I/O Compatiblility and Dominance.] Description [These minimizations are based on the structural information, and are less effective than simulation-based techniques. They are used for pre-processing since they are faster.Also, in some cases they go beyond what simulation based minimization can do. Here we consider 3 cases: Input Compatible, Output Compatible and Dominance.] SideEffects [The automaton might be changed. In that case return 1.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonMinimizeByIOCompatible( Ltl_Automaton_t *A, int verbosity) { int changed = 0; int flag; lsList states, incand, outcand; lsGen lsgen, lsgen2, lsgen3; vertex_t *state, *otherstate, *s; LtlSet_t *set, *set2; st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3, *tbl4; st_generator *stgen; /* We go through all the states in A->G, and check for Input-Compatible, * Output-Compatible, and Dominance */ states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (states, lsgen, state) { int localchanged = 0; /* Compute the Image adn PreImg of 'state' for later use */ tbl0 = AutomatonVertexGetPreImg(A->G, state); tbl1 = AutomatonVertexGetImg(A->G, state); /* ############################ * Check for Input Compatible * ############################*/ incand = AutomatonPickInputCandidate(A->G, state); lsForEachItem (incand, lsgen2, otherstate) { /* p is 'state', q is 'otherstate' */ /* p != q */ if (state == otherstate) continue; /* L(p) = L(q) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetEqual(set, set2)) continue; /* p \in Q0 <-> q \in Q0 */ if (st_is_member(A->Init, state) != st_is_member(A->Init, otherstate)) continue; /* p \in F <-> q \in F */ if (!AutomatonPfairEquivQfair(A, state, otherstate)) continue; /* preImg(p) - {p,q} == preImg(q) - {p,q} */ tbl2 = AutomatonVertexGetPreImg(A->G, otherstate); tbl3 = st_init_table(st_ptrcmp, st_ptrhash); st_insert(tbl3, state, state); st_insert(tbl3 , otherstate, otherstate); flag = StTableIsEqual(tbl0, tbl2, tbl3); st_free_table(tbl2); st_free_table(tbl3); if (!flag) continue; /* q \in [delta(p)+delta(q)] <-> p \in [delta(p)+delta(q)] */ tbl2 = AutomatonVertexGetImg(A->G, otherstate); if ( (st_is_member(tbl1,state) || st_is_member(tbl2,state)) != (st_is_member(tbl1,otherstate) || st_is_member(tbl2,otherstate)) ) { st_free_table(tbl2); continue; } /* ######## (state, otherstate) :: input compatible ####### * we merge the two state by deleting 'state' * Notice that now we have the following data available: * tbl0 = PreImg(state), * tbl1 = Img(state), * tbl2 = Img(otherstate) */ /* Update intial states */ StTableDelete(A->Init, (char *)state); /* Add edges (otherstate, s), here s is the sucessor of 'state' */ st_foreach_item(tbl1, stgen, &s, NIL(char *)) { if (s != state && !st_is_member(tbl2, s)) g_add_edge(otherstate, s); } /* Remove 'otherstate' also if state isn't in dontcare */ if (!st_is_member(A->dontcare, state)) StTableDelete(A->dontcare, (char *)otherstate); /* Remove 'state' from dontcare (if applicable) */ StTableDelete(A->dontcare, (char *)state); /* Update fairness conditions */ lsForEachItem (A->Fair, lsgen3, FairSet) { StTableDelete(FairSet, (char *)state); } /* Remove 'state' from the automaton */ g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); st_free_table(tbl2); /* terminate iteration on incand list */ changed = localchanged = 1; lsFinish(lsgen2); break; } lsDestroy(incand, (void (*)(lsGeneric)) 0); if (localchanged) { st_free_table(tbl0); st_free_table(tbl1); continue; } /* ############################ * Check for Output Compatible * ############################ */ outcand = AutomatonPickOutputCandidate(A->G, state); lsForEachItem (outcand, lsgen2, otherstate) { /* p != q */ if (state == otherstate) continue; /* L(p) = L(q) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetEqual(set, set2)) continue; /* p \in F <-> q \in F */ if (!AutomatonPfairEquivQfair(A, state, otherstate)) continue; /* Img(p) - {p,q} == Img(q) - {p,q} */ tbl2 = AutomatonVertexGetImg(A->G, otherstate); tbl3 = st_init_table(st_ptrcmp, st_ptrhash); st_insert(tbl3, state, state); st_insert(tbl3, otherstate, otherstate); flag = StTableIsEqual(tbl1, tbl2, tbl3); st_free_table(tbl3); if (!flag) { st_free_table(tbl2); continue; } /* q \in delta(p) + p \in delta(p)] <-> * q \in delta(q) + p \in delta(q)] */ flag = 0; if ( (st_is_member(tbl1, state) || st_is_member(tbl1, otherstate)) != (st_is_member(tbl2, state) || st_is_member(tbl2, otherstate)) ) { st_free_table(tbl2); continue; } /* ######## (state, otherstate) :: output compatible ####### * Merge the two state by deleting 'state' * Notice that now we have the following data: * tbl0 = PreImg(state) * tbl1 = Img(state) * tbl2 = Img(otherstate) */ tbl3 = AutomatonVertexGetPreImg(A->G, otherstate); /* Add 'otherstate to Q0 if 'state' is in it */ if (st_is_member(A->Init, state)) { st_delete(A->Init, &state, NIL(char *)); if(!st_is_member(A->Init, otherstate)) st_insert(A->Init, otherstate, otherstate); } /* Add edge (s, otherstate) where 's' is in PreImg(state) */ st_foreach_item(tbl0, stgen, &s, NIL(char *)) { if (s != state && s != otherstate && !st_is_member(tbl3, s)) g_add_edge(s, otherstate); } /* Add edge (otherstate, otherstate) if there exist (state, state) or * (state, otherstate) */ if (st_is_member(tbl1, otherstate) || st_is_member(tbl1, state)) if (!st_is_member(tbl2, otherstate)) g_add_edge(otherstate, otherstate); /* Update don't care conditions. If 'state' isn't in dontcare, also * remove 'otherstate' */ if (!st_is_member(A->dontcare, state)) { StTableDelete(A->dontcare, (char *)otherstate); } StTableDelete(A->dontcare, (char *)state); /* Remove 'state' from FairSets */ lsForEachItem (A->Fair, lsgen3, FairSet) { StTableDelete(FairSet, (char *)state); } /* Remove 'state' from the automaton */ g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); st_free_table(tbl2); st_free_table(tbl3); /* terminate iteration on incand list */ changed = localchanged = 1; lsFinish(lsgen2); break; } if (localchanged) { lsDestroy(outcand, (void (*)(lsGeneric)) 0); st_free_table(tbl0); st_free_table(tbl1); continue; } /* ############################ * Check for Dominance * ############################ * We already have the lsList 'outcand' */ lsForEachItem (outcand, lsgen2, otherstate) { /* p != q */ if (state == otherstate) continue; /* L(p) \leq L(q) (set(Lp) > set(Lq) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetInclude(set, set2)) continue; /* p \in Q0 -> q \in Q0 */ if (st_is_member(A->Init, state) && !st_is_member(A->Init, otherstate)) continue; /* p \in F -> q \in F */ if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; /* Img(p) is less than Img(q) */ tbl2 = AutomatonVertexGetImg(A->G, otherstate); flag = StTableInclude(tbl2, tbl1, NIL(st_table)); /* p is in Img(p) -> q is in Img(q) */ if (flag) { flag = (!st_is_member(tbl1, state) || st_is_member(tbl2, otherstate)); } st_free_table(tbl2); if (!flag) continue; /* PreImg(p)-{p} \leq PreImg(q)-{p} */ tbl3 = AutomatonVertexGetPreImg(A->G, otherstate); tbl4 = st_init_table(st_ptrcmp, st_ptrhash); st_insert(tbl4, state, state); flag = StTableInclude(tbl3, tbl0, tbl4); st_free_table(tbl4); st_free_table(tbl3); if (!flag) continue; /* ######## otherstate dominates state ####### * Remove 'state' * Notice that now we have the following data: * tbl0 = PreImg(state) * tbl1 = Img(state) */ /* Remove 'state' from Initial states */ StTableDelete(A->Init, (char *)state); /* Remove 'otherstate' if 'state' isn't in dontcare */ if (!st_is_member(A->dontcare, state)) { StTableDelete(A->dontcare, (char *)otherstate); } StTableDelete(A->dontcare, (char *)state); /* Remove 'state' from FairSets */ lsForEachItem (A->Fair, lsgen3, FairSet) { StTableDelete(FairSet, (char *)state); } /* Remove 'state' from the automaton */ g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); /* terminate iteration on incand list */ changed = localchanged = 1; lsFinish(lsgen2); break; } lsDestroy(outcand, (void (*)(lsGeneric)) 0); st_free_table(tbl0); st_free_table(tbl1); } lsDestroy(states, (void (*)(lsGeneric)) 0); return changed; } /**Function******************************************************************** Synopsis [Minimize the Automaton using Direct Simulation.] Description [Compute direct-simulation relation, and minimize the automaton according to the following two cases: 1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa) 2) Remove edges from their common predecessors to p if p is direct simulated by q.] SideEffects [The automaton might be changed. if so, return 1.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonMinimizeByDirectSimulation( Ltl_Automaton_t *A, int verbosity) { int changed = 0; int flag = 0; lsList states, otherstates, list, queue; lsGen lsgen, lsgen1; edge_t *e; vertex_t *state, *otherstate; vertex_t *p, *q, *s, *t, *u, *v; LtlSet_t *set, *set2; st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3; st_table *simul, *enqueued; st_generator *stgen, *stgen1, *stgen2; LtlPair_t *pair, *pair2; /* store the simulation-relation in hash tables and queue list */ simul = st_init_table(LtlPairCompare, LtlPairHash); enqueued = st_init_table(LtlPairCompare, LtlPairHash); queue = lsCreate(); /*###################################### * Initialize sim rln to all pairs (p,q) *###################################### */ states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (states, lsgen, state) { lsForEachItem (otherstates, lsgen1, otherstate) { /* p != q */ if (state == otherstate) continue; /* L(p) \leq L(q) (set(Lp) > set(Lq) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetInclude(set, set2)) continue; /* p \in F -> q \in F */ if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; /* put (state, otherstate) into simul-relation (candidate) */ pair = LtlPairNew((char *)state, (char *)otherstate); st_insert(simul, pair, pair); st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } } lsDestroy(states, (void (*)(lsGeneric)) NULL); lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); /*###################################### * Compute the "Greatest Fixpoint" *###################################### */ while (lsDelBegin(queue, &pair) != LS_NOMORE) { st_delete(enqueued, &pair, NIL(char *)); p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such * that (s, t) is in simulation relation candidate list */ tbl0 = AutomatonVertexGetImg(A->G, p); tbl1 = AutomatonVertexGetImg(A->G, q); st_foreach_item(tbl0, stgen, &s, NIL(char *)) { flag = 0; st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { flag = (s==t); if (flag) { st_free_gen(stgen1); break; } pair2 = LtlPairNew((char *)s, (char *)t); flag = st_is_member(simul, pair2); LtlPairFree(pair2); if (flag) { st_free_gen(stgen1); break; } } if (!flag) { st_free_gen(stgen); break; } } st_free_table(tbl0); st_free_table(tbl1); if (flag) continue; /* (p, q) is not a simulation relation */ st_delete(simul, &pair, &pair); LtlPairFree(pair); /* Enqueue perturbed pairs */ tbl2 = AutomatonVertexGetPreImg(A->G, p); tbl3 = AutomatonVertexGetPreImg(A->G, q); st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { pair2 = LtlPairNew((char *)u, (char *)v); if (st_lookup(simul, pair2, &pair)) { if (!st_is_member(enqueued, pair2)) { st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } } LtlPairFree(pair2); } } st_free_table(tbl2); st_free_table(tbl3); } lsDestroy(queue, (void (*)(lsGeneric))0); st_free_table(enqueued); /*###################################### * Simplify by Bi-Sim equivalent states *###################################### */ /* to store removed states */ tbl1 = st_init_table(st_ptrcmp, st_ptrhash); /* so that we can modify 'simul' within for loop */ tbl0 = st_copy(simul); st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* make sure neither has been removed */ if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) continue; /* make sure it is Bi-simulation by testing the other direction */ pair2 = LtlPairNew((char *)q, (char *)p); flag = st_lookup(simul, pair2, &pair); LtlPairFree(pair2); if (!flag) continue; /*#### Direct BI-SIMULATION equivalent states####*/ /* Theorem applies */ /* remove its swap: (q, p) from simul-rln */ st_delete(simul, &pair, &pair); LtlPairFree(pair); /* Remove p, and connect its predecessors to q */ tbl2 = AutomatonVertexGetPreImg(A->G, p); tbl3 = AutomatonVertexGetPreImg(A->G, q); st_foreach_item(tbl2, stgen1, &s, NIL(char *)) { if (s == p) continue; if (!st_is_member(tbl3, (char *)s)) g_add_edge(s, q); } st_free_table(tbl2); st_free_table(tbl3); /* Update the fair sets */ lsForEachItem (A->Fair, lsgen, FairSet) { StTableDelete(FairSet, (char *)p); } /* If 'p' is in Q0, Remove 'p' and put 'q' in Q0 */ if (st_is_member(A->Init, p)) { st_delete(A->Init, &p, NIL(char *)); if (!st_is_member(A->Init, q)) st_insert(A->Init, q, q); } /* Remove 'p' from dontcare (if it's in it ) */ StTableDelete(A->dontcare, (char *)p); /* Remove 'p' from the automaton */ st_insert(tbl1, p, p); g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); changed = 1; } st_free_table(tbl0); /*###################################### * Remove arcs to direct-simulated states *###################################### */ /* so that we can modify simul with the for loop */ tbl0 = st_copy(simul); st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { /* 'p' is simulated by 'q' */ p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Make sure neither hasn't been removed yet */ if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) continue; /*#### p is direct-simulated by q####*/ /* Theorem applies */ /* Drop arcs from their common predecessors to p */ tbl3 = AutomatonVertexGetPreImg(A->G, q); list = lsCopy(g_get_in_edges(p), (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (list, lsgen, e) { if (!st_is_member(tbl3, g_e_source(e))) continue; g_delete_edge(e, (void (*)(gGeneric))0); changed = 1; } lsDestroy(list, (void (*)(lsGeneric)) 0); st_free_table(tbl3); /* Remove 'p' from Q0 if 'q' is in Q0 */ if (st_is_member(A->Init, q)) { StTableDelete(A->Init, (char *)p); changed = 1; } } st_free_table (tbl0); st_free_table (tbl1); st_foreach_item(simul, stgen, &pair, NIL(char *)) { LtlPairFree(pair); } st_free_table (simul); return changed; } /**Function******************************************************************** Synopsis [Mark trivial SCCs as Fair states] Description [Mark trivial SCCs as Fair states] SideEffects [] SeeAlso [] ******************************************************************************/ void Ltl_AutomatonAddFairStates( Ltl_Automaton_t *A) { long isFair; lsGen lsgen1; st_generator *stgen, *stgen2; st_table *FairSet, *Class; Ltl_AutomatonComputeSCC(A, 1); if (A->Q) { Ltl_AutomatonFree((gGeneric) A->Q); A->Q = NIL(Ltl_Automaton_t); } A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); /* Mark trivial SCCs as Fair states */ st_foreach_item(A->SCC, stgen, &Class, &isFair) { vertex_t *state; if (isFair == 2) { /* trivial SCC */ lsForEachItem (A->Fair, lsgen1, FairSet) { st_foreach_item(Class, stgen2, &state, NIL(char *)) { if (!st_is_member(FairSet, state)) { if (st_is_member(A->dontcare, state)){ StTableDelete(A->dontcare, (char *)state); } st_insert(FairSet, state, state); } } } } } } /**Function******************************************************************** Synopsis [Maximize the Automaton using Direct Simulation.] Description [Compute direct-simulation relation, and minimize the automaton according to the following two cases: 1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa) 2) Remove edges from their common predecessors to p if p is direct simulated by q.] SideEffects [The automaton might be changed. if so, return 1.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonMaximizeByDirectSimulation( Ltl_Automaton_t *A, int verbosity) { int changed = 0; int flag = 0; lsList states, otherstates, queue; lsGen lsgen, lsgen1; vertex_t *state, *otherstate; vertex_t *p, *q, *s, *t, *u, *v; LtlSet_t *set, *set2; st_table *tbl0, *tbl1, *tbl2, *tbl3; st_table *simul, *enqueued; st_generator *stgen, *stgen1, *stgen2; LtlPair_t *pair, *pair2; /* Ltl_AutomatonAddFairStates(A); */ /* store the simulation-relation in hash tables and queue list */ simul = st_init_table(LtlPairCompare, LtlPairHash); enqueued = st_init_table(LtlPairCompare, LtlPairHash); queue = lsCreate(); /*###################################### * Initialize sim rln to all pairs (p,q) *###################################### */ states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (states, lsgen, state) { lsForEachItem (otherstates, lsgen1, otherstate) { /* p != q */ if (state == otherstate) continue; /* L(p) \leq L(q) (set(Lp) > set(Lq) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetInclude(set, set2)) continue; /* p \in F -> q \in F */ if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; /* put (state, otherstate) into simul-relation (candidate) */ pair = LtlPairNew((char *)state, (char *)otherstate); st_insert(simul, pair, pair); st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } } lsDestroy(states, (void (*)(lsGeneric)) NULL); lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); /*###################################### * Compute the "Greatest Fixpoint" *###################################### */ while (lsDelBegin(queue, &pair) != LS_NOMORE) { st_delete(enqueued, &pair, NIL(char *)); p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such * that (s, t) is in simulation relation candidate list */ tbl0 = AutomatonVertexGetImg(A->G, p); tbl1 = AutomatonVertexGetImg(A->G, q); st_foreach_item(tbl0, stgen, &s, NIL(char *)) { flag = 0; st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { flag = (s==t); if (flag) { st_free_gen(stgen1); break; } pair2 = LtlPairNew((char *)s, (char *)t); flag = st_is_member(simul, pair2); LtlPairFree(pair2); if (flag) { st_free_gen(stgen1); break; } } if (!flag) { st_free_gen(stgen); break; } } st_free_table(tbl0); st_free_table(tbl1); if (flag) continue; /* (p, q) is not a simulation relation */ st_delete(simul, &pair, &pair); LtlPairFree(pair); /* Enqueue perturbed pairs */ tbl2 = AutomatonVertexGetPreImg(A->G, p); tbl3 = AutomatonVertexGetPreImg(A->G, q); st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { pair2 = LtlPairNew((char *)u, (char *)v); if (st_lookup(simul, pair2, &pair)) { if (!st_is_member(enqueued, pair2)) { st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } } LtlPairFree(pair2); } } st_free_table(tbl2); st_free_table(tbl3); } lsDestroy(queue, (void (*)(lsGeneric))0); st_free_table(enqueued); /*###################################### * Add arcs to direct-simulated states *###################################### */ /* so that we can modify simul with the for-loop */ tbl0 = st_copy(simul); st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { /* 'p' is simulated by 'q' */ p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Add arcs from the predecessors of q to p */ tbl2 = AutomatonVertexGetPreImg(A->G, p); tbl3 = AutomatonVertexGetPreImg(A->G, q); st_foreach_item(tbl3, stgen1, &s, NIL(char *)) { if (!st_is_member(tbl2, s)){ g_add_edge(s, p); changed = 1; } } st_free_table(tbl2); st_free_table(tbl3); } st_free_table (tbl0); st_foreach_item(simul, stgen, &pair, NIL(char *)) { LtlPairFree(pair); } st_free_table (simul); return changed; } /**Function******************************************************************** Synopsis [Minimize the Automaton using Reverse Simulation.] Description [Compute Reverse-Simulation relation, and minimize the automaton according to the following 2 cases: 1) remove p if (p,q) is a Bi-Simulation relation 2) remove edges from p to their common sucessors if p is reverse simulated by q.] SideEffects [The automaton might be changed. if so, return 1.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonMinimizeByReverseSimulation( Ltl_Automaton_t *A, int verbosity) { int changed = 0; int flag = 0; lsList states, otherstates, list, queue; lsGen lsgen, lsgen1; edge_t *e; vertex_t *state, *otherstate; vertex_t *p, *q, *s, *t, *u, *v; LtlSet_t *set, *set2; st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3; st_table *simul, *enqueued; st_generator *stgen, *stgen1, *stgen2; LtlPair_t *pair, *pair2; /* store the simulation-relation in hash tables and queue list */ simul = st_init_table(LtlPairCompare, LtlPairHash); enqueued = st_init_table(LtlPairCompare, LtlPairHash); queue = lsCreate(); /*###################################### * Initialize sim rln to all pairs (p,q) *###################################### */ states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (states, lsgen, state) { lsForEachItem (otherstates, lsgen1, otherstate) { /* p != q */ if (state == otherstate) continue; /* L(p) <= L(q), in other words, (set(Lp) >= set(Lq) */ set = LtlAutomatonVertexGetLabels(state); set2 = LtlAutomatonVertexGetLabels(otherstate); if (!LtlSetInclude(set, set2)) continue; /* p is in Q0 -> q is in Q0 */ if (st_is_member(A->Init, state) && !st_is_member(A->Init, otherstate)) continue; /* p is in F -> q is in F */ if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; /* put (state, otherstate) into simul-relation */ pair = LtlPairNew((char *)state, (char *)otherstate); st_insert(simul, pair, pair); st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } } lsDestroy(states, (void (*)(lsGeneric)) NULL); lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); /*###################################### * Compute the "Greatest Fixpoint" *###################################### */ while (lsDelBegin(queue, &pair) != LS_NOMORE) { st_delete(enqueued, &pair, NIL(char *)); p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* For each 's' in Img(p), there must exists a 't' Img(q) such that * (s, t) is also a reverse simulation pair */ tbl0 = AutomatonVertexGetPreImg(A->G, p); tbl1 = AutomatonVertexGetPreImg(A->G, q); st_foreach_item(tbl0, stgen, &s, NIL(char *)) { flag = 0; st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { flag = (s==t); if (flag) { st_free_gen(stgen1); break; } pair2 = LtlPairNew((char *)s, (char *)t); flag = st_is_member(simul, pair2); LtlPairFree(pair2); if (flag) { st_free_gen(stgen1); break; } } if (!flag) { st_free_gen(stgen); break; } } st_free_table(tbl0); st_free_table(tbl1); if (flag) continue; /* (p, q) is not a simulation relation */ st_delete(simul, &pair, &pair); LtlPairFree(pair); /* Enqueue perturbed pairs */ tbl2 = AutomatonVertexGetImg(A->G, p); tbl3 = AutomatonVertexGetImg(A->G, q); st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { pair2 = LtlPairNew((char *)u, (char *)v); if (st_lookup(simul, pair2, &pair)) if(!st_is_member(enqueued, pair2)) { st_insert(enqueued, pair, pair); lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); } LtlPairFree(pair2); } } st_free_table(tbl2); st_free_table(tbl3); } lsDestroy(queue, (void (*)(lsGeneric))0); st_free_table(enqueued); /*###################################### * Simplify by Bi-Sim equivalent states *###################################### */ /* to store removed states */ tbl1 = st_init_table(st_ptrcmp, st_ptrhash); /* so that we can modify simul with the for loop */ tbl0 = st_copy(simul); st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Make sure neither has been removed */ if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) continue; /* Make sure it is Bi-simulation by checking the other direction*/ pair2 = LtlPairNew((char *)q, (char *)p); flag = st_lookup(simul, pair2, &pair); LtlPairFree(pair2); if (!flag) continue; /*#### Direct BI-SIMULATION equivalent states####*/ /* Theorem applies */ /* Remove its swap: (q, p) from simul-rln */ st_delete(simul, &pair, &pair); LtlPairFree(pair); /* Remove 'p' and connect 'q' to all its successors */ tbl2 = AutomatonVertexGetImg(A->G, p); tbl3 = AutomatonVertexGetImg(A->G, q); st_foreach_item(tbl2, stgen1, &s, NIL(char *)) { if (s == p) continue; if (!st_is_member(tbl3, s)) g_add_edge(q, s); } st_free_table(tbl2); st_free_table(tbl3); /* Update the fairsets (remove 'p') */ lsForEachItem (A->Fair, lsgen, FairSet) { StTableDelete(FairSet, (char *)p); } /* Remove 'p' from Q0 */ StTableDelete(A->Init, (char *)p); /* Remove 'p' form dontcare if it's in it */ StTableDelete(A->dontcare, (char *)p); /* Remove 'p' from the automaton */ st_insert(tbl1, p, p); g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); changed = 1; } st_free_table(tbl0); /*###################################### * Remove arcs from Reverse-simulated states *#####################################*/ /* so that we can modify simul with the for loop */ tbl0 = st_copy(simul); st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { /* 'p' is simulated by 'q' */ p = (vertex_t *)pair->First; q = (vertex_t *)pair->Second; /* Make sure that neither has been removed */ if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) continue; /*#### p is reverse-simulated by q####*/ /* Theorem applies */ /* Drop arcs from 'p' to their common successors */ tbl3 = AutomatonVertexGetImg(A->G, q); list = lsCopy(g_get_out_edges(p), (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (list, lsgen, e) { if (!st_is_member(tbl3, g_e_dest(e))) continue; g_delete_edge(e, (void (*)(gGeneric))0); changed = 1; } lsDestroy(list, (void (*)(lsGeneric)) 0); st_free_table(tbl3); } st_free_table (tbl0); st_free_table (tbl1); st_foreach_item(simul, stgen, &pair, NIL(char *)) { LtlPairFree(pair); } st_free_table (simul); return changed; } /**Function******************************************************************** Synopsis [Remove states that cannot reach any fair SCC and perform other simplifications (simplify fair sets).] Description [We consider the following cases concerning fair SCCs: 1. Remove redundant transitions from predecessors of universal states (a state with TRUE label and a self-loop, and it belongs to all fair sets.) 2. Remove all states that can not reach any fair SCC 3. Remove duplicate fair set and Shrink the fair sets ] SideEffects [The automaton might be changed, in which case return 1. Also, the A->SCC and A->Q are RE-computed.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonMinimizeByPrune( Ltl_Automaton_t *A, int verbosity) { st_generator *stgen, *stgen1, *stgen2; st_table *FairSet, *otherset, *Class, *scc, *rest; st_table *tbl, *tbl1, *tbl2; lsList states, list; lsGen lsgen, lsgen1; vertex_t *state, *s, *greatest, *qstate; edge_t *e; long isFair; int flag, totalnum, procnum; /* Eliminate redundant edges from the predecessors of universal states. * (A universal state is a state labeled 'TRUE' with a self-loop, and it * should belong to all FairSets) */ states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); lsForEachItem (states, lsgen, state) { /* label = TRUE */ if (LtlSetCardinality(LtlAutomatonVertexGetLabels(state)) != 0) continue; /* self-loop */ if (!AutomatonVertexHasSelfLoop(A->G, state)) continue; /* blongs to all fairSet */ flag = 1; lsForEachItem (A->Fair, lsgen1, FairSet) { if (!st_is_member(FairSet, state)) { flag = 0; lsFinish(lsgen1); break; } } if (!flag) continue; /* We can apply the theorem: Remove edges from its predecessors to * other siblings */ tbl = AutomatonVertexGetPreImg(A->G, state); st_foreach_item(tbl, stgen, &s, NIL(char *)) { if (s == state) continue; list = lsCopy(g_get_out_edges(s), (lsGeneric (*)(lsGeneric))0); lsForEachItem(list, lsgen1, e) { if (g_e_dest(e) != state) g_delete_edge(e, (void (*)(gGeneric))0); } lsDestroy(list, (void (*)(lsGeneric))0); } st_free_table(tbl); } /*2) Compute all the SCCs, and build the SCC-quotient graph * every time before pruning, we need to re-compute the SCC graph */ Ltl_AutomatonComputeSCC(A, 1); if (A->Q) { Ltl_AutomatonFree((gGeneric) A->Q); A->Q = NIL(Ltl_Automaton_t); } A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); /* Mark those states without loop going through as "don't care states" */ st_foreach_item(A->SCC, stgen, &Class, &isFair) { if (isFair == 2) StTableAppend(A->dontcare, Class); } /* Restrict automaton to those states that can reach a fair SCC * There are two cases: (a) with fairness (b) without fairness */ lsFirstItem(A->Q->Fair, &FairSet, NIL(lsHandle)); if (lsLength(A->Fair) > 0) { /* (a) */ tbl = st_init_table(st_ptrcmp, st_ptrhash); /* Find states that are on fair cycles */ st_foreach_item(FairSet, stgen, &qstate, NIL(char *)) { Class = AutomatonQuotientVertexGetClass(qstate); StTableAppend(tbl, Class); } /* Shrink fair sets in A->Fair */ lsForEachItem (A->Fair, lsgen, FairSet) { StTableRestrict(FairSet, tbl); } /* Find states that can reach fair cycles */ tbl1 = tbl; tbl = g_EF(A->G, tbl); st_free_table(tbl1); /* Remove the rest part of A->G */ StTableRestrict(A->Init, tbl); StTableRestrict(A->dontcare, tbl); lsForEachItem (states, lsgen, state) { if (!st_is_member(tbl, state)) g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); } }else { /* (b) */ /* Find all the reachable state */ tbl = g_reachable(A->G, A->Init); /* Remove the rest part of A->G */ StTableRestrict(A->Init, tbl); StTableRestrict(A->dontcare, tbl); lsForEachItem (states, lsgen, state) { if (!st_is_member(tbl, state)) g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); } } /* Clean up the Quotient graph */ st_foreach_item(A->SCC, stgen, &Class, &isFair) { StTableRestrict(Class, tbl); } st_free_table(tbl); /* 3. Remove duplicate FairSet */ /* Discard duplicate fair sets and fair sets including all states. Here we * also restrict fair sets by analyzing each SCC. If within an SCC, one fair * set dominates another, it can be restricted to the dominated one. As a * special case: if an SCC does not intersect all fair sets, its states are * removed from all fair sets. */ totalnum = lsLength(A->Fair); procnum = 0; while(lsDelBegin(A->Fair, &FairSet) != LS_NOMORE) { /* Remove this FairSet if it includes all states in the SCC */ if (st_count(FairSet) == lsLength(g_get_vertices(A->G))) { st_free_table(FairSet); totalnum--; }else { /* After restricted to the SCC: if fair set2 is contained in set1, * shrink set1 to set2 (remove (set1-set2) from set1 */ st_foreach_item(A->SCC, stgen, &scc, &isFair) { lsForEachItem(A->Fair, lsgen, otherset) { tbl1 = st_copy(scc); tbl2 = st_copy(scc); StTableRestrict(tbl1, FairSet); StTableRestrict(tbl2, otherset); if (StTableInclude(tbl1, tbl2, NIL(st_table))) { /* tbl1 <= (tbl1 - tbl2) */ StTableSubtract(tbl1, tbl2); StTableSubtract(FairSet, tbl1); } st_free_table(tbl1); st_free_table(tbl2); } } /* Remove the fair set if another fair set is contained in it */ flag = 1; lsForEachItem(A->Fair, lsgen, otherset) { if (StTableInclude(FairSet,otherset,NIL(st_table))) { flag = 0; lsFinish(lsgen); break; } } if (!flag) { st_free_table(FairSet); totalnum--; }else lsNewEnd(A->Fair, (lsGeneric) FairSet, NIL(lsHandle)); } procnum++; if (procnum > totalnum) break; } /* 4. GLB reduction */ /* If an SCC is a clique, and there is a state 's' whose label exactly matches * the GLB of all the labels of the clique, we can remove 's' from every fair * set such that it contains at least another state of the SCC besides 's' */ st_foreach_item(A->SCC, stgen, &Class, &isFair) { /* 1-state SCC won't work */ if (st_count(Class) <= 1) continue; /* must be a clique */ if (!AutomatonPartitionIsClique(A->G, Class)) continue; tbl = AutomatonPartitionLabelGLB(Class, A->labelTableNegate); if (!tbl) continue; rest = st_copy(Class); StTableSubtract(rest, tbl); lsForEachItem(A->Fair, lsgen, FairSet) { if (StTableInclude(FairSet, tbl, NIL(st_table)) && !StTableIsDisjoint(FairSet, rest, NIL(st_table))) /* we apply the theorem here */ StTableSubtract(FairSet, tbl); } st_free_table(rest); st_free_table(tbl); } /* 5. LUB reduction */ /* If an SCC contains a state 's' that simulates all the other states in the * same SCC (both forward and backward), then all states of the SCC except * 's' can be removed from all fair sets. The following code checks for a * special case of this theorem */ st_foreach_item(A->SCC, stgen, &Class, &isFair) { vertex_t *qstate; st_lookup(A->Q->SCC, Class, &qstate); /* 1-state SCC won't work */ if (st_count(Class) <= 1) continue; tbl = AutomatonPartitionLabelLUB(Class, A->labelTableNegate); if (!tbl) continue; st_foreach_item(tbl, stgen1, &greatest, NIL(char *)) { /* that state should have a self-loop */ if (!AutomatonVertexHasSelfLoop(A->G, greatest)) continue; /* that state should be initial if the SCC contains initial states */ if (st_is_member(A->Q->Init, qstate) && !st_is_member(A->Init, greatest)) continue; /* that state should belong to FairSet if the SCC intersect it */ flag = 1; lsForEachItem(A->Fair, lsgen, FairSet) { if (!st_is_member(FairSet, greatest) && !StTableIsDisjoint(FairSet,Class,NIL(st_table))){ flag = 0; lsFinish(lsgen); break; } } if (!flag) continue; /* Every state outside of the SCC with a transition into the SCC * should also have a transition to that state */ tbl1 = st_init_table(st_ptrcmp, st_ptrhash); st_foreach_item(Class, stgen2, &state, NIL(char *)) { tbl2 = AutomatonVertexGetPreImg(A->G, state); StTableAppend(tbl1, tbl2); st_free_table(tbl2); } tbl2 = AutomatonVertexGetPreImg(A->G, greatest); flag = StTableInclude(tbl2, tbl1, Class); st_free_table(tbl2); st_free_table(tbl1); if (!flag) continue; /* we now apply the theorem */ tbl1 = st_copy(Class); if (st_is_member(tbl1, greatest)) st_delete(tbl1, &greatest, NIL(char *)); lsForEachItem(A->Fair, lsgen, FairSet) { StTableSubtract(FairSet, tbl1); } st_free_table(tbl1); } st_free_table(tbl); } lsDestroy(states, (void (*)(lsGeneric))0); return 1; } /**Function******************************************************************** Synopsis [Compute the SCCs of the Automaton.] Description [Traverse the entire reachable graph of the automaton, and put all the SCCs in a hash table. If force=1, the existing partition (A->SCC) is freed and the new partition is computed. If force=0, the partition is computed only if A->SCC=null.] SideEffects [A->SCC is assigned the new partition.] SeeAlso [] ******************************************************************************/ void Ltl_AutomatonComputeSCC( Ltl_Automaton_t *A, int force) { st_generator *stgen; st_table *component; /* compute A->SCC if not exist */ if (!force && A->SCC) return; if (force && A->SCC) { st_foreach_item(A->SCC, stgen, &component, NIL(char *)) { st_free_table(component); } st_free_table(A->SCC); } A->SCC = g_SCC(A->G, A->Init); return; } /**Function******************************************************************** Synopsis [Return 1 if if the automaton is 'WEAK'] Description [The definition of WEAK: For each fair SCC in the automaton, every fairset F contains all its states. A special case: If there is no fairness constraint at all, it's WEAK.] SideEffects [Compute the SCCs and Quotient graph(A->SCC,A->Q) if not exist.] SeeAlso [] ******************************************************************************/ int Ltl_AutomatonIsWeak( Ltl_Automaton_t *A) { int weak; long isFair; st_generator *stgen; st_table *scc, *FairSet; lsGen lsgen; /* A SCC without fairness constraint is WEAK */ if (lsLength(A->Fair) == 0) return 1; /* compute the partition(A->SCC) and Quotient graph(A->Q) if not exist */ if (!A->SCC) Ltl_AutomatonComputeSCC(A,0); if (!A->Q) A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); /* weak: for each SCC, * either it's included in all FairSets * or it intersects none of them */ weak = 1; st_foreach_item(A->SCC, stgen, &scc, &isFair) { int flag = 0; /* intersect none of them ? */ lsForEachItem (A->Fair, lsgen, FairSet) { if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) { lsFinish(lsgen); flag = 1; break; } } if (!flag) continue; /* included in all of them ? */ lsForEachItem (A->Fair, lsgen, FairSet) { if (!StTableInclude(FairSet, scc, NIL(st_table))) { weak = 0; lsFinish(lsgen); break; } } if (!weak) { st_free_gen(stgen); break; } } return weak; } /**Function******************************************************************** Synopsis [Return the strength of the automaton.] Description [0 -terminal 1 -weak 2 -strong.] SideEffects [Compute the parition and quotient graph if not exist.] SeeAlso [] ******************************************************************************/ Mc_AutStrength_t Ltl_AutomatonGetStrength( Ltl_Automaton_t *A) { Mc_AutStrength_t result; vertex_t *qstate, *state, *state2; st_generator *stgen, *stgen1, *stgen2; st_table *tbl, *FairSet, *scc; lsList cover; lsGen lsgen; /* Every time we need to re-compute the partition(A->SCC) and * the Quotient graph(A->Q) */ Ltl_AutomatonComputeSCC(A, 1); if (A->Q) { Ltl_AutomatonFree((gGeneric) A->Q); A->Q = NIL(Ltl_Automaton_t); } A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); /* is it strong ? */ if (!Ltl_AutomatonIsWeak(A)) return Mc_Aut_Strong_c /*2*/; /* it's terminal (0) if all the weak SCCs are COMPLETE and FINAL.*/ result = Mc_Aut_Terminal_c; st_foreach_item(A->SCC, stgen, &scc, NIL(char *)) { int disjoint_flag = 1; int final_flag = 1; int complete_flag = 1; /* if it does not intersect any fair set, we don't care about it */ if (lsLength(A->Fair) == 0) disjoint_flag = 0; else { lsForEachItem(A->Fair, lsgen, FairSet) { if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) { disjoint_flag = 0; lsFinish(lsgen); break; } } } if (disjoint_flag) continue; /* FINAL: * it shouldn't be trivial, and shouldn't have edge to other sccs */ st_lookup(A->Q->SCC, scc, &qstate); tbl = AutomatonVertexGetImg(A->Q->G, qstate); final_flag = (st_count(tbl) == 1 && st_is_member(tbl, qstate)); st_free_table(tbl); if (!final_flag) { st_free_gen(stgen); result = Mc_Aut_Weak_c; /* weak */ break; } /* COMPLETE: * for each state in the SCC: the union of the labels in all * its successors is tautology */ st_foreach_item(scc, stgen1, &state, NIL(char *)) { tbl = AutomatonVertexGetImg(A->G, state); cover = lsCreate(); st_foreach_item(tbl, stgen2, &state2, NIL(char *)) { lsNewEnd(cover, (lsGeneric)LtlAutomatonVertexGetLabels(state2), NIL(lsHandle)); } st_free_table(tbl); complete_flag = LtlCoverIsTautology(cover, A->labelTableNegate); lsDestroy(cover, (void (*)(lsGeneric))0); if (!complete_flag) { st_free_gen(stgen1); break; } } if (!complete_flag) { st_free_gen(stgen); result = Mc_Aut_Weak_c; /* weak */ break; } } /* Weak = 1; Terminal = 0 */ return result; } /**Function******************************************************************** Synopsis [Return the Quotient graph for the given partition.] Description [The Quotient graph is represented as an automaton Q: Q->SCC : partition component TO vertex in Q graph hash table Q->Init: initial vertices in Q graph Q->Fair: only 1 FairSet in it, which contains the Q vertices corresponding to the fair components Q->G : The actual graph_t Each Q vertex is associated with an automaton node: node->index: the index # of the Q vertex node->Class: the partition component associated with this vertex. NOTICE: the Quotient graph is NOT a DAG, non-trivial SCCs have self-loops.] SideEffects [A->SCC is updated with the following information: if (key) is a trivial SCC (obviously non-fair), (value)=2; if (key) is a non-trivial non-fair SCC, (value) = 0; if (key) is a fair SCC, (value)=1; otherwise, (value)=1; The result should be freed by the caller.] SeeAlso [] ******************************************************************************/ Ltl_Automaton_t * Ltl_AutomatonCreateQuotient( Ltl_Automaton_t *A, st_table *partition) { long isFair; int flag; st_generator *stgen, *stgen1; st_table *Class, *FairSet; lsGen lsgen; st_table *Avtx2Qvtx, *Class2Qvtx, *EdgeUtable; Ltl_Automaton_t *Q; Ltl_AutomatonNode_t *node; vertex_t *q, *p; edge_t *e; LtlPair_t *pair; /* create the Q graph as a Automaton */ Q = Ltl_AutomatonCreate(); Q->isQuotientGraph = 1; /*### for each class, add vtx in Q->G ###*/ /* hash tables : (vtx in A, vtx in Q), (class_st_table, vtx in Q) */ Avtx2Qvtx = st_init_table(st_ptrcmp, st_ptrhash); Class2Qvtx = st_init_table(st_ptrcmp, st_ptrhash); st_foreach_item(partition, stgen, &Class, NIL(char *)) { /* add 'q' in Q->G */ q = g_add_vertex(Q->G); node = Ltl_AutomatonNodeCreate(Q); node->Class = Class; q->user_data = (gGeneric) node; st_insert(Class2Qvtx, Class, q); /* hash table (A_vtx -> Q_vtx) */ flag = 0; st_foreach_item(Class, stgen1, &p, NIL(char *)) { st_insert(Avtx2Qvtx, p, q); if (st_is_member(A->Init, p)) flag = 1; } /* if any state in class is in A->Init, put class into Q->Init */ if (flag) st_insert(Q->Init, q, q); } /*### for each (class, class2), add edges ###*/ /* edge unique table in Q graph, key = (class, class2) */ EdgeUtable = st_init_table(LtlPairCompare, LtlPairHash); pair = LtlPairNew(0,0); foreach_edge(A->G, lsgen, e) { if (!st_lookup(Avtx2Qvtx, g_e_source(e), &pair->First)) continue; if (!st_lookup(Avtx2Qvtx, g_e_dest(e), &pair->Second)) continue; /* only consider reachable states in A->G */ if (!st_is_member(EdgeUtable, pair)) { LtlPair_t *tmpPair = LtlPairNew(pair->First, pair->Second); st_insert(EdgeUtable, tmpPair, tmpPair); g_add_edge((vertex_t *)pair->First, (vertex_t *)pair->Second); } } /*### put fair sccs into the only FairSet ###*/ /* isFair = 1 (fair SCC); isFair = 0 (non-trivial non-fair SCC); * isFair = 2 (dontcare: trivial SCC, obviously non-fair)*/ FairSet = st_init_table(st_ptrcmp, st_ptrhash); st_foreach_item(partition, stgen, &Class, &isFair) { st_insert(partition, Class, (char *)0); /* it should be a nontrivial scc (size >1 or have self-loop) */ if (st_count(Class)==1) { st_lookup(Class2Qvtx, Class, &pair->First); st_lookup(Class2Qvtx, Class, &pair->Second); if (!st_is_member(EdgeUtable, pair)) { /*trivial scc (1 state without self-loop) */ st_insert(partition, Class, (char *)2); continue; } } /* for non trivial SCC, check if it intersect all FairSets */ if (!StTableIsFair(A->Fair, Class)) continue; /* it's a "fair SCC" */ st_insert(partition, Class, (char *)1); st_lookup(Class2Qvtx, Class, &pair->First); st_insert(FairSet, pair->First, pair->First); } lsNewEnd(Q->Fair, (lsGeneric) FairSet, (lsHandle *) 0); /* free */ LtlPairFree(pair); st_foreach_item(EdgeUtable, stgen, &pair, NIL(char *)) { LtlPairFree(pair); } st_free_table(EdgeUtable); st_free_table(Avtx2Qvtx); /* st_free_table(Class2Qvtx); */ Q->SCC = Class2Qvtx; return Q; } /**Function******************************************************************** Synopsis [Return the node index associated with the given vertex.] SideEffects [] ******************************************************************************/ int Ltl_AutomatonVtxGetNodeIdx( vertex_t *v) { Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data; return node->index; } /**Function******************************************************************** Synopsis [Return the automaton node label set associated with the vertex.] SideEffects [The result is owned by the node, and should not be freed.] ******************************************************************************/ LtlSet_t * LtlAutomatonVertexGetLabels( vertex_t *vtx) { Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) vtx->user_data; return node->Labels; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Return the input-compatible candidates.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ static lsList AutomatonPickInputCandidate( graph_t *G, vertex_t *vtx) { st_table *uTable; lsList candi, preImg; lsGen lsgen, lsgen2; edge_t *e, *e2; vertex_t *s, *t; int size; preImg = g_get_in_edges(vtx); /* shouldn't be freed */ size = lsLength(preImg); /* No predecessor */ if (size == 0) { return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); } /* The only predecessor is itself */ if (size == 1) { lsFirstItem(preImg, &e, NIL(lsHandle)); if (g_e_source(e) == vtx) { /* all the vertices in G */ return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); } } /* Has predecessor(s) other than itself */ uTable = st_init_table(st_ptrcmp, st_ptrhash); candi = lsCreate(); lsForEachItem (preImg, lsgen, e) { s = g_e_source(e); foreach_out_edge(s, lsgen2, e2) { t = g_e_dest(e2); if (t != vtx) { if(!st_insert(uTable, t, t)) lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle)); } } if (size == 1) { if (!st_insert(uTable, s, s)) lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle)); } } st_free_table(uTable); return candi; } /**Function******************************************************************** Synopsis [Return the output-compatible candidates.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ static lsList AutomatonPickOutputCandidate( graph_t *G, vertex_t *vtx) { st_table *uTable; lsList candi, Img; lsGen lsgen, lsgen2; edge_t *e, *e2; vertex_t *s, *t; int size; Img = g_get_out_edges(vtx); size = lsLength(Img); /* No successor */ if (size == 0) { return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); } /* The only successor is itself */ if (size == 1) { lsFirstItem(Img, &e, NIL(lsHandle)); if (g_e_dest(e) == vtx) { return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); } } /* Has successor(s) other than itself */ uTable = st_init_table(st_ptrcmp, st_ptrhash); candi = lsCreate(); lsForEachItem(Img, lsgen, e) { s = g_e_dest(e); foreach_in_edge(s, lsgen2, e2) { t = g_e_source(e2); if (t != vtx) { if(!st_insert(uTable, t, t)) lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle)); } } if (size == 1) { if(!st_insert(uTable, s, s)) lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle)); } } st_free_table(uTable); return candi; } /**Function******************************************************************** Synopsis [Return the pre-image of the given vertex in the hash table.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ static st_table * AutomatonVertexGetPreImg( graph_t *G, vertex_t *vtx) { lsList preImg; lsGen lsgen; edge_t *e; vertex_t *s; st_table *uTable; preImg = g_get_in_edges(vtx); uTable = st_init_table(st_ptrcmp, st_ptrhash); lsForEachItem(preImg, lsgen, e) { s = g_e_source(e); st_insert(uTable, s, s); } return uTable; } /**Function******************************************************************** Synopsis [Return the image of the given vertex in the hash table.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ static st_table * AutomatonVertexGetImg( graph_t *G, vertex_t *vtx) { lsList Img; lsGen lsgen; edge_t *e; vertex_t *s; st_table *uTable; Img = g_get_out_edges(vtx); uTable = st_init_table(st_ptrcmp, st_ptrhash); lsForEachItem(Img, lsgen, e) { s = g_e_dest(e); st_insert(uTable, s, s); } return uTable; } /**Function******************************************************************** Synopsis [Return 1 iff the given vertex has a self-loop.] SideEffects [] ******************************************************************************/ static int AutomatonVertexHasSelfLoop( graph_t *G, vertex_t *vtx) { lsList Img; lsGen lsgen; edge_t *e; int flag = 0; Img = g_get_out_edges(vtx); lsForEachItem(Img, lsgen, e) { if (g_e_dest(e) == vtx) { flag = 1; lsFinish(lsgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 iff the following statement in the automaton holds: For each fair set, both states are in it or none of them] SideEffects [] ******************************************************************************/ static int AutomatonPfairEquivQfair( Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate) { int flag = 1; st_table *FairSet; lsGen lsgen; lsForEachItem (A->Fair, lsgen, FairSet) { if (st_is_member(FairSet, state) != st_is_member(FairSet, otherstate)) { flag = 0; lsFinish(lsgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 iff the following statement in the automaton holds: For each fair set, if 'state' is in it, 'otherstate' must also in it.] SideEffects [] ******************************************************************************/ static int AutomatonPfairImplyQfair( Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate) { int flag = 1; st_table *FairSet; lsGen lsgen; lsForEachItem (A->Fair, lsgen, FairSet) { if (st_is_member(FairSet, state) && !st_is_member(FairSet, otherstate)) { flag = 0; lsFinish(lsgen); break; } } return flag; } /**Function******************************************************************** Synopsis [If 'item' is in the hash table, Delete it and return the real key; Otherwise, return 0.] SideEffects ['item' will not be modified.] ******************************************************************************/ static char * StTableDelete( st_table *tbl, char *item) { char *key = item; if (st_is_member(tbl, key)) { st_delete(tbl, &key, NIL(char *)); return key; }else return NIL(char); } /**Function******************************************************************** Synopsis [Append the tbl2 to tbl1 and return tbl1.] SideEffects [tbl1 is permenently changed.] ******************************************************************************/ static st_table * StTableAppend( st_table *tbl1, st_table *tbl2) { char *key, *value; st_generator *stgen; st_foreach_item(tbl2, stgen, &key, &value) { if (!st_is_member(tbl1, key)) st_insert(tbl1, key, value); } return tbl1; } /**Function******************************************************************** Synopsis [Remove from tbl1 all the items that are not in tbl2.] SideEffects [tbl1 is changed and returned.] ******************************************************************************/ static st_table * StTableRestrict( st_table *tbl1, st_table *tbl2) { char *key, *value; st_table *tbl = st_copy(tbl1); st_generator *stgen; st_foreach_item(tbl, stgen, &key, &value) { if (!st_is_member(tbl2, key)) st_delete(tbl1, &key, &value); } st_free_table(tbl); return tbl1; } /**Function******************************************************************** Synopsis [Remove from tbl1 all the items that are in tbl2.] SideEffects [tbl1 is changed and returned.] ******************************************************************************/ static st_table * StTableSubtract( st_table *tbl1, st_table *tbl2) { char *key, *value; st_generator *stgen; st_foreach_item(tbl2, stgen, &key, &value) { if (st_is_member(tbl1, key)) st_delete(tbl1, &key, &value); } return tbl1; } /**Function******************************************************************** Synopsis [Return 1 if tbl1 and tbl2 have the same items except those also in 'dontcare'. 'dontcare' can be a null pointer.] SideEffects [] ******************************************************************************/ static int StTableIsEqual( st_table *tbl1, st_table *tbl2, st_table *dontcare) { int flag = 1; st_generator *stgen; vertex_t *vtx; flag = 1; st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) { if (dontcare) { if (st_is_member(dontcare,vtx)) continue; } if (!st_is_member(tbl2,vtx)) { flag = 0; st_free_gen(stgen); break; } } if (!flag) return 0; st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) { if (dontcare) { if (st_is_member(dontcare,vtx)) continue; } if (!st_is_member(tbl1, vtx)) { flag = 0; st_free_gen(stgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 if 'larger' include every items in 'small' except those also in 'dontcare'. Notice that 'dontcare' can be a null pointer.] SideEffects [] ******************************************************************************/ static int StTableInclude( st_table *large, st_table *small, st_table *dontcare) { int flag = 1; st_generator *stgen; vertex_t *vtx; flag = 1; st_foreach_item(small, stgen, &vtx, NIL(char *)) { if (dontcare) { if (st_is_member(dontcare, vtx)) continue; } if (!st_is_member(large,vtx)) { flag = 0; st_free_gen(stgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 if the two tables shares nothing except those items also in 'dontcare'. Notice that 'dontcare' can be a null pointer.] SideEffects [] ******************************************************************************/ static int StTableIsDisjoint( st_table *tbl1, st_table *tbl2, st_table *dontcare) { int flag = 1; st_generator *stgen; vertex_t *vtx; flag = 1; st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) { if (dontcare) { if (st_is_member(dontcare, vtx)) continue; } if (st_is_member(tbl2,vtx)) { flag = 0; st_free_gen(stgen); break; } } if (!flag) return 0; st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) { if (dontcare) { if (st_is_member(dontcare, vtx)) continue; } if (st_is_member(tbl1,vtx)) { flag = 0; st_free_gen(stgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 if the given tables intersect every tables in the list.] SideEffects [] ******************************************************************************/ static int StTableIsFair( lsList A_Fair, st_table *Class) { int flag; st_table *FairSet; lsGen lsgen; flag = 1; lsForEachItem (A_Fair, lsgen, FairSet) { if (StTableIsDisjoint(FairSet,Class,NIL(st_table))) { flag = 0; lsFinish(lsgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Return 1 if the given table forms a clique (for each state, there are edges to all the states in the set).] SideEffects [] ******************************************************************************/ static int AutomatonPartitionIsClique( graph_t *G, st_table *set) { int flag = 1; st_table *Img; st_generator *stgen; vertex_t *state; st_foreach_item(set, stgen, &state, NIL(char *)) { Img = AutomatonVertexGetImg(G, state); flag = StTableInclude(Img, set, NIL(st_table)); st_free_table(Img); if (!flag) { st_free_gen(stgen); break; } } return flag; } /**Function******************************************************************** Synopsis [Find the Least Upper Bound of the labels of a set of states, and Return a hash table of states that satisfy this 'LUB'. Return null if the hash table is empty.] SideEffects [The result should be freed by the caller.] ******************************************************************************/ static st_table * AutomatonPartitionLabelLUB( st_table *set, array_t *Negate) { vertex_t *state; st_table *greatest = NIL(st_table); st_generator *stgen; LtlSet_t *lub = NIL(LtlSet_t); LtlSet_t *label; st_foreach_item(set, stgen, &state, NIL(char *)) { label = LtlAutomatonVertexGetLabels(state); if (greatest) { if (LtlSetEqual(label, lub)) st_insert(greatest, state, state); else if (LtlSetInclude(lub, label)) { LtlSetAssign(lub, label); st_free_table(greatest); greatest = st_init_table(st_ptrcmp, st_ptrhash); st_insert(greatest, state, state); }else if (!LtlSetInclude(label, lub)) { st_free_table(greatest); greatest = NIL(st_table); st_free_gen(stgen); break; } }else { lub = LtlSetCopy(label); greatest = st_init_table(st_ptrcmp, st_ptrhash); st_insert(greatest, state, state); } } if (lub) LtlSetFree(lub); return greatest; } /**Function******************************************************************** Synopsis [Find the Greatest Lower Bound of the labels of a set of states, and Return a hash table of A state that satisfy this 'GLB'. Return null if the hash table is empty.] SideEffects [The result should be freed by the caller.] ******************************************************************************/ static st_table * AutomatonPartitionLabelGLB( st_table *set, array_t *Negate) { vertex_t *state, *least; LtlSet_t *glb, *label; st_table *tbl; st_generator *stgen; least = NIL(vertex_t); glb = NIL(LtlSet_t); st_foreach_item(set, stgen, &state, NIL(char *)) { label = LtlAutomatonVertexGetLabels(state); if (!glb) glb = LtlSetCopy(label); else LtlSetOR(glb, glb, label); if (LtlSetIsContradictory(glb, Negate)) { least = NIL(vertex_t); st_free_gen(stgen); break; }else if (!least) { if (LtlSetEqual(glb, label)) least = state; }else if (!LtlSetEqual(glb, LtlAutomatonVertexGetLabels(least))) { if (LtlSetEqual(glb, label)) least = state; else least = NIL(vertex_t); } } if (glb) LtlSetFree(glb); if (least) { tbl = st_init_table(st_ptrcmp, st_ptrhash); st_insert(tbl, least, least); }else tbl = NIL(st_table); return tbl; } /**Function******************************************************************** Synopsis [Return the partition component (a st_table) associated with the given vertex in the Quotient graph.] SideEffects [The result is owned by the node, and should NOT be freed.] ******************************************************************************/ static st_table * AutomatonQuotientVertexGetClass( vertex_t *vtx) { Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *)vtx->user_data; return node->Class; } /**Function******************************************************************** Synopsis [Return the node index associated with the given vertex.] SideEffects [] ******************************************************************************/ /*static int AutomatonVtxGetNodeIdx( vertex_t *v) { Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data; return node->index; }*/