diff --git a/ChangeLog b/ChangeLog index 52101a242..cc7d469b3 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2003-07-25 Alexandre Duret-Lutz + * src/tgba/tgba.hh (tgba::~tgba): Make it public. + * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files. + * src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh. + (libtgba_la_SOURCES): Add tgbatba.cc. + * src/tgbatest/ltl2tgba.cc: Add option -D. + * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... * src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 604b4e5e1..284f67a64 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -18,7 +18,8 @@ tgba_HEADERS = \ tgbabddcoredata.hh \ tgbabddfactory.hh \ tgbaexplicit.hh \ - tgbaproduct.hh + tgbaproduct.hh \ + tgbatba.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -32,4 +33,5 @@ libtgba_la_SOURCES = \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ tgbaexplicit.cc \ - tgbaproduct.cc + tgbaproduct.cc \ + tgbatba.cc diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 4dc64bbdc..7fad18bdd 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -33,9 +33,10 @@ namespace spot { protected: tgba(); - virtual ~tgba(); public: + virtual ~tgba(); + /// \brief Get the initial state of the automaton. /// /// The state has been allocated with \c new. It is the diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc new file mode 100644 index 000000000..862d2ad20 --- /dev/null +++ b/src/tgba/tgbatba.cc @@ -0,0 +1,253 @@ +#include +#include "tgbatba.hh" +#include "bddprint.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + + /// \brief A state for spot::tgba_tba_proxy. + /// + /// This state is in fact a pair of state: the state from the tgba + /// automaton, and the "counter" (we use the accepting set + /// BDD variable instead of an integer counter). + class state_tba_proxy : public state + { + public: + state_tba_proxy(state* s, bdd acc) + : s_(s), acc_(acc) + { + } + + /// Copy constructor + state_tba_proxy(const state_tba_proxy& o) + : state(), + s_(o.real_state()->clone()), + acc_(o.accepting_cond()) + { + } + + virtual + ~state_tba_proxy() + { + delete s_; + } + + state* + real_state() const + { + return s_; + } + + bdd + accepting_cond() const + { + return acc_; + } + + virtual int + compare(const state* other) const + { + const state_tba_proxy* o = dynamic_cast(other); + assert(o); + int res = s_->compare(o->real_state()); + if (res != 0) + return res; + return acc_.id() - o->accepting_cond().id(); + } + + virtual + state_tba_proxy* clone() const + { + return new state_tba_proxy(*this); + } + + private: + state* s_; + bdd acc_; + }; + + + /// \brief Iterate over the successors of tgba_tba_proxy computed on the fly. + class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator + { + public: + tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it, + bdd acc, bdd next_acc, + bdd the_accepting_cond) + : it_(it), acc_(acc), next_acc_(next_acc), + the_accepting_cond_(the_accepting_cond) + { + } + + virtual + ~tgba_tba_proxy_succ_iterator() + { + } + + // iteration + + void + first() + { + it_->first(); + } + + void + next() + { + it_->next(); + } + + bool + done() const + { + return it_->done(); + } + + // inspection + + state_tba_proxy* + current_state() const + { + state* s = it_->current_state(); + bdd acc; + // Transition in the ACC_ accepting set should be directed + // to the NEXT_ACC_ accepting set. + if (acc_ == bddtrue + || (acc_ & it_->current_accepting_conditions()) == acc_) + acc = next_acc_; + else + acc = acc_; + return new state_tba_proxy(s, acc); + } + + bdd + current_condition() const + { + return it_->current_condition(); + } + + bdd + current_accepting_conditions() const + { + return the_accepting_cond_; + } + + protected: + tgba_succ_iterator* it_; + bdd acc_; + bdd next_acc_; + bdd the_accepting_cond_; + }; + + + tgba_tba_proxy::tgba_tba_proxy(const tgba* a) + : a_(a) + { + bdd all = a_->all_accepting_conditions(); + + // We will use one accepting condition for this automata. + // Let's call it Acc[True]. + int v = get_dict() + ->register_accepting_variable(ltl::constant::true_instance(), this); + the_accepting_cond_ = bdd_ithvar(v); + + // Now build the "cycle" of accepting conditions. + + bdd last = bdd_satone(all); + all &= !last; + + acc_cycle_[bddtrue] = last; + + while (all != bddfalse) + { + bdd next = bdd_satone(all); + all &= !next; + acc_cycle_[last] = next; + last = next; + } + + acc_cycle_[last] = bddtrue; + } + + tgba_tba_proxy::~tgba_tba_proxy() + { + get_dict()->unregister_all_my_variables(this); + } + + state* + tgba_tba_proxy::get_init_state() const + { + cycle_map::const_iterator i = acc_cycle_.find(bddtrue); + assert(i != acc_cycle_.end()); + return new state_tba_proxy(a_->get_init_state(), i->second); + } + + tgba_succ_iterator* + tgba_tba_proxy::succ_iter(const state* local_state, + const state* global_state, + const tgba* global_automaton) const + { + const state_tba_proxy* s = + dynamic_cast(local_state); + assert(s); + + tgba_succ_iterator* it = a_->succ_iter(s->real_state(), + global_state, global_automaton); + bdd acc = s->accepting_cond(); + cycle_map::const_iterator i = acc_cycle_.find(acc); + assert(i != acc_cycle_.end()); + return + new tgba_tba_proxy_succ_iterator(it, acc, i->second, + (acc == bddtrue) + ? the_accepting_cond_ : bddfalse); + } + + bdd_dict* + tgba_tba_proxy::get_dict() const + { + return a_->get_dict(); + } + + std::string + tgba_tba_proxy::format_state(const state* state) const + { + const state_tba_proxy* s = + dynamic_cast(state); + assert(s); + return a_->format_state(s->real_state()) + "(" + + bdd_format_set(get_dict(), s->accepting_cond()) + ")"; + } + + bdd + tgba_tba_proxy::all_accepting_conditions() const + { + return the_accepting_cond_; + } + + bdd + tgba_tba_proxy::neg_accepting_conditions() const + { + return !the_accepting_cond_; + } + + bdd + tgba_tba_proxy::compute_support_conditions(const state* state) const + { + const state_tba_proxy* s = + dynamic_cast(state); + assert(s); + return a_->support_conditions(s->real_state()); + } + + bdd + tgba_tba_proxy::compute_support_variables(const state* state) const + { + const state_tba_proxy* s = + dynamic_cast(state); + assert(s); + return a_->support_variables(s->real_state()); + } + +} diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh new file mode 100644 index 000000000..825bec6c2 --- /dev/null +++ b/src/tgba/tgbatba.hh @@ -0,0 +1,62 @@ +#ifndef SPOT_TGBA_TGBATBA_HH +# define SPOT_TGBA_TGBATBA_HH + +#include "tgba.hh" +#include "misc/bddlt.hh" + +namespace spot +{ + + /// \brief Degeneralize a spot::tgba on the fly. + /// + /// This class acts as a proxy in front of a spot::tgba, that should + /// be degeneralized on the fly. + /// + /// This automaton is a spot::tgba, but it will always have exactly + /// one accepting condition. + /// + /// The degeneralization is done by synchronizing the input + /// automaton with a "counter" automaton such as the one shown in + /// "On-the-fly Verification of Linear Temporal Logic" (Jean-Michel + /// Couveur, FME99). + /// + /// If the input automaton uses N accepting conditions, the output + /// automaton can have at most max(N,1)+1 times more states and + /// transitions. + class tgba_tba_proxy : public tgba + { + public: + tgba_tba_proxy(const tgba* a); + + virtual ~tgba_tba_proxy(); + + virtual state* get_init_state() const; + + virtual tgba_succ_iterator* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; + + virtual bdd_dict* get_dict() const; + + virtual std::string format_state(const state* state) const; + + virtual bdd all_accepting_conditions() const; + virtual bdd neg_accepting_conditions() const; + + protected: + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + + private: + const tgba* a_; + typedef std::map cycle_map; + cycle_map acc_cycle_; + bdd the_accepting_cond_; + // Disallow copy. + tgba_tba_proxy(const tgba_tba_proxy&); + tgba_tba_proxy& tgba_tba_proxy::operator=(const tgba_tba_proxy&); + }; + +} +#endif // SPOT_TGBA_TGBATBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 95e818ef1..9b681af77 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -7,6 +7,7 @@ #include "tgba/bddprint.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgba/tgbatba.hh" void syntax(char* prog) @@ -18,6 +19,7 @@ syntax(char* prog) << std::endl << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl + << " -D degeneralize the automaton" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl @@ -33,6 +35,7 @@ main(int argc, char** argv) int exit_code = 0; bool debug_opt = false; + bool degeneralize_opt = false; int output = 0; int formula_index = 0; @@ -55,6 +58,10 @@ main(int argc, char** argv) { debug_opt = true; } + else if (!strcmp(argv[formula_index], "-D")) + { + degeneralize_opt = true; + } else if (!strcmp(argv[formula_index], "-r")) { output = 1; @@ -88,28 +95,34 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); if (f) { - spot::tgba_bdd_concrete* a = spot::ltl_to_tgba(f, dict); + spot::tgba_bdd_concrete* concrete = spot::ltl_to_tgba(f, dict); + spot::tgba* a = concrete; spot::ltl::destroy(f); + + spot::tgba* degeneralized = 0; + if (degeneralize_opt) + a = degeneralized = new spot::tgba_tba_proxy(a); + switch (output) { case 0: spot::dotty_reachable(std::cout, a); break; case 1: - spot::bdd_print_dot(std::cout, a->get_dict(), - a->get_core_data().relation); + spot::bdd_print_dot(std::cout, concrete->get_dict(), + concrete->get_core_data().relation); break; case 2: - spot::bdd_print_dot(std::cout, a->get_dict(), - a->get_core_data().accepting_conditions); + spot::bdd_print_dot(std::cout, concrete->get_dict(), + concrete->get_core_data().accepting_conditions); break; case 3: - spot::bdd_print_set(std::cout, a->get_dict(), - a->get_core_data().relation); + spot::bdd_print_set(std::cout, concrete->get_dict(), + concrete->get_core_data().relation); break; case 4: - spot::bdd_print_set(std::cout, a->get_dict(), - a->get_core_data().accepting_conditions); + spot::bdd_print_set(std::cout, concrete->get_dict(), + concrete->get_core_data().accepting_conditions); break; case 5: a->get_dict()->dump(std::cout); @@ -120,7 +133,11 @@ main(int argc, char** argv) default: assert(!"unknown output option"); } - delete a; + + if (degeneralize_opt) + delete degeneralized; + + delete concrete; } else {