diff --git a/NEWS b/NEWS index 6ba5382b2..18a4a8c11 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 6fdf5b2dc..d204f08aa 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -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 #include #include +#include #include #include +#include +#include +#include #include #include +#include #include -#include 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,45 +670,99 @@ 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 (matched && !opt->acc_words.empty()) - for (auto& word_aut: opt->acc_words) - if (spot::product(aut, word_aut)->is_empty()) - { - matched = false; - break; - } - - if (matched && !opt->rej_words.empty()) - for (auto& word_aut: opt->rej_words) - if (!spot::product(aut, word_aut)->is_empty()) - { - matched = false; - break; - } - - // 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 (!opt->acc_words.empty() && !opt->rej_words.empty()) { - auto min = minimize_obligation(aut, f); - assert(min); - if (aut == min) + aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); + + if (matched && !opt->acc_words.empty()) + for (auto& word_aut: opt->acc_words) + if (spot::product(aut, word_aut)->is_empty()) + { + matched = false; + break; + } + + if (matched && !opt->rej_words.empty()) + for (auto& word_aut: opt->rej_words) + if (!spot::product(aut, word_aut)->is_empty()) + { + 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 (obligation) { - // Not an obligation - matched = false; + auto min = minimize_obligation(aut, f); + assert(min); + if (aut == min) + { + // Not an obligation + matched = false; + } + else + { + matched &= !guarantee || is_terminal_automaton(min); + matched &= !safety || is_safety_mwdba(min); + } } - else + // 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)) { - matched &= !guarantee || is_terminal_automaton(min); - matched &= !safety || is_safety_mwdba(min); + 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); + } } } } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index eaa48f309..f02faaa2c 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -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()) diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 378cd14bc..4908c3705 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -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); diff --git a/tests/Makefile.am b/tests/Makefile.am index c61078503..c27cbbc36 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 = \ diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test new file mode 100755 index 000000000..57b78d551 --- /dev/null +++ b/tests/core/hierarchy.test @@ -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 . + +. ./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`