VIS
|
00001 00017 #include "ltlInt.h" 00018 00019 static char rcsid[] UNUSED = "$Id: ltlMinimize.c,v 1.33 2009/04/09 02:21:13 fabio Exp $"; 00020 00021 /*---------------------------------------------------------------------------*/ 00022 /* Constant declarations */ 00023 /*---------------------------------------------------------------------------*/ 00024 00025 /*---------------------------------------------------------------------------*/ 00026 /* Structure declarations */ 00027 /*---------------------------------------------------------------------------*/ 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Type declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 /*---------------------------------------------------------------------------*/ 00034 /* Variable declarations */ 00035 /*---------------------------------------------------------------------------*/ 00036 00037 /*---------------------------------------------------------------------------*/ 00038 /* Macro declarations */ 00039 /*---------------------------------------------------------------------------*/ 00040 00043 /*---------------------------------------------------------------------------*/ 00044 /* Static function prototypes */ 00045 /*---------------------------------------------------------------------------*/ 00046 00047 static lsList AutomatonPickInputCandidate(graph_t *G, vertex_t *vtx); 00048 static lsList AutomatonPickOutputCandidate(graph_t *G, vertex_t *vtx); 00049 static st_table * AutomatonVertexGetPreImg(graph_t *G, vertex_t *vtx); 00050 static st_table * AutomatonVertexGetImg(graph_t *G, vertex_t *vtx); 00051 static int AutomatonVertexHasSelfLoop(graph_t *G, vertex_t *vtx); 00052 static int AutomatonPfairEquivQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate); 00053 static int AutomatonPfairImplyQfair(Ltl_Automaton_t *A, vertex_t *state, vertex_t *otherstate); 00054 static char * StTableDelete(st_table *tbl, char *item); 00055 static st_table * StTableAppend(st_table *tbl1, st_table *tbl2); 00056 static st_table * StTableRestrict(st_table *tbl1, st_table *tbl2); 00057 static st_table * StTableSubtract(st_table *tbl1, st_table *tbl2); 00058 static int StTableIsEqual(st_table *tbl1, st_table *tbl2, st_table *dontcare); 00059 static int StTableInclude(st_table *large, st_table *small, st_table *dontcare); 00060 static int StTableIsDisjoint(st_table *tbl1, st_table *tbl2, st_table *dontcare); 00061 static int StTableIsFair(lsList A_Fair, st_table *Class); 00062 static int AutomatonPartitionIsClique(graph_t *G, st_table *set); 00063 static st_table * AutomatonPartitionLabelLUB(st_table *set, array_t *Negate); 00064 static st_table * AutomatonPartitionLabelGLB(st_table *set, array_t *Negate); 00065 static st_table * AutomatonQuotientVertexGetClass(vertex_t *vtx); 00066 /*static int AutomatonVtxGetNodeIdx(vertex_t *v);*/ 00067 00071 /*---------------------------------------------------------------------------*/ 00072 /* Definition of exported functions */ 00073 /*---------------------------------------------------------------------------*/ 00074 00075 00092 int 00093 Ltl_AutomatonMinimizeByIOCompatible( 00094 Ltl_Automaton_t *A, 00095 int verbosity) 00096 { 00097 int changed = 0; 00098 int flag; 00099 lsList states, incand, outcand; 00100 lsGen lsgen, lsgen2, lsgen3; 00101 vertex_t *state, *otherstate, *s; 00102 LtlSet_t *set, *set2; 00103 st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3, *tbl4; 00104 st_generator *stgen; 00105 00106 00107 /* We go through all the states in A->G, and check for Input-Compatible, 00108 * Output-Compatible, and Dominance 00109 */ 00110 states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); 00111 lsForEachItem (states, lsgen, state) { 00112 int localchanged = 0; 00113 /* Compute the Image adn PreImg of 'state' for later use */ 00114 tbl0 = AutomatonVertexGetPreImg(A->G, state); 00115 tbl1 = AutomatonVertexGetImg(A->G, state); 00116 00117 /* ############################ 00118 * Check for Input Compatible 00119 * ############################*/ 00120 incand = AutomatonPickInputCandidate(A->G, state); 00121 lsForEachItem (incand, lsgen2, otherstate) { 00122 /* p is 'state', q is 'otherstate' */ 00123 /* p != q */ 00124 if (state == otherstate) continue; 00125 /* L(p) = L(q) */ 00126 set = LtlAutomatonVertexGetLabels(state); 00127 set2 = LtlAutomatonVertexGetLabels(otherstate); 00128 if (!LtlSetEqual(set, set2)) continue; 00129 /* p \in Q0 <-> q \in Q0 */ 00130 if (st_is_member(A->Init, state) != 00131 st_is_member(A->Init, otherstate)) 00132 continue; 00133 /* p \in F <-> q \in F */ 00134 if (!AutomatonPfairEquivQfair(A, state, otherstate)) continue; 00135 /* preImg(p) - {p,q} == preImg(q) - {p,q} */ 00136 tbl2 = AutomatonVertexGetPreImg(A->G, otherstate); 00137 tbl3 = st_init_table(st_ptrcmp, st_ptrhash); 00138 st_insert(tbl3, state, state); 00139 st_insert(tbl3 , otherstate, otherstate); 00140 flag = StTableIsEqual(tbl0, tbl2, tbl3); 00141 st_free_table(tbl2); 00142 st_free_table(tbl3); 00143 if (!flag) continue; 00144 /* q \in [delta(p)+delta(q)] <-> p \in [delta(p)+delta(q)] */ 00145 tbl2 = AutomatonVertexGetImg(A->G, otherstate); 00146 if ( (st_is_member(tbl1,state) || 00147 st_is_member(tbl2,state)) 00148 != 00149 (st_is_member(tbl1,otherstate) || 00150 st_is_member(tbl2,otherstate)) ) { 00151 st_free_table(tbl2); 00152 continue; 00153 } 00154 00155 /* ######## (state, otherstate) :: input compatible ####### 00156 * we merge the two state by deleting 'state' 00157 * Notice that now we have the following data available: 00158 * tbl0 = PreImg(state), 00159 * tbl1 = Img(state), 00160 * tbl2 = Img(otherstate) 00161 */ 00162 00163 /* Update intial states */ 00164 StTableDelete(A->Init, (char *)state); 00165 /* Add edges (otherstate, s), here s is the sucessor of 'state' */ 00166 st_foreach_item(tbl1, stgen, &s, NIL(char *)) { 00167 if (s != state && !st_is_member(tbl2, s)) 00168 g_add_edge(otherstate, s); 00169 } 00170 /* Remove 'otherstate' also if state isn't in dontcare */ 00171 if (!st_is_member(A->dontcare, state)) 00172 StTableDelete(A->dontcare, (char *)otherstate); 00173 /* Remove 'state' from dontcare (if applicable) */ 00174 StTableDelete(A->dontcare, (char *)state); 00175 /* Update fairness conditions */ 00176 lsForEachItem (A->Fair, lsgen3, FairSet) { 00177 StTableDelete(FairSet, (char *)state); 00178 } 00179 /* Remove 'state' from the automaton */ 00180 g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 00181 00182 st_free_table(tbl2); 00183 /* terminate iteration on incand list */ 00184 changed = localchanged = 1; 00185 00186 lsFinish(lsgen2); 00187 break; 00188 } 00189 lsDestroy(incand, (void (*)(lsGeneric)) 0); 00190 if (localchanged) { 00191 st_free_table(tbl0); 00192 st_free_table(tbl1); 00193 continue; 00194 } 00195 00196 00197 /* ############################ 00198 * Check for Output Compatible 00199 * ############################ 00200 */ 00201 outcand = AutomatonPickOutputCandidate(A->G, state); 00202 lsForEachItem (outcand, lsgen2, otherstate) { 00203 /* p != q */ 00204 if (state == otherstate) continue; 00205 /* L(p) = L(q) */ 00206 set = LtlAutomatonVertexGetLabels(state); 00207 set2 = LtlAutomatonVertexGetLabels(otherstate); 00208 if (!LtlSetEqual(set, set2)) continue; 00209 /* p \in F <-> q \in F */ 00210 if (!AutomatonPfairEquivQfair(A, state, otherstate)) continue; 00211 /* Img(p) - {p,q} == Img(q) - {p,q} */ 00212 tbl2 = AutomatonVertexGetImg(A->G, otherstate); 00213 tbl3 = st_init_table(st_ptrcmp, st_ptrhash); 00214 st_insert(tbl3, state, state); 00215 st_insert(tbl3, otherstate, otherstate); 00216 flag = StTableIsEqual(tbl1, tbl2, tbl3); 00217 st_free_table(tbl3); 00218 if (!flag) { 00219 st_free_table(tbl2); 00220 continue; 00221 } 00222 /* q \in delta(p) + p \in delta(p)] <-> 00223 * q \in delta(q) + p \in delta(q)] 00224 */ 00225 flag = 0; 00226 if ( (st_is_member(tbl1, state) || 00227 st_is_member(tbl1, otherstate)) 00228 != 00229 (st_is_member(tbl2, state) || 00230 st_is_member(tbl2, otherstate)) ) { 00231 st_free_table(tbl2); 00232 continue; 00233 } 00234 00235 /* ######## (state, otherstate) :: output compatible ####### 00236 * Merge the two state by deleting 'state' 00237 * Notice that now we have the following data: 00238 * tbl0 = PreImg(state) 00239 * tbl1 = Img(state) 00240 * tbl2 = Img(otherstate) 00241 */ 00242 tbl3 = AutomatonVertexGetPreImg(A->G, otherstate); 00243 00244 /* Add 'otherstate to Q0 if 'state' is in it */ 00245 if (st_is_member(A->Init, state)) { 00246 st_delete(A->Init, &state, NIL(char *)); 00247 if(!st_is_member(A->Init, otherstate)) 00248 st_insert(A->Init, otherstate, otherstate); 00249 } 00250 /* Add edge (s, otherstate) where 's' is in PreImg(state) */ 00251 st_foreach_item(tbl0, stgen, &s, NIL(char *)) { 00252 if (s != state && s != otherstate && 00253 !st_is_member(tbl3, s)) 00254 g_add_edge(s, otherstate); 00255 } 00256 /* Add edge (otherstate, otherstate) if there exist (state, state) or 00257 * (state, otherstate) 00258 */ 00259 if (st_is_member(tbl1, otherstate) || 00260 st_is_member(tbl1, state)) 00261 if (!st_is_member(tbl2, otherstate)) 00262 g_add_edge(otherstate, otherstate); 00263 /* Update don't care conditions. If 'state' isn't in dontcare, also 00264 * remove 'otherstate' 00265 */ 00266 if (!st_is_member(A->dontcare, state)) { 00267 StTableDelete(A->dontcare, (char *)otherstate); 00268 } 00269 StTableDelete(A->dontcare, (char *)state); 00270 /* Remove 'state' from FairSets */ 00271 lsForEachItem (A->Fair, lsgen3, FairSet) { 00272 StTableDelete(FairSet, (char *)state); 00273 } 00274 /* Remove 'state' from the automaton */ 00275 g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 00276 00277 st_free_table(tbl2); 00278 st_free_table(tbl3); 00279 /* terminate iteration on incand list */ 00280 changed = localchanged = 1; 00281 00282 lsFinish(lsgen2); 00283 break; 00284 } 00285 if (localchanged) { 00286 lsDestroy(outcand, (void (*)(lsGeneric)) 0); 00287 st_free_table(tbl0); 00288 st_free_table(tbl1); 00289 continue; 00290 } 00291 00292 00293 /* ############################ 00294 * Check for Dominance 00295 * ############################ 00296 * We already have the lsList 'outcand' 00297 */ 00298 lsForEachItem (outcand, lsgen2, otherstate) { 00299 /* p != q */ 00300 if (state == otherstate) continue; 00301 /* L(p) \leq L(q) (set(Lp) > set(Lq) */ 00302 set = LtlAutomatonVertexGetLabels(state); 00303 set2 = LtlAutomatonVertexGetLabels(otherstate); 00304 if (!LtlSetInclude(set, set2)) continue; 00305 /* p \in Q0 -> q \in Q0 */ 00306 if (st_is_member(A->Init, state) && 00307 !st_is_member(A->Init, otherstate)) 00308 continue; 00309 /* p \in F -> q \in F */ 00310 if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; 00311 /* Img(p) is less than Img(q) */ 00312 tbl2 = AutomatonVertexGetImg(A->G, otherstate); 00313 flag = StTableInclude(tbl2, tbl1, NIL(st_table)); 00314 /* p is in Img(p) -> q is in Img(q) */ 00315 if (flag) { 00316 flag = (!st_is_member(tbl1, state) || 00317 st_is_member(tbl2, otherstate)); 00318 } 00319 st_free_table(tbl2); 00320 if (!flag) continue; 00321 /* PreImg(p)-{p} \leq PreImg(q)-{p} */ 00322 tbl3 = AutomatonVertexGetPreImg(A->G, otherstate); 00323 tbl4 = st_init_table(st_ptrcmp, st_ptrhash); 00324 st_insert(tbl4, state, state); 00325 flag = StTableInclude(tbl3, tbl0, tbl4); 00326 st_free_table(tbl4); 00327 st_free_table(tbl3); 00328 if (!flag) continue; 00329 00330 /* ######## otherstate dominates state ####### 00331 * Remove 'state' 00332 * Notice that now we have the following data: 00333 * tbl0 = PreImg(state) 00334 * tbl1 = Img(state) 00335 */ 00336 /* Remove 'state' from Initial states */ 00337 StTableDelete(A->Init, (char *)state); 00338 /* Remove 'otherstate' if 'state' isn't in dontcare */ 00339 if (!st_is_member(A->dontcare, state)) { 00340 StTableDelete(A->dontcare, (char *)otherstate); 00341 } 00342 StTableDelete(A->dontcare, (char *)state); 00343 /* Remove 'state' from FairSets */ 00344 lsForEachItem (A->Fair, lsgen3, FairSet) { 00345 StTableDelete(FairSet, (char *)state); 00346 } 00347 /* Remove 'state' from the automaton */ 00348 g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 00349 00350 /* terminate iteration on incand list */ 00351 changed = localchanged = 1; 00352 00353 lsFinish(lsgen2); 00354 break; 00355 } 00356 lsDestroy(outcand, (void (*)(lsGeneric)) 0); 00357 00358 00359 st_free_table(tbl0); 00360 st_free_table(tbl1); 00361 00362 } 00363 lsDestroy(states, (void (*)(lsGeneric)) 0); 00364 00365 00366 return changed; 00367 } 00368 00384 int 00385 Ltl_AutomatonMinimizeByDirectSimulation( 00386 Ltl_Automaton_t *A, 00387 int verbosity) 00388 { 00389 int changed = 0; 00390 int flag = 0; 00391 00392 lsList states, otherstates, list, queue; 00393 lsGen lsgen, lsgen1; 00394 00395 edge_t *e; 00396 vertex_t *state, *otherstate; 00397 vertex_t *p, *q, *s, *t, *u, *v; 00398 LtlSet_t *set, *set2; 00399 00400 st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3; 00401 st_table *simul, *enqueued; 00402 st_generator *stgen, *stgen1, *stgen2; 00403 00404 LtlPair_t *pair, *pair2; 00405 00406 00407 /* store the simulation-relation in hash tables and queue list */ 00408 simul = st_init_table(LtlPairCompare, LtlPairHash); 00409 enqueued = st_init_table(LtlPairCompare, LtlPairHash); 00410 queue = lsCreate(); 00411 00412 /*###################################### 00413 * Initialize sim rln to all pairs (p,q) 00414 *###################################### 00415 */ 00416 states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); 00417 otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); 00418 lsForEachItem (states, lsgen, state) { 00419 lsForEachItem (otherstates, lsgen1, otherstate) { 00420 /* p != q */ 00421 if (state == otherstate) continue; 00422 /* L(p) \leq L(q) (set(Lp) > set(Lq) */ 00423 set = LtlAutomatonVertexGetLabels(state); 00424 set2 = LtlAutomatonVertexGetLabels(otherstate); 00425 if (!LtlSetInclude(set, set2)) continue; 00426 /* p \in F -> q \in F */ 00427 if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; 00428 00429 /* put (state, otherstate) into simul-relation (candidate) */ 00430 pair = LtlPairNew((char *)state, (char *)otherstate); 00431 st_insert(simul, pair, pair); 00432 st_insert(enqueued, pair, pair); 00433 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00434 } 00435 } 00436 lsDestroy(states, (void (*)(lsGeneric)) NULL); 00437 lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); 00438 00439 00440 /*###################################### 00441 * Compute the "Greatest Fixpoint" 00442 *###################################### 00443 */ 00444 while (lsDelBegin(queue, &pair) != LS_NOMORE) { 00445 st_delete(enqueued, &pair, NIL(char *)); 00446 p = (vertex_t *)pair->First; 00447 q = (vertex_t *)pair->Second; 00448 00449 /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such 00450 * that (s, t) is in simulation relation candidate list 00451 */ 00452 tbl0 = AutomatonVertexGetImg(A->G, p); 00453 tbl1 = AutomatonVertexGetImg(A->G, q); 00454 st_foreach_item(tbl0, stgen, &s, NIL(char *)) { 00455 flag = 0; 00456 st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { 00457 flag = (s==t); 00458 if (flag) { 00459 st_free_gen(stgen1); 00460 break; 00461 } 00462 pair2 = LtlPairNew((char *)s, (char *)t); 00463 flag = st_is_member(simul, pair2); 00464 LtlPairFree(pair2); 00465 if (flag) { 00466 st_free_gen(stgen1); 00467 break; 00468 } 00469 } 00470 if (!flag) { 00471 st_free_gen(stgen); 00472 break; 00473 } 00474 } 00475 st_free_table(tbl0); 00476 st_free_table(tbl1); 00477 if (flag) continue; 00478 00479 /* (p, q) is not a simulation relation */ 00480 st_delete(simul, &pair, &pair); 00481 LtlPairFree(pair); 00482 00483 /* Enqueue perturbed pairs */ 00484 tbl2 = AutomatonVertexGetPreImg(A->G, p); 00485 tbl3 = AutomatonVertexGetPreImg(A->G, q); 00486 st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { 00487 st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { 00488 pair2 = LtlPairNew((char *)u, (char *)v); 00489 if (st_lookup(simul, pair2, &pair)) { 00490 if (!st_is_member(enqueued, pair2)) { 00491 st_insert(enqueued, pair, pair); 00492 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00493 } 00494 } 00495 LtlPairFree(pair2); 00496 } 00497 } 00498 st_free_table(tbl2); 00499 st_free_table(tbl3); 00500 00501 } 00502 lsDestroy(queue, (void (*)(lsGeneric))0); 00503 st_free_table(enqueued); 00504 00505 00506 /*###################################### 00507 * Simplify by Bi-Sim equivalent states 00508 *###################################### 00509 */ 00510 /* to store removed states */ 00511 tbl1 = st_init_table(st_ptrcmp, st_ptrhash); 00512 /* so that we can modify 'simul' within for loop */ 00513 tbl0 = st_copy(simul); 00514 st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { 00515 p = (vertex_t *)pair->First; 00516 q = (vertex_t *)pair->Second; 00517 /* make sure neither has been removed */ 00518 if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) 00519 continue; 00520 /* make sure it is Bi-simulation by testing the other direction */ 00521 pair2 = LtlPairNew((char *)q, (char *)p); 00522 flag = st_lookup(simul, pair2, &pair); 00523 LtlPairFree(pair2); 00524 if (!flag) continue; 00525 00526 /*#### Direct BI-SIMULATION equivalent states####*/ 00527 /* Theorem applies */ 00528 /* remove its swap: (q, p) from simul-rln */ 00529 st_delete(simul, &pair, &pair); 00530 LtlPairFree(pair); 00531 /* Remove p, and connect its predecessors to q */ 00532 tbl2 = AutomatonVertexGetPreImg(A->G, p); 00533 tbl3 = AutomatonVertexGetPreImg(A->G, q); 00534 st_foreach_item(tbl2, stgen1, &s, NIL(char *)) { 00535 if (s == p) continue; 00536 if (!st_is_member(tbl3, (char *)s)) 00537 g_add_edge(s, q); 00538 } 00539 st_free_table(tbl2); 00540 st_free_table(tbl3); 00541 /* Update the fair sets */ 00542 lsForEachItem (A->Fair, lsgen, FairSet) { 00543 StTableDelete(FairSet, (char *)p); 00544 } 00545 /* If 'p' is in Q0, Remove 'p' and put 'q' in Q0 */ 00546 if (st_is_member(A->Init, p)) { 00547 st_delete(A->Init, &p, NIL(char *)); 00548 if (!st_is_member(A->Init, q)) 00549 st_insert(A->Init, q, q); 00550 } 00551 /* Remove 'p' from dontcare (if it's in it ) */ 00552 StTableDelete(A->dontcare, (char *)p); 00553 00554 /* Remove 'p' from the automaton */ 00555 st_insert(tbl1, p, p); 00556 g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 00557 changed = 1; 00558 } 00559 st_free_table(tbl0); 00560 00561 00562 /*###################################### 00563 * Remove arcs to direct-simulated states 00564 *###################################### 00565 */ 00566 /* so that we can modify simul with the for loop */ 00567 tbl0 = st_copy(simul); 00568 st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { 00569 /* 'p' is simulated by 'q' */ 00570 p = (vertex_t *)pair->First; 00571 q = (vertex_t *)pair->Second; 00572 /* Make sure neither hasn't been removed yet */ 00573 if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) 00574 continue; 00575 00576 /*#### p is direct-simulated by q####*/ 00577 /* Theorem applies */ 00578 /* Drop arcs from their common predecessors to p */ 00579 tbl3 = AutomatonVertexGetPreImg(A->G, q); 00580 list = lsCopy(g_get_in_edges(p), (lsGeneric (*)(lsGeneric)) NULL); 00581 lsForEachItem (list, lsgen, e) { 00582 if (!st_is_member(tbl3, g_e_source(e))) continue; 00583 g_delete_edge(e, (void (*)(gGeneric))0); 00584 changed = 1; 00585 } 00586 lsDestroy(list, (void (*)(lsGeneric)) 0); 00587 st_free_table(tbl3); 00588 /* Remove 'p' from Q0 if 'q' is in Q0 */ 00589 if (st_is_member(A->Init, q)) { 00590 StTableDelete(A->Init, (char *)p); 00591 changed = 1; 00592 } 00593 00594 } 00595 st_free_table (tbl0); 00596 00597 st_free_table (tbl1); 00598 00599 st_foreach_item(simul, stgen, &pair, NIL(char *)) { 00600 LtlPairFree(pair); 00601 } 00602 st_free_table (simul); 00603 00604 return changed; 00605 } 00606 00607 00619 void 00620 Ltl_AutomatonAddFairStates( 00621 Ltl_Automaton_t *A) 00622 { 00623 00624 long isFair; 00625 00626 lsGen lsgen1; 00627 00628 st_generator *stgen, *stgen2; 00629 st_table *FairSet, *Class; 00630 00631 Ltl_AutomatonComputeSCC(A, 1); 00632 if (A->Q) { 00633 Ltl_AutomatonFree((gGeneric) A->Q); 00634 A->Q = NIL(Ltl_Automaton_t); 00635 } 00636 A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); 00637 /* 00638 Mark trivial SCCs as Fair states 00639 */ 00640 st_foreach_item(A->SCC, stgen, &Class, &isFair) { 00641 vertex_t *state; 00642 00643 if (isFair == 2) { /* trivial SCC */ 00644 lsForEachItem (A->Fair, lsgen1, FairSet) { 00645 st_foreach_item(Class, stgen2, &state, NIL(char *)) { 00646 if (!st_is_member(FairSet, state)) { 00647 if (st_is_member(A->dontcare, state)){ 00648 StTableDelete(A->dontcare, (char *)state); 00649 } 00650 st_insert(FairSet, state, state); 00651 } 00652 } 00653 } 00654 } 00655 } 00656 } 00657 00658 00674 int 00675 Ltl_AutomatonMaximizeByDirectSimulation( 00676 Ltl_Automaton_t *A, 00677 int verbosity) 00678 { 00679 int changed = 0; 00680 int flag = 0; 00681 00682 lsList states, otherstates, queue; 00683 lsGen lsgen, lsgen1; 00684 00685 vertex_t *state, *otherstate; 00686 vertex_t *p, *q, *s, *t, *u, *v; 00687 LtlSet_t *set, *set2; 00688 00689 st_table *tbl0, *tbl1, *tbl2, *tbl3; 00690 st_table *simul, *enqueued; 00691 st_generator *stgen, *stgen1, *stgen2; 00692 00693 LtlPair_t *pair, *pair2; 00694 00695 /* 00696 Ltl_AutomatonAddFairStates(A); 00697 */ 00698 /* store the simulation-relation in hash tables and queue list */ 00699 simul = st_init_table(LtlPairCompare, LtlPairHash); 00700 enqueued = st_init_table(LtlPairCompare, LtlPairHash); 00701 queue = lsCreate(); 00702 00703 /*###################################### 00704 * Initialize sim rln to all pairs (p,q) 00705 *###################################### 00706 */ 00707 states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); 00708 otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); 00709 lsForEachItem (states, lsgen, state) { 00710 lsForEachItem (otherstates, lsgen1, otherstate) { 00711 /* p != q */ 00712 if (state == otherstate) continue; 00713 /* L(p) \leq L(q) (set(Lp) > set(Lq) */ 00714 set = LtlAutomatonVertexGetLabels(state); 00715 set2 = LtlAutomatonVertexGetLabels(otherstate); 00716 if (!LtlSetInclude(set, set2)) continue; 00717 /* p \in F -> q \in F */ 00718 if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; 00719 00720 /* put (state, otherstate) into simul-relation (candidate) */ 00721 pair = LtlPairNew((char *)state, (char *)otherstate); 00722 st_insert(simul, pair, pair); 00723 st_insert(enqueued, pair, pair); 00724 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00725 } 00726 } 00727 lsDestroy(states, (void (*)(lsGeneric)) NULL); 00728 lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); 00729 00730 00731 /*###################################### 00732 * Compute the "Greatest Fixpoint" 00733 *###################################### 00734 */ 00735 while (lsDelBegin(queue, &pair) != LS_NOMORE) { 00736 st_delete(enqueued, &pair, NIL(char *)); 00737 p = (vertex_t *)pair->First; 00738 q = (vertex_t *)pair->Second; 00739 00740 /* Check for each 's' in Img(p), if there exists a 't' in Img(q) such 00741 * that (s, t) is in simulation relation candidate list 00742 */ 00743 tbl0 = AutomatonVertexGetImg(A->G, p); 00744 tbl1 = AutomatonVertexGetImg(A->G, q); 00745 st_foreach_item(tbl0, stgen, &s, NIL(char *)) { 00746 flag = 0; 00747 st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { 00748 flag = (s==t); 00749 if (flag) { 00750 st_free_gen(stgen1); 00751 break; 00752 } 00753 pair2 = LtlPairNew((char *)s, (char *)t); 00754 flag = st_is_member(simul, pair2); 00755 LtlPairFree(pair2); 00756 if (flag) { 00757 st_free_gen(stgen1); 00758 break; 00759 } 00760 } 00761 if (!flag) { 00762 st_free_gen(stgen); 00763 break; 00764 } 00765 } 00766 st_free_table(tbl0); 00767 st_free_table(tbl1); 00768 if (flag) continue; 00769 00770 /* (p, q) is not a simulation relation */ 00771 st_delete(simul, &pair, &pair); 00772 LtlPairFree(pair); 00773 00774 /* Enqueue perturbed pairs */ 00775 tbl2 = AutomatonVertexGetPreImg(A->G, p); 00776 tbl3 = AutomatonVertexGetPreImg(A->G, q); 00777 st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { 00778 st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { 00779 pair2 = LtlPairNew((char *)u, (char *)v); 00780 if (st_lookup(simul, pair2, &pair)) { 00781 if (!st_is_member(enqueued, pair2)) { 00782 st_insert(enqueued, pair, pair); 00783 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00784 } 00785 } 00786 LtlPairFree(pair2); 00787 } 00788 } 00789 st_free_table(tbl2); 00790 st_free_table(tbl3); 00791 00792 } 00793 lsDestroy(queue, (void (*)(lsGeneric))0); 00794 st_free_table(enqueued); 00795 00796 00797 /*###################################### 00798 * Add arcs to direct-simulated states 00799 *###################################### 00800 */ 00801 00802 /* so that we can modify simul with the for-loop */ 00803 tbl0 = st_copy(simul); 00804 st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { 00805 /* 'p' is simulated by 'q' */ 00806 p = (vertex_t *)pair->First; 00807 q = (vertex_t *)pair->Second; 00808 /* 00809 Add arcs from the predecessors of q to p 00810 */ 00811 tbl2 = AutomatonVertexGetPreImg(A->G, p); 00812 tbl3 = AutomatonVertexGetPreImg(A->G, q); 00813 st_foreach_item(tbl3, stgen1, &s, NIL(char *)) { 00814 if (!st_is_member(tbl2, s)){ 00815 g_add_edge(s, p); 00816 changed = 1; 00817 } 00818 } 00819 st_free_table(tbl2); 00820 st_free_table(tbl3); 00821 } 00822 st_free_table (tbl0); 00823 00824 st_foreach_item(simul, stgen, &pair, NIL(char *)) { 00825 LtlPairFree(pair); 00826 } 00827 st_free_table (simul); 00828 00829 return changed; 00830 } 00831 00832 00848 int 00849 Ltl_AutomatonMinimizeByReverseSimulation( 00850 Ltl_Automaton_t *A, 00851 int verbosity) 00852 { 00853 int changed = 0; 00854 int flag = 0; 00855 00856 lsList states, otherstates, list, queue; 00857 lsGen lsgen, lsgen1; 00858 00859 edge_t *e; 00860 vertex_t *state, *otherstate; 00861 vertex_t *p, *q, *s, *t, *u, *v; 00862 LtlSet_t *set, *set2; 00863 00864 st_table *FairSet, *tbl0, *tbl1, *tbl2, *tbl3; 00865 st_table *simul, *enqueued; 00866 st_generator *stgen, *stgen1, *stgen2; 00867 00868 LtlPair_t *pair, *pair2; 00869 00870 00871 /* store the simulation-relation in hash tables and queue list */ 00872 simul = st_init_table(LtlPairCompare, LtlPairHash); 00873 enqueued = st_init_table(LtlPairCompare, LtlPairHash); 00874 queue = lsCreate(); 00875 00876 /*###################################### 00877 * Initialize sim rln to all pairs (p,q) 00878 *###################################### 00879 */ 00880 states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); 00881 otherstates = lsCopy(states, (lsGeneric (*)(lsGeneric)) NULL); 00882 lsForEachItem (states, lsgen, state) { 00883 lsForEachItem (otherstates, lsgen1, otherstate) { 00884 /* p != q */ 00885 if (state == otherstate) continue; 00886 /* L(p) <= L(q), in other words, (set(Lp) >= set(Lq) */ 00887 set = LtlAutomatonVertexGetLabels(state); 00888 set2 = LtlAutomatonVertexGetLabels(otherstate); 00889 if (!LtlSetInclude(set, set2)) continue; 00890 /* p is in Q0 -> q is in Q0 */ 00891 if (st_is_member(A->Init, state) && 00892 !st_is_member(A->Init, otherstate)) 00893 continue; 00894 /* p is in F -> q is in F */ 00895 if (!AutomatonPfairImplyQfair(A, state, otherstate)) continue; 00896 00897 /* put (state, otherstate) into simul-relation */ 00898 pair = LtlPairNew((char *)state, (char *)otherstate); 00899 st_insert(simul, pair, pair); 00900 st_insert(enqueued, pair, pair); 00901 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00902 } 00903 } 00904 lsDestroy(states, (void (*)(lsGeneric)) NULL); 00905 lsDestroy(otherstates, (void (*)(lsGeneric)) NULL); 00906 00907 00908 /*###################################### 00909 * Compute the "Greatest Fixpoint" 00910 *###################################### 00911 */ 00912 while (lsDelBegin(queue, &pair) != LS_NOMORE) { 00913 st_delete(enqueued, &pair, NIL(char *)); 00914 p = (vertex_t *)pair->First; 00915 q = (vertex_t *)pair->Second; 00916 00917 /* For each 's' in Img(p), there must exists a 't' Img(q) such that 00918 * (s, t) is also a reverse simulation pair 00919 */ 00920 tbl0 = AutomatonVertexGetPreImg(A->G, p); 00921 tbl1 = AutomatonVertexGetPreImg(A->G, q); 00922 st_foreach_item(tbl0, stgen, &s, NIL(char *)) { 00923 flag = 0; 00924 st_foreach_item(tbl1, stgen1, &t, NIL(char *)) { 00925 flag = (s==t); 00926 if (flag) { 00927 st_free_gen(stgen1); 00928 break; 00929 } 00930 pair2 = LtlPairNew((char *)s, (char *)t); 00931 flag = st_is_member(simul, pair2); 00932 LtlPairFree(pair2); 00933 if (flag) { 00934 st_free_gen(stgen1); 00935 break; 00936 } 00937 } 00938 if (!flag) { 00939 st_free_gen(stgen); 00940 break; 00941 } 00942 } 00943 st_free_table(tbl0); 00944 st_free_table(tbl1); 00945 00946 if (flag) continue; 00947 00948 /* (p, q) is not a simulation relation */ 00949 st_delete(simul, &pair, &pair); 00950 LtlPairFree(pair); 00951 00952 /* Enqueue perturbed pairs */ 00953 tbl2 = AutomatonVertexGetImg(A->G, p); 00954 tbl3 = AutomatonVertexGetImg(A->G, q); 00955 st_foreach_item(tbl2, stgen1, &u, NIL(char *)) { 00956 st_foreach_item(tbl3, stgen2, &v, NIL(char *)) { 00957 pair2 = LtlPairNew((char *)u, (char *)v); 00958 if (st_lookup(simul, pair2, &pair)) 00959 if(!st_is_member(enqueued, pair2)) { 00960 st_insert(enqueued, pair, pair); 00961 lsNewEnd(queue, (lsGeneric)pair, NIL(lsHandle)); 00962 } 00963 LtlPairFree(pair2); 00964 } 00965 } 00966 st_free_table(tbl2); 00967 st_free_table(tbl3); 00968 } 00969 lsDestroy(queue, (void (*)(lsGeneric))0); 00970 st_free_table(enqueued); 00971 00972 00973 /*###################################### 00974 * Simplify by Bi-Sim equivalent states 00975 *###################################### 00976 */ 00977 /* to store removed states */ 00978 tbl1 = st_init_table(st_ptrcmp, st_ptrhash); 00979 /* so that we can modify simul with the for loop */ 00980 tbl0 = st_copy(simul); 00981 st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { 00982 p = (vertex_t *)pair->First; 00983 q = (vertex_t *)pair->Second; 00984 /* Make sure neither has been removed */ 00985 if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) 00986 continue; 00987 /* Make sure it is Bi-simulation by checking the other direction*/ 00988 pair2 = LtlPairNew((char *)q, (char *)p); 00989 flag = st_lookup(simul, pair2, &pair); 00990 LtlPairFree(pair2); 00991 if (!flag) continue; 00992 00993 /*#### Direct BI-SIMULATION equivalent states####*/ 00994 /* Theorem applies */ 00995 /* Remove its swap: (q, p) from simul-rln */ 00996 st_delete(simul, &pair, &pair); 00997 LtlPairFree(pair); 00998 /* Remove 'p' and connect 'q' to all its successors */ 00999 tbl2 = AutomatonVertexGetImg(A->G, p); 01000 tbl3 = AutomatonVertexGetImg(A->G, q); 01001 st_foreach_item(tbl2, stgen1, &s, NIL(char *)) { 01002 if (s == p) continue; 01003 if (!st_is_member(tbl3, s)) 01004 g_add_edge(q, s); 01005 } 01006 st_free_table(tbl2); 01007 st_free_table(tbl3); 01008 /* Update the fairsets (remove 'p') */ 01009 lsForEachItem (A->Fair, lsgen, FairSet) { 01010 StTableDelete(FairSet, (char *)p); 01011 } 01012 /* Remove 'p' from Q0 */ 01013 StTableDelete(A->Init, (char *)p); 01014 /* Remove 'p' form dontcare if it's in it */ 01015 StTableDelete(A->dontcare, (char *)p); 01016 01017 /* Remove 'p' from the automaton */ 01018 st_insert(tbl1, p, p); 01019 g_delete_vertex(p, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 01020 changed = 1; 01021 } 01022 st_free_table(tbl0); 01023 01024 01025 /*###################################### 01026 * Remove arcs from Reverse-simulated states 01027 *#####################################*/ 01028 /* so that we can modify simul with the for loop */ 01029 tbl0 = st_copy(simul); 01030 st_foreach_item (tbl0, stgen, &pair, NIL(char *)) { 01031 /* 'p' is simulated by 'q' */ 01032 p = (vertex_t *)pair->First; 01033 q = (vertex_t *)pair->Second; 01034 /* Make sure that neither has been removed */ 01035 if (st_is_member(tbl1, p) || st_is_member(tbl1, q)) 01036 continue; 01037 01038 /*#### p is reverse-simulated by q####*/ 01039 /* Theorem applies */ 01040 /* Drop arcs from 'p' to their common successors */ 01041 tbl3 = AutomatonVertexGetImg(A->G, q); 01042 list = lsCopy(g_get_out_edges(p), (lsGeneric (*)(lsGeneric)) NULL); 01043 lsForEachItem (list, lsgen, e) { 01044 if (!st_is_member(tbl3, g_e_dest(e))) continue; 01045 g_delete_edge(e, (void (*)(gGeneric))0); 01046 changed = 1; 01047 } 01048 lsDestroy(list, (void (*)(lsGeneric)) 0); 01049 st_free_table(tbl3); 01050 } 01051 st_free_table (tbl0); 01052 01053 st_free_table (tbl1); 01054 01055 st_foreach_item(simul, stgen, &pair, NIL(char *)) { 01056 LtlPairFree(pair); 01057 } 01058 st_free_table (simul); 01059 01060 return changed; 01061 } 01062 01063 01082 int 01083 Ltl_AutomatonMinimizeByPrune( 01084 Ltl_Automaton_t *A, 01085 int verbosity) 01086 { 01087 st_generator *stgen, *stgen1, *stgen2; 01088 st_table *FairSet, *otherset, *Class, *scc, *rest; 01089 st_table *tbl, *tbl1, *tbl2; 01090 lsList states, list; 01091 lsGen lsgen, lsgen1; 01092 vertex_t *state, *s, *greatest, *qstate; 01093 edge_t *e; 01094 long isFair; 01095 int flag, totalnum, procnum; 01096 01097 /* Eliminate redundant edges from the predecessors of universal states. 01098 * (A universal state is a state labeled 'TRUE' with a self-loop, and it 01099 * should belong to all FairSets) 01100 */ 01101 states = lsCopy(g_get_vertices(A->G), (lsGeneric (*)(lsGeneric)) NULL); 01102 lsForEachItem (states, lsgen, state) { 01103 /* label = TRUE */ 01104 if (LtlSetCardinality(LtlAutomatonVertexGetLabels(state)) != 0) 01105 continue; 01106 /* self-loop */ 01107 if (!AutomatonVertexHasSelfLoop(A->G, state)) continue; 01108 /* blongs to all fairSet */ 01109 flag = 1; 01110 lsForEachItem (A->Fair, lsgen1, FairSet) { 01111 if (!st_is_member(FairSet, state)) { 01112 flag = 0; 01113 lsFinish(lsgen1); 01114 break; 01115 } 01116 } 01117 if (!flag) continue; 01118 /* We can apply the theorem: Remove edges from its predecessors to 01119 * other siblings 01120 */ 01121 tbl = AutomatonVertexGetPreImg(A->G, state); 01122 st_foreach_item(tbl, stgen, &s, NIL(char *)) { 01123 if (s == state) continue; 01124 list = lsCopy(g_get_out_edges(s), (lsGeneric (*)(lsGeneric))0); 01125 lsForEachItem(list, lsgen1, e) { 01126 if (g_e_dest(e) != state) 01127 g_delete_edge(e, (void (*)(gGeneric))0); 01128 } 01129 lsDestroy(list, (void (*)(lsGeneric))0); 01130 } 01131 st_free_table(tbl); 01132 } 01133 01134 01135 /*2) Compute all the SCCs, and build the SCC-quotient graph 01136 * every time before pruning, we need to re-compute the SCC graph 01137 */ 01138 Ltl_AutomatonComputeSCC(A, 1); 01139 if (A->Q) { 01140 Ltl_AutomatonFree((gGeneric) A->Q); 01141 A->Q = NIL(Ltl_Automaton_t); 01142 } 01143 A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); 01144 01145 /* Mark those states without loop going through as "don't care states" */ 01146 st_foreach_item(A->SCC, stgen, &Class, &isFair) { 01147 if (isFair == 2) 01148 StTableAppend(A->dontcare, Class); 01149 } 01150 01151 /* Restrict automaton to those states that can reach a fair SCC 01152 * There are two cases: (a) with fairness (b) without fairness 01153 */ 01154 lsFirstItem(A->Q->Fair, &FairSet, NIL(lsHandle)); 01155 if (lsLength(A->Fair) > 0) { 01156 /* (a) */ 01157 tbl = st_init_table(st_ptrcmp, st_ptrhash); 01158 /* Find states that are on fair cycles */ 01159 st_foreach_item(FairSet, stgen, &qstate, NIL(char *)) { 01160 Class = AutomatonQuotientVertexGetClass(qstate); 01161 StTableAppend(tbl, Class); 01162 } 01163 /* Shrink fair sets in A->Fair */ 01164 lsForEachItem (A->Fair, lsgen, FairSet) { 01165 StTableRestrict(FairSet, tbl); 01166 } 01167 /* Find states that can reach fair cycles */ 01168 tbl1 = tbl; 01169 tbl = g_EF(A->G, tbl); 01170 st_free_table(tbl1); 01171 /* Remove the rest part of A->G */ 01172 StTableRestrict(A->Init, tbl); 01173 StTableRestrict(A->dontcare, tbl); 01174 lsForEachItem (states, lsgen, state) { 01175 if (!st_is_member(tbl, state)) 01176 g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 01177 } 01178 }else { 01179 /* (b) */ 01180 /* Find all the reachable state */ 01181 tbl = g_reachable(A->G, A->Init); 01182 /* Remove the rest part of A->G */ 01183 StTableRestrict(A->Init, tbl); 01184 StTableRestrict(A->dontcare, tbl); 01185 lsForEachItem (states, lsgen, state) { 01186 if (!st_is_member(tbl, state)) 01187 g_delete_vertex(state, Ltl_AutomatonNodeFree, (void(*)(gGeneric))0); 01188 } 01189 } 01190 /* Clean up the Quotient graph */ 01191 st_foreach_item(A->SCC, stgen, &Class, &isFair) { 01192 StTableRestrict(Class, tbl); 01193 } 01194 st_free_table(tbl); 01195 01196 01197 /* 3. Remove duplicate FairSet */ 01198 /* Discard duplicate fair sets and fair sets including all states. Here we 01199 * also restrict fair sets by analyzing each SCC. If within an SCC, one fair 01200 * set dominates another, it can be restricted to the dominated one. As a 01201 * special case: if an SCC does not intersect all fair sets, its states are 01202 * removed from all fair sets. 01203 */ 01204 totalnum = lsLength(A->Fair); 01205 procnum = 0; 01206 while(lsDelBegin(A->Fair, &FairSet) != LS_NOMORE) { 01207 /* Remove this FairSet if it includes all states in the SCC */ 01208 if (st_count(FairSet) == lsLength(g_get_vertices(A->G))) { 01209 st_free_table(FairSet); 01210 totalnum--; 01211 }else { 01212 /* After restricted to the SCC: if fair set2 is contained in set1, 01213 * shrink set1 to set2 (remove (set1-set2) from set1 01214 */ 01215 st_foreach_item(A->SCC, stgen, &scc, &isFair) { 01216 lsForEachItem(A->Fair, lsgen, otherset) { 01217 tbl1 = st_copy(scc); 01218 tbl2 = st_copy(scc); 01219 StTableRestrict(tbl1, FairSet); 01220 StTableRestrict(tbl2, otherset); 01221 if (StTableInclude(tbl1, tbl2, NIL(st_table))) { 01222 /* tbl1 <= (tbl1 - tbl2) */ 01223 StTableSubtract(tbl1, tbl2); 01224 StTableSubtract(FairSet, tbl1); 01225 } 01226 st_free_table(tbl1); 01227 st_free_table(tbl2); 01228 } 01229 } 01230 /* Remove the fair set if another fair set is contained in it */ 01231 flag = 1; 01232 lsForEachItem(A->Fair, lsgen, otherset) { 01233 if (StTableInclude(FairSet,otherset,NIL(st_table))) { 01234 flag = 0; 01235 lsFinish(lsgen); 01236 break; 01237 } 01238 } 01239 if (!flag) { 01240 st_free_table(FairSet); 01241 totalnum--; 01242 }else 01243 lsNewEnd(A->Fair, (lsGeneric) FairSet, NIL(lsHandle)); 01244 } 01245 procnum++; 01246 if (procnum > totalnum) break; 01247 } 01248 01249 /* 4. GLB reduction */ 01250 /* If an SCC is a clique, and there is a state 's' whose label exactly matches 01251 * the GLB of all the labels of the clique, we can remove 's' from every fair 01252 * set such that it contains at least another state of the SCC besides 's' 01253 */ 01254 st_foreach_item(A->SCC, stgen, &Class, &isFair) { 01255 /* 1-state SCC won't work */ 01256 if (st_count(Class) <= 1) continue; 01257 /* must be a clique */ 01258 if (!AutomatonPartitionIsClique(A->G, Class)) continue; 01259 tbl = AutomatonPartitionLabelGLB(Class, A->labelTableNegate); 01260 if (!tbl) continue; 01261 rest = st_copy(Class); 01262 StTableSubtract(rest, tbl); 01263 lsForEachItem(A->Fair, lsgen, FairSet) { 01264 if (StTableInclude(FairSet, tbl, NIL(st_table)) && 01265 !StTableIsDisjoint(FairSet, rest, NIL(st_table))) 01266 /* we apply the theorem here */ 01267 StTableSubtract(FairSet, tbl); 01268 } 01269 st_free_table(rest); 01270 st_free_table(tbl); 01271 } 01272 01273 /* 5. LUB reduction */ 01274 /* If an SCC contains a state 's' that simulates all the other states in the 01275 * same SCC (both forward and backward), then all states of the SCC except 01276 * 's' can be removed from all fair sets. The following code checks for a 01277 * special case of this theorem 01278 */ 01279 st_foreach_item(A->SCC, stgen, &Class, &isFair) { 01280 vertex_t *qstate; 01281 st_lookup(A->Q->SCC, Class, &qstate); 01282 /* 1-state SCC won't work */ 01283 if (st_count(Class) <= 1) continue; 01284 tbl = AutomatonPartitionLabelLUB(Class, A->labelTableNegate); 01285 if (!tbl) continue; 01286 st_foreach_item(tbl, stgen1, &greatest, NIL(char *)) { 01287 /* that state should have a self-loop */ 01288 if (!AutomatonVertexHasSelfLoop(A->G, greatest)) continue; 01289 /* that state should be initial if the SCC contains initial states */ 01290 if (st_is_member(A->Q->Init, qstate) && 01291 !st_is_member(A->Init, greatest)) 01292 continue; 01293 /* that state should belong to FairSet if the SCC intersect it */ 01294 flag = 1; 01295 lsForEachItem(A->Fair, lsgen, FairSet) { 01296 if (!st_is_member(FairSet, greatest) && 01297 !StTableIsDisjoint(FairSet,Class,NIL(st_table))){ 01298 flag = 0; 01299 lsFinish(lsgen); 01300 break; 01301 } 01302 } 01303 if (!flag) continue; 01304 /* Every state outside of the SCC with a transition into the SCC 01305 * should also have a transition to that state 01306 */ 01307 tbl1 = st_init_table(st_ptrcmp, st_ptrhash); 01308 st_foreach_item(Class, stgen2, &state, NIL(char *)) { 01309 tbl2 = AutomatonVertexGetPreImg(A->G, state); 01310 StTableAppend(tbl1, tbl2); 01311 st_free_table(tbl2); 01312 } 01313 tbl2 = AutomatonVertexGetPreImg(A->G, greatest); 01314 flag = StTableInclude(tbl2, tbl1, Class); 01315 st_free_table(tbl2); 01316 st_free_table(tbl1); 01317 if (!flag) continue; 01318 01319 /* we now apply the theorem */ 01320 tbl1 = st_copy(Class); 01321 if (st_is_member(tbl1, greatest)) 01322 st_delete(tbl1, &greatest, NIL(char *)); 01323 lsForEachItem(A->Fair, lsgen, FairSet) { 01324 StTableSubtract(FairSet, tbl1); 01325 } 01326 st_free_table(tbl1); 01327 } 01328 st_free_table(tbl); 01329 } 01330 01331 01332 lsDestroy(states, (void (*)(lsGeneric))0); 01333 01334 return 1; 01335 } 01336 01337 01338 01339 01356 void 01357 Ltl_AutomatonComputeSCC( 01358 Ltl_Automaton_t *A, 01359 int force) 01360 { 01361 st_generator *stgen; 01362 st_table *component; 01363 01364 /* compute A->SCC if not exist */ 01365 if (!force && A->SCC) 01366 return; 01367 01368 if (force && A->SCC) { 01369 st_foreach_item(A->SCC, stgen, &component, NIL(char *)) { 01370 st_free_table(component); 01371 } 01372 st_free_table(A->SCC); 01373 } 01374 01375 A->SCC = g_SCC(A->G, A->Init); 01376 01377 return; 01378 } 01379 01394 int 01395 Ltl_AutomatonIsWeak( 01396 Ltl_Automaton_t *A) 01397 { 01398 int weak; 01399 long isFair; 01400 st_generator *stgen; 01401 st_table *scc, *FairSet; 01402 lsGen lsgen; 01403 01404 /* A SCC without fairness constraint is WEAK */ 01405 if (lsLength(A->Fair) == 0) 01406 return 1; 01407 01408 /* compute the partition(A->SCC) and Quotient graph(A->Q) if not exist */ 01409 if (!A->SCC) 01410 Ltl_AutomatonComputeSCC(A,0); 01411 if (!A->Q) 01412 A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); 01413 01414 /* weak: for each SCC, 01415 * either it's included in all FairSets 01416 * or it intersects none of them 01417 */ 01418 weak = 1; 01419 st_foreach_item(A->SCC, stgen, &scc, &isFair) { 01420 int flag = 0; 01421 /* intersect none of them ? */ 01422 lsForEachItem (A->Fair, lsgen, FairSet) { 01423 if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) { 01424 lsFinish(lsgen); 01425 flag = 1; 01426 break; 01427 } 01428 } 01429 if (!flag) continue; 01430 01431 /* included in all of them ? */ 01432 lsForEachItem (A->Fair, lsgen, FairSet) { 01433 if (!StTableInclude(FairSet, scc, NIL(st_table))) { 01434 weak = 0; 01435 lsFinish(lsgen); 01436 break; 01437 } 01438 } 01439 01440 if (!weak) { 01441 st_free_gen(stgen); 01442 break; 01443 } 01444 } 01445 01446 return weak; 01447 } 01448 01460 Mc_AutStrength_t 01461 Ltl_AutomatonGetStrength( 01462 Ltl_Automaton_t *A) 01463 { 01464 Mc_AutStrength_t result; 01465 vertex_t *qstate, *state, *state2; 01466 st_generator *stgen, *stgen1, *stgen2; 01467 st_table *tbl, *FairSet, *scc; 01468 lsList cover; 01469 lsGen lsgen; 01470 01471 /* Every time we need to re-compute the partition(A->SCC) and 01472 * the Quotient graph(A->Q) 01473 */ 01474 Ltl_AutomatonComputeSCC(A, 1); 01475 if (A->Q) { 01476 Ltl_AutomatonFree((gGeneric) A->Q); 01477 A->Q = NIL(Ltl_Automaton_t); 01478 } 01479 A->Q = Ltl_AutomatonCreateQuotient(A, A->SCC); 01480 01481 /* is it strong ? */ 01482 if (!Ltl_AutomatonIsWeak(A)) 01483 return Mc_Aut_Strong_c /*2*/; 01484 01485 /* it's terminal (0) if all the weak SCCs are COMPLETE and FINAL.*/ 01486 result = Mc_Aut_Terminal_c; 01487 st_foreach_item(A->SCC, stgen, &scc, NIL(char *)) { 01488 int disjoint_flag = 1; 01489 int final_flag = 1; 01490 int complete_flag = 1; 01491 01492 /* if it does not intersect any fair set, we don't care about it */ 01493 if (lsLength(A->Fair) == 0) 01494 disjoint_flag = 0; 01495 else { 01496 lsForEachItem(A->Fair, lsgen, FairSet) { 01497 if (!StTableIsDisjoint(FairSet, scc, NIL(st_table))) { 01498 disjoint_flag = 0; 01499 lsFinish(lsgen); 01500 break; 01501 } 01502 } 01503 } 01504 if (disjoint_flag) continue; 01505 01506 /* FINAL: 01507 * it shouldn't be trivial, and shouldn't have edge to other sccs 01508 */ 01509 st_lookup(A->Q->SCC, scc, &qstate); 01510 tbl = AutomatonVertexGetImg(A->Q->G, qstate); 01511 final_flag = (st_count(tbl) == 1 && st_is_member(tbl, qstate)); 01512 st_free_table(tbl); 01513 if (!final_flag) { 01514 st_free_gen(stgen); 01515 result = Mc_Aut_Weak_c; /* weak */ 01516 break; 01517 } 01518 01519 /* COMPLETE: 01520 * for each state in the SCC: the union of the labels in all 01521 * its successors is tautology 01522 */ 01523 st_foreach_item(scc, stgen1, &state, NIL(char *)) { 01524 tbl = AutomatonVertexGetImg(A->G, state); 01525 cover = lsCreate(); 01526 st_foreach_item(tbl, stgen2, &state2, NIL(char *)) { 01527 lsNewEnd(cover, (lsGeneric)LtlAutomatonVertexGetLabels(state2), 01528 NIL(lsHandle)); 01529 } 01530 st_free_table(tbl); 01531 complete_flag = LtlCoverIsTautology(cover, A->labelTableNegate); 01532 lsDestroy(cover, (void (*)(lsGeneric))0); 01533 if (!complete_flag) { 01534 st_free_gen(stgen1); 01535 break; 01536 } 01537 } 01538 if (!complete_flag) { 01539 st_free_gen(stgen); 01540 result = Mc_Aut_Weak_c; /* weak */ 01541 break; 01542 } 01543 } 01544 01545 /* Weak = 1; Terminal = 0 */ 01546 return result; 01547 } 01548 01578 Ltl_Automaton_t * 01579 Ltl_AutomatonCreateQuotient( 01580 Ltl_Automaton_t *A, 01581 st_table *partition) 01582 { 01583 long isFair; 01584 int flag; 01585 st_generator *stgen, *stgen1; 01586 st_table *Class, *FairSet; 01587 lsGen lsgen; 01588 01589 st_table *Avtx2Qvtx, *Class2Qvtx, *EdgeUtable; 01590 Ltl_Automaton_t *Q; 01591 Ltl_AutomatonNode_t *node; 01592 vertex_t *q, *p; 01593 edge_t *e; 01594 LtlPair_t *pair; 01595 01596 /* create the Q graph as a Automaton */ 01597 Q = Ltl_AutomatonCreate(); 01598 Q->isQuotientGraph = 1; 01599 01600 /*### for each class, add vtx in Q->G ###*/ 01601 /* hash tables : (vtx in A, vtx in Q), (class_st_table, vtx in Q) */ 01602 Avtx2Qvtx = st_init_table(st_ptrcmp, st_ptrhash); 01603 Class2Qvtx = st_init_table(st_ptrcmp, st_ptrhash); 01604 st_foreach_item(partition, stgen, &Class, NIL(char *)) { 01605 /* add 'q' in Q->G */ 01606 q = g_add_vertex(Q->G); 01607 node = Ltl_AutomatonNodeCreate(Q); 01608 node->Class = Class; 01609 q->user_data = (gGeneric) node; 01610 st_insert(Class2Qvtx, Class, q); 01611 /* hash table (A_vtx -> Q_vtx) */ 01612 flag = 0; 01613 st_foreach_item(Class, stgen1, &p, NIL(char *)) { 01614 st_insert(Avtx2Qvtx, p, q); 01615 if (st_is_member(A->Init, p)) 01616 flag = 1; 01617 } 01618 /* if any state in class is in A->Init, put class into Q->Init */ 01619 if (flag) 01620 st_insert(Q->Init, q, q); 01621 } 01622 01623 01624 /*### for each (class, class2), add edges ###*/ 01625 /* edge unique table in Q graph, key = (class, class2) */ 01626 EdgeUtable = st_init_table(LtlPairCompare, LtlPairHash); 01627 pair = LtlPairNew(0,0); 01628 foreach_edge(A->G, lsgen, e) { 01629 if (!st_lookup(Avtx2Qvtx, g_e_source(e), &pair->First)) 01630 continue; 01631 if (!st_lookup(Avtx2Qvtx, g_e_dest(e), &pair->Second)) 01632 continue; 01633 /* only consider reachable states in A->G */ 01634 if (!st_is_member(EdgeUtable, pair)) { 01635 LtlPair_t *tmpPair = LtlPairNew(pair->First, pair->Second); 01636 st_insert(EdgeUtable, tmpPair, tmpPair); 01637 g_add_edge((vertex_t *)pair->First, (vertex_t *)pair->Second); 01638 } 01639 } 01640 01641 /*### put fair sccs into the only FairSet ###*/ 01642 /* isFair = 1 (fair SCC); isFair = 0 (non-trivial non-fair SCC); 01643 * isFair = 2 (dontcare: trivial SCC, obviously non-fair)*/ 01644 FairSet = st_init_table(st_ptrcmp, st_ptrhash); 01645 st_foreach_item(partition, stgen, &Class, &isFair) { 01646 st_insert(partition, Class, (char *)0); 01647 01648 /* it should be a nontrivial scc (size >1 or have self-loop) */ 01649 if (st_count(Class)==1) { 01650 st_lookup(Class2Qvtx, Class, &pair->First); 01651 st_lookup(Class2Qvtx, Class, &pair->Second); 01652 if (!st_is_member(EdgeUtable, pair)) { 01653 /*trivial scc (1 state without self-loop) */ 01654 st_insert(partition, Class, (char *)2); 01655 continue; 01656 } 01657 } 01658 /* for non trivial SCC, check if it intersect all FairSets */ 01659 if (!StTableIsFair(A->Fair, Class)) continue; 01660 /* it's a "fair SCC" */ 01661 st_insert(partition, Class, (char *)1); 01662 01663 st_lookup(Class2Qvtx, Class, &pair->First); 01664 st_insert(FairSet, pair->First, pair->First); 01665 } 01666 lsNewEnd(Q->Fair, (lsGeneric) FairSet, (lsHandle *) 0); 01667 01668 /* free */ 01669 LtlPairFree(pair); 01670 st_foreach_item(EdgeUtable, stgen, &pair, NIL(char *)) { 01671 LtlPairFree(pair); 01672 } 01673 st_free_table(EdgeUtable); 01674 01675 st_free_table(Avtx2Qvtx); 01676 /* st_free_table(Class2Qvtx); */ 01677 Q->SCC = Class2Qvtx; 01678 01679 return Q; 01680 } 01681 01689 int 01690 Ltl_AutomatonVtxGetNodeIdx( 01691 vertex_t *v) 01692 { 01693 Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data; 01694 return node->index; 01695 } 01696 01704 LtlSet_t * 01705 LtlAutomatonVertexGetLabels( 01706 vertex_t *vtx) 01707 { 01708 Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) vtx->user_data; 01709 return node->Labels; 01710 } 01711 01712 01713 /*---------------------------------------------------------------------------*/ 01714 /* Definition of static functions */ 01715 /*---------------------------------------------------------------------------*/ 01716 01724 static lsList 01725 AutomatonPickInputCandidate( 01726 graph_t *G, 01727 vertex_t *vtx) 01728 { 01729 st_table *uTable; 01730 lsList candi, preImg; 01731 lsGen lsgen, lsgen2; 01732 edge_t *e, *e2; 01733 vertex_t *s, *t; 01734 int size; 01735 01736 preImg = g_get_in_edges(vtx); /* shouldn't be freed */ 01737 size = lsLength(preImg); 01738 01739 /* No predecessor */ 01740 if (size == 0) { 01741 return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); 01742 } 01743 /* The only predecessor is itself */ 01744 if (size == 1) { 01745 lsFirstItem(preImg, &e, NIL(lsHandle)); 01746 if (g_e_source(e) == vtx) { /* all the vertices in G */ 01747 return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); 01748 } 01749 } 01750 /* Has predecessor(s) other than itself */ 01751 uTable = st_init_table(st_ptrcmp, st_ptrhash); 01752 candi = lsCreate(); 01753 lsForEachItem (preImg, lsgen, e) { 01754 s = g_e_source(e); 01755 foreach_out_edge(s, lsgen2, e2) { 01756 t = g_e_dest(e2); 01757 if (t != vtx) { 01758 if(!st_insert(uTable, t, t)) 01759 lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle)); 01760 } 01761 } 01762 if (size == 1) { 01763 if (!st_insert(uTable, s, s)) 01764 lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle)); 01765 } 01766 } 01767 st_free_table(uTable); 01768 01769 return candi; 01770 } 01771 01779 static lsList 01780 AutomatonPickOutputCandidate( 01781 graph_t *G, 01782 vertex_t *vtx) 01783 { 01784 st_table *uTable; 01785 lsList candi, Img; 01786 lsGen lsgen, lsgen2; 01787 edge_t *e, *e2; 01788 vertex_t *s, *t; 01789 int size; 01790 01791 Img = g_get_out_edges(vtx); 01792 size = lsLength(Img); 01793 01794 /* No successor */ 01795 if (size == 0) { 01796 return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); 01797 } 01798 /* The only successor is itself */ 01799 if (size == 1) { 01800 lsFirstItem(Img, &e, NIL(lsHandle)); 01801 if (g_e_dest(e) == vtx) { 01802 return lsCopy(g_get_vertices(G), (lsGeneric (*)(lsGeneric)) NULL); 01803 } 01804 } 01805 /* Has successor(s) other than itself */ 01806 uTable = st_init_table(st_ptrcmp, st_ptrhash); 01807 candi = lsCreate(); 01808 lsForEachItem(Img, lsgen, e) { 01809 s = g_e_dest(e); 01810 foreach_in_edge(s, lsgen2, e2) { 01811 t = g_e_source(e2); 01812 if (t != vtx) { 01813 if(!st_insert(uTable, t, t)) 01814 lsNewEnd(candi, (lsGeneric) t, NIL(lsHandle)); 01815 } 01816 } 01817 if (size == 1) { 01818 if(!st_insert(uTable, s, s)) 01819 lsNewEnd(candi, (lsGeneric)s, NIL(lsHandle)); 01820 } 01821 } 01822 st_free_table(uTable); 01823 01824 return candi; 01825 } 01826 01827 01835 static st_table * 01836 AutomatonVertexGetPreImg( 01837 graph_t *G, 01838 vertex_t *vtx) 01839 { 01840 lsList preImg; 01841 lsGen lsgen; 01842 edge_t *e; 01843 vertex_t *s; 01844 st_table *uTable; 01845 01846 preImg = g_get_in_edges(vtx); 01847 01848 uTable = st_init_table(st_ptrcmp, st_ptrhash); 01849 lsForEachItem(preImg, lsgen, e) { 01850 s = g_e_source(e); 01851 st_insert(uTable, s, s); 01852 } 01853 01854 return uTable; 01855 } 01856 01864 static st_table * 01865 AutomatonVertexGetImg( 01866 graph_t *G, 01867 vertex_t *vtx) 01868 { 01869 lsList Img; 01870 lsGen lsgen; 01871 edge_t *e; 01872 vertex_t *s; 01873 st_table *uTable; 01874 01875 Img = g_get_out_edges(vtx); 01876 01877 uTable = st_init_table(st_ptrcmp, st_ptrhash); 01878 lsForEachItem(Img, lsgen, e) { 01879 s = g_e_dest(e); 01880 st_insert(uTable, s, s); 01881 } 01882 01883 return uTable; 01884 } 01885 01893 static int 01894 AutomatonVertexHasSelfLoop( 01895 graph_t *G, 01896 vertex_t *vtx) 01897 { 01898 lsList Img; 01899 lsGen lsgen; 01900 edge_t *e; 01901 int flag = 0; 01902 01903 Img = g_get_out_edges(vtx); 01904 01905 lsForEachItem(Img, lsgen, e) { 01906 if (g_e_dest(e) == vtx) { 01907 flag = 1; 01908 lsFinish(lsgen); 01909 break; 01910 } 01911 } 01912 01913 return flag; 01914 } 01915 01924 static int 01925 AutomatonPfairEquivQfair( 01926 Ltl_Automaton_t *A, 01927 vertex_t *state, 01928 vertex_t *otherstate) 01929 { 01930 int flag = 1; 01931 st_table *FairSet; 01932 lsGen lsgen; 01933 01934 lsForEachItem (A->Fair, lsgen, FairSet) { 01935 if (st_is_member(FairSet, state) != 01936 st_is_member(FairSet, otherstate)) { 01937 flag = 0; 01938 lsFinish(lsgen); 01939 break; 01940 } 01941 } 01942 01943 return flag; 01944 } 01945 01954 static int 01955 AutomatonPfairImplyQfair( 01956 Ltl_Automaton_t *A, 01957 vertex_t *state, 01958 vertex_t *otherstate) 01959 { 01960 int flag = 1; 01961 st_table *FairSet; 01962 lsGen lsgen; 01963 01964 lsForEachItem (A->Fair, lsgen, FairSet) { 01965 if (st_is_member(FairSet, state) && 01966 !st_is_member(FairSet, otherstate)) { 01967 flag = 0; 01968 lsFinish(lsgen); 01969 break; 01970 } 01971 } 01972 01973 return flag; 01974 } 01975 01984 static char * 01985 StTableDelete( 01986 st_table *tbl, 01987 char *item) 01988 { 01989 char *key = item; 01990 01991 if (st_is_member(tbl, key)) { 01992 st_delete(tbl, &key, NIL(char *)); 01993 return key; 01994 }else 01995 return NIL(char); 01996 } 01997 02005 static st_table * 02006 StTableAppend( 02007 st_table *tbl1, 02008 st_table *tbl2) 02009 { 02010 char *key, *value; 02011 st_generator *stgen; 02012 02013 st_foreach_item(tbl2, stgen, &key, &value) { 02014 if (!st_is_member(tbl1, key)) 02015 st_insert(tbl1, key, value); 02016 } 02017 02018 return tbl1; 02019 } 02020 02028 static st_table * 02029 StTableRestrict( 02030 st_table *tbl1, 02031 st_table *tbl2) 02032 { 02033 char *key, *value; 02034 st_table *tbl = st_copy(tbl1); 02035 st_generator *stgen; 02036 02037 st_foreach_item(tbl, stgen, &key, &value) { 02038 if (!st_is_member(tbl2, key)) 02039 st_delete(tbl1, &key, &value); 02040 } 02041 st_free_table(tbl); 02042 02043 return tbl1; 02044 } 02045 02053 static st_table * 02054 StTableSubtract( 02055 st_table *tbl1, 02056 st_table *tbl2) 02057 { 02058 char *key, *value; 02059 st_generator *stgen; 02060 02061 st_foreach_item(tbl2, stgen, &key, &value) { 02062 if (st_is_member(tbl1, key)) 02063 st_delete(tbl1, &key, &value); 02064 } 02065 02066 return tbl1; 02067 } 02068 02077 static int 02078 StTableIsEqual( 02079 st_table *tbl1, 02080 st_table *tbl2, 02081 st_table *dontcare) 02082 { 02083 int flag = 1; 02084 st_generator *stgen; 02085 vertex_t *vtx; 02086 02087 flag = 1; 02088 st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) { 02089 if (dontcare) { 02090 if (st_is_member(dontcare,vtx)) continue; 02091 } 02092 if (!st_is_member(tbl2,vtx)) { 02093 flag = 0; 02094 st_free_gen(stgen); 02095 break; 02096 } 02097 } 02098 if (!flag) return 0; 02099 02100 st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) { 02101 if (dontcare) { 02102 if (st_is_member(dontcare,vtx)) continue; 02103 } 02104 if (!st_is_member(tbl1, vtx)) { 02105 flag = 0; 02106 st_free_gen(stgen); 02107 break; 02108 } 02109 } 02110 return flag; 02111 } 02112 02121 static int 02122 StTableInclude( 02123 st_table *large, 02124 st_table *small, 02125 st_table *dontcare) 02126 { 02127 int flag = 1; 02128 st_generator *stgen; 02129 vertex_t *vtx; 02130 02131 flag = 1; 02132 st_foreach_item(small, stgen, &vtx, NIL(char *)) { 02133 if (dontcare) { 02134 if (st_is_member(dontcare, vtx)) continue; 02135 } 02136 if (!st_is_member(large,vtx)) { 02137 flag = 0; 02138 st_free_gen(stgen); 02139 break; 02140 } 02141 } 02142 02143 return flag; 02144 } 02145 02146 02155 static int 02156 StTableIsDisjoint( 02157 st_table *tbl1, 02158 st_table *tbl2, 02159 st_table *dontcare) 02160 { 02161 int flag = 1; 02162 st_generator *stgen; 02163 vertex_t *vtx; 02164 02165 flag = 1; 02166 st_foreach_item(tbl1, stgen, &vtx, NIL(char *)) { 02167 if (dontcare) { 02168 if (st_is_member(dontcare, vtx)) continue; 02169 } 02170 if (st_is_member(tbl2,vtx)) { 02171 flag = 0; 02172 st_free_gen(stgen); 02173 break; 02174 } 02175 } 02176 if (!flag) return 0; 02177 02178 st_foreach_item(tbl2, stgen, &vtx, NIL(char *)) { 02179 if (dontcare) { 02180 if (st_is_member(dontcare, vtx)) continue; 02181 } 02182 if (st_is_member(tbl1,vtx)) { 02183 flag = 0; 02184 st_free_gen(stgen); 02185 break; 02186 } 02187 } 02188 return flag; 02189 } 02190 02198 static int 02199 StTableIsFair( 02200 lsList A_Fair, 02201 st_table *Class) 02202 { 02203 int flag; 02204 st_table *FairSet; 02205 lsGen lsgen; 02206 02207 flag = 1; 02208 lsForEachItem (A_Fair, lsgen, FairSet) { 02209 if (StTableIsDisjoint(FairSet,Class,NIL(st_table))) { 02210 flag = 0; 02211 lsFinish(lsgen); 02212 break; 02213 } 02214 } 02215 02216 return flag; 02217 } 02218 02227 static int 02228 AutomatonPartitionIsClique( 02229 graph_t *G, 02230 st_table *set) 02231 { 02232 int flag = 1; 02233 st_table *Img; 02234 st_generator *stgen; 02235 vertex_t *state; 02236 02237 st_foreach_item(set, stgen, &state, NIL(char *)) { 02238 Img = AutomatonVertexGetImg(G, state); 02239 flag = StTableInclude(Img, set, NIL(st_table)); 02240 st_free_table(Img); 02241 if (!flag) { 02242 st_free_gen(stgen); 02243 break; 02244 } 02245 } 02246 02247 return flag; 02248 } 02249 02259 static st_table * 02260 AutomatonPartitionLabelLUB( 02261 st_table *set, 02262 array_t *Negate) 02263 { 02264 vertex_t *state; 02265 st_table *greatest = NIL(st_table); 02266 st_generator *stgen; 02267 LtlSet_t *lub = NIL(LtlSet_t); 02268 LtlSet_t *label; 02269 02270 st_foreach_item(set, stgen, &state, NIL(char *)) { 02271 label = LtlAutomatonVertexGetLabels(state); 02272 if (greatest) { 02273 if (LtlSetEqual(label, lub)) 02274 st_insert(greatest, state, state); 02275 else if (LtlSetInclude(lub, label)) { 02276 LtlSetAssign(lub, label); 02277 st_free_table(greatest); 02278 greatest = st_init_table(st_ptrcmp, st_ptrhash); 02279 st_insert(greatest, state, state); 02280 }else if (!LtlSetInclude(label, lub)) { 02281 st_free_table(greatest); 02282 greatest = NIL(st_table); 02283 st_free_gen(stgen); 02284 break; 02285 } 02286 }else { 02287 lub = LtlSetCopy(label); 02288 greatest = st_init_table(st_ptrcmp, st_ptrhash); 02289 st_insert(greatest, state, state); 02290 } 02291 } 02292 02293 if (lub) 02294 LtlSetFree(lub); 02295 02296 return greatest; 02297 } 02298 02308 static st_table * 02309 AutomatonPartitionLabelGLB( 02310 st_table *set, 02311 array_t *Negate) 02312 { 02313 vertex_t *state, *least; 02314 LtlSet_t *glb, *label; 02315 st_table *tbl; 02316 st_generator *stgen; 02317 02318 least = NIL(vertex_t); 02319 glb = NIL(LtlSet_t); 02320 st_foreach_item(set, stgen, &state, NIL(char *)) { 02321 label = LtlAutomatonVertexGetLabels(state); 02322 if (!glb) 02323 glb = LtlSetCopy(label); 02324 else 02325 LtlSetOR(glb, glb, label); 02326 02327 if (LtlSetIsContradictory(glb, Negate)) { 02328 least = NIL(vertex_t); 02329 st_free_gen(stgen); 02330 break; 02331 }else if (!least) { 02332 if (LtlSetEqual(glb, label)) 02333 least = state; 02334 }else if (!LtlSetEqual(glb, LtlAutomatonVertexGetLabels(least))) { 02335 if (LtlSetEqual(glb, label)) 02336 least = state; 02337 else 02338 least = NIL(vertex_t); 02339 } 02340 } 02341 02342 if (glb) 02343 LtlSetFree(glb); 02344 02345 if (least) { 02346 tbl = st_init_table(st_ptrcmp, st_ptrhash); 02347 st_insert(tbl, least, least); 02348 }else 02349 tbl = NIL(st_table); 02350 02351 return tbl; 02352 } 02353 02362 static st_table * 02363 AutomatonQuotientVertexGetClass( 02364 vertex_t *vtx) 02365 { 02366 Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *)vtx->user_data; 02367 return node->Class; 02368 } 02369 02377 /*static int 02378 AutomatonVtxGetNodeIdx( 02379 vertex_t *v) 02380 { 02381 Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) v->user_data; 02382 return node->index; 02383 }*/