From df1bf80d1fe535d04f4aefbf06f3cd0c94601836 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 23 Nov 2004 18:39:12 +0000 Subject: [PATCH] * src/tgbaalgos/gv04.cc (gv04::result): New struct to compute counter examples. (gv04:check): Return a gv04::result. --- ChangeLog | 22 ++-- src/tgbaalgos/gv04.cc | 260 +++++++++++++++++++++++++++++++++++++++--- 2 files changed, 261 insertions(+), 21 deletions(-) diff --git a/ChangeLog b/ChangeLog index 6ec70bc9d..2334d52bf 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,4 +1,10 @@ -2004-11-23 Poitrenaud Denis +2004-11-23 Alexandre Duret-Lutz + + * src/tgbaalgos/gv04.cc (gv04::result): New struct to compute + counter examples. + (gv04:check): Return a gv04::result. + +2004-11-23 Denis Poitrenaud * src/tgbaalgos/tau03opt.cc: Fix a warning. @@ -25,7 +31,7 @@ new algorithm. * src/tgbatest/emptchk.test: Test it. -2004-11-22 Poitrenaud Denis +2004-11-22 Denis Poitrenaud * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, src/tgbaalgos/weight.hh: New files. @@ -53,7 +59,7 @@ * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. (ce_stat): New struct. -2004-11-17 Poitrenaud Denis +2004-11-17 Denis Poitrenaud * src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo. * src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now @@ -81,7 +87,7 @@ src/misc/random.hh, src/misc/version.hh, src/tgba/state.hh: More Doxygen groups. -2004-11-17 Poitrenaud Denis +2004-11-17 Denis Poitrenaud * src/tgbaalgos/magic.hh: Fix a comment and remove se05 interface. * src/tgbaalgos/magic.cc: Fix a comment. @@ -187,7 +193,7 @@ of randtgba. * src/tgbatest/emptchk.test: Adjust. -2004-11-15 Poitrenaud Denis +2004-11-15 Denis Poitrenaud * src/tgbaalgos/magic.cc: Fix a stupid bug. * src/tgbaalgos/se05.cc: Fix the same bug. @@ -209,7 +215,7 @@ * src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the supplied stream, not std::cout. -2004-11-15 Poitrenaud Denis +2004-11-15 Denis Poitrenaud * src/tgbaalgos/magic.cc: Add a bit state hashing version. * src/tgbaalgos/se05.cc: Add a bit state hashing version. @@ -269,7 +275,7 @@ * src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword some help strings. -2004-11-09 Poitrenaud Denis +2004-11-09 Denis Poitrenaud * src/tgbaalgos/magic.cc: rewrite to externalize the heap and prepare it to a bit state hashing version. @@ -1462,7 +1468,7 @@ * wrap/python/spot.i: Process tgbaalgos/neverclaim.hh. * wrap/python/cgi/ltl2tgba.in: Display the never claim on demand. -2004-04-21 Denis Poitrenaud +2004-04-21 Denis Poitrenaud * src/ltlvisit/tostring.hh (to_spin_string): New function. Convert a formula into a string parsable by Spin. diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 9bcecb5df..aedec4cf0 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -30,6 +30,8 @@ #include #include +#include +#include #include "tgba/tgba.hh" #include "misc/hash.hh" #include "emptiness.hh" @@ -43,10 +45,7 @@ namespace spot struct stack_entry { const state* s; // State stored in stack entry. - tgba_succ_iterator* nexttr; // Next transition to explore. - // (The paper uses lasttr for the - // last transition, but nexttr is - // easier for our iterators.) + tgba_succ_iterator* lasttr; // Last transition explored from this state. int lowlink; // Lowlink value if this entry. int pre; // DFS predecessor. int acc; // Accepting state link. @@ -83,7 +82,7 @@ namespace spot ~gv04() { for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i) - delete i->nexttr; + delete i->lasttr; hash_type::const_iterator s = h.begin(); while (s != h.end()) { @@ -103,13 +102,22 @@ namespace spot while (!violation && dftop >= 0) { - tgba_succ_iterator* iter = stack[dftop].nexttr; - trace << "Main iteration (top = " << top << ", dftop = " << dftop << ", s = " << a->format_state(stack[dftop].s) << ")" << std::endl; + tgba_succ_iterator* iter = stack[dftop].lasttr; + if (!iter) + { + iter = stack[dftop].lasttr = a->succ_iter(stack[dftop].s); + iter->first(); + } + else + { + iter->next(); + } + if (iter->done()) { trace << " No more successors" << std::endl; @@ -119,7 +127,6 @@ namespace spot { const state* s_prime = iter->current_state(); bool acc = iter->current_acceptance_conditions() == accepting; - iter->next(); inc_transitions(); trace << " Next successor: s_prime = " @@ -156,7 +163,7 @@ namespace spot set_states(h.size()); } if (violation) - return new emptiness_check_result; + return new result(*this); return 0; } @@ -168,9 +175,7 @@ namespace spot h[s] = ++top; - tgba_succ_iterator* iter = a->succ_iter(s); - iter->first(); - stack_entry ss = { s, iter, top, dftop, 0 }; + stack_entry ss = { s, 0, top, dftop, 0 }; if (accepting) ss.acc = dftop; // This differs from GV04 to support TBA. @@ -199,7 +204,7 @@ namespace spot assert(static_cast(top + 1) == stack.size()); for (int i = top; i >= dftop; --i) { - delete stack[i].nexttr; + delete stack[i].lasttr; stack.pop_back(); dec_depth(); } @@ -235,6 +240,235 @@ namespace spot return os; } + struct result: public emptiness_check_result + { + result(gv04& data) + : data(data) + { + } + + virtual tgba_run* + accepting_run() + { + tgba_run* res = new tgba_run; + + // Transitively update the lowlinks, so we can use them in + // the BDS bellow. + for (int i = 0; i <= data.top; ++i) + { + int l = data.stack[i].lowlink; + if (l < i) + { + int ll = data.stack[i].lowlink = data.stack[l].lowlink; + for (int j = i - 1; data.stack[j].lowlink != ll; --j) + data.stack[j].lowlink = ll; + } + } +#ifdef TRACE + for (int i = 0; i <= data.top; ++i) + { + trace << "state " << i << " (" + << data.a->format_state(data.stack[i].s) + << ") has lowlink = " << data.stack[i].lowlink << std::endl; + } +#endif + + // We will use the root of the last SCC as the start of the + // cycle. + int scc_root = data.stack[data.dftop].lowlink; + assert(scc_root >= 0); + + // Construct the prefix by unwinding the DFS stack before + // scc_root. + int father = data.stack[scc_root].pre; + while (father >= 0) + { + tgba_run::step st = + { + data.stack[father].s->clone(), + data.stack[father].lasttr->current_condition(), + data.stack[father].lasttr->current_acceptance_conditions() + }; + res->prefix.push_front(st); + father = data.stack[father].pre; + } + + // Construct the cycle in two phases. A first BFS find the + // shortest path from scc_root to an accepting transition. + // A second BFS then search a path back to scc_root. If + // there is no acceptance conditions we just use the second + // BFS to find a cycle around scc_root. + const state* bfs_start = data.stack[scc_root].s; + const state* bfs_end = bfs_start; + if (data.accepting != bddfalse) + { + trace << "1st BFS" << std::endl; + + // Records backlinks to parent state during the BFS. + // (This also stores the propositions of this link.) + std::map father; + // BFS queue. + std::deque todo; + // Initial state. + todo.push_back(bfs_start); + + while (!todo.empty()) + { + const state* src = todo.front(); + todo.pop_front(); + tgba_succ_iterator* i = data.a->succ_iter(src); + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + + trace << " state " << data.a->format_state(dest); + + // Do not escape the SCC + hash_type::const_iterator j = data.h.find(dest); + if (// This state was never visited so far. + j == data.h.end() + // Or it was discarded + || j->second >= data.stack.size() + // Or it was discarded (but its stack slot reused) + || data.stack[j->second].s->compare(dest) + // Or it is still on the stack but not in the SCC + || data.stack[j->second].lowlink < scc_root) + { + trace << " ignored" << std::endl; + delete dest; + continue; + } + trace << " explored" << std::endl; + delete dest; + dest = j->first; + + bdd cond = i->current_condition(); + bdd acc = i->current_acceptance_conditions(); + tgba_run::step s = { src, cond, acc }; + + if (acc != bddfalse) + { + // Found it! + + tgba_run::steps p; + while (s.s != bfs_start) + { + p.push_front(s); + s = father[s.s]; + } + p.push_front(s); + res->cycle.splice(res->cycle.end(), p); + // Exit this BFS, and start the next one at dest. + todo.clear(); + bfs_start = dest; + break; + } + + // Common case: record backlinks and continue BFS + // for unvisited states. + if (father.find(dest) == father.end()) + { + todo.push_back(dest); + father[dest] = s; + } + } + delete i; + } + } + // Second BFS. + if (bfs_start != bfs_end || res->cycle.empty()) + { + trace << "2nd BFS" << std::endl; + + // Records backlinks to parent state during the BFS. + // (This also stores the propositions of this link.) + std::map father; + // BFS queue. + std::deque todo; + // Initial state. + todo.push_back(bfs_start); + + while (!todo.empty()) + { + const state* src = todo.front(); + todo.pop_front(); + tgba_succ_iterator* i = data.a->succ_iter(src); + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + + trace << " state " << data.a->format_state(dest); + + // Do not escape the SCC + hash_type::const_iterator j = data.h.find(dest); + if (// This state was never visited so far. + j == data.h.end() + // Or it was discarded + || j->second >= data.stack.size() + // Or it was discarded (but its stack slot reused) + || data.stack[j->second].s->compare(dest) + // Or it is still on the stack but not in the SCC + || data.stack[j->second].lowlink < scc_root) + { + trace << " ignored" << std::endl; + delete dest; + continue; + } + trace << " explored" << std::endl; + delete dest; + dest = j->first; + + bdd cond = i->current_condition(); + bdd acc = i->current_acceptance_conditions(); + tgba_run::step s = { src, cond, acc }; + + if (dest == bfs_end) + { + // Found it! + tgba_run::steps p; + while (s.s != bfs_start) + { + p.push_front(s); + s = father[s.s]; + } + p.push_front(s); + res->cycle.splice(res->cycle.end(), p); + // Exit this BFS. + todo.clear(); + break; + } + + // Common case: record backlinks and continue BFS + // for unvisited states. + if (father.find(dest) == father.end()) + { + todo.push_back(dest); + father[dest] = s; + } + } + delete i; + } + } + + // Clone every state in the cycle before returning it. (We + // didn't do that before in the algorithm, because it's + // easier to follow if every state manipulated in the BFS is + // the instance in the hash table.) + for (tgba_run::steps::iterator i = res->cycle.begin(); + i != res->cycle.end(); ++i) + i->s = i->s->clone(); + + assert(res->cycle.begin() != res->cycle.end()); + + return res; + } + + gv04& data; + }; + + }; } // anonymous