diff --git a/ChangeLog b/ChangeLog index 925f787da..fb4e8a348 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,27 @@ +2003-05-26 Alexandre Duret-Lutz + + 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. + + * src/Makefile.am (SUBDIRS): Add tgba. + (libspot_la_LIBADD): Add tgba/libtgba.la. + * src/tgba/Makefile.am, src/tgba/bddfactory.cc, + src/tgba/bddfactory.hh, src/tgba/dictunion.cc, + src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh, + src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh, + src/tgba/succiter.hh, src/tgba/succiterconcrete.cc, + src/tgba/succiterconcrete.hh, src/tgba/succlist.hh, + src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc, + src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc, + src/tgba/tgbabddconcretefactory.hh, + src/tgba/tgbabddconcreteproduct.cc, + src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc, + src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc, + src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh, + src/tgba/tgbabddtranslatefactory.cc, + src/tgba/tgbabddtranslatefactory.hh: New files. + 2003-05-23 Alexandre Duret-Lutz * m4/gccwarn.m4: Do not use -Winline, this is inappropriate diff --git a/configure.ac b/configure.ac index 58a985961..c792f2b8f 100644 --- a/configure.ac +++ b/configure.ac @@ -31,6 +31,7 @@ AC_CONFIG_FILES([ src/ltltest/Makefile src/ltltest/defs src/ltlvisit/Makefile + src/tgba/Makefile src/misc/Makefile wrap/Makefile ]) diff --git a/src/Makefile.am b/src/Makefile.am index 51a4e9328..dfe45f213 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,7 +1,7 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse ltltest +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse ltltest tgba lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -9,4 +9,5 @@ libspot_la_LIBADD = \ ltlenv/libltlenv.la \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ - ltlast/libltlast.la + ltlast/libltlast.la \ + tgba/libtgba.la diff --git a/src/tgba/.cvsignore b/src/tgba/.cvsignore new file mode 100644 index 000000000..799fc9785 --- /dev/null +++ b/src/tgba/.cvsignore @@ -0,0 +1,6 @@ +.deps +.libs +*.lo +*.la +Makefile +Makefile.in diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am new file mode 100644 index 000000000..febfde8df --- /dev/null +++ b/src/tgba/Makefile.am @@ -0,0 +1,31 @@ +AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +noinst_LTLIBRARIES = libtgba.la +libtgba_la_SOURCES = \ + bddfactory.cc \ + bddfactory.hh \ + dictunion.cc \ + dictunion.hh \ + ltl2tgba.cc \ + ltl2tgba.hh \ + state.hh \ + statebdd.cc \ + statebdd.hh \ + succiter.hh \ + succiterconcrete.cc \ + succiterconcrete.hh \ + tgba.hh \ + tgbabddconcrete.cc \ + tgbabddconcrete.hh \ + tgbabddconcretefactory.cc \ + tgbabddconcretefactory.hh \ + tgbabddconcreteproduct.cc \ + tgbabddconcreteproduct.hh \ + tgbabddcoredata.cc \ + tgbabddcoredata.hh \ + tgbabdddict.cc \ + tgbabdddict.hh \ + tgbabddfactory.hh \ + tgbabddtranslatefactory.cc \ + tgbabddtranslatefactory.hh diff --git a/src/tgba/bddfactory.cc b/src/tgba/bddfactory.cc new file mode 100644 index 000000000..5bef3476f --- /dev/null +++ b/src/tgba/bddfactory.cc @@ -0,0 +1,48 @@ +#include "bddfactory.hh" + +namespace spot +{ + bdd_factory::bdd_factory() + : varused(0) + { + initialize(); + } + + int + bdd_factory::create_node() + { + return create_nodes(1); + } + + int + bdd_factory::create_pair() + { + return create_nodes(2); + } + + int + bdd_factory::create_nodes(int i) + { + int res = varused; + varused += i; + if (varnum < varused) + { + bdd_extvarnum(varused - varnum); + varnum = varused; + } + return res; + } + + void + bdd_factory::initialize() + { + if (initialized) + return; + initialized = true; + bdd_init(50000, 5000); + bdd_setvarnum(varnum); + } + + bool bdd_factory::initialized = false; + int bdd_factory::varnum = 2; +} diff --git a/src/tgba/bddfactory.hh b/src/tgba/bddfactory.hh new file mode 100644 index 000000000..29b504b08 --- /dev/null +++ b/src/tgba/bddfactory.hh @@ -0,0 +1,33 @@ +#ifndef SPOT_TGBA_BDDFACTORY_HH +# define SPOT_TGBA_BDDFACTORY_HH + +#include + +namespace spot +{ + + class bdd_factory + { + public: + bdd_factory(); + + int create_node(); + int create_pair(); + + static bdd + ithvar(int i) + { + return bdd_ithvar(i); + } + + protected: + static void initialize(); + int create_nodes(int i); + + static bool initialized; + static int varnum; + int varused; + }; +} + +#endif // SPOT_TGBA_BDDFACTORY_HH diff --git a/src/tgba/dictunion.cc b/src/tgba/dictunion.cc new file mode 100644 index 000000000..96c1c1aaf --- /dev/null +++ b/src/tgba/dictunion.cc @@ -0,0 +1,75 @@ +#include +#include "dictunion.hh" +#include + +namespace spot +{ + + tgba_bdd_dict + 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) + { + res.prom_map[*f] = v; + res.prom_formula_map[v] = *f; + ++v; + } + for (f = var.begin(); f != var.end(); ++f) + { + res.var_map[*f] = v; + res.var_formula_map[v] = *f; + ++v; + } + for (f = now.begin(); f != now.end(); ++f) + { + res.now_map[*f] = v; + res.now_formula_map[v] = *f; + v += 2; + } + + assert (v == want); + return res; + } + +} diff --git a/src/tgba/dictunion.hh b/src/tgba/dictunion.hh new file mode 100644 index 000000000..159db3d2d --- /dev/null +++ b/src/tgba/dictunion.hh @@ -0,0 +1,12 @@ +#ifndef SPOT_TGBA_DICTUNION_HH +# define SPOT_TGBA_DICTUNION_HH + +#include "tgbabdddict.hh" + +namespace spot +{ + tgba_bdd_dict + tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r); +} + +#endif // SPOT_TGBA_DICTUNION_HH diff --git a/src/tgba/ltl2tgba.cc b/src/tgba/ltl2tgba.cc new file mode 100644 index 000000000..9bd46371f --- /dev/null +++ b/src/tgba/ltl2tgba.cc @@ -0,0 +1,183 @@ +#include "ltlast/visitor.hh" +#include "ltlast/allnodes.hh" +#include "tgbabddconcretefactory.hh" + +#include "ltl2tgba.hh" +// FIXME: Add ref to Couvreur's paper. + +namespace spot +{ + using namespace ltl; + class ltl_trad_visitor: public const_visitor + { + public: + ltl_trad_visitor(tgba_bdd_concrete_factory& fact) + : fact_(fact) + { + } + + virtual + ~ltl_trad_visitor() + { + } + + bdd + result() + { + return res_; + } + + void + visit(const atomic_prop* node) + { + res_ = fact_.ithvar(fact_.create_atomic_prop(node)); + } + + void + visit(const constant* node) + { + switch (node->val()) + { + case constant::True: + res_ = bddtrue; + return; + case constant::False: + res_ = bddfalse; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const unop* node) + { + switch (node->op()) + { + case unop::F: + case unop::G: + // FIXME: We can normalize on the fly, here. + assert(!"unexpected operator, normalize first"); + case unop::Not: + res_ = bdd_not(recurse(node->child())); + return; + case unop::X: + // FIXME: Can be smarter on X(a U b) and X(a R b). + int v = fact_.create_state(node->child()); + bdd now = fact_.ithvar(v); + bdd next = fact_.ithvar(v + 1); + fact_.add_relation(bdd_apply(now, recurse(node->child()), + bddop_biimp)); + res_ = next; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const binop* node) + { + bdd f1 = recurse(node->first()); + bdd f2 = recurse(node->second()); + + switch (node->op()) + { + case binop::Xor: + res_ = bdd_apply(f1, f2, bddop_xor); + return; + case binop::Implies: + res_ = bdd_apply(f1, f2, bddop_imp); + return; + case binop::Equiv: + res_ = bdd_apply(f1, f2, bddop_biimp); + return; + case binop::U: + { + int v = fact_.create_state(node); + bdd now = fact_.ithvar(v); + bdd next = fact_.ithvar(v + 1); + + bdd promise_f2 = + fact_.ithvar(fact_.create_promise(node->second())); + /* + f1 U f2 <=> f2 | (f1 & X(f1 U f2)) + In other words: + now <=> f2 | (f1 & next) + + The rightmost conjunction, f1 & next, doesn't actually + encodes the fact that f2 should be fulfilled at some + point. We use the `promise_f2' variable for this purpose. + */ + fact_.add_relation(bdd_apply(now, + f2 | (promise_f2 & f1 & next), + bddop_biimp)); + res_ = now; + return; + } + case binop::R: + { + int v = fact_.create_state(node); + bdd now = fact_.ithvar(v); + bdd next = fact_.ithvar(v + 1); + /* + f1 R f2 <=> f2 & (f1 | X(f1 U f2)) + In other words: + now <=> f2 & (f1 | next) + */ + fact_.add_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp)); + res_ = now; + return; + } + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const multop* node) + { + int op = -1; + switch (node->op()) + { + case multop::And: + op = bddop_and; + res_ = bddtrue; + break; + case multop::Or: + op = bddop_or; + res_ = bddfalse; + break; + } + assert(op != -1); + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + { + res_ = bdd_apply(res_, recurse(node->nth(n)), op); + } + } + + bdd + recurse(const formula* f) + { + ltl_trad_visitor v(*this); + f->accept(v); + return v.result(); + } + + private: + bdd res_; + tgba_bdd_concrete_factory& fact_; + }; + + tgba_bdd_concrete + ltl_to_tgba(const formula* f) + { + tgba_bdd_concrete_factory fact; + ltl_trad_visitor v(fact); + f->accept(v); + tgba_bdd_concrete g(fact); + g.set_init_state(v.result()); + return g; + } +} diff --git a/src/tgba/ltl2tgba.hh b/src/tgba/ltl2tgba.hh new file mode 100644 index 000000000..b2c25c8de --- /dev/null +++ b/src/tgba/ltl2tgba.hh @@ -0,0 +1,13 @@ +#ifndef SPOT_TGBA_LTL2TGBA_HH +# define SPOT_TGBA_LTL2TGBA_HH + +#include "ltlast/formula.hh" +#include "tgbabddconcrete.hh" + +namespace spot +{ + tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f); +} + +#endif // SPOT_TGBA_LTL2TGBA_HH + diff --git a/src/tgba/state.hh b/src/tgba/state.hh new file mode 100644 index 000000000..1de81eb95 --- /dev/null +++ b/src/tgba/state.hh @@ -0,0 +1,25 @@ +#ifndef SPOT_TGBA_STATE_HH +# define SPOT_TGBA_STATE_HH + +namespace spot +{ + class state + { + public: + // Compares two states (that come from the same automaton). + // + // This method returns an integer less than, equal to, or greater + // than zero if THIS is found, respectively, to be less than, equal + // to, or greater than OTHER according to some implicit total order. + // + // This method should not be called to compare state from + // different automata. + virtual int compare(const state& other) const = 0; + + virtual ~state() + { + } + }; +} + +#endif // SPOT_TGBA_STATE_HH diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc new file mode 100644 index 000000000..eea428255 --- /dev/null +++ b/src/tgba/statebdd.cc @@ -0,0 +1,16 @@ +#include "statebdd.hh" +#include + +namespace spot +{ + int + state_bdd::compare(const state& other) const + { + // This method should not be called to compare states from different + // automata, and all states from the same automaton will use the same + // state class. + const state_bdd* o = dynamic_cast(&other); + assert(o); + return o->as_bdd().id() - state_.id(); + } +} diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh new file mode 100644 index 000000000..e5e0ab431 --- /dev/null +++ b/src/tgba/statebdd.hh @@ -0,0 +1,30 @@ +#ifndef SPOT_TGBA_STATEBDD_HH +# define SPOT_TGBA_STATEBDD_HH + +#include +#include "state.hh" + +namespace spot +{ + class state_bdd: public state + { + public: + state_bdd(bdd s) + : state_(s) + { + } + + bdd + as_bdd() const + { + return state_; + } + + virtual int compare(const state& other) const; + + protected: + bdd state_; + }; +} + +#endif // SPOT_TGBA_STATEBDD_HH diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh new file mode 100644 index 000000000..71a242b4b --- /dev/null +++ b/src/tgba/succiter.hh @@ -0,0 +1,31 @@ +#ifndef SPOT_TGBA_SUCCITER_H +# define SPOT_TGBA_SUCCITER_H + +#include "statebdd.hh" + +namespace spot +{ + + class tgba_succ_iterator + { + public: + virtual + ~tgba_succ_iterator() + { + } + + // iteration + virtual void first() = 0; + virtual void next() = 0; + virtual bool done() = 0; + + // inspection + virtual state_bdd current_state() = 0; + virtual bdd current_condition() = 0; + virtual bdd current_promise() = 0; + }; + +} + + +#endif // SPOT_TGBA_SUCCITER_H diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc new file mode 100644 index 000000000..6a882848f --- /dev/null +++ b/src/tgba/succiterconcrete.cc @@ -0,0 +1,64 @@ +#include "succiterconcrete.hh" + +namespace spot +{ + tgba_succ_iterator_concrete::tgba_succ_iterator_concrete + (const tgba_bdd_core_data& d, bdd successors) + : data_(d), succ_set_(successors), next_succ_set_(successors), + current_(bddfalse) + { + } + + tgba_succ_iterator_concrete::~tgba_succ_iterator_concrete() + { + } + + void + tgba_succ_iterator_concrete::first() + { + next_succ_set_ = succ_set_; + if (!done()) + next(); + } + + void + tgba_succ_iterator_concrete::next() + { + assert(!done()); + + // FIXME: Iterating on the successors this way (calling bdd_satone + // and NANDing out the result from the set) requires several descent + // of the BDD. Maybe it would be faster to compute all satisfying + // formula in one operation. + next_succ_set_ &= !current_; + current_ = bdd_satone(next_succ_set_); + } + + bool + tgba_succ_iterator_concrete::done() + { + return next_succ_set_ == bddfalse; + } + + state_bdd + tgba_succ_iterator_concrete::current_state() + { + assert(!done()); + return bdd_exist(current_, data_.notnow_set); + } + + bdd + tgba_succ_iterator_concrete::current_condition() + { + assert(!done()); + return bdd_exist(current_, data_.notvar_set); + } + + bdd + tgba_succ_iterator_concrete::current_promise() + { + assert(!done()); + return bdd_exist(current_, data_.notprom_set); + } + +} diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh new file mode 100644 index 000000000..8620575e6 --- /dev/null +++ b/src/tgba/succiterconcrete.hh @@ -0,0 +1,33 @@ +#ifndef SPOT_TGBA_SUCCITERCONCRETE_HH +# define SPOT_TGBA_SUCCITERCONCRETE_HH + +#include "succiter.hh" +#include "tgbabddcoredata.hh" + +namespace spot +{ + class tgba_succ_iterator_concrete: public tgba_succ_iterator + { + public: + tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors); + virtual ~tgba_succ_iterator_concrete(); + + // iteration + void first(); + void next(); + bool done(); + + // inspection + state_bdd current_state(); + bdd current_condition(); + bdd current_promise(); + + private: + const tgba_bdd_core_data& data_; + bdd succ_set_; // The set of successors. + bdd next_succ_set_; // Unexplored successors (including current_). + bdd current_; // Current successor. + }; +} + +#endif // SPOT_TGBA_SUCCITERCONCRETE_HH diff --git a/src/tgba/succlist.hh b/src/tgba/succlist.hh new file mode 100644 index 000000000..b3ae8a2b2 --- /dev/null +++ b/src/tgba/succlist.hh @@ -0,0 +1,15 @@ +#ifndef SPOT_WAUTO_SUCCLIST_HH +# define SPOT_WAUTO_SUCCLIST_HH + +namespace spot +{ + + struct successor_list + { + virtual + + }; + +} + +#endif SPOT_WAUTO_SUCCLIST_HH diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh new file mode 100644 index 000000000..7232ea142 --- /dev/null +++ b/src/tgba/tgba.hh @@ -0,0 +1,8 @@ +#ifndef SPOT_TGBA_TGBA_HH +# define SPOT_TGBA_TGBA_HH + +# include "tgbabddconcrete.hh" +# include "tgbabddconcreteproduct.hh" +# include "ltl2tgba.hh" + +#endif // SPOT_TGBA_TGBA_HH diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc new file mode 100644 index 000000000..bc3064e6e --- /dev/null +++ b/src/tgba/tgbabddconcrete.cc @@ -0,0 +1,58 @@ +#include "tgbabddconcrete.hh" + +namespace spot +{ + tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact) + : data_(fact.get_core_data()), dict_(fact.get_dict()) + { + } + + tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) + : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init) + { + } + + tgba_bdd_concrete::~tgba_bdd_concrete() + { + } + + void + tgba_bdd_concrete::set_init_state(bdd s) + { + init_ = s; + } + + state_bdd + tgba_bdd_concrete::get_init_state() const + { + return init_; + } + + tgba_succ_iterator_concrete* + tgba_bdd_concrete::succ_iter(bdd state) const + { + bdd succ_set = bdd_replace(bdd_exist(data_.relation & state, + data_.now_set), + data_.next_to_now); + return new tgba_succ_iterator_concrete(data_, succ_set); + } + + tgba_succ_iterator_concrete* + tgba_bdd_concrete::init_iter() const + { + return new tgba_succ_iterator_concrete(data_, init_); + } + + const tgba_bdd_dict& + tgba_bdd_concrete::get_dict() const + { + return dict_; + } + + const tgba_bdd_core_data& + tgba_bdd_concrete::get_core_data() const + { + return data_; + } + +} diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh new file mode 100644 index 000000000..5417daefd --- /dev/null +++ b/src/tgba/tgbabddconcrete.hh @@ -0,0 +1,34 @@ +#ifndef SPOT_TGBA_TGBABDDCONCRETE_HH +# define SPOT_TGBA_TGBABDDCONCRETE_HH + +#include "statebdd.hh" +#include "tgbabddfactory.hh" +#include "succiterconcrete.hh" + +namespace spot +{ + class tgba_bdd_concrete + { + public: + tgba_bdd_concrete(const tgba_bdd_factory& fact); + tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init); + ~tgba_bdd_concrete(); + + void set_init_state(bdd s); + state_bdd get_init_state() const; + + tgba_succ_iterator_concrete* succ_iter(bdd state) const; + tgba_succ_iterator_concrete* init_iter() const; + + const tgba_bdd_dict& get_dict() const; + const tgba_bdd_core_data& get_core_data() const; + + protected: + tgba_bdd_core_data data_; + tgba_bdd_dict dict_; + bdd init_; + friend class tgba_tgba_succ_iterator; + }; +} + +#endif // SPOT_TGBA_TGBABDDCONCRETE_HH diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc new file mode 100644 index 000000000..a60ce8056 --- /dev/null +++ b/src/tgba/tgbabddconcretefactory.cc @@ -0,0 +1,84 @@ +#include "tgbabddconcretefactory.hh" + +namespace spot +{ + tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory() + { + } + + int + tgba_bdd_concrete_factory::create_state(const ltl::formula* f) + { + // Do not build a state that already exists. + tgba_bdd_dict::fv_map::iterator sii = dict_.now_map.find(f); + if (sii != dict_.now_map.end()) + return sii->second; + + int num = create_pair(); + + dict_.now_map[f] = num; + dict_.now_formula_map[num] = f; + + // Record that num+1 should be renamed as num when + // the next state becomes current. + bdd_setpair(data_.next_to_now, num + 1, num); + + // Keep track of all "Now" variables for easy + // existential quantification. + data_.declare_now_next (ithvar(num), ithvar(num + 1)); + return num; + } + + int + tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) + { + // Do not build a variable that already exists. + tgba_bdd_dict::fv_map::iterator sii = dict_.var_map.find(f); + if (sii != dict_.var_map.end()) + return sii->second; + + int num = create_node(); + dict_.var_map[f] = num; + dict_.var_formula_map[num] = f; + + // Keep track of all atomic proposition for easy + // existential quantification. + data_.declare_atomic_prop(ithvar(num)); + return num; + } + + int + tgba_bdd_concrete_factory::create_promise(const ltl::formula* f) + { + // Do not build a promise that already exists. + tgba_bdd_dict::fv_map::iterator sii = dict_.prom_map.find(f); + if (sii != dict_.prom_map.end()) + return sii->second; + + int num = create_node(); + dict_.prom_map[f] = num; + dict_.prom_formula_map[num] = f; + + // Keep track of all promises for easy existential quantification. + data_.declare_promise(ithvar(num)); + return num; + } + + const tgba_bdd_core_data& + tgba_bdd_concrete_factory::get_core_data() const + { + return data_; + } + + const tgba_bdd_dict& + tgba_bdd_concrete_factory::get_dict() const + { + return dict_; + } + + void + tgba_bdd_concrete_factory::add_relation(bdd new_rel) + { + data_.relation &= new_rel; + } +} diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh new file mode 100644 index 000000000..a47458f62 --- /dev/null +++ b/src/tgba/tgbabddconcretefactory.hh @@ -0,0 +1,31 @@ +#ifndef SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH +# define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH + +#include "ltlast/formula.hh" +#include "bddfactory.hh" +#include "tgbabddfactory.hh" + +namespace spot +{ + + class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory + { + public: + virtual ~tgba_bdd_concrete_factory(); + + int create_state(const ltl::formula* f); + int create_atomic_prop(const ltl::formula* f); + int create_promise(const ltl::formula* f); + + const tgba_bdd_core_data& get_core_data() const; + const tgba_bdd_dict& get_dict() const; + + void add_relation(bdd new_rel); + + private: + tgba_bdd_core_data data_; + tgba_bdd_dict dict_; + }; + +} +#endif // SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc new file mode 100644 index 000000000..1c08b1e43 --- /dev/null +++ b/src/tgba/tgbabddconcreteproduct.cc @@ -0,0 +1,59 @@ +#include "tgbabddconcreteproduct.hh" +#include "tgbabddtranslatefactory.hh" +#include "dictunion.hh" + +namespace spot +{ + class tgba_bdd_product_factory: public tgba_bdd_factory + { + public: + tgba_bdd_product_factory(const tgba_bdd_concrete& left, + const tgba_bdd_concrete& right) + : dict_(tgba_bdd_dict_union(left.get_dict(), + right.get_dict())), + fact_left_(left, dict_), + fact_right_(right, dict_), + data_(fact_left_.get_core_data(), fact_right_.get_core_data()), + init_(fact_left_.get_init_state() & fact_right_.get_init_state()) + { + } + + virtual + ~tgba_bdd_product_factory() + { + } + + const tgba_bdd_core_data& + get_core_data() const + { + return data_; + } + + const tgba_bdd_dict& + get_dict() const + { + return dict_; + } + + bdd + get_init_state() const + { + return init_; + } + + private: + tgba_bdd_dict dict_; + tgba_bdd_translate_factory fact_left_; + tgba_bdd_translate_factory fact_right_; + tgba_bdd_core_data data_; + bdd init_; + }; + + tgba_bdd_concrete + product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right) + { + + tgba_bdd_product_factory p(left, right); + return tgba_bdd_concrete(p, p.get_init_state()); + } +} diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh new file mode 100644 index 000000000..1d8625c11 --- /dev/null +++ b/src/tgba/tgbabddconcreteproduct.hh @@ -0,0 +1,12 @@ +#ifndef SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH +# define SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH + +#include "tgbabddconcrete.hh" + +namespace spot +{ + tgba_bdd_concrete + product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right); +} + +#endif // SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc new file mode 100644 index 000000000..68972794b --- /dev/null +++ b/src/tgba/tgbabddcoredata.cc @@ -0,0 +1,74 @@ +#include "tgbabddcoredata.hh" + +namespace spot +{ + tgba_bdd_core_data::tgba_bdd_core_data() + : relation(bddtrue), + now_set(bddtrue), negnow_set(bddtrue), notnow_set(bddtrue), + notvar_set(bddtrue), notprom_set(bddtrue), next_to_now(bdd_newpair()) + { + } + + tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy) + : relation(copy.relation), + now_set(copy.now_set), negnow_set(copy.negnow_set), + notnow_set(copy.notnow_set), notvar_set(copy.notvar_set), + notprom_set(copy.notprom_set), + next_to_now(bdd_copypair(copy.next_to_now)) + { + } + + // Merge two core_data. + tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& left, + const tgba_bdd_core_data& right) + : relation(left.relation & right.relation), + now_set(left.now_set & right.now_set), + negnow_set(left.negnow_set & right.negnow_set), + notnow_set(left.notnow_set & right.notnow_set), + notvar_set(left.notvar_set & right.notvar_set), + notprom_set(left.notprom_set & right.notprom_set), + next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now)) + { + } + + const tgba_bdd_core_data& + tgba_bdd_core_data::operator= (const tgba_bdd_core_data& copy) + { + if (this != ©) + { + this->~tgba_bdd_core_data(); + new (this) tgba_bdd_core_data(copy); + } + return *this; + } + + tgba_bdd_core_data::~tgba_bdd_core_data() + { + bdd_freepair(next_to_now); + } + + void + tgba_bdd_core_data::declare_now_next(bdd now, bdd next) + { + now_set &= now; + negnow_set &= !now; + notnow_set &= next; + bdd both = now & next; + notvar_set &= both; + notprom_set &= both; + } + + void + tgba_bdd_core_data::declare_atomic_prop(bdd var) + { + notnow_set &= var; + notprom_set &= var; + } + + void + tgba_bdd_core_data::declare_promise(bdd prom) + { + notnow_set &= prom; + notvar_set &= prom; + } +} diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh new file mode 100644 index 000000000..08a35ef94 --- /dev/null +++ b/src/tgba/tgbabddcoredata.hh @@ -0,0 +1,54 @@ +#ifndef SPOT_TGBA_TGBABDDCOREDATA_HH +# define SPOT_TGBA_TGBABDDCOREDATA_HH + +#include + +namespace spot +{ + struct tgba_bdd_core_data + { + // RELATION encodes the transition relation of the TGBA. + // It uses four kinds of variables: + // - "Now" variables, that encode the current state + // - "Next" variables, that encode the destination state + // - atomic propositions, which are things to verify before going on + // to the next state + // - promises: a U b, or F b, both implie that b should be verified + // eventually. We encode this with Prom[b], and check + // that promises are fullfilled in the emptyness check. + bdd relation; + + // The conjunction of all Now variables, in their positive form. + bdd now_set; + // The conjunction of all Now variables, in their negated form. + bdd negnow_set; + // The (positive) conjunction of all variables which are not Now variables. + bdd notnow_set; + // The (positive) conjunction of all variables which are not atomic + // propositions. + bdd notvar_set; + // The (positive) conjunction of all variables which are not promises. + bdd notprom_set; + + // Record pairings between Next and Now variables. + bddPair* next_to_now; + + + tgba_bdd_core_data(); + tgba_bdd_core_data(const tgba_bdd_core_data& copy); + + // Merge two core_data. + tgba_bdd_core_data(const tgba_bdd_core_data& left, + const tgba_bdd_core_data& right); + + const tgba_bdd_core_data& operator= (const tgba_bdd_core_data& copy); + + ~tgba_bdd_core_data(); + + void declare_now_next(bdd now, bdd next); + void declare_atomic_prop(bdd var); + void declare_promise(bdd prom); + }; +} + +#endif // SPOT_TGBA_TGBABDDCOREDATA_HH diff --git a/src/tgba/tgbabdddict.cc b/src/tgba/tgbabdddict.cc new file mode 100644 index 000000000..b9e2db10c --- /dev/null +++ b/src/tgba/tgbabdddict.cc @@ -0,0 +1,32 @@ +#include "tgbabdddict.hh" +#include "ltlvisit/tostring.hh" + +namespace spot +{ + std::ostream& + tgba_bdd_dict::dump(std::ostream& os) const + { + fv_map::const_iterator sii; + os << "Atomic Propositions:" << std::endl; + for (sii = var_map.begin(); sii != var_map.end(); ++sii) + { + os << " " << sii->second << ": "; + to_string(sii->first, os) << std::endl; + } + os << "States:" << std::endl; + for (sii = now_map.begin(); sii != now_map.end(); ++sii) + { + os << " " << sii->second << ": Now["; + to_string(sii->first, os) << "]" << std::endl; + os << " " << sii->second + 1 << ": Next["; + to_string(sii->first, os) << "]" << std::endl; + } + os << "Promises:" << std::endl; + for (sii = prom_map.begin(); sii != prom_map.end(); ++sii) + { + os << " " << sii->second << ": "; + to_string(sii->first, os) << std::endl; + } + return os; + } +} diff --git a/src/tgba/tgbabdddict.hh b/src/tgba/tgbabdddict.hh new file mode 100644 index 000000000..00e39314d --- /dev/null +++ b/src/tgba/tgbabdddict.hh @@ -0,0 +1,30 @@ +#ifndef SPOT_TGBA_TGBABDDDICT_H +# define SPOT_TGBA_TGBABDDDICT_H + +#include +#include +#include "ltlast/formula.hh" + +namespace spot +{ + struct tgba_bdd_dict + { + // Dictionaries for BDD variables. + + // formula-to-BDD-variable maps + typedef std::map fv_map; + // BDD-variable-to-formula maps + typedef std::map vf_map; + + fv_map now_map; + vf_map now_formula_map; + fv_map var_map; + vf_map var_formula_map; + fv_map prom_map; + vf_map prom_formula_map; + + std::ostream& dump(std::ostream& os) const; + }; +} + +#endif // SPOT_TGBA_TGBABDDDICT_H diff --git a/src/tgba/tgbabddfactory.hh b/src/tgba/tgbabddfactory.hh new file mode 100644 index 000000000..69239f0d7 --- /dev/null +++ b/src/tgba/tgbabddfactory.hh @@ -0,0 +1,17 @@ +#ifndef SPOT_TGBA_TGBABDDFACTORY_H +# define SPOT_TGBA_TGBABDDFACTORY_H + +#include "tgbabddcoredata.hh" +#include "tgbabdddict.hh" + +namespace spot +{ + class tgba_bdd_factory + { + public: + virtual const tgba_bdd_core_data& get_core_data() const = 0; + virtual const tgba_bdd_dict& get_dict() const = 0; + }; +} + +#endif // SPOT_TGBA_TGBABDDFACTORY_H diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc new file mode 100644 index 000000000..ba4e7862f --- /dev/null +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -0,0 +1,93 @@ +#include "tgbabddtranslatefactory.hh" +#include "dictunion.hh" + +namespace spot +{ + tgba_bdd_translate_factory::tgba_bdd_translate_factory + (const tgba_bdd_concrete& from, const tgba_bdd_dict& to) + : dict_(to) + { + bddPair* rewrite = compute_pairs(from.get_dict()); + + const tgba_bdd_core_data& in = from.get_core_data(); + + data_.relation = bdd_replace(in.relation, rewrite); + data_.now_set = bdd_replace(in.now_set, rewrite); + data_.negnow_set = bdd_replace(in.negnow_set, rewrite); + data_.notnow_set = bdd_replace(in.notnow_set, rewrite); + data_.notvar_set = bdd_replace(in.notvar_set, rewrite); + data_.notprom_set = bdd_replace(in.notprom_set, rewrite); + + init_ = bdd_replace(from.get_init_state().as_bdd(), rewrite); + + bdd_freepair(rewrite); + } + + tgba_bdd_translate_factory::~tgba_bdd_translate_factory() + { + } + + bddPair* + tgba_bdd_translate_factory::compute_pairs(const tgba_bdd_dict& from) + { + bddPair* rewrite = bdd_newpair(); + + tgba_bdd_dict::fv_map::const_iterator i_from; + tgba_bdd_dict::fv_map::const_iterator i_to; + + from.dump(std::cerr); + + for (i_from = from.now_map.begin(); i_from != from.now_map.end(); ++i_from) + { + i_to = dict_.now_map.find(i_from->first); + assert(i_to != dict_.now_map.end()); + + bdd_setpair(rewrite, i_from->second, i_to->second); + bdd_setpair(rewrite, i_from->second + 1, i_to->second + 1); + bdd_setpair(data_.next_to_now, i_to->second + 1, i_to->second); + } + for (i_from = from.var_map.begin(); i_from != from.var_map.end(); ++i_from) + { + i_to = dict_.var_map.find(i_from->first); + assert(i_to != dict_.var_map.end()); + bdd_setpair(rewrite, i_from->second, i_to->second); + } + for (i_from = from.prom_map.begin(); + i_from != from.prom_map.end(); + ++i_from) + { + i_to = dict_.prom_map.find(i_from->first); + assert(i_to != dict_.prom_map.end()); + bdd_setpair(rewrite, i_from->second, i_to->second); + } + return rewrite; + } + + const tgba_bdd_core_data& + tgba_bdd_translate_factory::get_core_data() const + { + return data_; + } + + const tgba_bdd_dict& + tgba_bdd_translate_factory::get_dict() const + { + return dict_; + } + + bdd + tgba_bdd_translate_factory::get_init_state() const + { + return init_; + } + + + tgba_bdd_concrete + defrag(const tgba_bdd_concrete& a) + { + const tgba_bdd_dict& ad = a.get_dict(); + tgba_bdd_dict u = tgba_bdd_dict_union(ad, ad); + tgba_bdd_translate_factory f(a, u); + return tgba_bdd_concrete(f, f.get_init_state()); + } +} diff --git a/src/tgba/tgbabddtranslatefactory.hh b/src/tgba/tgbabddtranslatefactory.hh new file mode 100644 index 000000000..f47627223 --- /dev/null +++ b/src/tgba/tgbabddtranslatefactory.hh @@ -0,0 +1,34 @@ +#ifndef SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH +# define SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH + +#include "tgbabddfactory.hh" +#include "tgbabddconcrete.hh" + +namespace spot +{ + + class tgba_bdd_translate_factory: public tgba_bdd_factory + { + public: + tgba_bdd_translate_factory(const tgba_bdd_concrete& from, + const tgba_bdd_dict& to); + + virtual ~tgba_bdd_translate_factory(); + + bddPair* compute_pairs(const tgba_bdd_dict& from); + + const tgba_bdd_core_data& get_core_data() const; + const tgba_bdd_dict& get_dict() const; + + bdd get_init_state() const; + + private: + tgba_bdd_core_data data_; + tgba_bdd_dict dict_; + bdd init_; + }; + + tgba_bdd_concrete defrag(const tgba_bdd_concrete& a); +} + +#endif // SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH