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

* src/tgba/tgbabddconcretefactory.hh

Browse source 
(tgba_bdd_concrete_factory::add_relation): Rename as ...
(tgba_bdd_concrete_factory::constrain_relation): ... this.
* src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc:
Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-10 14:13:56 +00:00
parent f661b0adc4
commit b963af66f1
4 changed files with 18 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,5 +1,11 @@
2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do
not create Now/Next variable when G is the root of the formula. 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::ltl_trad_visitor): Take a root argument.

2
src/tgba/tgbabddconcretefactory.cc
View file

@ -135,7 +135,7 @@ namespace spot
} }
void void
tgba_bdd_concrete_factory::add_relation(bdd new_rel) tgba_bdd_concrete_factory::constrain_relation(bdd new_rel)
{ {
data_.relation &= new_rel; data_.relation &= new_rel;
} }

2
src/tgba/tgbabddconcretefactory.hh
View file

@ -53,7 +53,7 @@ namespace spot
const tgba_bdd_dict& get_dict() const; const tgba_bdd_dict& get_dict() const;
/// Add a new constraint to the relation. /// 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. /// \brief Perfom final computations before the relation can be used.
/// ///

17
src/tgbaalgos/ltl2tgba.cc
View file

@ -73,7 +73,7 @@ namespace spot
bdd now = fact_.ithvar(v); bdd now = fact_.ithvar(v);
bdd next = fact_.ithvar(v + 1); bdd next = fact_.ithvar(v + 1);
bdd x = recurse(node->child()); 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 `x | next', doesn't actually encode the fact that x
should be fulfilled eventually. We ensure this by should be fulfilled eventually. We ensure this by
@ -95,7 +95,7 @@ namespace spot
// This saves 2 BDD variables. // This saves 2 BDD variables.
if (root_) if (root_)
{ {
fact_.add_relation(child); fact_.constrain_relation(child);
res_ = child; res_ = child;
return; return;
} }
@ -103,7 +103,8 @@ namespace spot
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, child & next, bddop_biimp)); fact_.constrain_relation(bdd_apply(now, child & next,
bddop_biimp));
res_ = now; res_ = now;
return; return;
} }
@ -117,8 +118,8 @@ namespace spot
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);
fact_.add_relation(bdd_apply(now, recurse(node->child()), fact_.constrain_relation(bdd_apply(now, recurse(node->child()),
bddop_biimp)); bddop_biimp));
res_ = next; res_ = next;
return; return;
} }
@ -154,7 +155,8 @@ namespace spot
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, f2 | (f1 & next), bddop_biimp)); fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
bddop_biimp));
/* /*
The rightmost conjunction, f1 & next, doesn't actually The rightmost conjunction, f1 & next, doesn't actually
encode the fact that f2 should be fulfilled eventually. encode the fact that f2 should be fulfilled eventually.
@ -175,7 +177,8 @@ namespace spot
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, f2 & (f1 | next), bddop_biimp)); fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
bddop_biimp));
res_ = now; res_ = now;
return; return;
} }