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

implement is_liveness() and is_liveness_automaton()

* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh,
spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Here.
* bin/ltlfilt.cc (--liveness): New filter.
* NEWS: Mention those.
* tests/core/ltlfilt.test, tests/python/ltlsimple.py: Add test cases.
parent d2316b14
Pipeline #4290 passed with stages
in 170 minutes and 3 seconds
......@@ -15,11 +15,8 @@ New in spot 2.6.2.dev (not yet released)
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
been dropped as it was not used.
Build:
- We no longer distribute the Python-based CGI script + javascript
code for the online translator. Its replacement has its own
repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/
- ltlfilt learned --liveness to match formulas representing liveness
properties.
Library:
......@@ -64,6 +61,10 @@ New in spot 2.6.2.dev (not yet released)
with arbitrary acceptance condition into a parity automaton,
based on a last-appearance record (LAR) construction.
- The new function is_liveness() and is_liveness_automaton() can be
used to check whether a formula or an automaton represents a
liveness property.
Bugs fixed:
- Running "ltl2tgba -B" on formulas of the type FG(safety) would
......
......@@ -700,11 +700,12 @@ namespace
if (matched && (obligation || recurrence || persistence
|| !opt->acc_words.empty()
|| !opt->rej_words.empty()))
|| !opt->rej_words.empty()
|| liveness))
{
spot::twa_graph_ptr aut = nullptr;
if (!opt->acc_words.empty() || !opt->rej_words.empty())
if (!opt->acc_words.empty() || !opt->rej_words.empty() || liveness)
{
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
......@@ -724,6 +725,7 @@ namespace
break;
}
matched &= !liveness || is_liveness_automaton(aut);
}
// Some combinations of options can be simplified.
......
......@@ -469,4 +469,9 @@ namespace spot
const op* vd = v.data();
return nesting_depth(f, vd, vd + v.size());
}
bool is_liveness(formula f)
{
return is_liveness_automaton(ltl_to_tgba_fm(f, spot::make_bdd_dict()));
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
......@@ -184,4 +184,14 @@ namespace spot
///
/// The string should be terminated by '\0' or ']'.
SPOT_API unsigned nesting_depth(formula f, const char* opers);
/// \brief Check whether a formula represents a liveness property.
///
/// A formula represents a liveness property if any finite prefix
/// can be extended into a word accepted by the formula.
///
/// The test is done by conversion to automaton. If you already
/// have an automaton, use spot::is_liveness_automaton() instead.
SPOT_API bool is_liveness(formula f);
}
......@@ -22,6 +22,9 @@
#include <spot/misc/hash.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/sccfilter.hh>
using namespace std::string_literals;
......@@ -401,4 +404,13 @@ namespace spot
std::string num = std::to_string(scc_num);
return decompose_scc(sm, (accepting ? ('a' + num) : num).c_str());
}
bool
is_liveness_automaton(const const_twa_graph_ptr& aut)
{
auto mon = minimize_monitor(scc_filter_states(aut));
return mon->num_states() == 1 && is_complete(mon);
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire
// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire
// de Recherche et Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -104,7 +104,7 @@ namespace spot
/// SCCs).
///
/// A minimized WDBA (as returned by a successful run of
/// minimize_obligation()) represent safety property if it is a
/// minimize_obligation()) represents safety property if it is a
/// safety automaton.
///
/// \param aut the automaton to check
......@@ -115,6 +115,15 @@ namespace spot
is_safety_automaton(const const_twa_graph_ptr& aut,
scc_info* sm = nullptr);
/// \brief Whether the automaton represents a liveness property.
///
/// An automaton represents a liveness property if after forcing the
/// acceptance condition to true, the resulting automaton accepts
/// all words. In other words, there is no prefix that cannot be
/// extended into an accepting word.
SPOT_API bool
is_liveness_automaton(const const_twa_graph_ptr& aut);
/// \brief Check whether an automaton is weak or terminal.
///
/// This sets the "inherently weak", "weak", "very-weak" and
......
......@@ -127,6 +127,16 @@ Fb
F(a & X(!a & b))
EOF
checkopt --liveness <<EOF
GFa | FGb
F(GFa | Gb)
F(b W GFa)
GFa | Gb
b W GFa
a U Fb
F(a & !Xa & Xb)
EOF
checkopt --safety <<EOF
!({a;b[*];c}!)
G(a & Xb)
......
......@@ -142,3 +142,6 @@ def myparse(input):
# This used to fail, because myparse would return a pointer
# to pf.f inside the destroyed pf.
assert myparse('a U b') == spot.formula('a U b')
assert spot.is_liveness('a <-> GFb')
assert not spot.is_liveness('a & GFb')
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