diff --git a/ChangeLog b/ChangeLog index fb4e8a348..c20c1869c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2003-05-26 Alexandre Duret-Lutz + * src/tgba/tgba.hh: Rename as ... + * src/tgba/public.hh: .. this. + * src/tgba/tgba.hh: New file. + * src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh. + * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba. + (tgba_bdd_concrete::init_iter): Delete. + (tgba_bdd_concrete::succ_iter): Take a state_bdd as argument, + not a bdd. + * src/tgba/tgbabddconcrete.cc: Likewise. + 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/Makefile.am b/src/tgba/Makefile.am index febfde8df..39605da82 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -9,6 +9,7 @@ libtgba_la_SOURCES = \ dictunion.hh \ ltl2tgba.cc \ ltl2tgba.hh \ + public.hh \ state.hh \ statebdd.cc \ statebdd.hh \ diff --git a/src/tgba/public.hh b/src/tgba/public.hh new file mode 100644 index 000000000..011420f60 --- /dev/null +++ b/src/tgba/public.hh @@ -0,0 +1,9 @@ +#ifndef SPOT_TGBA_PUBLIC_HH +# define SPOT_TGBA_PUBLIC_HH + +# include "tgba.hh" +# include "tgbabddconcrete.hh" +# include "tgbabddconcreteproduct.hh" +# include "ltl2tgba.hh" + +#endif // SPOT_TGBA_PUBLIC_HH diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 7232ea142..43b214b7f 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -1,8 +1,26 @@ #ifndef SPOT_TGBA_TGBA_HH # define SPOT_TGBA_TGBA_HH -# include "tgbabddconcrete.hh" -# include "tgbabddconcreteproduct.hh" -# include "ltl2tgba.hh" +#include "statebdd.hh" +#include "succiter.hh" +#include "tgbabdddict.hh" + +namespace spot +{ + class tgba + { + public: + virtual + ~tgba() + { + } + + virtual state_bdd get_init_state() const = 0; + virtual tgba_succ_iterator* succ_iter(state_bdd state) const = 0; + + virtual const tgba_bdd_dict& get_dict() const = 0; + }; + +} #endif // SPOT_TGBA_TGBA_HH diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index bc3064e6e..39c5b4f20 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -29,20 +29,14 @@ namespace spot } tgba_succ_iterator_concrete* - tgba_bdd_concrete::succ_iter(bdd state) const + tgba_bdd_concrete::succ_iter(state_bdd state) const { - bdd succ_set = bdd_replace(bdd_exist(data_.relation & state, + bdd succ_set = bdd_replace(bdd_exist(data_.relation & state.as_bdd(), 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 { diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 5417daefd..62e9901c7 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -1,28 +1,28 @@ #ifndef SPOT_TGBA_TGBABDDCONCRETE_HH # define SPOT_TGBA_TGBABDDCONCRETE_HH +#include "tgba.hh" #include "statebdd.hh" #include "tgbabddfactory.hh" #include "succiterconcrete.hh" namespace spot { - class tgba_bdd_concrete + class tgba_bdd_concrete: public tgba { 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; - + + tgba_succ_iterator_concrete* succ_iter(state_bdd state) 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_;