From 5a39d40b2c4d12fc144032498f801bc505ee9d4e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 14 May 2005 20:56:19 +0000 Subject: [PATCH] * src/ltlvisit/syntimpl.cc: Fix detection of purely eventual formulae. --- ChangeLog | 4 ++++ src/ltlvisit/syntimpl.cc | 23 ++++++++++++----------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/ChangeLog b/ChangeLog index 1dbe181ce..e2ae68f99 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2005-05-13 Alexandre Duret-Lutz + + * src/ltlvisit/syntimpl.cc: Fix detection of purely eventual formulae. + 2005-05-12 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc: Fix handling of fair_loop_approx. diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 9efb99c9a..533b05883 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -98,23 +98,24 @@ namespace spot case binop::Xor: case binop::Equiv: case binop::Implies: - universal = recurse_un(f1) & recurse_un(f2); - eventual = recurse_ev(f1) & recurse_ev(f2); + universal = recurse_un(f1) && recurse_un(f2); + eventual = recurse_ev(f1) && recurse_ev(f2); return; case binop::U: universal = recurse_un(f1) & recurse_un(f2); - if ((f1 == constant::true_instance()) || - (recurse_ev(f1))) + if ((f1 == constant::true_instance()) + // Both operand must be purely eventual, unlike in + // the proceedings of Concur'00. (The revision of + // the paper available at + // http://www1.bell-labs.com/project/TMP/ is fixed.) + || (recurse_ev(f1) && recurse_ev(f2))) eventual = true; return; case binop::R: - eventual = recurse_ev(f1) & recurse_ev(f2); - if ((f1 == constant::false_instance())) - //|| - //(recurse_un(f1))) + eventual = recurse_ev(f1) && recurse_ev(f2); + if ((f1 == constant::false_instance()) + || (recurse_un(f1) && recurse_un(f2))) universal = true; - if (!universal) - universal = recurse_un(f1) & recurse_un(f2); return; } /* Unreachable code. */