diff --git a/ChangeLog b/ChangeLog index c0ef4778c..049d61ab5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2003-07-10 Alexandre Duret-Lutz + * src/tgba/tgbabddconcretefactory.hh + (tgba_bdd_concrete_factory::add_relation): Rename as ... + (tgba_bdd_concrete_factory::constrain_relation): ... this. + * src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc: + Adjust. + * 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. diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index a92fda890..d7101f50d 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -135,7 +135,7 @@ namespace spot } void - tgba_bdd_concrete_factory::add_relation(bdd new_rel) + tgba_bdd_concrete_factory::constrain_relation(bdd new_rel) { data_.relation &= new_rel; } diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index c73f1d1f5..a8c180868 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -53,7 +53,7 @@ namespace spot const tgba_bdd_dict& get_dict() const; /// Add a new constraint to the relation. - void add_relation(bdd new_rel); + void constrain_relation(bdd new_rel); /// \brief Perfom final computations before the relation can be used. /// diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba.cc index 2447f64bc..3b8986682 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba.cc @@ -73,7 +73,7 @@ namespace spot bdd now = fact_.ithvar(v); bdd next = fact_.ithvar(v + 1); bdd x = recurse(node->child()); - fact_.add_relation(bdd_apply(now, x | next, bddop_biimp)); + fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); /* `x | next', doesn't actually encode the fact that x should be fulfilled eventually. We ensure this by @@ -95,7 +95,7 @@ namespace spot // This saves 2 BDD variables. if (root_) { - fact_.add_relation(child); + fact_.constrain_relation(child); res_ = child; return; } @@ -103,7 +103,8 @@ namespace spot int v = fact_.create_state(node); bdd now = fact_.ithvar(v); bdd next = fact_.ithvar(v + 1); - fact_.add_relation(bdd_apply(now, child & next, bddop_biimp)); + fact_.constrain_relation(bdd_apply(now, child & next, + bddop_biimp)); res_ = now; return; } @@ -117,8 +118,8 @@ namespace spot 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)); + fact_.constrain_relation(bdd_apply(now, recurse(node->child()), + bddop_biimp)); res_ = next; return; } @@ -154,7 +155,8 @@ namespace spot int v = fact_.create_state(node); bdd now = fact_.ithvar(v); bdd next = fact_.ithvar(v + 1); - fact_.add_relation(bdd_apply(now, f2 | (f1 & next), bddop_biimp)); + fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), + bddop_biimp)); /* The rightmost conjunction, f1 & next, doesn't actually encode the fact that f2 should be fulfilled eventually. @@ -175,7 +177,8 @@ namespace spot int v = fact_.create_state(node); bdd now = fact_.ithvar(v); bdd next = fact_.ithvar(v + 1); - fact_.add_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp)); + fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), + bddop_biimp)); res_ = now; return; }