alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl2tgba_fm: don't tag weak automata if unambiguous is used

Browse source 
Part of a bug reported by Simon Jantsch.  Test cases in next patch.

* spot/twaalgos/ltl2tgba_fm.cc: Here.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2019-02-02 14:37:39 +01:00
parent ea9d894d01
commit d4203c8ad0
2 changed files with 31 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -25,6 +25,9 @@ New in spot 2.7.0.dev (not yet release)
tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of
formulas with MS-DOS line endings. formulas with MS-DOS line endings.
- The core translation for unambiguous automata was incorrectly
tagging some non-weak automata as weak.
New in spot 2.7 (2018-12-11) New in spot 2.7 (2018-12-11)
Command-line tools: Command-line tools:

48
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008-2018 Laboratoire de Recherche et Développement // Copyright (C) 2008-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -1926,14 +1926,14 @@ namespace spot
twa_graph_ptr a = make_twa_graph(dict); twa_graph_ptr a = make_twa_graph(dict);
auto namer = a->create_namer<formula>(); auto namer = a->create_namer<formula>();
// Translating syntactic persistence will give a weak automaton, unless // Even if the input is a persistence formula, the unambiguous option might
// the unambiguous option is used. In the "unambiguous" case, formulas // cause the resulting automaton not to be weak. For instance formulas
// such as "FGa | FGb" (note: not "F(Ga | Gb)") will introduce terms like // such as "FGa | FGb" (note: not "F(Ga | Gb)") will introduce terms like
// "FGb&GF!a" that are not syntactic persistence. // "FGb&GF!a" that are not syntactic persistence.
bool will_be_weak = (unambiguous bool one_set_enough = (unambiguous
? f2.is_syntactic_obligation() ? f2.is_syntactic_obligation()
: f2.is_syntactic_persistence()); : f2.is_syntactic_persistence());
translate_dict d(a, s, exprop, will_be_weak, unambiguous); translate_dict d(a, s, exprop, one_set_enough, unambiguous);
// Compute the set of all promises that can possibly occur inside // Compute the set of all promises that can possibly occur inside
// the formula. These are the right-hand sides of U or F // the formula. These are the right-hand sides of U or F
@ -2198,21 +2198,29 @@ namespace spot
acc.set_generalized_buchi(); acc.set_generalized_buchi();
// The unambiguous option can introduce sub-terms that are not if (orig_f.is_syntactic_stutter_invariant())
// 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); a->prop_stutter_invariant(true);
if (orig_f.is_syntactic_guarantee()) // We cannot assume weak automata if the unambibuous construction
{ // is used.
a->prop_terminal(true); //
assert(a->num_sets() <= 1); // In an obligation formula such as (b W Ga)&F!a, initial state is
} // not accepting and goes to a state (b W Ga) that is accepting.
// Adding the unambiguous option will add a back-edge between
// these two states, creating an non-weak SCC.
//
// For guarantee formulas, X(G(b))) -> (!((a) W (G(b)))) has a
// non-weak output.
if (unambiguous) if (unambiguous)
a->prop_unambiguous(true); {
a->prop_unambiguous(true);
}
else
{
if (orig_f.is_syntactic_persistence())
a->prop_weak(true);
if (orig_f.is_syntactic_guarantee())
a->prop_terminal(true);
}
// Set the following to true to preserve state names. // Set the following to true to preserve state names.
a->release_formula_namer(namer, false); a->release_formula_namer(namer, false);