Commit 729921c0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 95d732e3
......@@ -36,7 +36,6 @@
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/sccinfo.hh>
//#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<formula>();
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())
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment