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

* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do

Browse source 
not create Now/Next variable when G is the root of the formula.
(ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
(ltl_trad_visitor::recurse): Create a new visitor, do not copy
the current one.
(ltl_to_tgba): Build ltl_trad_visitor with root = true.

* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
Remove FIXME about handling X(a U b) and X(a R b) better, it's
done naturally.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-10 13:55:20 +00:00
parent 871f421b5e
commit f661b0adc4
2 changed files with 28 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,5 +1,16 @@
2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do
not create Now/Next variable when G is the root of the formula.
(ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
(ltl_trad_visitor::recurse): Create a new visitor, do not copy
the current one.
(ltl_to_tgba): Build ltl_trad_visitor with root = true.
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
Remove FIXME about handling X(a U b) and X(a R b) better, it's
done naturally.
* src/tgbatest/spotlbtt.test: Make 100 rounds. * src/tgbatest/spotlbtt.test: Make 100 rounds.
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):

24
src/tgbaalgos/ltl2tgba.cc
View file

@ -19,8 +19,8 @@ namespace spot
class ltl_trad_visitor: public const_visitor class ltl_trad_visitor: public const_visitor
{ {
public: public:
ltl_trad_visitor(tgba_bdd_concrete_factory& fact) ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
: fact_(fact) : fact_(fact), root_(root)
{ {
} }
@ -88,12 +88,22 @@ namespace spot
} }
case unop::G: case unop::G:
{ {
bdd child = recurse(node->child());
// If G occurs at the top of the formula we don't
// need Now/Next variables. We just constrain
// the relation so that the child always happens.
// This saves 2 BDD variables.
if (root_)
{
fact_.add_relation(child);
res_ = child;
return;
}
// Gx <=> x && XGx // Gx <=> x && XGx
int v = fact_.create_state(node); int v = fact_.create_state(node);
bdd now = fact_.ithvar(v); bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1); bdd next = fact_.ithvar(v + 1);
fact_.add_relation(bdd_apply(now, recurse(node->child()) & next, fact_.add_relation(bdd_apply(now, child & next, bddop_biimp));
bddop_biimp));
res_ = now; res_ = now;
return; return;
} }
@ -104,7 +114,6 @@ namespace spot
} }
case unop::X: case unop::X:
{ {
// FIXME: Can be smarter on X(a U b) and X(a R b).
int v = fact_.create_state(node->child()); int v = fact_.create_state(node->child());
bdd now = fact_.ithvar(v); bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1); bdd next = fact_.ithvar(v + 1);
@ -201,7 +210,7 @@ namespace spot
bdd bdd
recurse(const formula* f) recurse(const formula* f)
{ {
ltl_trad_visitor v(*this); ltl_trad_visitor v(fact_);
f->accept(v); f->accept(v);
return v.result(); return v.result();
} }
@ -209,6 +218,7 @@ namespace spot
private: private:
bdd res_; bdd res_;
tgba_bdd_concrete_factory& fact_; tgba_bdd_concrete_factory& fact_;
bool root_;
}; };
tgba_bdd_concrete tgba_bdd_concrete
@ -224,7 +234,7 @@ namespace spot
// Traverse the formula and draft the automaton in a factory. // Traverse the formula and draft the automaton in a factory.
tgba_bdd_concrete_factory fact; tgba_bdd_concrete_factory fact;
ltl_trad_visitor v(fact); ltl_trad_visitor v(fact, true);
f2->accept(v); f2->accept(v);
ltl::destroy(f2); ltl::destroy(f2);
fact.finish(); fact.finish();