diff --git a/ChangeLog b/ChangeLog index b0d3d6125..d7d44b70d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,23 @@ 2004-10-27 Alexandre Duret-Lutz + Introduce an emptiness-check interface, and modify the existing + algorithms to conform to it, uniformly. This will unfortunately + break third-party code that were using these algorithms. + * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files. + * src/tgbaalgos/Makefile.am: New files. + * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to + conform to the new emptiness-check interface. + * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, + src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, + src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: + Likewise. The classes have been renamed are as following + emptiness_check -> couvreur99_check + emptiness_check_shy -> couvreur99_check_shy + emptiness_check_status -> couvreur99_check_status + counter_example -> couvreur99_check_result + * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh, + iface/gspn/ssp.cc: Adjust to renaming and new interface. + * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: New files. * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS, diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 917de45e3..47ac376c1 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -216,25 +216,25 @@ main(int argc, char **argv) case Couvreur4: case Couvreur5: { - spot::emptiness_check* ec; + spot::couvreur99_check* ec; switch (check) { case Couvreur: - ec = new spot::emptiness_check(prod); + ec = new spot::couvreur99_check(prod); break; case Couvreur2: - ec = new spot::emptiness_check_shy(prod); + ec = new spot::couvreur99_check_shy(prod); break; #ifdef SSP case Couvreur3: - ec = spot::emptiness_check_ssp_semi(prod); + ec = spot::couvreur99_check_ssp_semi(prod); break; case Couvreur4: - ec = spot::emptiness_check_ssp_shy_semi(prod); + ec = spot::couvreur99_check_ssp_shy_semi(prod); break; case Couvreur5: - ec = spot::emptiness_check_ssp_shy(prod); + ec = spot::couvreur99_check_ssp_shy(prod); break; #endif default: @@ -244,30 +244,32 @@ main(int argc, char **argv) ec = 0; } - bool res = ec->check(); - - const spot::emptiness_check_status* ecs = ec->result(); - if (!res) + spot::emptiness_check_result* res = ec->check(); + const spot::couvreur99_check_status* ecs = ec->result(); + if (res) { if (compute_counter_example) { - spot::counter_example* ce; + spot::couvreur99_check_result* ce; #ifndef SSP - ce = new spot::counter_example(ecs); + ce = new spot::couvreur99_check_result(ecs); #else switch (check) { case Couvreur: case Couvreur2: case Couvreur5: - ce = new spot::counter_example(ecs); + ce = new spot::couvreur99_check_result(ecs); break; default: ce = spot::counter_example_ssp(ecs); } #endif - ce->print_result(std::cout, proj ? model : 0); + spot::tgba_run* run = ce->accepting_run(); + // FIXME: reimplement the projection + spot::print_tgba_run(std::cout, run, prod); ce->print_stats(std::cout); + delete run; delete ce; } else @@ -275,6 +277,7 @@ main(int argc, char **argv) std::cout << "non empty" << std::endl; ecs->print_stats(std::cout); } + delete res; } else { @@ -283,7 +286,7 @@ main(int argc, char **argv) } std::cout << std::endl; delete ec; - if (!res) + if (res) exit(1); } break; @@ -292,12 +295,19 @@ main(int argc, char **argv) spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); spot::magic_search ms(d); - if (ms.check()) + spot::emptiness_check_result* res = ms.check(); + if (res) { if (compute_counter_example) - ms.print_result (std::cout, proj ? model : 0); + { + spot::tgba_run* run = res->accepting_run(); + // FIXME: reimplement the projection + spot::print_tgba_run(std::cout, run, prod); + delete run; + } else std::cout << "non-empty" << std::endl; + delete res; exit(1); } else diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 9676ce0f1..8962cbd4c 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -802,7 +802,7 @@ namespace spot hash_type h; ///< Map of visited states. friend class numbered_state_heap_ssp_const_iterator; - friend class emptiness_check_shy_ssp; + friend class couvreur99_check_shy_ssp; }; @@ -896,12 +896,12 @@ namespace spot }; - class emptiness_check_shy_ssp : public emptiness_check_shy + class couvreur99_check_shy_ssp : public couvreur99_check_shy { public: - emptiness_check_shy_ssp(const tgba* a) - : emptiness_check_shy(a, - numbered_state_heap_ssp_factory_semi::instance()) + couvreur99_check_shy_ssp(const tgba* a) + : couvreur99_check_shy(a, + numbered_state_heap_ssp_factory_semi::instance()) { } @@ -976,36 +976,37 @@ namespace spot - emptiness_check* - emptiness_check_ssp_semi(const tgba* ssp_automata) + couvreur99_check* + couvreur99_check_ssp_semi(const tgba* ssp_automata) { assert(dynamic_cast(ssp_automata)); return - new emptiness_check(ssp_automata, - numbered_state_heap_ssp_factory_semi::instance()); + new couvreur99_check(ssp_automata, + numbered_state_heap_ssp_factory_semi::instance()); } - emptiness_check* - emptiness_check_ssp_shy_semi(const tgba* ssp_automata) + couvreur99_check* + couvreur99_check_ssp_shy_semi(const tgba* ssp_automata) { assert(dynamic_cast(ssp_automata)); return - new emptiness_check_shy - (ssp_automata, + new couvreur99_check_shy + (ssp_automata, numbered_state_heap_ssp_factory_semi::instance()); } - emptiness_check* - emptiness_check_ssp_shy(const tgba* ssp_automata) + couvreur99_check* + couvreur99_check_ssp_shy(const tgba* ssp_automata) { assert(dynamic_cast(ssp_automata)); - return new emptiness_check_shy_ssp(ssp_automata); + return new couvreur99_check_shy_ssp(ssp_automata); } - counter_example* - counter_example_ssp(const emptiness_check_status* status) + couvreur99_check_result* + counter_example_ssp(const couvreur99_check_status* status) { - return new counter_example(status, - connected_component_ssp_factory::instance()); + return new + couvreur99_check_result(status, + connected_component_ssp_factory::instance()); } } diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index 5e4996bf8..ff6b6f731 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -48,11 +48,12 @@ namespace spot const ltl::declarative_environment& env_; }; - emptiness_check* emptiness_check_ssp_semi(const tgba* ssp_automata); - emptiness_check* emptiness_check_ssp_shy_semi(const tgba* ssp_automata); - emptiness_check* emptiness_check_ssp_shy(const tgba* ssp_automata); + couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata); + couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); + couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata); - counter_example* counter_example_ssp(const emptiness_check_status* status); + couvreur99_check_result* + counter_example_ssp(const couvreur99_check_status* status); } #endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 3ddabb01d..5d623cb0a 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ dotty.hh \ dupexp.hh \ + emptiness.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ @@ -44,6 +45,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ dotty.cc \ dupexp.cc \ + emptiness.cc \ lbtt.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc new file mode 100644 index 000000000..58a5af248 --- /dev/null +++ b/src/tgbaalgos/emptiness.cc @@ -0,0 +1,111 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "emptiness.hh" +#include "tgba/tgba.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + + tgba_run::~tgba_run() + { + for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i) + delete i->s; + for (steps::const_iterator i = cycle.begin(); i != cycle.end(); ++i) + delete i->s; + } + + tgba_run::tgba_run(const tgba_run& run) + { + for (steps::const_iterator i = run.prefix.begin(); + i != run.prefix.end(); ++i) + { + step s = { s.s->clone(), i->label, i->acc }; + prefix.push_back(s); + } + for (steps::const_iterator i = run.cycle.begin(); + i != run.cycle.end(); ++i) + { + step s = { s.s->clone(), i->label, i->acc }; + cycle.push_back(s); + } + } + + std::ostream& print_tgba_run(std::ostream& os, + const tgba_run* run, + const tgba* a) + { + bdd_dict* d = a->get_dict(); + os << "Prefix:" << std::endl; + for (tgba_run::steps::const_iterator i = run->prefix.begin(); + i != run->prefix.end(); ++i) + { + os << " " << a->format_state(i->s) << std::endl; + os << " | "; + bdd_print_set(os, d, i->label); + os << "\t"; + bdd_print_accset(os, d, i->acc); + os << std::endl; + } + os << "Cycle:" << std::endl; + for (tgba_run::steps::const_iterator i = run->cycle.begin(); + i != run->cycle.end(); ++i) + { + os << " " << a->format_state(i->s) << std::endl; + os << " | "; + bdd_print_set(os, d, i->label); + os << "\t"; + bdd_print_accset(os, d, i->acc); + os << std::endl; + } + return os; + } + + + tgba_run& + tgba_run::operator=(const tgba_run& run) + { + if (&run != this) + { + this->~tgba_run(); + new(this) tgba_run(run); + } + return *this; + } + + + tgba_run* + emptiness_check_result::accepting_run() + { + return 0; + } + + emptiness_check::~emptiness_check() + { + } + + std::ostream& + emptiness_check::print_stats(std::ostream& os) const + { + return os; + } +} diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh new file mode 100644 index 000000000..f3daee52e --- /dev/null +++ b/src/tgbaalgos/emptiness.hh @@ -0,0 +1,107 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_EMPTINESS_HH +# define SPOT_TGBAALGOS_EMPTINESS_HH + +#include +#include +#include +#include "tgba/state.hh" + +namespace spot +{ + + /// An accepted run, for a tgba. + struct tgba_run + { + struct step { + const state* s; + bdd label; + bdd acc; + }; + + typedef std::list steps; + + steps prefix; + steps cycle; + + ~tgba_run(); + tgba_run() + { + }; + tgba_run(const tgba_run& run); + tgba_run& operator=(const tgba_run& run); + }; + + class tgba; + std::ostream& print_tgba_run(std::ostream& os, + const tgba_run* run, + const tgba* a); + + /// \brief The result of an emptiness check. + /// + /// Instances of these class should not last longer than the + /// instances of emptiness_check that produced them as they + /// may reference data internal to the check. + class emptiness_check_result + { + public: + /// \brief Return a run accepted by the automata passed to + /// the emptiness check. + /// + /// This method might actually compute the acceptance run. (Not + /// all emptiness check algorithms actually produce a + /// counter-example as a side-effect of checking emptiness, some + /// need some post-processing.) + /// + /// This can also return 0 if the emptiness check algorithm + /// cannot produce a counter example (that does not mean there + /// 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(); + }; + + /// Common interface to emptiness check algorithms. + class emptiness_check + { + public: + virtual ~emptiness_check(); + + /// \brief Check whether the automaton contain an accepting run. + /// + /// Return 0 if the automaton accept no run. Return an instance + /// of emptiness_check_result otherwise. This instance might + /// allow to obtain one sample acceptance run. The result has to + /// be destroyed before the emptiness_check instance that + /// generated it. + /// + /// Some emptiness_check algorithms may allow check() to be called + /// several time, but generally you should not assume that. + virtual emptiness_check_result* check() = 0; + + /// Print statistics, if any. + virtual std::ostream& print_stats(std::ostream& os) const; + }; + +} + +#endif // SPOT_TGBAALGOS_EMPTINESS_HH diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 8c7d2d970..0a0f24a86 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -28,15 +28,22 @@ namespace spot namespace { typedef std::pair pair_state_iter; + typedef std::pair state_proposition; } - counter_example::counter_example(const emptiness_check_status* ecs, - const explicit_connected_component_factory* - eccf) - : ecs_(ecs) + couvreur99_check_result::couvreur99_check_result + (const couvreur99_check_status* ecs, + const explicit_connected_component_factory* eccf) + : ecs_(ecs), eccf_(eccf) { + } + + tgba_run* + couvreur99_check_result::accepting_run() + { + run_ = new tgba_run; + assert(!ecs_->root.empty()); - assert(suffix.empty()); scc_stack::stack_type root = ecs_->root.s; int comp_size = root.size(); @@ -45,7 +52,7 @@ namespace spot new explicit_connected_component*[comp_size]; for (int j = comp_size - 1; 0 <= j; --j) { - scc[j] = eccf->build(); + scc[j] = eccf_->build(); scc[j]->index = root.top().index; scc[j]->condition = root.top().condition; root.pop(); @@ -74,7 +81,9 @@ namespace spot numbered_state_heap::state_index_p spi = ecs_->h->index(ecs_->aut->get_init_state()); assert(spi.first); - suffix.push_front(spi.first); + /// FIXME: Should compute label and acceptance condition. + tgba_run::step s = { spi.first, bddtrue, bddfalse }; + run_->prefix.push_front(s); // We build a path trough each SCC in the stack. For the // first SCC, the starting state is the initial state of the @@ -93,7 +102,7 @@ namespace spot father_map father; // Initial state of the BFS. - const state* start = suffix.back(); + const state* start = run_->prefix.back().s; { tgba_succ_iterator* i = ecs_->aut->succ_iter(start); todo.push_back(pair_state_iter(start, i)); @@ -114,20 +123,26 @@ namespace spot if (!h_dest) { // If we have found a state in the next SCC. - // Unwind the path and populate SUFFIX. + // Unwind the path and populate RUN_->PREFIX. h_dest = scc[k+1]->has_state(dest); if (h_dest) { - state_sequence seq; + tgba_run::steps seq; - seq.push_front(h_dest); + /// FIXME: Should compute label and acceptance + /// condition. + tgba_run::step s = { h_dest, bddtrue, bddfalse }; + seq.push_front(s); while (src->compare(start)) { - seq.push_front(src); + /// FIXME: Should compute label and acceptance + /// condition. + tgba_run::step s = { h_dest, bddtrue, bddfalse }; + seq.push_front(s); src = father[src]; } - // Append SEQ to SUFFIX. - suffix.splice(suffix.end(), seq); + // Append SEQ to RUN_->PREFIX. + run_->prefix.splice(run_->prefix.end(), seq); // Exit this BFS for this SCC. while (!todo.empty()) { @@ -152,24 +167,37 @@ namespace spot } } - accepting_path(scc[comp_size - 1], suffix.back(), + accepting_path(scc[comp_size - 1], run_->prefix.back().s, scc[comp_size - 1]->condition); - + run_->prefix.pop_back(); // this state belongs to the cycle. for (int j = comp_size - 1; 0 <= j; --j) delete scc[j]; delete[] scc; + + // Clone every state in the run before returning it. (We didn't + // do that before in the algorithm, because it's easier to follow + // if every state manipulated is the instance in the hash table.) + for (tgba_run::steps::iterator i = run_->prefix.begin(); + i != run_->prefix.end(); ++i) + i->s = i->s->clone(); + for (tgba_run::steps::iterator i = run_->cycle.begin(); + i != run_->cycle.end(); ++i) + i->s = i->s->clone(); + + return run_; } void - counter_example::complete_cycle(const explicit_connected_component* scc, - const state* from, - const state* to) + couvreur99_check_result::complete_cycle(const explicit_connected_component* + scc, + const state* from, + const state* to) { - // If by change or period already ends on the state we have + // If by chance our cycle already ends on the state we have // to reach back, we are done. if (from == to - && !period.empty()) + && !run_->cycle.empty()) return; // Records backlinks to parent state during the BFS. @@ -207,18 +235,22 @@ namespace spot bdd cond = i->current_condition(); // If we have reached our destination, unwind the path - // and populate PERIOD. + // and populate RUN_->CYCLE. if (h_dest == to) { - cycle_path p; - p.push_front(state_proposition(h_dest, cond)); + tgba_run::steps p; + // FIXME: should compute acceptance condition. + tgba_run::step s = { h_dest, cond, bddfalse }; + p.push_front(s); while (src != from) { const state_proposition& psi = father[src]; - p.push_front(state_proposition(src, psi.second)); + // FIXME: should compute acceptance condition. + tgba_run::step s = { src, psi.second, bddfalse }; + p.push_front(s); src = psi.first; } - period.splice(period.end(), p); + run_->cycle.splice(run_->cycle.end(), p); // Exit the BFS, but release all iterators first. while (!todo.empty()) @@ -257,8 +289,10 @@ namespace spot } void - counter_example::accepting_path(const explicit_connected_component* scc, - const state* start, bdd acc_to_traverse) + couvreur99_check_result::accepting_path(const explicit_connected_component* + scc, + const state* start, bdd + acc_to_traverse) { // State seen during the DFS. typedef Sgi::hash_setcurrent_acceptance_conditions() | todo.top().acc; - path.push_back(state_proposition(h_dest, - iter->current_condition())); + tgba_run::step st = { h_dest, iter->current_condition(), + iter->current_acceptance_conditions() }; + path.push_back(st); // Advance iterator for next step. iter->next(); @@ -377,71 +412,30 @@ namespace spot path.pop_back(); } - // Append our best path to the period. - for (cycle_path::iterator it = best_path.begin(); + // Append our best path to the run_->cycle. + for (tgba_run::steps::iterator it = best_path.begin(); it != best_path.end(); ++it) - period.push_back(*it); + run_->cycle.push_back(*it); // Prepare to find another path for the remaining acceptance // conditions. acc_to_traverse -= best_acc; - start = period.back().first; + start = run_->cycle.back().s; } // Complete the path so that it goes back to its beginning, // forming a cycle. - complete_cycle(scc, start, suffix.back()); + complete_cycle(scc, start, run_->prefix.back().s); } - std::ostream& - counter_example::print_result(std::ostream& os, const tgba* restrict) const - { - os << "Prefix:" << std::endl; - const bdd_dict* d = ecs_->aut->get_dict(); - for (state_sequence::const_iterator i_se = suffix.begin(); - i_se != suffix.end(); ++i_se) - { - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(*i_se, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(*i_se) << std::endl; - } - } - os << "Cycle:" <second) << std::endl; - os << " "; - if (restrict) - { - const state* s = ecs_->aut->project_state(it->first, restrict); - assert(s); - os << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << ecs_->aut->format_state(it->first) << std::endl; - } - } - return os; - } - - void - counter_example::print_stats(std::ostream& os) const + couvreur99_check_result::print_stats(std::ostream& os) const { ecs_->print_stats(os); - os << suffix.size() << " states in suffix" << std::endl; - os << period.size() << " states in period" << std::endl; + // FIXME: This is bogusly assuming run_ exists. (Even if we + // created it, the user might have delete it.) + os << run_->prefix.size() << " states in run_->prefix" << std::endl; + os << run_->cycle.size() << " states in run_->cycle" << std::endl; } } diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index f541e3522..8a9dac437 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -24,35 +24,26 @@ #include "status.hh" #include "explscc.hh" +#include "tgbaalgos/emptiness.hh" namespace spot { - /// Compute a counter example from a spot::emptiness_check_status - class counter_example + /// Compute a counter example from a spot::couvreur99_check_status + class couvreur99_check_result: public emptiness_check_result { public: - counter_example(const emptiness_check_status* ecs, - const explicit_connected_component_factory* - eccf = connected_component_hash_set_factory::instance()); + couvreur99_check_result(const couvreur99_check_status* ecs, + const explicit_connected_component_factory* + eccf = + connected_component_hash_set_factory::instance()); - typedef std::pair state_proposition; - typedef std::list state_sequence; - typedef std::list cycle_path; - state_sequence suffix; - cycle_path period; - /// \brief Display the example computed by counter_example(). - /// - /// \param os the output stream - /// \param restrict optional automaton to project the example on. - std::ostream& print_result(std::ostream& os, - const tgba* restrict = 0) const; + virtual tgba_run* accepting_run(); - /// Output statistics about this object. void print_stats(std::ostream& os) const; protected: - /// Called by counter_example to find a path which traverses all + /// Called by couvreur99_check_result to find a path which traverses all /// acceptance conditions in the accepted SCC. void accepting_path (const explicit_connected_component* scc, const state* start, bdd acc_to_traverse); @@ -63,7 +54,9 @@ namespace spot const state* from, const state* to); private: - const emptiness_check_status* ecs_; + 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 1582f809c..a60eee5ca 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "gtec.hh" +#include "ce.hh" namespace spot { @@ -28,19 +29,19 @@ namespace spot typedef std::pair pair_state_iter; } - emptiness_check::emptiness_check(const tgba* a, - const numbered_state_heap_factory* nshf) + couvreur99_check::couvreur99_check(const tgba* a, + const numbered_state_heap_factory* nshf) { - ecs_ = new emptiness_check_status(a, nshf); + ecs_ = new couvreur99_check_status(a, nshf); } - emptiness_check::~emptiness_check() + couvreur99_check::~couvreur99_check() { delete ecs_; } void - emptiness_check::remove_component(const state* from) + couvreur99_check::remove_component(const state* from) { // Remove from H all states which are reachable from state FROM. @@ -87,12 +88,12 @@ namespace spot } } - bool - emptiness_check::check() + emptiness_check_result* + couvreur99_check::check() { // We use five main data in this algorithm: - // * emptiness_check::root, a stack of strongly connected components (SCC), - // * emptiness_check::h, a hash of all visited nodes, with their order, + // * couvreur99_check::root, a stack of strongly connected components (SCC), + // * couvreur99_check::h, a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) // * arc, a stack of acceptance conditions between each of these SCC, std::stack arc; @@ -220,25 +221,25 @@ namespace spot delete todo.top().second; todo.pop(); } - return false; + return new couvreur99_check_result(ecs_); } } // This automaton recognizes no word. - return true; + return 0; } - const emptiness_check_status* - emptiness_check::result() const + const couvreur99_check_status* + couvreur99_check::result() const { return ecs_; } ////////////////////////////////////////////////////////////////////// - emptiness_check_shy::emptiness_check_shy(const tgba* a, - const numbered_state_heap_factory* - nshf) - : emptiness_check(a, nshf), num(1) + couvreur99_check_shy::couvreur99_check_shy(const tgba* a, + const numbered_state_heap_factory* + nshf) + : couvreur99_check(a, nshf), num(1) { // Setup depth-first search from the initial state. todo.push(pair_state_successors(0, succ_queue())); @@ -246,12 +247,12 @@ namespace spot ecs_->aut->get_init_state())); } - emptiness_check_shy::~emptiness_check_shy() + couvreur99_check_shy::~couvreur99_check_shy() { } - bool - emptiness_check_shy::check() + emptiness_check_result* + couvreur99_check_shy::check() { for (;;) @@ -336,7 +337,7 @@ namespace spot } todo.pop(); } - return false; + return new couvreur99_check_result(ecs_); } } // Remove that state from the queue, so we do not @@ -354,7 +355,7 @@ namespace spot todo.pop(); if (todo.empty()) // This automaton recognizes no word. - return true; + return 0; // When backtracking the root of an SCC, we must also // remove that SCC from the ARC/ROOT stacks. We must @@ -393,7 +394,7 @@ namespace spot } int* - emptiness_check_shy::find_state(const state* s) + couvreur99_check_shy::find_state(const state* s) { return ecs_->h->find(s).second; } diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 58e02b0ba..91916fa93 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -23,6 +23,7 @@ # define SPOT_TGBAALGOS_GTEC_GTEC_HH #include "status.hh" +#include "tgbaalgos/emptiness.hh" namespace spot { @@ -51,32 +52,32 @@ namespace spot /// it return false, a stack of SCC has been built is available /// using result() (spot::counter_example needs it). /// - /// There are two variants of this algorithm: spot::emptiness_check and - /// spot::emptiness_check_shy. They differ in their memory usage, the + /// There are two variants of this algorithm: spot::couvreur99_check and + /// spot::couvreur99_check_shy. They differ in their memory usage, the /// number for successors computed before they are used and the way /// the depth first search is directed. /// - /// spot::emptiness_check performs a straightforward depth first search. + /// spot::couvreur99_check performs a straightforward depth first search. /// The DFS stacks store tgba_succ_iterators, so that only the /// iterators which really are explored are computed. /// - /// spot::emptiness_check_shy tries to explore successors which are + /// spot::couvreur99_check_shy tries to explore successors which are /// visited states first. this helps to merge SCCs and generally /// helps to produce shorter counter-examples. However this /// algorithm cannot stores unprocessed successors as /// tgba_succ_iterators: it must compute all successors of a state /// at once in order to decide which to explore first, and must keep /// a list of all unexplored successors in its DFS stack. - class emptiness_check + class couvreur99_check: public emptiness_check { public: - emptiness_check(const tgba* a, - const numbered_state_heap_factory* nshf - = numbered_state_heap_hash_map_factory::instance()); - virtual ~emptiness_check(); + couvreur99_check(const tgba* a, + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); + virtual ~couvreur99_check(); /// Check whether the automaton's language is empty. - virtual bool check(); + virtual emptiness_check_result* check(); /// \brief Return the status of the emptiness-check. /// @@ -85,11 +86,11 @@ namespace spot /// /// This status should not be deleted, it is a pointer /// to a member of this class that will be deleted when - /// the emptiness_check object is deleted. - const emptiness_check_status* result() const; + /// the couvreur99 object is deleted. + const couvreur99_check_status* result() const; protected: - emptiness_check_status* ecs_; + couvreur99_check_status* ecs_; /// \brief Remove a strongly component from the hash. /// /// This function remove all accessible state from a given @@ -98,19 +99,19 @@ namespace spot void remove_component(const state* start_delete); }; - /// \brief A version of spot::emptiness_check that tries to visit + /// \brief A version of spot::couvreur99_check that tries to visit /// known states first. /// - /// See the documentation for spot::emptiness_check - class emptiness_check_shy : public emptiness_check + /// See the documentation for spot::couvreur99_check + class couvreur99_check_shy : public couvreur99_check { public: - emptiness_check_shy(const tgba* a, - const numbered_state_heap_factory* nshf - = numbered_state_heap_hash_map_factory::instance()); - virtual ~emptiness_check_shy(); + couvreur99_check_shy(const tgba* a, + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); + virtual ~couvreur99_check_shy(); - virtual bool check(); + virtual emptiness_check_result* check(); protected: struct successor { @@ -120,8 +121,8 @@ namespace spot }; // We use five main data in this algorithm: - // * emptiness_check::root, a stack of strongly connected components (SCC), - // * emptiness_check::h, a hash of all visited nodes, with their order, + // * couvreur99_check::root, a stack of strongly connected components (SCC), + // * couvreur99_check::h, a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) // * arc, a stack of acceptance conditions between each of these SCC, std::stack arc; diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc index 37d3f5828..70b3c2fe7 100644 --- a/src/tgbaalgos/gtec/status.cc +++ b/src/tgbaalgos/gtec/status.cc @@ -24,7 +24,7 @@ namespace spot { - emptiness_check_status::emptiness_check_status + couvreur99_check_status::couvreur99_check_status (const tgba* aut, const numbered_state_heap_factory* nshf) : aut(aut), @@ -32,13 +32,13 @@ namespace spot { } - emptiness_check_status::~emptiness_check_status() + couvreur99_check_status::~couvreur99_check_status() { delete h; } void - emptiness_check_status::print_stats(std::ostream& os) const + couvreur99_check_status::print_stats(std::ostream& os) const { os << h->size() << " unique states visited" << std::endl; os << root.size() diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 067ee5460..2fe6c1fad 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -34,12 +34,12 @@ namespace spot /// This contains everything needed to construct a counter-example: /// the automata, the stack of SCCs traversed by the counter-example, /// and the heap of visited states with their indexes. - class emptiness_check_status + class couvreur99_check_status { public: - emptiness_check_status(const tgba* aut, + couvreur99_check_status(const tgba* aut, const numbered_state_heap_factory* nshf); - ~emptiness_check_status(); + ~couvreur99_check_status(); const tgba* aut; scc_stack root; diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index ad5e768ac..fe589e7e2 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -26,6 +26,34 @@ namespace spot { + magic_search::result::result(magic_search& ms) + : ms_(ms) + { + } + + tgba_run* + magic_search::result::accepting_run() + { + tgba_run* run = new tgba_run; + + stack_type::const_reverse_iterator i, e = ms_.stack.rend(); + tstack_type::const_reverse_iterator ti; + tgba_run::steps* l = &run->prefix; + + for (i = ms_.stack.rbegin(), ti = ms_.tstack.rbegin(); i != e; ++i, ++ti) + { + if (i->first.s->compare(ms_.x) == 0) + l = &run->cycle; + + // FIXME: We need to keep track of the acceptance condition. + tgba_run::step s = { i->first.s->clone(), *ti, bddfalse }; + l->push_back(s); + } + + return run; + } + + magic_search::magic_search(const tgba_tba_proxy* a) : a(a), x(0) { @@ -89,7 +117,7 @@ namespace spot return false; } - bool + emptiness_check_result* magic_search::check() { if (stack.empty()) @@ -118,7 +146,7 @@ namespace spot delete s_prime; tstack.push_front(c); assert(stack.size() == tstack.size()); - return true; + return new result(*this); } if (!has(s_prime, magic)) { @@ -149,49 +177,7 @@ namespace spot } assert(tstack.empty()); - return false; - } - - std::ostream& - magic_search::print_result(std::ostream& os, const tgba* restrict) const - { - stack_type::const_reverse_iterator i; - tstack_type::const_reverse_iterator ti; - os << "Prefix:" << std::endl; - const bdd_dict* d = a->get_dict(); - for (i = stack.rbegin(), ti = tstack.rbegin(); - i != stack.rend(); ++i, ++ti) - { - if (i->first.s->compare(x) == 0) - os <<"Cycle:" <first.s; - if (restrict) - { - s = a->project_state(s, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << " " << a->format_state(s) << std::endl; - } - os << " | " << bdd_format_set(d, *ti) << std::endl; - } - - if (restrict) - { - const state* s = a->project_state(x, restrict); - assert(s); - os << " " << restrict->format_state(s) << std::endl; - delete s; - } - else - { - os << " " << a->format_state(x) << std::endl; - } - return os; + return 0; } } diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index e0e95f508..e1c17a3f3 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -27,6 +27,7 @@ #include #include #include "tgba/tgbatba.hh" +#include "emptiness.hh" namespace spot { @@ -53,11 +54,11 @@ namespace spot /// isbn = {0-444-81648-8} /// } /// \endverbatim - struct magic_search + struct magic_search : public emptiness_check { /// Initialize the Magic Search algorithm on the automaton \a a. magic_search(const tgba_tba_proxy *a); - ~magic_search(); + virtual ~magic_search(); /// \brief Perform a Magic Search. /// @@ -66,14 +67,7 @@ namespace spot /// /// check() can be called several times until it return false, /// to enumerate all accepting paths. - bool check(); - - /// \brief Print the last accepting path found. - /// - /// Restrict printed states to \a the state space of restrict if - /// supplied. - std::ostream& print_result(std::ostream& os, - const tgba* restrict = 0) const; + virtual emptiness_check_result* check(); private: @@ -116,8 +110,18 @@ namespace spot const tgba_tba_proxy* a; ///< The automata to check. /// The state for which we are currently seeking an SCC. const state* x; - }; +#ifndef SWIG + class result: public emptiness_check_result + { + public: + result(magic_search& ms); + virtual tgba_run* accepting_run(); + private: + magic_search& ms_; + }; +#endif // SWIG + }; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 316d17ed3..0c9e9c7ca 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -533,66 +533,60 @@ main(int argc, char** argv) assert(!"unknown output option"); } + spot::emptiness_check* ec = 0; + spot::tgba* ec_a = 0; switch (echeck) { case None: break; case Couvreur: + ec_a = a; + ec = new spot::couvreur99_check(a); + break; + case Couvreur2: - { - std::cout << "Tarjan Couvreur" << std::endl; - spot::emptiness_check* ec; - if (echeck == Couvreur) - ec = new spot::emptiness_check(a); - else - ec = new spot::emptiness_check_shy(a); - bool res = ec->check(); - if (expect_counter_example) - { - if (res) - { - exit_code = 1; - delete ec; - break; - } - spot::counter_example ce(ec->result()); - ce.print_result(std::cout); - ce.print_stats(std::cout); - } - else - { - exit_code = !res; - } - delete ec; - } + ec_a = a; + ec = new spot::couvreur99_check_shy(a); break; case MagicSearch: - { - std::cout << "Magic Search" << std::endl; - spot::magic_search ms(degeneralized); - bool res = ms.check(); - if (expect_counter_example) - { - if (!res) - { - exit_code = 1; - break; - } - do - ms.print_result(std::cout); - while (magic_many && ms.check()); - } - else - { - exit_code = res; - } - } + ec_a = degeneralized; + ec = new spot::magic_search(degeneralized); break; + } - default: - assert(0); + if (ec) + { + do + { + spot::emptiness_check_result* res = ec->check(); + if (expect_counter_example != !!res) + exit_code = 1; + + if (!res) + { + std::cout << "no accepting run found" << std::endl; + break; + } + else + { + + spot::tgba_run* run = res->accepting_run(); + if (!run) + { + std::cout << "an accepting run exist" << std::endl; + } + else + { + spot::print_tgba_run(std::cout, run, ec_a); + delete run; + } + } + delete res; + } + while (magic_many); + delete ec; } if (f)