diff --git a/ChangeLog b/ChangeLog index ae1ba9a6a..c087884be 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-06-03 Alexandre Duret-Lutz + + * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc, + src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc, + src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc, + src/tgba/tgbabddtranslateproxy.cc: Include . + 2003-06-02 Alexandre Duret-Lutz * src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files. @@ -92,7 +99,7 @@ not a bdd. * src/tgba/tgbabddconcrete.cc: Likewise. - Initial code for TGBA (Transition Generalized BŽüchi Automata). + Initial code for TGBA (Transition Generalized Büchi Automata). Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, a LTL-to-TGBA translator using Couvreur's algorithm. diff --git a/src/tgba/dictunion.cc b/src/tgba/dictunion.cc index 96c1c1aaf..302c8a98b 100644 --- a/src/tgba/dictunion.cc +++ b/src/tgba/dictunion.cc @@ -1,6 +1,7 @@ #include #include "dictunion.hh" #include +#include namespace spot { @@ -9,45 +10,45 @@ namespace spot tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r) { tgba_bdd_dict res; - + std::set now; std::set var; std::set prom; - + tgba_bdd_dict::fv_map::const_iterator i; - + // Merge Now variables. for (i = l.now_map.begin(); i != l.now_map.end(); ++i) now.insert(i->first); for (i = r.now_map.begin(); i != r.now_map.end(); ++i) now.insert(i->first); - + // Merge atomic propositions. for (i = l.var_map.begin(); i != l.var_map.end(); ++i) var.insert(i->first); for (i = r.var_map.begin(); i != r.var_map.end(); ++i) var.insert(i->first); - + // Merge promises. for (i = l.prom_map.begin(); i != l.prom_map.end(); ++i) prom.insert(i->first); for (i = r.prom_map.begin(); i != r.prom_map.end(); ++i) prom.insert(i->first); - + // Ensure we have enough BDD variables. int have = bdd_extvarnum(0); int want = now.size() * 2 + var.size() + prom.size(); if (have < want) bdd_setvarnum(want); - + // Fill in the "defragmented" union dictionary. - + // FIXME: Make some experiments with ordering of prom/var/now variables. // Maybe there is one order that usually produces smaller BDDs? - + // Next BDD variable to use. int v = 0; - + std::set::const_iterator f; for (f = prom.begin(); f != prom.end(); ++f) { @@ -67,7 +68,7 @@ namespace spot res.now_formula_map[v] = *f; v += 2; } - + assert (v == want); return res; } diff --git a/src/tgba/ltl2tgba.cc b/src/tgba/ltl2tgba.cc index 865a505ce..637ef9e15 100644 --- a/src/tgba/ltl2tgba.cc +++ b/src/tgba/ltl2tgba.cc @@ -1,6 +1,7 @@ #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" #include "tgbabddconcretefactory.hh" +#include #include "ltl2tgba.hh" diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 7a57b0751..42aa77cf5 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -1,4 +1,5 @@ #include "succiterconcrete.hh" +#include namespace spot { diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index d2e38c9d5..58ef6b8b6 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -1,5 +1,6 @@ #include "tgbabddconcrete.hh" #include "bddprint.hh" +#include namespace spot { diff --git a/src/tgba/tgbabddprod.cc b/src/tgba/tgbabddprod.cc index 316420e91..73b74961d 100644 --- a/src/tgba/tgbabddprod.cc +++ b/src/tgba/tgbabddprod.cc @@ -1,6 +1,7 @@ #include "tgbabddprod.hh" #include "tgbabddtranslateproxy.hh" #include "dictunion.hh" +#include namespace spot { @@ -14,7 +15,7 @@ namespace spot delete right_; } - int + int state_bdd_product::compare(const state* other) const { const state_bdd_product* o = dynamic_cast(other); @@ -33,7 +34,7 @@ namespace spot : left_(left), right_(right) { } - + void tgba_bdd_product_succ_iterator::step_() { @@ -63,7 +64,7 @@ namespace spot } } - void + void tgba_bdd_product_succ_iterator::first() { left_->first(); @@ -71,21 +72,21 @@ namespace spot next_non_false_(); } - void + void tgba_bdd_product_succ_iterator::next() { step_(); next_non_false_(); } - bool + bool tgba_bdd_product_succ_iterator::done() { return right_->done(); } - - - state_bdd* + + + state_bdd* tgba_bdd_product_succ_iterator::current_state() { state_bdd* ls = dynamic_cast(left_->current_state()); @@ -94,13 +95,13 @@ namespace spot assert(rs); return new state_bdd_product(ls, rs); } - - bdd + + bdd tgba_bdd_product_succ_iterator::current_condition() { return current_cond_; } - + bdd tgba_bdd_product_succ_iterator::current_promise() { return left_->current_promise() & right_->current_promise(); @@ -145,17 +146,17 @@ namespace spot delete right_; } - state* + state* tgba_bdd_product::get_init_state() const { state_bdd* ls = dynamic_cast(left_->get_init_state()); state_bdd* rs = dynamic_cast(right_->get_init_state()); assert(ls); assert(rs); - return new state_bdd_product(ls, rs); + return new state_bdd_product(ls, rs); } - tgba_bdd_product_succ_iterator* + tgba_bdd_product_succ_iterator* tgba_bdd_product::succ_iter(const state* state) const { const state_bdd_product* s = dynamic_cast(state); @@ -166,21 +167,21 @@ namespace spot return new tgba_bdd_product_succ_iterator(li, ri); } - const tgba_bdd_dict& + const tgba_bdd_dict& tgba_bdd_product::get_dict() const { return dict_; } - std::string + std::string tgba_bdd_product::format_state(const state* state) const { const state_bdd_product* s = dynamic_cast(state); assert(s); - return (left_->format_state(s->left()) - + " * " + return (left_->format_state(s->left()) + + " * " + right_->format_state(s->right())); } - - + + } diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index 39a407885..d0e933fbf 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -1,5 +1,6 @@ #include "tgbabddtranslatefactory.hh" #include "dictunion.hh" +#include namespace spot { diff --git a/src/tgba/tgbabddtranslateproxy.cc b/src/tgba/tgbabddtranslateproxy.cc index 44e7f2546..51d34764c 100644 --- a/src/tgba/tgbabddtranslateproxy.cc +++ b/src/tgba/tgbabddtranslateproxy.cc @@ -1,38 +1,39 @@ #include "tgbabddtranslateproxy.hh" #include "bddprint.hh" +#include namespace spot { // tgba_bdd_translate_proxy_succ_iterator // -------------------------------------- - + tgba_bdd_translate_proxy_succ_iterator:: tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it, bddPair* rewrite) : iter_(it), rewrite_(rewrite) { } - - void + + void tgba_bdd_translate_proxy_succ_iterator::first() { iter_->first(); } - - void + + void tgba_bdd_translate_proxy_succ_iterator::next() { iter_->next(); } - - bool + + bool tgba_bdd_translate_proxy_succ_iterator::done() { return iter_->done(); } - state_bdd* + state_bdd* tgba_bdd_translate_proxy_succ_iterator::current_state() { state_bdd* s = iter_->current_state(); @@ -40,13 +41,13 @@ namespace spot return s; } - bdd + bdd tgba_bdd_translate_proxy_succ_iterator::current_condition() { return bdd_replace(iter_->current_condition(), rewrite_); } - bdd + bdd tgba_bdd_translate_proxy_succ_iterator::current_promise() { return bdd_replace(iter_->current_promise(), rewrite_); @@ -56,7 +57,7 @@ namespace spot // tgba_bdd_translate_proxy // ------------------------ - tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from, + tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from, const tgba_bdd_dict& to) : from_(from), to_(to) { @@ -97,8 +98,8 @@ namespace spot bdd_freepair(rewrite_from_); bdd_freepair(rewrite_to_); } - - state_bdd* + + state_bdd* tgba_bdd_translate_proxy::get_init_state() const { state_bdd* s = dynamic_cast(from_.get_init_state()); @@ -107,24 +108,24 @@ namespace spot return s; } - tgba_bdd_translate_proxy_succ_iterator* + tgba_bdd_translate_proxy_succ_iterator* tgba_bdd_translate_proxy::succ_iter(const state* state) const { const state_bdd* s = dynamic_cast(state); assert(s); - state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_)); - tgba_succ_iterator_concrete* it = + state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_)); + tgba_succ_iterator_concrete* it = dynamic_cast(from_.succ_iter(&s2)); assert(it); return new tgba_bdd_translate_proxy_succ_iterator(it, rewrite_to_); } - const tgba_bdd_dict& + const tgba_bdd_dict& tgba_bdd_translate_proxy::get_dict() const { return to_; } - + std::string tgba_bdd_translate_proxy::format_state(const state* state) const {