From 6459877a1ab2210e6a937cddafdb6f2fba6dafce Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 31 Oct 2017 17:21:38 +0100 Subject: [PATCH] overhaul the stutter-invariance checks * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and document the api. * spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section. * tests/python/stutter-inv-states.ipynb: Rename as ... * tests/python/stutter-inv.ipynb: ... this, and add more comments. * tests/Makefile.am, doc/org/tut.org: Adjust renaming. * bench/stutter/stutter_invariance_randomgraph.cc, bench/stutter/stutter_invariance_formulas.cc, bench/stutter/Makefile.am: Make it compile again. * bin/autfilt.cc: Call inplace variants. * NEWS: Mention the overhaul. --- NEWS | 12 + bench/stutter/Makefile.am | 5 +- bench/stutter/stutter_invariance_formulas.cc | 10 +- .../stutter/stutter_invariance_randomgraph.cc | 7 +- bin/autfilt.cc | 4 +- doc/mainpage.dox | 3 +- doc/org/tut.org | 2 +- spot/twa/twa.hh | 3 + spot/twaalgos/stutter.cc | 283 +-- spot/twaalgos/stutter.hh | 207 ++- tests/Makefile.am | 2 +- ...ter-inv-states.ipynb => stutter-inv.ipynb} | 1513 +++++++++-------- 12 files changed, 1169 insertions(+), 882 deletions(-) rename tests/python/{stutter-inv-states.ipynb => stutter-inv.ipynb} (65%) diff --git a/NEWS b/NEWS index d15d97911..ed607fb64 100644 --- a/NEWS +++ b/NEWS @@ -126,6 +126,10 @@ New in spot 2.4.1.dev (not yet released) can be passed to disable this behavior (or use -x degen-remscc=0 from the command-line). + - The functions for detecting stutter-invariant formulas or automata + have been overhauled. Their interface changed slightly. They are + now fully documented. + - In addition to detecting stutter-invariant formulas/automata, some can now study a stutter-sensitive automaton and detect the subset of states that are stutter-invariant. See @@ -146,6 +150,14 @@ New in spot 2.4.1.dev (not yet released) spot::scc_info::marks(), spot::scc_info::marks_of() and spot::scc_info::acc_sets_of() respectively. + Backward incompatible changes: + + - The spot::closure(), spot::sl2(), spot::is_stutter_invariant() + functions no longuer takes && arguments. The former two have + spot::closure_inplace() and spot::sl2_inplace() variant. These + function also do not take to list of atomic propositions as an + argument anymore. + Bugs fixed: - Automata produced by "genaut --ks-nca=N" were incorrectly marked diff --git a/bench/stutter/Makefile.am b/bench/stutter/Makefile.am index 398cc597e..5f7a85c8d 100644 --- a/bench/stutter/Makefile.am +++ b/bench/stutter/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +## Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -24,7 +24,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = \ $(top_builddir)/bin/libcommon.a \ $(top_builddir)/lib/libgnu.la \ - $(top_builddir)/spot/libspot.la + $(top_builddir)/spot/libspot.la \ + $(top_builddir)/buddy/src/libbddx.la bin_PROGRAMS = stutter_invariance_randomgraph \ stutter_invariance_formulas diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index 9d9385123..2007891af 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -66,9 +66,8 @@ namespace spot::twa_graph_ptr a = trans.run(f); spot::twa_graph_ptr na = trans.run(spot::formula::Not(f)); spot::atomic_prop_set* ap = spot::atomic_prop_collect(f); - bdd apdict = spot::atomic_prop_collect_as_bdd(f, a); - std::cout << formula << ',' << ap->size() << ','; + delete ap; stats.print(a); stats.print(na); @@ -82,9 +81,9 @@ namespace sw.start(); bool res = spot::is_stutter_invariant(std::move(dup_a), std::move(dup_na), - apdict, algo); + algo); auto time = sw.stop(); - std::cout<< time << ','; + std::cout << time << ','; if (algo > 1 && prev != res) { @@ -96,7 +95,6 @@ namespace prev = res; } std::cout << prev << '\n'; - delete ap; return 0; } }; diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index be2a7ff64..69c007bbb 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -77,8 +77,7 @@ main(int argc, char** argv) do { spot::srand(++seed); - a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5, - true); + a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5, true); } while (a->is_empty()); auto na = spot::remove_fin(spot::dualize(a)); @@ -102,7 +101,7 @@ main(int argc, char** argv) sw.start(); bool res = spot::is_stutter_invariant(std::move(dup_a), std::move(dup_na), - apdict, algo); + algo); auto time = sw.stop(); std::cout << time; if (algo > 1 && res != prev) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 0455aa45e..d261c4af0 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1160,11 +1160,11 @@ namespace aut = opt->excl_ap.constrain(aut, false); if (opt_destut) - aut = spot::closure(std::move(aut)); + aut = spot::closure_inplace(std::move(aut)); if (opt_instut == 1) aut = spot::sl(std::move(aut)); else if (opt_instut == 2) - aut = spot::sl2(std::move(aut)); + aut = spot::sl2_inplace(std::move(aut)); if (!opt_keep_states.empty()) aut = mask_keep_accessible_states(aut, opt_keep_states, diff --git a/doc/mainpage.dox b/doc/mainpage.dox index d5b76d0a5..6c5930f1f 100644 --- a/doc/mainpage.dox +++ b/doc/mainpage.dox @@ -19,11 +19,12 @@ /// /// \section pointers Handy starting points /// -/// \li spot::formula Base class for an LTL or PSL formula. +/// \li spot::formula Base class for an LTL or PSL formula. /// \li spot::parse_infix_psl() Parsing a text string into a /// spot::formula. /// \li spot::twa Base class for Transition-based /// ω-Automata. +/// \li spot::twa_algorithms Algorithms on ω-Automata. /// \li spot::translator Convert a spot::formula into a /// spot::twa. /// \li spot::kripke Base class for Kripke structures. diff --git a/doc/org/tut.org b/doc/org/tut.org index 1de492e0f..d11352df7 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -83,4 +83,4 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata. -- [[https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html][=stutter-inv-states.ipynb=]] detecting stutter-invariant formulas and states. +- [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties. diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 273d5f793..d9699cc67 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1687,6 +1687,9 @@ namespace spot /// \addtogroup twa_io Input/Output of TωA /// \ingroup twa_algorithms + /// \addtogroup stutter_inv Stutter-invariance checks + /// \ingroup twa_algorithms + /// \addtogroup twa_ltl Translating LTL formulas into TωA /// \ingroup twa_algorithms diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 4cb673227..ec6f25a2d 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -210,12 +210,11 @@ namespace spot class tgbasl final : public twa { public: - tgbasl(const const_twa_ptr& a, bdd atomic_propositions) - : twa(a->get_dict()), a_(a), aps_(atomic_propositions) + tgbasl(const_twa_ptr a) + : twa(a->get_dict()), a_(a) { - get_dict()->register_all_propositions_of(&a_, this); - assert(num_sets() == 0); - set_generalized_buchi(a_->num_sets()); + copy_ap_of(a); + copy_acceptance_of(a_); } virtual const state* get_init_state() const override @@ -227,7 +226,7 @@ namespace spot { const state_tgbasl* s = down_cast(state); return new twasl_succ_iterator(a_->succ_iter(s->real_state()), s, - a_->get_dict(), aps_); + a_->get_dict(), ap_vars()); } virtual std::string format_state(const state* state) const override @@ -240,14 +239,13 @@ namespace spot private: const_twa_ptr a_; - bdd aps_; }; typedef std::shared_ptr tgbasl_ptr; - inline tgbasl_ptr make_tgbasl(const const_twa_ptr& aut, bdd ap) + inline tgbasl_ptr make_tgbasl(const const_twa_ptr& aut) { - return std::make_shared(aut, ap); + return std::make_shared(aut); } @@ -272,22 +270,11 @@ namespace spot } twa_graph_ptr - sl(const twa_graph_ptr& a) - { - return sl(a, a->ap_vars()); - } - - twa_graph_ptr - sl2(const twa_graph_ptr& a) - { - return sl2(a, a->ap_vars()); - } - - twa_graph_ptr - sl(const const_twa_graph_ptr& a, bdd atomic_propositions) + sl(const_twa_graph_ptr a) { // The result automaton uses numbered states. twa_graph_ptr res = make_twa_graph(a->get_dict()); + bdd atomic_propositions = a->ap_vars(); // We use the same BDD variables as the input. res->copy_ap_of(a); res->copy_acceptance_of(a); @@ -348,10 +335,9 @@ namespace spot } twa_graph_ptr - sl2(twa_graph_ptr&& a, bdd atomic_propositions) + sl2_inplace(twa_graph_ptr a) { - if (atomic_propositions == bddfalse) - atomic_propositions = a->ap_vars(); + bdd atomic_propositions = a->ap_vars(); unsigned num_states = a->num_states(); unsigned num_edges = a->num_edges(); std::vector selfloops(num_states, bddfalse); @@ -415,15 +401,13 @@ namespace spot } twa_graph_ptr - sl2(const const_twa_graph_ptr& a, bdd atomic_propositions) + sl2(const_twa_graph_ptr a) { - return sl2(make_twa_graph(a, twa::prop_set::all()), - atomic_propositions); + return sl2_inplace(make_twa_graph(a, twa::prop_set::all())); } - twa_graph_ptr - closure(twa_graph_ptr&& a) + closure_inplace(twa_graph_ptr a) { a->prop_keep({false, // state_based false, // inherently_weak @@ -506,33 +490,145 @@ namespace spot } twa_graph_ptr - closure(const const_twa_graph_ptr& a) + closure(const_twa_graph_ptr a) { - return closure(make_twa_graph(a, twa::prop_set::all())); + return closure_inplace(make_twa_graph(a, twa::prop_set::all())); } - // The stutter check algorithm to use can be overridden via an - // environment variable. - static int default_stutter_check_algorithm() + namespace { - static const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); - if (stutter_check) - { - char* endptr; - long res = strtol(stutter_check, &endptr, 10); - if (*endptr || res < 0 || res > 9) - throw - std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); - return res; - } - else - { - return 8; // The best variant, according to our benchmarks. - } + // The stutter check algorithm to use can be overridden via an + // environment variable. + static int default_stutter_check_algorithm() + { + static const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); + if (stutter_check) + { + char* endptr; + long res = strtol(stutter_check, &endptr, 10); + if (*endptr || res < 0 || res > 9) + throw + std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); + return res; + } + else + { + return 8; // The best variant, according to our benchmarks. + } + } + } + + namespace + { + // The own_f and own_nf tell us whether we can modify the aut_f + // and aut_nf automata inplace. + static bool do_si_check(const_twa_graph_ptr aut_f, bool own_f, + const_twa_graph_ptr aut_nf, bool own_nf, + int algo) + { + auto cl = [](const_twa_graph_ptr a, bool own) { + if (own) + return closure_inplace(std::const_pointer_cast + (std::move(a))); + return closure(std::move(a)); + }; + auto sl_2 = [](const_twa_graph_ptr a, bool own) { + if (own) + return sl2_inplace(std::const_pointer_cast(std::move(a))); + return sl2(std::move(a)); + }; + + switch (algo) + { + case 1: // sl(aut_f) x sl(aut_nf) + return product(sl(std::move(aut_f)), + sl(std::move(aut_nf)))->is_empty(); + case 2: // sl(cl(aut_f)) x aut_nf + return product(sl(cl(std::move(aut_f), own_f)), + std::move(aut_nf))->is_empty(); + case 3: // (cl(sl(aut_f)) x aut_nf + return product(closure_inplace(sl(std::move(aut_f))), + std::move(aut_nf))->is_empty(); + case 4: // sl2(aut_f) x sl2(aut_nf) + return product(sl_2(std::move(aut_f), own_f), + sl_2(std::move(aut_nf), own_nf)) + ->is_empty(); + case 5: // sl2(cl(aut_f)) x aut_nf + return product(sl2_inplace(cl(std::move(aut_f), own_f)), + std::move(aut_nf))->is_empty(); + case 6: // (cl(sl2(aut_f)) x aut_nf + return product(closure_inplace(sl_2(std::move(aut_f), own_f)), + std::move(aut_nf))->is_empty(); + case 7: // on-the-fly sl(aut_f) x sl(aut_nf) + return otf_product(make_tgbasl(std::move(aut_f)), + make_tgbasl(std::move(aut_nf)))->is_empty(); + case 8: // cl(aut_f) x cl(aut_nf) + return product(cl(std::move(aut_f), own_f), + cl(std::move(aut_nf), own_nf))->is_empty(); + default: + throw std::runtime_error("is_stutter_invariant(): " + "invalid algorithm number"); + SPOT_UNREACHABLE(); + } + } + + bool + is_stutter_invariant_aux(twa_graph_ptr aut_f, + bool own_f, + const_twa_graph_ptr aut_nf = nullptr, + int algo = 0) + { + trival si = aut_f->prop_stutter_invariant(); + if (si.is_known()) + return si.is_true(); + if (aut_nf) + { + trival si_n = aut_nf->prop_stutter_invariant(); + if (si_n.is_known()) + { + bool res = si_n.is_true(); + aut_f->prop_stutter_invariant(res); + return res; + } + } + + if (algo == 0) + algo = default_stutter_check_algorithm(); + + bool own_nf = false; + if (!aut_nf) + { + twa_graph_ptr tmp = aut_f; + if (!is_deterministic(aut_f)) + { + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + tmp = p.run(aut_f); + } + aut_nf = dualize(std::move(tmp)); + own_nf = true; + } + bool res = do_si_check(aut_f, own_f, + std::move(aut_nf), own_nf, + algo); + aut_f->prop_stutter_invariant(res); + return res; + } + } bool - is_stutter_invariant(formula f) + is_stutter_invariant(twa_graph_ptr aut_f, + const_twa_graph_ptr aut_nf, + int algo) + { + return is_stutter_invariant_aux(aut_f, false, aut_nf, algo); + } + + bool + is_stutter_invariant(formula f, twa_graph_ptr aut_f) { if (f.is_ltl_formula() && f.is_syntactic_stutter_invariant()) return true; @@ -562,55 +658,18 @@ namespace spot } // Prepare for an automata-based check. - translator trans; - auto aut_f = trans.run(f); - auto aut_nf = trans.run(formula::Not(f)); - bdd aps = atomic_prop_collect_as_bdd(f, aut_f); - return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps, algo); - } - - bool - is_stutter_invariant(twa_graph_ptr&& aut_f, - twa_graph_ptr&& aut_nf, bdd aps, int algo) - { - if (algo == 0) - algo = default_stutter_check_algorithm(); - - switch (algo) + translator trans(aut_f ? aut_f->get_dict() : make_bdd_dict()); + bool own_f = false; + if (!aut_f) { - case 1: // sl(aut_f) x sl(aut_nf) - return product(sl(std::move(aut_f), aps), - sl(std::move(aut_nf), aps))->is_empty(); - case 2: // sl(cl(aut_f)) x aut_nf - return product(sl(closure(std::move(aut_f)), aps), - std::move(aut_nf))->is_empty(); - case 3: // (cl(sl(aut_f)) x aut_nf - return product(closure(sl(std::move(aut_f), aps)), - std::move(aut_nf))->is_empty(); - case 4: // sl2(aut_f) x sl2(aut_nf) - return product(sl2(std::move(aut_f), aps), - sl2(std::move(aut_nf), aps))->is_empty(); - case 5: // sl2(cl(aut_f)) x aut_nf - return product(sl2(closure(std::move(aut_f)), aps), - std::move(aut_nf))->is_empty(); - case 6: // (cl(sl2(aut_f)) x aut_nf - return product(closure(sl2(std::move(aut_f), aps)), - std::move(aut_nf))->is_empty(); - case 7: // on-the-fly sl(aut_f) x sl(aut_nf) - return otf_product(make_tgbasl(aut_f, aps), - make_tgbasl(aut_nf, aps))->is_empty(); - case 8: // cl(aut_f) x cl(aut_nf) - return product(closure(std::move(aut_f)), - closure(std::move(aut_nf)))->is_empty(); - default: - throw std::runtime_error("invalid algorithm number for " - "is_stutter_invariant()"); - SPOT_UNREACHABLE(); + aut_f = trans.run(f); + own_f = true; } + return is_stutter_invariant_aux(aut_f, own_f, trans.run(formula::Not(f))); } trival - check_stutter_invariance(const twa_graph_ptr& aut, formula f, + check_stutter_invariance(twa_graph_ptr aut, formula f, bool do_not_determinize) { trival is_stut = aut->prop_stutter_invariant(); @@ -619,33 +678,15 @@ namespace spot twa_graph_ptr neg = nullptr; if (f) - { - neg = translator(aut->get_dict()).run(formula::Not(f)); - } - else - { - twa_graph_ptr tmp = aut; - if (!is_deterministic(aut)) - { - if (do_not_determinize) - return trival::maybe(); - spot::postprocessor p; - p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic); - p.set_level(spot::postprocessor::Low); - tmp = p.run(aut); - } - neg = dualize(tmp); - } + neg = translator(aut->get_dict()).run(formula::Not(f)); + else if (!is_deterministic(aut) && do_not_determinize) + return trival::maybe(); - is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), - std::move(neg), aut->ap_vars()); - aut->prop_stutter_invariant(is_stut); - return is_stut; + return is_stutter_invariant(aut, std::move(neg)); } std::vector - stutter_invariant_states(const const_twa_graph_ptr& pos, formula f, + stutter_invariant_states(const_twa_graph_ptr pos, formula f, bool local) { if (f.is_syntactic_stutter_invariant() @@ -657,7 +698,7 @@ namespace spot // Based on an idea by Joachim Klein. std::vector - stutter_invariant_states(const const_twa_graph_ptr& pos, + stutter_invariant_states(const_twa_graph_ptr pos, const_twa_graph_ptr neg, bool local) { @@ -720,7 +761,7 @@ namespace spot namespace { static - void highlight_vector(const twa_graph_ptr& aut, + void highlight_vector(twa_graph_ptr aut, const std::vector& v, unsigned color) { @@ -742,7 +783,7 @@ namespace spot } void - highlight_stutter_invariant_states(const twa_graph_ptr& pos, + highlight_stutter_invariant_states(twa_graph_ptr pos, formula f, unsigned color, bool local) { @@ -750,7 +791,7 @@ namespace spot } void - highlight_stutter_invariant_states(const twa_graph_ptr& pos, + highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg, unsigned color, bool local) { diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index ba2bf9099..bebb5910e 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -21,79 +21,220 @@ #include +/// \defgroup stutter_inv Stutter-invariance checks and related functions + namespace spot { + /// \ingroup stutter_inv + /// \brief Close the automaton by allowing letters to be duplicated. + /// + /// Any letter that enters a state will spawn a copy of this state + /// with a self-loop using the same letter. For more details + /// about this function, see + /** \verbatim + @InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for + {$\omega$}-Regular Languages}, + booktitle = {Proceedings of the 22th International SPIN + Symposium on Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug + } + \endverbatim */ SPOT_API twa_graph_ptr - sl(const twa_graph_ptr&); + sl(const_twa_graph_ptr aut); + + /// @{ + /// \ingroup stutter_inv + /// \brief Close the automaton by allowing letters to be duplicated. + /// + /// For any transition (s,d) labeled by a letter ℓ, we add a state x + /// and three transitions (s,x), (x,x), (x,d) all labeled by ℓ. + /// For more details about this function, see + /** \verbatim + @InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for + {$\omega$}-Regular Languages}, + booktitle = {Proceedings of the 22th International SPIN + Symposium on Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug + } + \endverbatim */ + /// + /// The inplace version of the function modifies the input + /// automaton. + SPOT_API twa_graph_ptr + sl2_inplace(twa_graph_ptr aut); SPOT_API twa_graph_ptr - sl(const const_twa_graph_ptr&, bdd); + sl2(const_twa_graph_ptr aut); + /// @} + + /// @{ + /// \ingroup stutter_inv + /// \brief Close the automaton by allowing duplicate letter removal. + /// + /// This is done by adding shortcuts into the automaton. If (x,y) is + /// a transition labeled by B, and (y,z) is a transition labeled by C, + /// we add a transition (x,z) labeled by B∧C. + /// + /// For more details about this function, see + /** \verbatim + @InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for + {$\omega$}-Regular Languages}, + booktitle = {Proceedings of the 22th International SPIN + Symposium on Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug + } + \endverbatim */ + /// + /// + /// The inplace version of the function modifies the input + /// automaton. + SPOT_API twa_graph_ptr + closure_inplace(twa_graph_ptr aut); SPOT_API twa_graph_ptr - sl2(const twa_graph_ptr&); + closure(const_twa_graph_ptr aut); + /// @} - SPOT_API twa_graph_ptr - sl2(const const_twa_graph_ptr&, bdd); - -#ifndef SWIG - SPOT_API twa_graph_ptr - sl2(twa_graph_ptr&&, bdd = bddfalse); -#endif - - SPOT_API twa_graph_ptr - closure(const const_twa_graph_ptr&); - -#ifndef SWIG - SPOT_API twa_graph_ptr - closure(twa_graph_ptr&&); -#endif - - /// \ingroup ltl_misc - /// \brief Check if a formula has the stutter invariance property. + /// \ingroup stutter_inv + /// \brief Check if a formula is stutter invariant. + /// + /// It first calls spot::formula::is_syntactic_stutter_invariant() + /// to test for the absence of X, but if some X is found, is an + /// automaton-based check is performed to detect reliably (and + /// rather efficiently) whether the language is actually + /// stutter-invariant. + /// + /// If you already have an automaton for f, passing it at a second + /// argument will save some time. If you also have an automaton for + /// the negation of f, it is better to use the overload of + /// is_stutter_invariant() that takes two automata. + /// + /// The prop_stutter_invariant() property of \a aut_f is set as a + /// side-effect. + /// + /// For more details about this function, see + /** \verbatim + @InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for + {$\omega$}-Regular Languages}, + booktitle = {Proceedings of the 22th International SPIN + Symposium on Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug + } + \endverbatim */ SPOT_API bool - is_stutter_invariant(formula f); + is_stutter_invariant(formula f, twa_graph_ptr aut_f = nullptr); + /// \ingroup stutter_inv + /// \brief Check if an automaton has the stutter invariance + /// property. + /// + /// The automaton-based check requires the complement automaton to + /// be built. If you have one, passing it as the second argument + /// will avoid a costly determinization in case \a aut_f is + /// non-deterministic. + /// + /// The prop_stutter_invariant() property of \a aut_f is set as a + /// side-effect. + /// + /// For more details about this function, see + /** \verbatim + @InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for + {$\omega$}-Regular Languages}, + booktitle = {Proceedings of the 22th International SPIN + Symposium on Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug + } + \endverbatim */ SPOT_API bool - is_stutter_invariant(twa_graph_ptr&& aut_f, - twa_graph_ptr&& aut_nf, bdd aps, + is_stutter_invariant(twa_graph_ptr aut_f, + const_twa_graph_ptr aut_nf = nullptr, int algo = 0); + /// \ingroup stutter_inv /// \brief Check whether \a aut is stutter-invariant /// - /// This procedure requires the negation of \a aut to - /// be computed. This is easily done of \a aut is deterministic - /// or if a formula represented by \a aut is known. Otherwise - /// \a aut will be complemented by determinization, which can + /// This procedure requires the negation of \a aut_f to + /// be computed. This is easily done of \a aut_f is deterministic + /// or if a formula represented by \a aut_f is known. Otherwise + /// \a aut_f will be complemented by determinization, which can /// be expansive. The determinization can be forbidden using /// the \a do_not_determinize flag. /// /// If no complemented automaton could be constructed, the /// the result will be returned as trival::maybe(). + /// + /// This variant of is_stutter_invariant() is used for the + /// --check=stutter option of command-line tools. SPOT_API trival - check_stutter_invariance(const twa_graph_ptr& aut, + check_stutter_invariance(twa_graph_ptr aut_f, formula f = nullptr, bool do_not_determinize = false); ///@{ + /// \ingroup stutter_inv /// \brief Determinate the states that are stutter-invariant in \a pos. /// + /// A state is stutter-invariant if the language recognized from + /// this state is stutter-invariant, or if the state can only be + /// reached by passing though a stutter-invariant state. + /// /// The algorithm needs to compute the complement of \a pos. You can /// avoid that costly operation by either supplying the complement /// automaton, or supplying a formula for the (positive) automaton. SPOT_API std::vector - stutter_invariant_states(const const_twa_graph_ptr& pos, + stutter_invariant_states(const_twa_graph_ptr pos, const_twa_graph_ptr neg = nullptr, bool local = false); SPOT_API std::vector - stutter_invariant_states(const const_twa_graph_ptr& pos, formula f_pos, + stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos, bool local = false); ///@} ///@{ + /// \ingroup stutter_inv /// \brief Highlight the states of \a pos that are stutter-invariant. /// + /// A state is stutter-invariant if the language recognized from + /// this state is stutter-invariant, or if the state can only be + /// reached by passing though a stutter-invariant state. + /// /// The algorithm needs to compute the complement of \a pos. You can /// avoid that costly operation by either supplying the complement /// automaton, or supplying a formula for the (positive) automaton. @@ -104,11 +245,11 @@ namespace spot /// stutter_invariant_states(), and using the resulting vector to /// setup the "highlight-states" property of the automaton. SPOT_API void - highlight_stutter_invariant_states(const twa_graph_ptr& pos, + highlight_stutter_invariant_states(twa_graph_ptr pos, formula f_pos, unsigned color = 0, bool local = false); SPOT_API void - highlight_stutter_invariant_states(const twa_graph_ptr& pos, + highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg = nullptr, unsigned color = 0, bool local = false); diff --git a/tests/Makefile.am b/tests/Makefile.am index 017decc34..7763accfa 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -333,7 +333,7 @@ TESTS_ipython = \ python/product.ipynb \ python/randaut.ipynb \ python/randltl.ipynb \ - python/stutter-inv-states.ipynb \ + python/stutter-inv.ipynb \ python/testingaut.ipynb \ python/word.ipynb diff --git a/tests/python/stutter-inv-states.ipynb b/tests/python/stutter-inv.ipynb similarity index 65% rename from tests/python/stutter-inv-states.ipynb rename to tests/python/stutter-inv.ipynb index 5fe738bb1..bb104dbad 100644 --- a/tests/python/stutter-inv-states.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.3" }, "name": "" }, @@ -29,7 +29,7 @@ "collapsed": false, "input": [ "import spot\n", - "spot.setup(show_default='.ba')\n", + "spot.setup(show_default='.ban')\n", "from IPython.display import display" ], "language": "python", @@ -41,9 +41,415 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Detecting stutter-invariant states\n", + "# Stutter-invariant languages\n", "\n", - "Spot can easily check whether a formula is stutter invariant. The check is automaton-based, so it can detect stutter invariant formulas even if they use the `X` operator as `f1` below." + "A language $L$ is said to be _stutter-invariant_ iff $\\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_{i+1}\\ldots\\in L \\iff \\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_i\\ell_{i+1}\\ldots\\in L$, i.e., if duplicating a letter in a word or removing a duplicated letter does not change the membership of that word to $L$. These languages are also called _stutter-insensitive_. We use the adjective _sutter-sensitive_ to describe a language that is not stutter-invariant. Of course we can extend this vocabulary to LTL formulas or automata that represent stutter-invariant languages.\n", + "\n", + "Stutter-invariant languages play an important role in model checking. When verifying a stutter-invariant specification against a system, we know that we have some freedom in how we discretize the time in the model: as long as we do not hide changes of model variables that are observed by the specification, we can merge multiple steps of the model. This, combined by careful analysis of actions of the model that are independent, is the basis for a set of techniques known as _partial-order reductions_ (POR) that postpone the visit of some successors in the model, because we know we can always visit them later." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Stutter-invariant formulas\n", + "\n", + "When the specification is expressed as an LTL formula, a well known way to ensure it is _stutter-invariant_ is to forbid the use of the `X` operator. Testing whether a formula is `X`-free can be done in constant time using the `is_syntactic_stutter_invariant()` method." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.formula('a U b')\n", + "print(f.is_syntactic_stutter_invariant())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "True\n" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.formula('a U Xb')\n", + "print(f.is_syntactic_stutter_invariant())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "False\n" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "However some formula are syntactic-invariant despite their use of `X`. Spot implements some [automaton-based check](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) to detect stutter-invariance reliably and efficiently. This can be tested with the `is_stutter_invariant()` function." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "g = spot.formula('F(a & X(!a & Gb))')\n", + "print(g.is_syntactic_stutter_invariant())\n", + "print(spot.is_stutter_invariant(g))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "False\n", + "True\n" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Of course this `is_stutter_invariant()` function first checks whether the formula is `X`-free before wasting time building automata, so if you want to detect stutter-invariant formulas in your model checker, this is the only function to use. Also, if you hapen to already have an automaton `aut_g` for `g`, you should pass it as a second argument to avoid it being recomputed: `spot.is_stutter_invariant(g, aut_g)`." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "It is also known that any stutter-invariant LTL formula can be converted to an `X`-free LTL formula. Several proofs of that exist. Spot implements the rewriting of [K. Etessami](http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps) under the name `remove_x()`. Note that the output of this function is only equivalent to its input if the latter is stutter-invariant." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.remove_x(g)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land \\lnot b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land \\mathsf{G} b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} b \\lor \\mathsf{G} \\lnot b))))$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "text": [ + "F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & !b & Gb)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "Stutter-invariant automata" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Similarly to formulas, automata use a few bits to store some known properties about themselves, like whether they represent a stutter-invariant language. This property can be checked with the `prop_stutter_invariant()` method, but that returns a `trival` instance (i.e., yes, no, or maybe). Some algorithms will update that property whenever that is cheap or expliclitely asked for. For instance `spot.translate()` only sets the property if the translated formula is `X`-free." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.translate(g)\n", + "print(aut.prop_stutter_invariant())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "maybe\n" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "As suggested above, we can call `is_stutter_invariant()` by passing a formula and its automaton, to save on one translation. A second translation is still needed to complement the automaton." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.is_stutter_invariant(g, aut))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "True\n" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that `prop_stutter_invariant()` was updated as a side-effect so that any futher call to `is_stutter_invariant()` with this automaton will be instantaneous." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(aut.prop_stutter_invariant())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "yes\n" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "You have to be aware of this property being set in your back because if while playing with `is_stutter_invariant()` you the incorrect formula for an automaton by mistake, the automaton will have its property set incorrectly, and running `is_stutter_inariant()` with the correct formula will simply return the cached property.\n", + "\n", + "In doubt, you can always reset the property as follows:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut.prop_stutter_invariant(spot.trival_maybe())\n", + "print(aut.prop_stutter_invariant())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "maybe\n" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In case you have an automaton for which you do not have formula, you can also use `is_stutter_invariant()` by passing this automaton as the first argument. In that case a negated automaton will be constructed by determinization. If you do happen to have a negated automaton handy, you can pass it as a second argument to avoid that." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a1 = spot.automaton('''HOA: v1 \n", + "AP: 1 \"a\" \n", + "States: 2 \n", + "Start: 0 \n", + "Acceptance: 0 t\n", + "--BODY-- \n", + "State: 0 [0] 1 \n", + "State: 1 [t] 0 \n", + "--END--''')\n", + "display(a1)\n", + "print(spot.is_stutter_invariant(a1))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1c8045a660> >" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "False\n" + ] + } + ], + "prompt_number": 10 + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "Explaining why a formula is not sutter-invariant" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "As explained in our [Spin'15 paper](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) the sutter-invariant checks are implemented using simple operators suchs as `spot.closure(aut)`, that augment the language of L by adding words that can be obtained by removing duplicated letters, and `spot.sl(aut)` or `spot.sl2(aut)` that both augment the language that L by adding words that can be obtained by duplicating letters. The default `is_stutter_invariant()` function is implemented as `spot.product(spot.closure(aut), spot.closure(neg_aut)).is_empty()`, but that is just one possible implementation selected because it was more efficient.\n", + "\n", + "Using these bricks, we can modify the original algorithm so it uses a counterexample to explain why a formula is stutter-sensitive." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "def explain_stut(f):\n", + " f = spot.formula(f)\n", + " pos = spot.translate(f)\n", + " neg = spot.translate(spot.formula_Not(f))\n", + " word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word()\n", + " if word is None:\n", + " print(f, \"is stutter invariant\")\n", + " return\n", + " word.simplify()\n", + " waut = word.as_automaton()\n", + " if waut.intersects(pos):\n", + " acc, rej, aut = \"accepted\", \"rejected\", neg\n", + " else:\n", + " acc, rej, aut = \"rejected\", \"accepted\", pos\n", + " word2 = spot.sl2(waut).intersecting_word(aut)\n", + " word2.simplify()\n", + " print(\"\"\"{} is {} by {}\n", + " but if we stutter some of its letters, we get\n", + "{} which is {} by {}\"\"\".format(word, acc, f, word2, rej, f))" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 25 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "explain_stut('GF(a & Xb)')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "cycle{!a & !b; a & b} is rejected by GF(a & Xb)\n", + " but if we stutter some of its letters, we get\n", + "cycle{!a & !b; a & b; a & b} which is accepted by GF(a & Xb)\n" + ] + } + ], + "prompt_number": 26 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Detecting stutter-invariant states\n", + "\n", + "Even if the language of an automaton is not sutter invariant, some of its states may recognize a stutter-invariant language. (We assume the language of a state is the language the automaton would have when starting from this state.)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### First example\n", + "\n", + "For instance let us build a disjunction of a stutter-invariant formula and a stutter-sensitive one:" ] }, { @@ -71,7 +477,7 @@ ] } ], - "prompt_number": 2 + "prompt_number": 13 }, { "cell_type": "code", @@ -220,19 +626,19 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1b58d0> >" + " *' at 0x7f1c803f4de0> >" ] } ], - "prompt_number": 3 + "prompt_number": 14 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "While the automaton as a whole is stutter-sensitive, but we can see that eventually we will enter a sub-automaton that is stutter-invariant.\n", + "While the automaton as a whole is stutter-sensitive, we can see that eventually we will enter a sub-automaton that is stutter-invariant.\n", "\n", - "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number." + "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number. A state is marked as `True` if either its language is stutter-invariant, or if it appear below a stutter-invariant state (see the second example later). As always, the second argument, `f`, can be omitted (pass `None`) if the formula is unknown, or it can be replaced by a negated automaton if it is known. " ] }, { @@ -247,20 +653,20 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 4, + "prompt_number": 15, "text": [ "(False, True, False, True, True, True, True, True)" ] } ], - "prompt_number": 4 + "prompt_number": 15 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "The `highligh_...()` version colors the stutter-invariant states of the automaton for display.\n", - "(That 5 is the color number for red.)" + "For convenience, the `highligh_...()` version colors the stutter-invariant states of the automaton for display.\n", + "(That 5 is the color number for red in Spot's hard-coded palette.)" ] }, { @@ -410,25 +816,32 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1b58d0> >" + " *' at 0x7f1c803f4de0> >" ] } ], - "prompt_number": 5 + "prompt_number": 16 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton." + ] }, { "cell_type": "heading", - "level": 1, + "level": 3, "metadata": {}, "source": [ - "Another test case" + "Second example" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "The union of two stutter-sensitive formulas can be stutter-invariant. Let's make sure that our checks agree." + "This second example illustrates the fact that a state can be marked if it it not sutter-invariant but appear below a stutter-invariant state. We build our example automaton as the disjuction of the following two stutter-sensitive formulas, whose union is equivalent to the sutter-invariant formula `GF!a`." ] }, { @@ -442,7 +855,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 6 + "prompt_number": 17 }, { "cell_type": "code", @@ -465,26 +878,28 @@ ] } ], - "prompt_number": 7 + "prompt_number": 18 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here are the automata for `g1` and `g2`, note that none of the states are stutter-invariant." + ] }, { "cell_type": "code", "collapsed": false, "input": [ "aut1 = spot.translate(g1)\n", - "aut2 = spot.translate(g2)\n", - "aut = spot.product_or(aut1, aut2)\n", + "aut1.set_name(str(g1))\n", "spot.highlight_stutter_invariant_states(aut1, g1, 5)\n", "display(aut1)\n", + "\n", + "aut2 = spot.translate(g2)\n", + "aut2.set_name(str(g2))\n", "spot.highlight_stutter_invariant_states(aut2, g2, 5)\n", - "display(aut2)\n", - "# At this point it is unknown if AUT is stutter-invariant\n", - "assert(aut.prop_stutter_invariant().is_maybe())\n", - "spot.highlight_stutter_invariant_states(aut, g, 5)\n", - "display(aut)\n", - "# The stutter_invariant property is set on AUT as a side effect\n", - "# of calling sutter_invariant_states() or some variant of it.\n", - "assert(aut.prop_stutter_invariant().is_true())" + "display(aut2)" ], "language": "python", "metadata": {}, @@ -499,11 +914,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "G(F(a & Xa) & F!a)\n", "Inf(\n", "\u24ff\n", ")&Inf(\n", @@ -563,7 +979,7 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1b5660> >" + " *' at 0x7f1c80480540> >" ] }, { @@ -576,11 +992,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "FG(!a | X!a)\n", "Inf(\n", "\u24ff\n", ")\n", @@ -649,9 +1066,35 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1ce720> >" + " *' at 0x7f1c8045a6c0> >" ] - }, + } + ], + "prompt_number": 19 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Now we build the sum of these to automata. The stutter-invariance check detects that the initial state is stutter-invariant (i.e., the entire language is stutter-invariant) so all states below it are marked despite the fact that the language recognized from these individual states would not be stutter-invariant." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.sum(aut1, aut2)\n", + "# At this point it is unknown if AUT is stutter-invariant\n", + "assert(aut.prop_stutter_invariant().is_maybe())\n", + "spot.highlight_stutter_invariant_states(aut, g, 5)\n", + "display(aut)\n", + "# The stutter_invariant property is set on AUT as a side effect\n", + "# of calling sutter_invariant_states() or any variant of it.\n", + "assert(aut.prop_stutter_invariant().is_true())" + ], + "language": "python", + "metadata": {}, + "outputs": [ { "metadata": {}, "output_type": "display_data", @@ -662,327 +1105,347 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")) | Inf(\n", - "\u2777\n", - ")\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")) | Inf(\n", + "\u2777\n", + ")\n", "\n", - "\n", - "0\n", - "\n", - "0,0\n", + "\n", + "5\n", + "\n", + "5\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->5\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\u2776\n", + "\n", + "\n", + "!a\n", + "\u2776\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "1\n", - "\n", - "0,1\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\u2776\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", - "\n", - "2\n", - "\n", - "0,2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "3\n", - "\n", - "1,0\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "4\n", - "\n", - "1,2\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a\n", - "\u2776\n", - "\u2777\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", - "\u2777\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "1->4\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\u2777\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a\n", - "\u2776\n", - "\u2777\n", - "\n", - "\n", - "5\n", - "\n", - "0,3\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "6\n", - "\n", - "1,3\n", - "\n", - "\n", - "2->6\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a\n", + "\n", + "2->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "!a\n", + "\u2777\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\u2777\n", "\n", - "\n", - "7\n", - "\n", - "2,0\n", - "\n", - "\n", - "3->7\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "8\n", - "\n", - "2,1\n", - "\n", - "\n", - "3->8\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "4->8\n", - "\n", - "\n", - "!a\n", - "\u2777\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "!a\n", - "\u2776\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "6->5\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "9\n", - "\n", - "2,3\n", - "\n", - "\n", - "6->9\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "7->7\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "7->8\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "10\n", - "\n", - "2,2\n", - "\n", - "\n", - "7->10\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "8->8\n", - "\n", - "\n", - "!a\n", - "\u2777\n", - "\n", - "\n", - "8->10\n", - "\n", - "\n", - "a\n", - "\u2777\n", - "\n", - "\n", - "9->9\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "10->8\n", - "\n", - "\n", - "!a\n", - "\u2777\n", - "\n", - "\n", - "10->9\n", - "\n", - "\n", - "a\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a\n", + "\u2777\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f0b7c1b5810> >" + " *' at 0x7f1c80480660> >" ] } ], - "prompt_number": 8 + "prompt_number": 20 }, { - "cell_type": "heading", - "level": 1, + "cell_type": "markdown", "metadata": {}, "source": [ - "Global vs Local stuttering" + "### Third example\n", + "\n", + "These procedures work regardless of the acceptance condition. Here is an example with state-based co-B\u00fcchi acceptance.\n", + "\n", + "In this case we do not even have a formula to pass as second argument, so the check will perform a costly complementation by determinization." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.automaton('genaut --ks-nca=2 |')\n", + "spot.highlight_stutter_invariant_states(aut, None, 5, True)\n", + "display(aut)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "[co-B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "(!a & b) | (a & !b)\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !b) | (a & b)\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1c80370300> >" + ] + } + ], + "prompt_number": 27 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If the negated automaton is already known, it can be passed as second argument (instead of the positive formula) to avoid unnecessary work." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Global vs Local stuttering (experimental)\n", + "\n", + "Do not build anything on top of what follows, as it is likely to be removed." ] }, { @@ -1088,11 +1551,11 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1ce8a0> >" + " *' at 0x7f1c8045a690> >" ] } ], - "prompt_number": 9 + "prompt_number": 22 }, { "cell_type": "markdown", @@ -1100,7 +1563,10 @@ "source": [ "The above result uses a natural definition of \"stutter-invariant state\": a state is stutter-invariant if the language accepted from this state is.\n", "\n", - "We can also have a \"local\" variant of the stutter invariance check that considers the state as stutter invariant if you can stutter on (or remove duplicates of) the first letter read from that state, but not necessary do the same operations on a different letter that follows. Just pass `True` as the last optional parameter, as below." + "We can also have a \"local\" variant of the stutter invariance check that considers the state as stutter invariant if you can stutter on (or remove duplicates of) the first letter read from that state, but not necessary do the same operations on a different letter that follows. \n", + "In other words, state $q$ is a local stutter-invariant state iff $\\ell_1\\ell_2\\ldots \\in L(q) \\iff \\ell_1\\ell_1\\ell_2\\ldots \\in L(q)$.\n", + "\n", + "Just pass `True` as the last optional parameter, as below." ] }, { @@ -1204,17 +1670,17 @@ "\n" ], "text": [ - " *' at 0x7f0b7c1ce8a0> >" + " *' at 0x7f1c8045a690> >" ] } ], - "prompt_number": 10 + "prompt_number": 23 }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Note that an SCC can contain a mix of locally stutter-invariant and local stutter-sensitive states. So probably POR should be applied between two locally stutter-invariant states? Here is the deterministic version of the above automaton for example." + "Note that an SCC can contain a mix of locally stutter-invariant and local stutter-sensitive states. Here is the deterministic version of the above automaton for example." ] }, { @@ -1381,382 +1847,7 @@ ] } ], - "prompt_number": 11 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Support for more complex acceptance conditions\n", - "\n", - "This also works, although it's not clear how useful that is." - ] - }, - { - "cell_type": "code", - "collapsed": true, - "input": [ - "m = spot.formula('F(a & Xa & Gb) | GF!b')\n", - "aut = spot.translate(m, 'deterministic', 'generic')" - ], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": 12 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "spot.highlight_stutter_invariant_states(aut, m, 5, True)\n", - "display(aut)" - ], - "language": "python", - "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "display_data", - "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ") & (Inf(\n", - "\u2776\n", - ") | (Fin(\n", - "\u2777\n", - ") & Inf(\n", - "\u2778\n", - ")))\n", - "[parity min odd 4]\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\u2776\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!b\n", - "\u2776\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b\n", - "\u2776\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "!b\n", - "\u2776\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "b\n", - "\u2778\n", - "\n", - "\n", - "\n" - ], - "text": [ - " *' at 0x7f0b7c15f600> >" - ] - } - ], - "prompt_number": 13 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Checking an automaton without formula\n", - "\n", - "The check can also be applied on an automaton for which the formula is unknown, but in the case the input automaton will be complemented via determinization, so this is costlier." - ] - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "aut = spot.automaton('genaut --ks-nca=2 |')\n", - "spot.highlight_stutter_invariant_states(aut, None, 5, True)\n", - "display(aut)" - ], - "language": "python", - "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "display_data", - "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", - "[co-B\u00fcchi]\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\u24ff\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "(!a & b) | (a & !b)\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !b) | (a & b)\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a | b\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!a | b\n", - "\n", - "\n", - "\n" - ], - "text": [ - " *' at 0x7f0b7c13e660> >" - ] - } - ], - "prompt_number": 44 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "If the negated automaton is already known, it can be passed as second argument (instead of the positive formula) to avoid unnecessary work." - ] + "prompt_number": 24 } ], "metadata": {}