From abbd0eee0732f0d814b3c93a5a6babbbe97c0905 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Dec 2004 18:33:39 +0000 Subject: [PATCH] * src/tgbaalgos/gtec/status.hh (couvreur99_check_status::cycle_seed): New attribute. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Fill cycle_seed. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Revamp to compute a cycle from the cycle_start, and then the shortest prefix to this cycle. --- ChangeLog | 13 ++ iface/gspn/ltlgspn.cc | 6 +- iface/gspn/ssp.cc | 5 + iface/gspn/ssp.hh | 8 +- src/tgbaalgos/gtec/ce.cc | 236 ++++++++++++++++------------------- src/tgbaalgos/gtec/ce.hh | 11 +- src/tgbaalgos/gtec/gtec.cc | 13 +- src/tgbaalgos/gtec/status.hh | 1 + 8 files changed, 154 insertions(+), 139 deletions(-) diff --git a/ChangeLog b/ChangeLog index 1f844d16b..54836a96b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,18 @@ 2004-12-10 Alexandre Duret-Lutz + * src/tgbaalgos/gtec/status.hh + (couvreur99_check_status::cycle_seed): New attribute. + * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, + couvreur99_check_shy::check): Fill cycle_seed. + * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: + (couvreur99_check_result::accepting_run, + couvreur99_check_result::accepting_cycle): Revamp to compute a + cycle from the cycle_start, and then the shortest prefix to this + cycle. + + * iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, iface/gspn/ssp.cc: Disable + the functions that were using the interface I have just broken. + * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap::find): Clarify comment. diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 382f051cf..8cf826a89 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -263,7 +263,11 @@ main(int argc, char **argv) ce = new spot::couvreur99_check_result(ecs); break; default: - ce = spot::counter_example_ssp(ecs); + // ce = spot::counter_example_ssp(ecs); + std::cerr + << "counter_example_ssp() is no longer supported" + << std::endl; + exit(1); } #endif spot::tgba_run* run = ce->accepting_run(); diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index a65b85b04..69a2f9400 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -1003,6 +1003,10 @@ namespace spot return new couvreur99_check_shy_ssp(ssp_automata); } +#if 0 + // I rewrote couvreur99_check_result today, and it no longer use + // connected_component_ssp_factory. So this cannot work anymore. + // -- adl 2004-12-10. couvreur99_check_result* counter_example_ssp(const couvreur99_check_status* status) { @@ -1010,4 +1014,5 @@ namespace spot couvreur99_check_result(status, connected_component_ssp_factory::instance()); } +#endif } diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index 3973cc0e1..fe6e17a34 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -55,9 +55,13 @@ namespace spot couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata); - couvreur99_check_result* - counter_example_ssp(const couvreur99_check_status* status); /// @} + + // I rewrote couvreur99_check_result today, and it no longer use + // connected_component_ssp_factory. So this cannot work anymore. + // -- adl 2004-12-10. + // couvreur99_check_result* + // counter_example_ssp(const couvreur99_check_status* status); } #endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 762924f58..b231e51fb 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -24,10 +24,56 @@ namespace spot { + namespace + { + typedef Sgi::hash_set state_set; + class shortest_path: public bfs_steps + { + public: + shortest_path(const state_set* t, const couvreur99_check_status* ecs) + : bfs_steps(ecs->aut), target(t), ecs(ecs) + { + } + + const state* + search(const state* start, tgba_run::steps& l) + { + return this->bfs_steps::search(filter(start), l); + } + + const state* + filter(const state* s) + { + numbered_state_heap::state_index_p sip = ecs->h->find(s); + // Ignore unknown states ... + if (!sip.first) + { + delete s; + return 0; + } + // ... as well as dead states. + if (*sip.second == -1) + return 0; + return sip.first; + } + + bool + match(tgba_run::step&, const state* dest) + { + return target->find(dest) != target->end(); + } + + private: + state_set seen; + const state_set* target; + const couvreur99_check_status* ecs; + }; + } + couvreur99_check_result::couvreur99_check_result - (const couvreur99_check_status* ecs, - const explicit_connected_component_factory* eccf) - : emptiness_check_result(ecs->aut), ecs_(ecs), eccf_(eccf) + (const couvreur99_check_status* ecs) + : emptiness_check_result(ecs->aut), ecs_(ecs) { } @@ -38,153 +84,93 @@ namespace spot assert(!ecs_->root.empty()); - scc_stack::stack_type root = ecs_->root.s; - int comp_size = root.size(); - // Transform the stack of connected component into an array. - explicit_connected_component** scc = - new explicit_connected_component*[comp_size]; - for (int j = comp_size - 1; 0 <= j; --j) + // Compute an accepting cycle. + accepting_cycle(); + + // Compute the prefix: it's the shortest path from the initial + // state of the automata to any state of the cycle. + + // Register all states from the cycle as target of the BFS. + state_set ss; + for (tgba_run::steps::const_iterator i = run_->cycle.begin(); + i != run_->cycle.end(); ++i) + ss.insert(i->s); + shortest_path shpath(&ss, ecs_); + + const state* prefix_start = ecs_->aut->get_init_state(); + // There are two cases: either the initial state is already on + // the cycle, or it is not. If it is, we will have to rotate + // the cycle so it begins on this position. Otherwise we will shift + // the cycle so it begins on the state that follows the prefix. + // cycle_entry_point is that state. + const state* cycle_entry_point; + state_set::const_iterator ps = ss.find(prefix_start); + if (ps != ss.end()) { - scc[j] = eccf_->build(); - scc[j]->index = root.top().index; - scc[j]->condition = root.top().condition; - root.pop(); + // The initial state is on the cycle. + delete prefix_start; + cycle_entry_point = *ps; } - assert(root.empty()); - - // Build the set of states for all SCCs. - numbered_state_heap_const_iterator* i = ecs_->h->iterator(); - for (i->first(); !i->done(); i->next()) + else { - int index = i->get_index(); - // Skip states from dead SCCs. - if (index < 0) - continue; - assert(index != 0); - - // Find the SCC this state belongs to. - int j; - for (j = 1; j < comp_size; ++j) - if (index < scc[j]->index) - break; - scc[j - 1]->insert(i->get_state()); - } - delete i; - - numbered_state_heap::state_index_p spi = - ecs_->h->index(ecs_->aut->get_init_state()); - assert(spi.first); - - // We build a path trough each SCC in the stack. For the - // first SCC, the starting state is the initial state of the - // automaton. The destination state is the closest state - // from the next SCC. This destination state becomes the - // starting state when building a path through the next SCC. - const state* start = spi.first; - for (int k = 0; k < comp_size - 1; ++k) - { - - struct scc_bfs: bfs_steps - { - explicit_connected_component** scc; - int k; - bool in_next; - scc_bfs(const tgba* a, explicit_connected_component** scc, int k) - : bfs_steps(a), scc(scc), k(k) - { - } - - virtual const state* - filter(const state* s) - { - const state* h_s = scc[k]->has_state(s); - if (!h_s) - { - h_s = scc[k+1]->has_state(s); - in_next = true; - if (!h_s) - delete s; - } - else - { - in_next = false; - } - return h_s; - } - - virtual bool - match(tgba_run::step&, const state*) - { - return in_next; - } - - - } b(ecs_->aut, scc, k); - - start = b.search(start, run_->prefix); + // This initial state is outside the cycle. Compute the prefix. + cycle_entry_point = shpath.search(prefix_start, run_->prefix); } - accepting_cycle(scc[comp_size - 1], start, - scc[comp_size - 1]->condition); + // Locate cycle_entry_point on the cycle. + tgba_run::steps::iterator cycle_ep_it; + for (cycle_ep_it = run_->cycle.begin(); + cycle_ep_it != run_->cycle.end() + && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) + continue; + assert(cycle_ep_it != run_->cycle.end()); - for (int j = comp_size - 1; 0 <= j; --j) - delete scc[j]; - delete[] scc; + // Now shift the cycle so it starts on cycle_entry_point. + run_->cycle.splice(run_->cycle.end(), run_->cycle, + run_->cycle.begin(), cycle_ep_it); + run_->cycle.erase(run_->cycle.begin(), cycle_ep_it); return run_; } - namespace - { - struct triplet - { - const state* s; // Current state. - tgba_succ_iterator* iter; // Iterator to successor of the current state. - bdd acc; // All acceptance conditions traversed by - // the path so far. - - triplet (const state* s, tgba_succ_iterator* iter, bdd acc) - : s(s), iter(iter), acc(acc) - { - } - }; - - } - void - couvreur99_check_result::accepting_cycle(const explicit_connected_component* - scc, - const state* start, bdd - acc_to_traverse) + couvreur99_check_result::accepting_cycle() { + bdd acc_to_traverse = ecs_->aut->all_acceptance_conditions(); // Compute an accepting cycle using successive BFS that are // restarted from the point reached after we have discovered a // transition with a new acceptance conditions. // // This idea is taken from Product::findWitness in LBTT 1.1.2. - const state* substart = start; + const state* substart = ecs_->cycle_seed; do { struct scc_bfs: bfs_steps { - const explicit_connected_component* scc; - bool in_next; + const couvreur99_check_status* ecs; bdd& acc_to_traverse; - const state* start; - scc_bfs(const tgba* a, const explicit_connected_component* scc, - bdd& acc_to_traverse, const state* start) - : bfs_steps(a), scc(scc), acc_to_traverse(acc_to_traverse), - start(start) + int scc_root; + scc_bfs(const couvreur99_check_status* ecs, + bdd& acc_to_traverse) + : bfs_steps(ecs->aut), ecs(ecs), acc_to_traverse(acc_to_traverse), + scc_root(ecs->root.s.top().index) { } virtual const state* filter(const state* s) { - const state* h_s = scc->has_state(s); - if (!h_s) - delete s; - return h_s; + numbered_state_heap::state_index_p sip = ecs->h->find(s); + // Ignore unknown states. + if (!sip.first) + { + delete s; + return 0; + } + // Stay in the final SCC. + if (*sip.second < scc_root) + return 0; + return sip.first; } virtual bool @@ -193,7 +179,7 @@ namespace spot bdd less_acc = acc_to_traverse - st.acc; if (less_acc != acc_to_traverse || (acc_to_traverse == bddfalse - && s == start)) + && s == ecs->cycle_seed)) { acc_to_traverse = less_acc; return true; @@ -201,11 +187,11 @@ namespace spot return false; } - } b(ecs_->aut, scc, acc_to_traverse, start); + } b(ecs_, acc_to_traverse); substart = b.search(substart, run_->cycle); } - while (acc_to_traverse != bddfalse || substart != start); + while (acc_to_traverse != bddfalse || substart != ecs_->cycle_seed); } void diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index c56b25a27..30e612811 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -23,7 +23,6 @@ # define SPOT_TGBAALGOS_GTEC_CE_HH #include "status.hh" -#include "explscc.hh" #include "tgbaalgos/emptiness.hh" namespace spot @@ -32,11 +31,7 @@ namespace spot class couvreur99_check_result: public emptiness_check_result { public: - couvreur99_check_result(const couvreur99_check_status* ecs, - const explicit_connected_component_factory* - eccf = - connected_component_hash_set_factory::instance()); - + couvreur99_check_result(const couvreur99_check_status* ecs); virtual tgba_run* accepting_run(); @@ -45,12 +40,10 @@ namespace spot protected: /// Called by accepting_run() to find a cycle which traverses all /// acceptance conditions in the accepted SCC. - void accepting_cycle(const explicit_connected_component* scc, - const state* start, bdd acc_to_traverse); + void accepting_cycle(); private: const couvreur99_check_status* ecs_; - const explicit_connected_component_factory* eccf_; tgba_run* run_; }; } diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index d99db8d15..2893ab710 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -229,6 +229,9 @@ namespace spot todo.pop(); dec_depth(); } + // Use this state to start the computation of an accepting + // cycle. + ecs_->cycle_seed = spi.first; set_states(ecs_->states()); return new couvreur99_check_result(ecs_); } @@ -288,7 +291,8 @@ namespace spot succ_queue::iterator q = queue.begin(); while (q != queue.end()) { - int* i = find_state(q->s); + numbered_state_heap::state_index_p sip = ecs_->h->find(q->s); + int* i = sip.second; if (!i) { // Skip unknown states. @@ -333,10 +337,15 @@ namespace spot // merged SCC. ecs_->root.top().condition |= acc; + // Have we found all acceptance conditions? if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions()) { - /// q->s has already been freed by find_state(). + // Use this state to start the computation of an accepting + // cycle. + ecs_->cycle_seed = sip.first; + + /// q->s has already been freed by ecs_->h->find. queue.erase(q); // We have found an accepting SCC. Clean up TODO. // We must delete all states of apparing in TODO diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index e52c5dc90..1337fcbd6 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -44,6 +44,7 @@ namespace spot const tgba* aut; scc_stack root; numbered_state_heap* h; ///< Heap of visited states. + const state* cycle_seed; /// Output statistics about this object. void print_stats(std::ostream& os) const;