diff --git a/NEWS b/NEWS
index db6a9bb9b..13f2ce84c 100644
--- a/NEWS
+++ b/NEWS
@@ -46,7 +46,7 @@ New in spot 2.2.2.dev (Not yet released)
are automata-based and will also match pathological formulas.
* The --format option of ltlfilt/genltl/randltl/ltlgrind learned to
- print the class of a formula in the temporal hierachy of Manna &
+ print the class of a formula in the temporal hierarchy of Manna &
Pnueli using %h. Try to classify the Dwyer & al. patterns with:
genltl --dac --format='%[vw]h' | sort | uniq -c
@@ -130,6 +130,15 @@ New in spot 2.2.2.dev (Not yet released)
* The new function mp_class(f) returns the class of the formula
f in the temporal hierarchy of Manna & Pnueli.
+Bug fixed:
+
+ * The minimize_wdba() function was not correctly minimizing automata
+ with useless SCCs. This was not an issue for the LTL translation
+ (where useless SCCs are always removed first), but it was an issue
+ when deciding if a formula was safety or guarantee. As a
+ consequence, some tricky safety or guarantee properties were only
+ recognized as obligations.
+
New in spot 2.2.2 (2016-12-16)
Build:
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index d204f08aa..351b60aa4 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -734,8 +734,10 @@ namespace
}
else
{
- matched &= !guarantee || is_terminal_automaton(min);
- matched &= !safety || is_safety_mwdba(min);
+ spot::scc_info si(min);
+ matched &= !guarantee
+ || is_terminal_automaton(min, &si, true);
+ matched &= !safety || is_safety_automaton(min, &si);
}
}
// Recurrence properties are those that can be translated to
diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in
index baec65f70..474d10edf 100755
--- a/python/ajax/spotcgi.in
+++ b/python/ajax/spotcgi.in
@@ -1,7 +1,7 @@
#!@PYTHON@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
+# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -511,8 +511,8 @@ if output_type == 'f':
automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
minimized = spot.minimize_obligation(automaton, f)
if minimized != automaton:
- g = spot.is_terminal_automaton(minimized)
- s = spot.is_safety_mwdba(minimized)
+ g = spot.is_terminal_automaton(minimized, None, True)
+ s = spot.is_safety_automaton(minimized)
if s and not f.is_syntactic_safety():
unbufprint('pathologic safety')
if g and not f.is_syntactic_guarantee():
diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc
index 122665b5d..53c5531e3 100644
--- a/spot/tl/hierarchy.cc
+++ b/spot/tl/hierarchy.cc
@@ -66,8 +66,11 @@ namespace spot
auto min = minimize_obligation(aut, f);
if (aut != min) // An obligation.
{
- bool g = is_terminal_automaton(min);
- bool s = is_safety_mwdba(min);
+ scc_info si(min);
+ // The minimba WDBA can have some trivial accepting SCCs
+ // that we should ignore in is_terminal_automaton().
+ bool g = is_terminal_automaton(min, &si, true);
+ bool s = is_safety_automaton(min, &si);
if (g)
return s ? 'B' : 'G';
else
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 4bb295624..39685caf3 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -520,7 +520,7 @@ namespace spot
// (i.e., it is not the start of any accepting word).
scc_info sm(det_a);
- sm.determine_unknown_acceptance();
+
unsigned scc_count = sm.scc_count();
// SCC that have been marked as useless.
std::vector useless(scc_count);
@@ -539,18 +539,13 @@ namespace spot
bool transient = sm.is_trivial(m);
auto& succ = sm.succ(m);
- if (transient && succ.empty())
- {
- // A trivial SCC without successor is useless.
- useless[m] = true;
- d[m] = k - 1;
- continue;
- }
-
- // Compute the minimum color l of the successors.
- // Also SCCs are useless if all their successor are
- // useless.
- unsigned l = k;
+ // Compute the minimum color l of the successors. Also SCCs
+ // are useless if all their successor are useless. Note
+ // that Löding uses k-1 as level for non-final SCCs without
+ // successors but that seems bogus: using k+1 will make sure
+ // that a non-final SCCs without successor (i.e., a useless
+ // SCC) will be ignored in the computation of the level.
+ unsigned l = k + 1;
for (unsigned j: succ)
{
is_useless &= useless[j];
@@ -575,6 +570,8 @@ namespace spot
}
else
{
+ if (succ.empty())
+ is_useless = true;
d[m] = (l - 1) | 1; // largest odd number inferior or equal
}
}
diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc
index ef161fbcf..926da171c 100644
--- a/spot/twaalgos/strength.cc
+++ b/spot/twaalgos/strength.cc
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@@ -28,7 +28,8 @@ namespace spot
namespace
{
template
- bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si)
+ bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si,
+ bool ignore_trivial_term = false)
{
// Create an scc_info if the user did not give one to us.
bool need_si = !si;
@@ -89,7 +90,7 @@ namespace spot
// A terminal automaton should accept any word that as a prefix
// leading to an accepting edge. In other words, we cannot have
// an accepting edge that goes into a rejecting SCC.
- if (terminal && is_term)
+ if (terminal && is_term && !ignore_trivial_term)
for (auto& e: aut->edges())
if (si->is_rejecting_scc(si->scc_of(e.dst))
&& aut->acc().accepting(e.acc))
@@ -103,7 +104,12 @@ namespace spot
if (set)
{
if (terminal)
- aut->prop_terminal(is_term && is_weak);
+ {
+ if (!ignore_trivial_term)
+ aut->prop_terminal(is_term && is_weak);
+ else if (is_term && is_weak)
+ aut->prop_terminal(true);
+ }
aut->prop_weak(is_weak);
aut->prop_very_weak(is_single_state_scc && is_weak);
if (inweak)
@@ -116,13 +122,15 @@ namespace spot
}
bool
- is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
+ is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si,
+ bool ignore_trivial_term)
{
trival v = aut->prop_terminal();
if (v.is_known())
return v.is_true();
bool res =
- is_type_automaton(std::const_pointer_cast(aut), si);
+ is_type_automaton(std::const_pointer_cast(aut), si,
+ ignore_trivial_term);
std::const_pointer_cast(aut)->prop_terminal(res);
return res;
}
@@ -170,16 +178,27 @@ namespace spot
is_type_automaton(aut, si);
}
- bool is_safety_mwdba(const const_twa_graph_ptr& aut)
+ bool is_safety_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
- if (!(aut->acc().is_buchi() || aut->acc().is_all()))
- throw std::runtime_error
- ("is_safety_mwdba() should be called on a Buchi automaton");
+ if (aut->acc().is_t())
+ return true;
- for (auto& t: aut->edges())
- if (!aut->acc().accepting(t.acc))
- return false;
- return true;
+ bool need_si = !si;
+ if (need_si)
+ si = new scc_info(aut);
+
+ bool res = true;
+ unsigned scount = si->scc_count();
+ for (unsigned scc = 0; scc < scount; ++scc)
+ if (!si->is_trivial(scc) && si->is_rejecting_scc(scc))
+ {
+ res = false;
+ break;
+ }
+
+ if (need_si)
+ delete si;
+ return res;
}
diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh
index 66cea4db2..550c1815e 100644
--- a/spot/twaalgos/strength.hh
+++ b/spot/twaalgos/strength.hh
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@@ -29,6 +29,9 @@ namespace spot
/// are complete, and no accepting transitions lead to a
/// non-accepting SCC.
///
+ /// If ignore_trivial_scc is set, accepting transitions from trivial
+ /// SCCs are ignored.
+ ///
/// This property guarantees that a word is accepted if it has some
/// prefix that reaches an accepting transition.
///
@@ -41,8 +44,8 @@ namespace spot
/// the prop_terminal() property of the automaton as a side-effect,
/// so further calls will return in constant-time.
SPOT_API bool
- is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
-
+ is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr,
+ bool ignore_trivial_scc = false);
/// \brief Check whether an automaton is weak.
///
@@ -95,16 +98,22 @@ namespace spot
is_inherently_weak_automaton(const const_twa_graph_ptr& aut,
scc_info* sm = nullptr);
- /// \brief Check whether a minimized WDBA represents a safety
- /// property.
+ /// \brief Check whether an automaton is a safety automaton.
+ ///
+ /// A safety automaton has only accepting SCCs (or trivial
+ /// SCCs).
///
/// A minimized WDBA (as returned by a successful run of
- /// minimize_obligation()) represent safety property if it contains
- /// only accepting transitions.
+ /// minimize_obligation()) represent safety property if it is a
+ /// safety automaton.
///
/// \param aut the automaton to check
+ ///
+ /// \param sm an scc_info object for the automaton if available (it
+ /// will be built otherwise).
SPOT_API bool
- is_safety_mwdba(const const_twa_graph_ptr& aut);
+ is_safety_automaton(const const_twa_graph_ptr& aut,
+ scc_info* sm = nullptr);
/// \brief Check whether an automaton is weak or terminal.
///
diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test
index 9515d9011..c44f28f37 100755
--- a/tests/core/hierarchy.test
+++ b/tests/core/hierarchy.test
@@ -62,3 +62,7 @@ cat >expected <