From 88b60125022d884f6d6ff6e362d7674af3d05c8e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 4 Jul 2003 09:35:29 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare accepting conditions w.r.t. to Now variables, not Next. --- ChangeLog | 5 +++++ src/tgbaalgos/ltl2tgba.cc | 14 +++++++------- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/ChangeLog b/ChangeLog index b1a34d0d7..eed333f51 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2003-07-04 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare + accepting conditions w.r.t. to Now variables, not Next. + 2003-07-03 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first): diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba.cc index 9b80c5b8a..bc97c1d60 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba.cc @@ -76,13 +76,13 @@ namespace spot fact_.add_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 creating a new generalized Büchi accepting set, - Acc[x], and leave any transition going to NEXT without - checking X out of this set. Such accepting conditions - are checked for during the emptiness check. + should be fulfilled eventually. We ensure this by + creating a new generalized Büchi accepting set, Acc[x], + and leave out of this set any transition going off NOW + without checking X. Such accepting conditions are + checked for during the emptiness check. */ - fact_.declare_accepting_condition(x | !next, node->child()); + fact_.declare_accepting_condition(x | !now, node->child()); res_ = now; return; } @@ -152,7 +152,7 @@ namespace spot We declare an accepting condition for this purpose (see the comment in the unop::F case). */ - fact_.declare_accepting_condition(f2 | !next, node->second()); + fact_.declare_accepting_condition(f2 | !now, node->second()); res_ = now; return; }