alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgba/tgba.hh: Rename as ...

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2003-05-26 12:34:15 +00:00
parent c03934140f
commit 885143309a
6 changed files with 50 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,5 +1,15 @@
2003-05-26 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-05-26 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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). Initial code for TGBA (Transition Generalized Büchi Automata).
Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
a LTL-to-TGBA translator using Couvreur's algorithm. a LTL-to-TGBA translator using Couvreur's algorithm.

1
src/tgba/Makefile.am
View file

@ -9,6 +9,7 @@ libtgba_la_SOURCES = \
dictunion.hh \ dictunion.hh \
ltl2tgba.cc \ ltl2tgba.cc \
ltl2tgba.hh \ ltl2tgba.hh \
public.hh \
state.hh \ state.hh \
statebdd.cc \ statebdd.cc \
statebdd.hh \ statebdd.hh \

9
src/tgba/public.hh Normal file
View file

@ -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

24
src/tgba/tgba.hh
View file

@ -1,8 +1,26 @@
#ifndef SPOT_TGBA_TGBA_HH #ifndef SPOT_TGBA_TGBA_HH
# define SPOT_TGBA_TGBA_HH # define SPOT_TGBA_TGBA_HH
# include "tgbabddconcrete.hh" #include "statebdd.hh"
# include "tgbabddconcreteproduct.hh" #include "succiter.hh"
# include "ltl2tgba.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 #endif // SPOT_TGBA_TGBA_HH

10
src/tgba/tgbabddconcrete.cc
View file

@ -29,20 +29,14 @@ namespace spot
} }
tgba_succ_iterator_concrete* 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_.now_set),
data_.next_to_now); data_.next_to_now);
return new tgba_succ_iterator_concrete(data_, succ_set); 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& const tgba_bdd_dict&
tgba_bdd_concrete::get_dict() const tgba_bdd_concrete::get_dict() const
{ {

14
src/tgba/tgbabddconcrete.hh
View file

@ -1,28 +1,28 @@
#ifndef SPOT_TGBA_TGBABDDCONCRETE_HH #ifndef SPOT_TGBA_TGBABDDCONCRETE_HH
# define SPOT_TGBA_TGBABDDCONCRETE_HH # define SPOT_TGBA_TGBABDDCONCRETE_HH
#include "tgba.hh"
#include "statebdd.hh" #include "statebdd.hh"
#include "tgbabddfactory.hh" #include "tgbabddfactory.hh"
#include "succiterconcrete.hh" #include "succiterconcrete.hh"
namespace spot namespace spot
{ {
class tgba_bdd_concrete class tgba_bdd_concrete: public tgba
{ {
public: public:
tgba_bdd_concrete(const tgba_bdd_factory& fact); tgba_bdd_concrete(const tgba_bdd_factory& fact);
tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init); tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init);
~tgba_bdd_concrete(); ~tgba_bdd_concrete();
void set_init_state(bdd s); void set_init_state(bdd s);
state_bdd get_init_state() const; state_bdd get_init_state() const;
tgba_succ_iterator_concrete* succ_iter(bdd state) const; tgba_succ_iterator_concrete* succ_iter(state_bdd state) const;
tgba_succ_iterator_concrete* init_iter() const;
const tgba_bdd_dict& get_dict() const; const tgba_bdd_dict& get_dict() const;
const tgba_bdd_core_data& get_core_data() const; const tgba_bdd_core_data& get_core_data() const;
protected: protected:
tgba_bdd_core_data data_; tgba_bdd_core_data data_;
tgba_bdd_dict dict_; tgba_bdd_dict dict_;