diff --git a/NEWS b/NEWS index f5538ee54..167e4f770 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,9 @@ New in spot 2.10.4.dev (net yet released) if the output code should attempt to preserve aliases present in the HOA input. This defaults to "keep". + - autfilt has a new --to-finite option, illustrated on + https://spot.lrde.epita.fr/tut12.html + Library: - "original-classes" is a new named property similar to @@ -39,6 +42,21 @@ New in spot 2.10.4.dev (net yet released) - print_dot() learned option "@" to display aliases, as discussed above. + - to_finite() is a new function that help interpreting automata + build from LTLf formula using the from_ltlf() function. It replace + the previously suggested method of removing and atomic proposition + and simpifying automata, that failed to deal with states without + successors. See updated https://spot.lrde.epita.fr/tut12.html + + - the HOA parser learned to not ignore self-loops labeled with [f] + and to turn any state that have colors but no outgoing transitions + into a state with a [f] self-loop. This helps dealing with + automata containing states without successors, as in the output of + to_finite(). + + - purge_dead_states() will now also remove edges labeled by false + (except self-loops). + New in spot 2.10.4 (2022-02-01) Bug fixed: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 8f72a96c5..8fe95c396 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -159,6 +159,7 @@ enum { OPT_SUM_OR, OPT_SUM_AND, OPT_TERMINAL_SCCS, + OPT_TO_FINITE, OPT_TRIV_SCCS, OPT_USED_AP_N, OPT_UNUSED_AP_N, @@ -391,6 +392,10 @@ static const argp_option options[] = "solver can be set thanks to the SPOT_SATSOLVER environment variable" "(see spot-x)." , 0 }, + { "to-finite", OPT_TO_FINITE, "alive", OPTION_ARG_OPTIONAL, + "Convert an automaton with \"alive\" and \"!alive\" propositions " + "into a Büchi automaton interpretable as a finite automaton. " + "States with a outgoing \"!alive\" edge are marked as accepting.", 0 }, { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 }, { "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM", OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0}, @@ -688,6 +693,7 @@ static bool opt_rem_unused_ap = false; static bool opt_sep_sets = false; static bool opt_split_edges = false; static const char* opt_sat_minimize = nullptr; +static const char* opt_to_finite = nullptr; static int opt_highlight_nondet_states = -1; static int opt_highlight_nondet_edges = -1; static int opt_highlight_accepting_run = -1; @@ -1225,6 +1231,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_terminal_sccs_set = true; opt_art_sccs_set = true; break; + case OPT_TO_FINITE: + opt_to_finite = arg ? arg : "alive"; + break; case OPT_TRIV_SCCS: opt_triv_sccs = parse_range(arg, 0, std::numeric_limits::max()); opt_art_sccs_set = true; @@ -1648,6 +1657,9 @@ namespace if (opt_split_edges) aut = spot::split_edges(aut); + if (opt_to_finite) + aut = spot::to_finite(aut, opt_to_finite); + if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); diff --git a/doc/org/tut12.org b/doc/org/tut12.org index fbe01e53e..57444e230 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -38,11 +38,14 @@ finite semantics) property. The plan is as follows: #+END_SRC #+RESULTS: [[file:tut12a.svg]] -4. Remove the =alive= property, and, while we are at it, simplify the - Büchi automaton: +4. Remove the =alive= property, after marking as accepting all states + with an outgoing edge labeled by =!alive=. (Note that since Spot + does not actually support state-based acceptance, it needs to keep + a false self-loop on any accepting state without a successor in + order to mark it as accepting.) #+name: tut12b #+begin_src sh :exports none - ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --remove-ap=alive -B --small -d + ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --to-finite -d #+end_src #+BEGIN_SRC dot :file tut12b.svg :var txt=tut12b :exports results $txt @@ -66,22 +69,21 @@ The first four steps of the above sequence of operations can be executed as follows. Transforming LTLf to LTL can be done using [[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing -an atomic proposition from an automaton can be done using [[file:autfilt.org][=autfilt=]]'s -=--remove-ap= option (adding =--small= will also simplify the -automaton). Interpreting the resulting Büchi automaton as a finite -automaton is out of scope for Spot. +an atomic proposition while adapting the accepting states can be done +with [[file:autfilt.org][=autfilt=]]'s =--to-finite= option. Interpreting the resulting +Büchi automaton as a finite automaton is out of scope for Spot. #+begin_src sh ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | - autfilt --remove-ap=alive -B --small + autfilt --to-finite #+end_src #+RESULTS: #+begin_example HOA: v1 States: 4 -Start: 1 +Start: 2 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) @@ -90,17 +92,17 @@ properties: very-weak --BODY-- State: 0 [!2] 0 -[2] 3 -State: 1 -[0&!2] 0 -[!0&1&!2] 1 -[!0&1&2] 2 -[0&2] 3 +[2] 1 +State: 1 {0} +[t] 1 State: 2 -[!0&1] 2 -[0] 3 -State: 3 {0} -[t] 3 +[0&!2] 0 +[0&2] 1 +[!0&1&!2] 2 +[!0&1&2] 3 +State: 3 +[0] 1 +[!0&1] 3 --END-- #+end_example @@ -111,51 +113,42 @@ automaton is output. In Python, we use the =from_ltlf()= function to convert from LTLf to LTL and translate the result into a Büchi automaton using -=translate()= [[file:tut10.org][as usual]]. Then we need to use the =remove_ap()= object, -which we must first setup with some atomic propositions to remove. -Finally we call the =postprocess()= function for automata -simplifications. (Note that =postprocess()= is already called by -=translate()=, but in this case removing the atomic proposition allows -more simplification opportunities.) +=translate()= [[file:tut10.org][as usual]]. Then we need to call the =to_finite()= +function. #+begin_src python import spot # Translate LTLf to Büchi. -aut = spot.from_ltlf('(a U b) & Fc').translate('small', 'buchi', 'sbacc') -# Remove "alive" atomic proposition -rem = spot.remove_ap() -rem.add_ap('alive') -aut = rem.strip(aut) -# Simplify result and print it. Use postprocess('ba', 'det') -# if you always want a deterministic automaton. -aut = spot.postprocess(aut, 'ba') -print(aut.to_str('hoa')) +f = spot.from_ltlf('(a U b) & Fc') +aut = f.translate('small', 'buchi', 'sbacc') +# Remove "alive" atomic propositions and print result. +print(spot.to_finite(aut).to_str('hoa')) #+end_src #+RESULTS: #+begin_example HOA: v1 States: 4 -Start: 1 +Start: 2 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic -properties: terminal +properties: very-weak --BODY-- State: 0 [!2] 0 -[2] 3 -State: 1 -[0&!2] 0 -[!0&1&!2] 1 -[!0&1&2] 2 -[0&2] 3 +[2] 1 +State: 1 {0} +[t] 1 State: 2 -[!0&1] 2 -[0] 3 -State: 3 {0} -[t] 3 +[0&!2] 0 +[0&2] 1 +[!0&1&!2] 2 +[!0&1&2] 3 +State: 3 +[0] 1 +[!0&1] 3 --END-- #+end_example @@ -166,9 +159,9 @@ print of an automaton]]. * C++ version The C++ version is straightforward adaptation of the Python version. -The Python functions =translate()= and =postprocess()= are convenient -wrappers around the =spot::translator= and =spot::postprocessor= -objects that we need to use here. +(The Python function =translate()= is a convenient Python-only +wrappers around the =spot::translator= object that we need to use +here.) #+begin_src C++ #include @@ -189,17 +182,7 @@ objects that we need to use here. trans.set_pref(spot::postprocessor::SBAcc | spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); - - spot::remove_ap rem; - rem.add_ap("alive"); - aut = rem.strip(aut); - - spot::postprocessor post; - post.set_type(spot::postprocessor::Buchi); - post.set_pref(spot::postprocessor::SBAcc - | spot::postprocessor::Small); // or ::Deterministic - aut = post.run(aut); - + aut = spot::to_finite(aut); print_hoa(std::cout, aut) << '\n'; return 0; } @@ -209,26 +192,26 @@ objects that we need to use here. #+begin_example HOA: v1 States: 4 -Start: 1 +Start: 2 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic -properties: terminal +properties: very-weak --BODY-- State: 0 [!2] 0 -[2] 3 -State: 1 -[0&!2] 0 -[!0&1&!2] 1 -[!0&1&2] 2 -[0&2] 3 +[2] 1 +State: 1 {0} +[t] 1 State: 2 -[!0&1] 2 -[0] 3 -State: 3 {0} -[t] 3 +[0&!2] 0 +[0&2] 1 +[!0&1&!2] 2 +[!0&1&2] 3 +State: 3 +[0] 1 +[!0&1] 3 --END-- #+end_example @@ -252,12 +235,48 @@ When working with LTLf, there are two different semantics for the next operator: - The weak next: =X a= is true if =a= hold in the next step or if there are no next step. In particular, =X(0)= is true iff there are - no successor. (By the way, you cannot write =X0= because that as an + no successor. (By the way, you cannot write =X0= because that is an atomic proposition: use =X(0)= or =X 0=.) - The strong next: =X[!] a= is true if =a= hold in the next step *and* there must be a next step. In particular =X[!]1= asserts that there is a successor. +To see the difference between =X= and =X[!]=, consider the following translation +of =(a & Xa) | (b & X[!]b)=: +#+name: tut12c +#+begin_src sh :exports none + f="(a & Xa) | (b & X[!]b)" + ltlfilt --from-ltlf -f "$f" | ltl2tgba -B | autfilt --name="$f" --to-finite -d.nA +#+end_src +#+BEGIN_SRC dot :file tut12c.svg :var txt=tut12c :exports results + $txt +#+END_SRC +#+RESULTS: +[[file:tut12c.svg]] + + +Note that because in reality Spot supports only transitions-based +acceptance, and the above automaton is really stored as a Büchi +automaton that *we* decide to interpret as a finite automaton, there +is a bit of trickery involved to represent an "accepting state" +without any successor. While such a state makes sense in finite +automata, it makes no sense in ω-automata: we fake it by adding a +self-loop labeled by *false* (internally, this extra edge is carrying +the acceptance mark that is displayed on the state). For instance: +#+name: tut12d +#+begin_src sh :exports none + f="a | (b & X(0))" + ltlfilt --from-ltlf -f "$f" | ltl2tgba -B | autfilt --name="$f" --to-finite -d.nA +#+end_src +#+BEGIN_SRC dot :file tut12d.svg :var txt=tut12d :exports results + $txt +#+END_SRC +#+RESULTS: +[[file:tut12d.svg]] + + # LocalWords: utf LTLf html args ltlf src ltlfilt Fc tgba svg txt # LocalWords: ap De Giacomo Vardi IJCAI Dutta Memocode acc Buchi ba -# LocalWords: postprocess aut det str NFA DFA ltsmin iff +# LocalWords: postprocess aut det str NFA DFA ltsmin iff LTL Büchi +# LocalWords: automata ltl autfilt HOA buchi sbacc iostream hoa Xa +# LocalWords: Kripke nA diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 5bd55fd83..1e3de6781 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1379,6 +1379,13 @@ states: %empty } } } + if (res.acc_state && + !res.opts.want_kripke && + res.h->aut->get_graph().state_storage(res.cur_state).succ == 0) + { + res.h->aut->new_edge(res.cur_state, res.cur_state, + bddfalse, res.acc_state); + } } state: state-name labeled-edges | state-name unlabeled-edges @@ -1403,7 +1410,6 @@ state: state-name labeled-edges { res.h->ks->state_from_number(res.cur_state)->cond(res.state_label); } - } | error { @@ -1412,6 +1418,8 @@ state: state-name labeled-edges res.universal = spot::trival::maybe(); res.existential = spot::trival::maybe(); res.complete = spot::trival::maybe(); + // also do not try to preserve any color + res.acc_state = {}; } @@ -1595,7 +1603,12 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt } labeled-edge: trans-label checked-state-num trans-acc_opt { - if (res.cur_label != bddfalse) + if (res.cur_label != bddfalse || + // As a hack to allow states to be accepting + // even if they do not have transitions, we + // do not ignore false-labeled self-loops if they + // have some colors) + ($2 == res.cur_state && !!($3 | res.acc_state))) { if (res.opts.want_kripke) res.h->ks->new_edge(res.cur_state, $2); diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 62c0d10aa..051514550 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -713,8 +713,16 @@ namespace spot bool useless = true; while (t) { - // An edge is useful if all its - // destinations are useful. + // Erase any false edge, except self-loops (which can + // be used to store colors on state without successor + // with state-based acceptance). + if (t->cond == bddfalse && t->src != t->dst) + { + t.erase(); + continue; + } + // A non-false edge is useful if all its destinations + // are useful. bool usefuledge = true; for (unsigned d: univ_dests(t->dst)) if (!useful[d]) diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index bf721835a..942a1b4b5 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2019, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -174,4 +174,74 @@ namespace spot }); return res; } + + + twa_graph_ptr to_finite(const_twa_graph_ptr aut, const char* alive) + { + twa_graph_ptr res = + make_twa_graph(aut, + { false, false, true, false, false, false }); + + bdd rem = bddtrue; + bdd neg = bddfalse; + int v = res->get_dict()-> + has_registered_proposition(spot::formula::ap(alive), aut); + if (v >= 0) + { + rem = bdd_ithvar(v); + neg = bdd_nithvar(v); + res->unregister_ap(v); + } + + unsigned ns = res->num_states(); + std::vector isacc(ns, false); + for (unsigned s = 0; s < ns; ++s) + { + for (auto& e: res->out(s)) + if (bdd_implies(e.cond, neg)) + { + isacc[e.src] = true; + e.cond = bddfalse; + } + else + { + e.cond = bdd_exist(e.cond, rem); + } + } + + res->set_buchi(); + res->prop_state_acc(true); + + // Purge dead states will remove all states accessible via edges + // marked as "bddfalse" above, along with those edges. + auto old = new std::vector(ns); + std::iota(old->begin(), old->end(), 0); + res->set_named_prop("original-states", old); + res->purge_dead_states(); + ns = res->num_states(); + for (unsigned s = 0; s < ns; ++s) + { + if (isacc[(*old)[s]]) + { + acc_cond::mark_t m = {0}; + bool done = false; + for (auto& e: res->out(s)) + { + e.acc = m; + done = true; + } + if (!done) + res->new_edge(s, s, bddfalse, m); + } + else + { + acc_cond::mark_t m = {}; + for (auto& e: res->out(s)) + e.acc = m; + } + } + return res; + + } + } diff --git a/spot/twaalgos/remprop.hh b/spot/twaalgos/remprop.hh index 6bc6d425c..09d75ffac 100644 --- a/spot/twaalgos/remprop.hh +++ b/spot/twaalgos/remprop.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -40,4 +40,19 @@ namespace spot twa_graph_ptr strip(const_twa_graph_ptr aut) const; }; + + /// \brief Interpret the "live" part of an automaton as finite automaton. + /// + /// This functions assumes that there is a property "alive" is + /// that either true or false on all transitions, and that can only + /// switch from true to false. + /// + /// Because Spot does not support finite automata, this creates a + /// state-based Büchi automaton where any states with a !alive + /// outgoing transition in the original automaton is accepting, and + /// all alive/!alive occurrences are removed. + SPOT_API twa_graph_ptr + to_finite(const_twa_graph_ptr aut, const char* alive = "alive"); + + } diff --git a/tests/Makefile.am b/tests/Makefile.am index 86802f75b..1b5d63fee 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -272,6 +272,7 @@ TESTS_twa = \ core/degenscc.test \ core/randomize.test \ core/lbttparse.test \ + core/ltlf.test \ core/scc.test \ core/sccdot.test \ core/sccif.test \ diff --git a/tests/core/complete.test b/tests/core/complete.test index 80d284968..7f557f67c 100755 --- a/tests/core/complete.test +++ b/tests/core/complete.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +# Copyright (C) 2015-2017, 2022 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -236,6 +236,7 @@ properties: deterministic univ-branch State: 0 {0} [t] 0 State: 1 {0} +[f] 1 [t] 0 --END-- EOF @@ -272,7 +273,8 @@ properties: trans-labels explicit-labels state-acc deterministic properties: univ-branch --BODY-- State: 0 -State: 1 +State: 1 {0} +[f] 1 --END-- EOF diff out expected diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test new file mode 100755 index 000000000..a1979bc8d --- /dev/null +++ b/tests/core/ltlf.test @@ -0,0 +1,175 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2022 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 + +# ltlfilt --from-ltlf is also tested in ltlfilt.test +ltlfilt --from-ltlf=A -f 'a & Xa' -f 'a & X[!]a' \ + -f '(a U b) & (F(c) | F(d & X(0)))' >out +cat >expected< out2 +cat >expected2<out3 +cat >expected3 < out4 +diff out3 out4 +# Removing the [f] lines should not change anything for autfilt +grep -v '\[f\]' out4 > out3 +cmp out3 out4 && exit 1 # make sure we did remove something +autfilt out3 > out4 +diff out4 expected3