diff --git a/ChangeLog b/ChangeLog index 468dac800..1a9fce4cf 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2004-11-25 Alexandre Duret-Lutz + + * src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result): + Add the TGBA considered as a protected attribute, and provide an + automaton() accessor. + * src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, + src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow + this new interface. + 2004-11-24 Alexandre Duret-Lutz * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Revert diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index ccf481b3f..5d9bd1f59 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -73,6 +73,11 @@ namespace spot class emptiness_check_result { public: + emptiness_check_result(const tgba* a) + : a_(a) + { + } + /// \brief Return a run accepted by the automata passed to /// the emptiness check. /// @@ -86,14 +91,34 @@ namespace spot /// is no counter-example; the mere existence of an instance of /// this class asserts the existence of a counter-example). virtual tgba_run* accepting_run(); + + /// The automaton on which an accepting_run() was found. + const tgba* + automaton() const + { + return a_; + } + protected: + const tgba* a_; ///< The automaton. }; /// Common interface to emptiness check algorithms. class emptiness_check { public: + emptiness_check(const tgba* a) + : a_(a) + { + } virtual ~emptiness_check(); + /// The automaton that this emptiness-check inspects. + const tgba* + automaton() const + { + return a_; + } + /// \brief Check whether the automaton contain an accepting run. /// /// Return 0 if the automaton accept no run. Return an instance @@ -108,6 +133,9 @@ namespace spot /// Print statistics, if any. virtual std::ostream& print_stats(std::ostream& os) const; + + protected: + const tgba* a_; ///< The automaton. }; /// @} diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 383cf8161..762924f58 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -27,7 +27,7 @@ namespace spot couvreur99_check_result::couvreur99_check_result (const couvreur99_check_status* ecs, const explicit_connected_component_factory* eccf) - : ecs_(ecs), eccf_(eccf) + : emptiness_check_result(ecs->aut), ecs_(ecs), eccf_(eccf) { } diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 5f04112ff..2cacb7b91 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -31,6 +31,7 @@ namespace spot couvreur99_check::couvreur99_check(const tgba* a, const numbered_state_heap_factory* nshf) + : emptiness_check(a) { ecs_ = new couvreur99_check_status(a, nshf); } diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 43ab2ef1b..8a8e90c1f 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -52,9 +52,6 @@ namespace spot struct gv04: public emptiness_check, public ec_statistics { - // The automata to check. - const tgba* a; - // The unique accepting condition of the automaton \a a, // or bddfalse if there is no. bdd accepting; @@ -73,7 +70,7 @@ namespace spot bool violation; // Whether an accepting run was found. gv04(const tgba *a) - : a(a), accepting(a->all_acceptance_conditions()) + : emptiness_check(a), accepting(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); } @@ -97,19 +94,19 @@ namespace spot { top = dftop = -1; violation = false; - push(a->get_init_state(), false); + push(a_->get_init_state(), false); while (!violation && dftop >= 0) { trace << "Main iteration (top = " << top << ", dftop = " << dftop - << ", s = " << a->format_state(stack[dftop].s) + << ", 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 = stack[dftop].lasttr = a_->succ_iter(stack[dftop].s); iter->first(); } else @@ -129,7 +126,7 @@ namespace spot inc_transitions(); trace << " Next successor: s_prime = " - << a->format_state(s_prime) + << a_->format_state(s_prime) << (acc ? " (with accepting link)" : ""); hash_type::const_iterator i = h.find(s_prime); @@ -169,7 +166,7 @@ namespace spot void push(const state* s, bool accepting) { - trace << " push(s = " << a->format_state(s) + trace << " push(s = " << a_->format_state(s) << ", accepting = " << accepting << ")" << std::endl; h[s] = ++top; @@ -244,7 +241,7 @@ namespace spot gv04& data; result(gv04& data) - : data(data) + : emptiness_check_result(data.automaton()), data(data) { } @@ -269,7 +266,7 @@ namespace spot for (int i = 0; i <= data.top; ++i) { trace << "state " << i << " (" - << data.a->format_state(data.stack[i].s) + << data.a_->format_state(data.stack[i].s) << ") has lowlink = " << data.stack[i].lowlink << std::endl; } #endif @@ -306,7 +303,7 @@ namespace spot int scc_root; first_bfs(const gv04& data, int scc_root) - : bfs_steps(data.a), data(data), scc_root(scc_root) + : bfs_steps(data.automaton()), data(data), scc_root(scc_root) { } diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index dd07c5fde..2c06de500 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -50,9 +50,8 @@ namespace spot /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). magic_search(const tgba *a, size_t size) - : ec_statistics(), + : emptiness_check(a), h(size), - a(a), all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); @@ -88,7 +87,7 @@ namespace spot if (st_red.empty()) { assert(st_blue.empty()); - const state* s0 = a->get_init_state(); + const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); @@ -146,7 +145,7 @@ namespace spot const bdd& label, const bdd& acc) { inc_depth(); - tgba_succ_iterator* i = a->succ_iter(s); + tgba_succ_iterator* i = a_->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } @@ -171,9 +170,6 @@ namespace spot /// State targeted by the red dfs. const state* target; - /// The automata to check. - const tgba* a; - /// The unique accepting condition of the automaton \a a. bdd all_cond; @@ -184,14 +180,14 @@ namespace spot stack_item& f = st_blue.front(); # ifdef TRACE std::cout << "DFS_BLUE treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -256,7 +252,7 @@ namespace spot // functionnality, the test can be ommited. # ifdef TRACE std::cout << " It is blue and the arc from " - << a->format_state(st_blue.front().s) + << a_->format_state(st_blue.front().s) << " to it is accepting, start a red dfs" << std::endl; # endif @@ -290,14 +286,14 @@ namespace spot stack_item& f = st_red.front(); # ifdef TRACE std::cout << "DFS_RED treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -354,7 +350,7 @@ namespace spot { public: result(magic_search& ms) - : ms_(ms) + : emptiness_check_result(ms.automaton()), ms_(ms) { } virtual tgba_run* accepting_run() diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 76a6c8506..a5d9fe464 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -52,10 +52,9 @@ namespace spot /// \pre The automaton \a a must have at most one accepting /// condition (i.e. it is a TBA). se05_search(const tgba *a, size_t size) - : ec_statistics(), + : emptiness_check(a), current_weight(0), h(size), - a(a), all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() <= 1); @@ -91,7 +90,7 @@ namespace spot if (st_red.empty()) { assert(st_blue.empty()); - const state* s0 = a->get_init_state(); + const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); @@ -149,7 +148,7 @@ namespace spot const bdd& label, const bdd& acc) { inc_depth(); - tgba_succ_iterator* i = a->succ_iter(s); + tgba_succ_iterator* i = a_->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } @@ -175,9 +174,6 @@ namespace spot /// by the last dfs visiting it. heap h; - /// The automata to check. - const tgba* a; - /// The unique accepting condition of the automaton \a a. bdd all_cond; @@ -188,14 +184,14 @@ namespace spot stack_item& f = st_blue.front(); # ifdef TRACE std::cout << "DFS_BLUE treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -275,7 +271,7 @@ namespace spot // functionnality, the test can be ommited. # ifdef TRACE std::cout << " The arc from " - << a->format_state(st_blue.front().s) + << a_->format_state(st_blue.front().s) << " to the current state is accepting, start a " << "red dfs" << std::endl; # endif @@ -306,14 +302,14 @@ namespace spot stack_item& f = st_red.front(); # ifdef TRACE std::cout << "DFS_RED treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -379,7 +375,7 @@ namespace spot { public: result(se05_search& ms) - : ms_(ms) + : emptiness_check_result(ms.automaton()), ms_(ms) { } virtual tgba_run* accepting_run() diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 07e894bbe..3998163a0 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -52,9 +52,8 @@ namespace spot public: /// \brief Initialize the search algorithm on the automaton \a a tau03_search(const tgba *a, size_t size) - : ec_statistics(), + : emptiness_check(a), h(size), - a(a), all_cond(a->all_acceptance_conditions()) { assert(a->number_of_acceptance_conditions() > 0); @@ -86,12 +85,12 @@ namespace spot if (!st_blue.empty()) return 0; assert(st_red.empty()); - const state* s0 = a->get_init_state(); + const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, BLUE); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new emptiness_check_result; + return new emptiness_check_result(a_); return 0; } @@ -126,7 +125,7 @@ namespace spot const bdd& label, const bdd& acc) { inc_depth(); - tgba_succ_iterator* i = a->succ_iter(s); + tgba_succ_iterator* i = a_->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } @@ -148,9 +147,6 @@ namespace spot /// by the last dfs visiting it. heap h; - /// The automata to check. - const tgba* a; - /// The unique accepting condition of the automaton \a a. bdd all_cond; @@ -161,14 +157,14 @@ namespace spot stack_item& f = st_blue.front(); # ifdef TRACE std::cout << "DFS_BLUE treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -204,15 +200,15 @@ namespace spot # endif typename heap::color_ref c = h.get_color_ref(f.s); assert(!c.is_white()); - tgba_succ_iterator* i = a->succ_iter(f.s); + tgba_succ_iterator* i = a_->succ_iter(f.s); for (i->first(); !i->done(); i->next()) { inc_transitions(); const state *s_prime = i->current_state(); #ifdef TRACE std::cout << "DFS_BLUE rescanning the arc from " - << a->format_state(f.s) << " to " - << a->format_state(s_prime) << std::endl; + << a_->format_state(f.s) << " to " + << a_->format_state(s_prime) << std::endl; # endif bdd label = i->current_condition(); bdd acc = i->current_acceptance_conditions(); @@ -223,15 +219,15 @@ namespace spot { # ifdef TRACE std::cout << " "; - bdd_print_acc(std::cout, a->get_dict(), acu); + bdd_print_acc(std::cout, a_->get_dict(), acu); std::cout << " is not included in "; - bdd_print_acc(std::cout, a->get_dict(), - c_prime.get_acc()); + bdd_print_acc(std::cout, a_->get_dict(), + c_prime.get_acc()); std::cout << std::endl; std::cout << " Start a red dfs from " - << a->format_state(s_prime) + << a_->format_state(s_prime) << " propagating: "; - bdd_print_acc(std::cout, a->get_dict(), acu); + bdd_print_acc(std::cout, a_->get_dict(), acu); std::cout << std::endl; # endif c_prime.cumulate_acc(acu); @@ -271,14 +267,14 @@ namespace spot stack_item& f = st_red.front(); #ifdef TRACE std::cout << "DFS_RED treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); #ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index cd4fcb8ba..8de532401 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -67,10 +67,9 @@ namespace spot public: /// \brief Initialize the search algorithm on the automaton \a a tau03_opt_search(const tgba *a, size_t size) - : ec_statistics(), + : emptiness_check(a), current_weight(a->neg_acceptance_conditions()), h(size), - a(a), all_acc(a->all_acceptance_conditions()) { } @@ -101,12 +100,12 @@ namespace spot if (!st_blue.empty()) return 0; assert(st_red.empty()); - const state* s0 = a->get_init_state(); + const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, CYAN, current_weight); push(st_blue, s0, bddfalse, bddfalse); if (dfs_blue()) - return new emptiness_check_result; + return new emptiness_check_result(a_); return 0; } @@ -141,7 +140,7 @@ namespace spot const bdd& label, const bdd& acc) { inc_depth(); - tgba_succ_iterator* i = a->succ_iter(s); + tgba_succ_iterator* i = a_->succ_iter(s); i->first(); st.push_front(stack_item(s, i, label, acc)); } @@ -166,9 +165,6 @@ namespace spot /// by the last dfs visiting it. heap h; - /// The automata to check. - const tgba* a; - /// The unique accepting condition of the automaton \a a. bdd all_acc; @@ -179,14 +175,14 @@ namespace spot stack_item& f = st_blue.front(); # ifdef TRACE std::cout << "DFS_BLUE treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions(); @@ -229,12 +225,12 @@ namespace spot if ((c_prime.get_acc() & acu) != acu) { # ifdef TRACE - bdd_print_acc(std::cout, a->get_dict(), acu); + bdd_print_acc(std::cout, a_->get_dict(), acu); std::cout << " is not included in "; - bdd_print_acc(std::cout, a->get_dict(), - c_prime.get_acc()); + bdd_print_acc(std::cout, a_->get_dict(), + c_prime.get_acc()); std::cout << ", start a red dfs propagating: "; - bdd_print_acc(std::cout, a->get_dict(), acu); + bdd_print_acc(std::cout, a_->get_dict(), acu); std::cout << std::endl; # endif c_prime.cumulate_acc(acu); @@ -277,10 +273,10 @@ namespace spot { # ifdef TRACE std::cout << " The arc from " - << a->format_state(st_blue.front().s) + << a_->format_state(st_blue.front().s) << " to the current state implies to " << " start a red dfs propagating "; - bdd_print_acc(std::cout, a->get_dict(), acu); + bdd_print_acc(std::cout, a_->get_dict(), acu); std::cout << std::endl; # endif c_prime.cumulate_acc(acu); @@ -317,14 +313,14 @@ namespace spot stack_item& f = st_red.front(); # ifdef TRACE std::cout << "DFS_RED treats: " - << a->format_state(f.s) << std::endl; + << a_->format_state(f.s) << std::endl; # endif if (!f.it->done()) { const state *s_prime = f.it->current_state(); # ifdef TRACE std::cout << " Visit the successor: " - << a->format_state(s_prime) << std::endl; + << a_->format_state(s_prime) << std::endl; # endif bdd label = f.it->current_condition(); bdd acc = f.it->current_acceptance_conditions();