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

ltlfilt: add --recurrence and --persistence

Browse source 
* spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh
(rabin_to_buchi_maybe): Make this function public.
* bin/ltlfilt.cc: Implement the two options.
* tests/core/hierarchy.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new options.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-10 16:05:49 +01:00
parent 6190e4415b
commit de8a248fb2
6 changed files with 248 additions and 109 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -40,6 +40,11 @@ New in spot 2.2.2.dev (Not yet released)
too. See spot-x(7) for details. The defaults are those that were
best for the benchmark in bench/dtgbasat/.
* ltlfilt learned --recurrence and --persistence to match formulas
belonging to these two classes of the temporal hierarchy. Unlike
--syntactic-recurrence and --syntactic-persistence, the new checks
are automata-based and will also match pathological formulas.
Library:
* A twa is required to have at least one state, the initial state.

82
bin/ltlfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Copyright (C) 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.
@ -45,12 +45,16 @@
#include <spot/tl/exclusive.hh>
#include <spot/tl/ltlf.hh>
#include <spot/tl/print.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/word.hh>
#include <spot/twaalgos/product.hh>
const char argp_program_doc[] ="\
Read a list of formulas and output them back after some optional processing.\v\
@ -81,6 +85,8 @@ enum {
OPT_NEGATE,
OPT_NNF,
OPT_OBLIGATION,
OPT_PERSISTENCE,
OPT_RECURRENCE,
OPT_REJECT_WORD,
OPT_RELABEL,
OPT_RELABEL_BOOL,
@ -178,6 +184,10 @@ static const argp_option options[] =
"match guarantee formulas (even pathological)", 0 },
{ "obligation", OPT_OBLIGATION, nullptr, 0,
"match obligation formulas (even pathological)", 0 },
{ "persistence", OPT_PERSISTENCE, nullptr, 0,
"match persistence formulas (even pathological)", 0 },
{ "recurrence", OPT_RECURRENCE, nullptr, 0,
"match recurrence formulas (even pathological)", 0 },
{ "size", OPT_SIZE, "RANGE", 0,
"match formulas with size in RANGE", 0},
// backward compatibility
@ -272,6 +282,8 @@ static bool syntactic_si = false;
static bool safety = false;
static bool guarantee = false;
static bool obligation = false;
static bool recurrence = false;
static bool persistence = false;
static range size = { -1, -1 };
static range bsize = { -1, -1 };
enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling };
@ -422,6 +434,12 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_OBLIGATION:
obligation = true;
break;
case OPT_PERSISTENCE:
persistence = true;
break;
case OPT_RECURRENCE:
recurrence = true;
break;
case OPT_REJECT_WORD:
try
{
@ -652,11 +670,15 @@ namespace
|| simpl.are_equivalent(f, opt->equivalent_to);
matched &= !stutter_insensitive || spot::is_stutter_invariant(f);
if (matched && (obligation
if (matched && (obligation || recurrence || persistence
|| !opt->acc_words.empty()
|| !opt->rej_words.empty()))
{
auto aut = ltl_to_tgba_fm(f, simpl.get_dict());
spot::twa_graph_ptr aut = nullptr;
if (!opt->acc_words.empty() && !opt->rej_words.empty())
{
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
if (matched && !opt->acc_words.empty())
for (auto& word_aut: opt->acc_words)
@ -673,12 +695,35 @@ namespace
matched = false;
break;
}
}
// Some combinations of options can be simplified.
if (recurrence && persistence)
obligation = true;
if (obligation && recurrence)
recurrence = false;
if (obligation && persistence)
persistence = false;
// Try a syntactic match before looking at the automata.
if (matched &&
!((!persistence || f.is_syntactic_persistence())
&& (!recurrence || f.is_syntactic_recurrence())
&& (!guarantee || f.is_syntactic_guarantee())
&& (!safety || f.is_syntactic_safety())
&& (!obligation || f.is_syntactic_obligation())))
{
if (persistence)
aut = ltl_to_tgba_fm(spot::formula::Not(f),
simpl.get_dict(), true);
else if (!aut)
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
// Match obligations and subclasses using WDBA minimization.
// Because this is costly, we compute it later, so that we don't
// have to compute it on formulas that have been discarded for
// other reasons.
if (matched && obligation)
if (obligation)
{
auto min = minimize_obligation(aut, f);
assert(min);
@ -693,6 +738,33 @@ namespace
matched &= !safety || is_safety_mwdba(min);
}
}
// Recurrence properties are those that can be translated to
// deterministic BA. Persistence are those whose negation
// can be represented as DBA.
else if (!is_deterministic(aut))
{
assert(recurrence || persistence);
// if aut is a non-deterministic TGBA, we do
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
// BA will preserve determinism if possible.
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic
| spot::postprocessor::SBAcc);
p.set_level(spot::postprocessor::Low);
auto dra = p.run(aut);
if (dra->acc().is_generalized_buchi())
{
assert(is_deterministic(dra));
}
else
{
auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra));
assert(ba);
matched &= is_deterministic(ba);
}
}
}
}
matched ^= invert;

147
spot/twaalgos/remfin.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -305,79 +305,6 @@ namespace spot
return res;
}
static twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
{
if (!aut->prop_state_acc().is_true())
return nullptr;
auto code = aut->get_acceptance();
if (code.is_t())
return nullptr;
acc_cond::mark_t inf_pairs = 0U;
acc_cond::mark_t inf_alone = 0U;
acc_cond::mark_t fin_alone = 0U;
auto s = code.back().size;
// Rabin 1
if (code.back().op == acc_cond::acc_op::And && s == 4)
goto start_and;
// Co-Büchi
else if (code.back().op == acc_cond::acc_op::Fin && s == 1)
goto start_fin;
// Rabin >1
else if (code.back().op != acc_cond::acc_op::Or)
return nullptr;
while (s)
{
--s;
if (code[s].op == acc_cond::acc_op::And)
{
start_and:
auto o1 = code[--s].op;
auto m1 = code[--s].mark;
auto o2 = code[--s].op;
auto m2 = code[--s].mark;
// We expect
// Fin({n}) & Inf({n+1})
if (o1 != acc_cond::acc_op::Fin ||
o2 != acc_cond::acc_op::Inf ||
m1.count() != 1 ||
m2.count() != 1 ||
m2 != (m1 << 1U))
return nullptr;
inf_pairs |= m2;
}
else if (code[s].op == acc_cond::acc_op::Fin)
{
start_fin:
fin_alone |= code[--s].mark;
}
else if (code[s].op == acc_cond::acc_op::Inf)
{
auto m1 = code[--s].mark;
if (m1.count() != 1)
return nullptr;
inf_alone |= m1;
}
else
{
return nullptr;
}
}
trace << "inf_pairs: " << inf_pairs << '\n';
trace << "inf_alone: " << inf_alone << '\n';
trace << "fin_alone: " << fin_alone << '\n';
return ra_to_ba(aut, inf_pairs, inf_alone, fin_alone);
}
// If the DNF is
// Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) |
// Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4)
@ -486,6 +413,78 @@ namespace spot
}
}
twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
{
if (!aut->prop_state_acc().is_true())
return nullptr;
auto code = aut->get_acceptance();
if (code.is_t())
return nullptr;
acc_cond::mark_t inf_pairs = 0U;
acc_cond::mark_t inf_alone = 0U;
acc_cond::mark_t fin_alone = 0U;
auto s = code.back().size;
// Rabin 1
if (code.back().op == acc_cond::acc_op::And && s == 4)
goto start_and;
// Co-Büchi
else if (code.back().op == acc_cond::acc_op::Fin && s == 1)
goto start_fin;
// Rabin >1
else if (code.back().op != acc_cond::acc_op::Or)
return nullptr;
while (s)
{
--s;
if (code[s].op == acc_cond::acc_op::And)
{
start_and:
auto o1 = code[--s].op;
auto m1 = code[--s].mark;
auto o2 = code[--s].op;
auto m2 = code[--s].mark;
// We expect
// Fin({n}) & Inf({n+1})
if (o1 != acc_cond::acc_op::Fin ||
o2 != acc_cond::acc_op::Inf ||
m1.count() != 1 ||
m2.count() != 1 ||
m2 != (m1 << 1U))
return nullptr;
inf_pairs |= m2;
}
else if (code[s].op == acc_cond::acc_op::Fin)
{
start_fin:
fin_alone |= code[--s].mark;
}
else if (code[s].op == acc_cond::acc_op::Inf)
{
auto m1 = code[--s].mark;
if (m1.count() != 1)
return nullptr;
inf_alone |= m1;
}
else
{
return nullptr;
}
}
trace << "inf_pairs: " << inf_pairs << '\n';
trace << "inf_alone: " << inf_alone << '\n';
trace << "fin_alone: " << fin_alone << '\n';
return ra_to_ba(aut, inf_pairs, inf_alone, fin_alone);
}
twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
{
if (!aut->acc().uses_fin_acceptance())

18
spot/twaalgos/remfin.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -23,6 +23,22 @@
namespace spot
{
/// \brief Convert a state-based Rabin automaton to Büchi automaton,
/// preserving determinism when possible.
///
/// Return nullptr if the input is not a Rabin automaton, or is not
/// state-based.
///
/// This essentially applies the algorithm from "Deterministic
/// ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan,
/// A. Puri, and R. Brayton (ISAAC'94), but SCC-wise.
///
/// Unless you know what you are doing, you are probably better off
/// calling remove_fin() instead, as this will call more specialized
/// algorithms (e.g., for weak automata) when appropriate.
SPOT_API twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut);
/// \brief Rewrite an automaton without Fin acceptance.
SPOT_API twa_graph_ptr
remove_fin(const const_twa_graph_ptr& aut);

3
tests/Makefile.am
View file

@ -1,6 +1,6 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017
## Laboratoire de Recherche et Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -182,6 +182,7 @@ TESTS_tl = \
core/uwrm.test \
core/eventuniv.test \
core/stutter-ltl.test \
core/hierarchy.test \
core/format.test
TESTS_graph = \

46
tests/core/hierarchy.test Executable file
View file

@ -0,0 +1,46 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
test 11 -eq `genltl --dac | ltlfilt --syntactic-safety -c`
test 37 -eq `genltl --dac | ltlfilt --safety -c`
test 'Fp0' = `genltl --dac | ltlfilt --syntactic-guarantee`
test 'Fp0' = `genltl --dac | ltlfilt --guarantee`
test 25 -eq `genltl --dac | ltlfilt --syntactic-obligation -c`
test 40 -eq `genltl --dac | ltlfilt --obligation -c`
test 47 -eq `genltl --dac | ltlfilt --syntactic-recurrence -c`
test 52 -eq `genltl --dac | ltlfilt --recurrence -c`
test 29 -eq `genltl --dac | ltlfilt --syntactic-persistence -c`
test 41 -eq `genltl --dac | ltlfilt --persistence -c`
test 'G!p0 | F(p0 & (!p1 W p2))' = "`genltl --dac |
ltlfilt -v --obligation | ltlfilt --persistence`"
test 12 -eq `genltl --dac |
ltlfilt -v --obligation | ltlfilt --recurrence -c`
# There are only 3 formula that are not recurrence in the DAC set.
test 3 -eq `genltl --dac | ltlfilt --recurrence -v -c`
# There are only 3 formula that we cannot convert to DBA.
test 3 -eq `genltl --dac | ltl2tgba -G -D -S |
autfilt --generalized-rabin | dstar2tgba |
autfilt --is-deterministic -v -c`