From ca80561ad51cf187228befcb2ff273c4ee6767ef Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 May 2004 16:41:00 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then free all formulae entered into canonical_succ, to avoid errors when a formula is entered into canonical_succ but not into formulae_seen. * src/tgbatest/ltl2tgba.test: Add a new test, and check with -f. Report from Thomas Martinez. --- ChangeLog | 9 +++++++++ src/tgbaalgos/ltl2tgba_fm.cc | 19 ++++++++++++++----- src/tgbatest/ltl2tgba.test | 30 +++++++++++++++++++----------- 3 files changed, 42 insertions(+), 16 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7dc8dab7f..b302e884c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-05-03 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then + free all formulae entered into canonical_succ, to avoid errors + when a formula is entered into canonical_succ but not into + formulae_seen. + * src/tgbatest/ltl2tgba.test: Add a new test, and check with -f. + Report from Thomas Martinez. + 2004-04-23 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0u. diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 7fe2fd365..bd30a4f87 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -431,9 +431,14 @@ namespace spot formulae_to_translate.erase(formulae_to_translate.begin()); // Translate it into a BDD to simplify it. + // FIXME: Currently the same formula can be converted into a + // BDD twice. Once in the symb_merge block below, and then + // once here. f->accept(v); bdd res = v.result(); - canonical_succ[res] = f; + succ_to_formula::iterator cs = canonical_succ.find(res); + if (cs == canonical_succ.end()) + canonical_succ[res] = clone(f); std::string now = to_string(f); @@ -514,7 +519,7 @@ namespace spot } else { - canonical_succ[succbdd] = dest; + canonical_succ[succbdd] = clone(dest); } } @@ -539,9 +544,10 @@ namespace spot // way it will be explored before the other during the model // checking. dest_map::const_iterator i = dests.find(constant::true_instance()); - // conditions of the True arc, so when can remove them from - // all other arcs. It might sounds that this is not needed - // when exprop is used, but it fact it is complementary. + // COND_FOR_TRUE is the conditions of the True arc, so when + // can remove them from all other arcs. It might sounds that + // this is not needed when exprop is used, but in fact it is + // complementary. // // Consider // f = r(X(1) R p) = p.(1 + r(X(1) R p)) @@ -615,6 +621,9 @@ namespace spot for (std::set::iterator i = formulae_seen.begin(); i != formulae_seen.end(); ++i) destroy(*i); + for (succ_to_formula::iterator i = canonical_succ.begin(); + i != canonical_succ.end(); ++i) + destroy(i->second); // Turn all promises into real acceptance conditions. a->complement_all_acceptance_conditions(); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 2125c559c..1dbceb51e 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -25,17 +25,25 @@ set -e +check () +{ + run 0 ./ltl2tgba "$1" + run 0 ./ltl2tgba -f "$1" +} + # We don't check the output, but just running these might be enough to # trigger assertions. -run 0 ./ltl2tgba a -run 0 ./ltl2tgba 'a U b' -run 0 ./ltl2tgba 'X a' -run 0 ./ltl2tgba 'a & b & c' -run 0 ./ltl2tgba 'a | b | (c U (d & (g U (h ^ i))))' -run 0 ./ltl2tgba 'Xa & (b U !a) & (b U !a)' -run 0 ./ltl2tgba 'Fa & Xb & GFc & Gd' -run 0 ./ltl2tgba 'Fa & Xa & GFc & Gc' -run 0 ./ltl2tgba 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -run 0 ./ltl2tgba 'a R (b R c)' -run 0 ./ltl2tgba '(a U b) U (c U d)' +check a +check 'a U b' +check 'X a' +check 'a & b & c' +check 'a | b | (c U (d & (g U (h ^ i))))' +check 'Xa & (b U !a) & (b U !a)' +check 'Fa & Xb & GFc & Gd' +check 'Fa & Xa & GFc & Gc' +check 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +check 'a R (b R c)' +check '(a U b) U (c U d)' + +check '((Xp2)U(X(1)))*(p1 R(p2 R p0))'