From 729921c0a0a67e1443a26ff3d6d80c6d524748d4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Jun 2018 16:14:58 +0200 Subject: [PATCH] ltl2tgba_fm: mark persistence formulas as weak automata ... instead of inherently-weak. The reason they were tagged as inherently-weak is historical: this property was introduced 1.5 years before the weak propery. Fixes #351. * spot/twaalgos/ltl2tgba_fm.cc: Use prop_weak() instead of prop_inherently_weak(). Also be more conservative about the use of single_acc when unambiguous automata are generated. --- spot/twaalgos/ltl2tgba_fm.cc | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 63b993434..a3bd4e776 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -36,7 +36,6 @@ #include #include #include -//#include "twaalgos/dot.hh" namespace spot { @@ -1928,8 +1927,14 @@ namespace spot twa_graph_ptr a = make_twa_graph(dict); auto namer = a->create_namer(); - translate_dict d(a, s, exprop, f2.is_syntactic_persistence(), - unambiguous); + // Translating syntactic persistence will give a weak automaton, unless + // the unambiguous option is used. In the "unambiguous" case, formulas + // such as "FGa | FGb" (note: not "F(Ga | Gb)") will introduce terms like + // "FGb&GF!a" that are not syntactic persistence. + bool will_be_weak = (unambiguous + ? f2.is_syntactic_obligation() + : f2.is_syntactic_persistence()); + translate_dict d(a, s, exprop, will_be_weak, unambiguous); // Compute the set of all promises that can possibly occur inside // the formula. These are the right-hand sides of U or F @@ -2194,8 +2199,10 @@ namespace spot acc.set_generalized_buchi(); - if (f2.is_syntactic_persistence()) - a->prop_inherently_weak(true); + // The unambiguous option can introduce sub-terms that are not + // persistence, hence the resulting automaton might not be weak. + if (will_be_weak) + a->prop_weak(true); if (f2.is_syntactic_stutter_invariant()) a->prop_stutter_invariant(true); if (orig_f.is_syntactic_guarantee())