diff --git a/NEWS b/NEWS index c6b1e22eb..96c29bd4d 100644 --- a/NEWS +++ b/NEWS @@ -113,6 +113,12 @@ 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). + - 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 + https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html for + examples. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/doc/org/tut.org b/doc/org/tut.org index 208c09c90..1de492e0f 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -83,3 +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. diff --git a/python/spot/impl.i b/python/spot/impl.i index fbf311078..32dec7582 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -430,6 +430,7 @@ namespace std { %template(liststr) list; %template(vectorformula) vector; %template(vectorunsigned) vector; + %template(vectorbool) vector; %template(vectorstring) vector; %template(atomic_prop_set) set; %template(relabeling_map) map; diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 474ba4d87..4cb673227 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -30,12 +30,16 @@ #include #include #include +#include +#include +#include #include #include #include #include #include #include +#include namespace spot { @@ -639,4 +643,117 @@ namespace spot aut->prop_stutter_invariant(is_stut); return is_stut; } + + std::vector + stutter_invariant_states(const const_twa_graph_ptr& pos, formula f, + bool local) + { + if (f.is_syntactic_stutter_invariant() + || pos->prop_stutter_invariant().is_true()) + return std::vector(pos->num_states(), true); + auto neg = translator(pos->get_dict()).run(formula::Not(f)); + return stutter_invariant_states(pos, neg, local); + } + + // Based on an idea by Joachim Klein. + std::vector + stutter_invariant_states(const const_twa_graph_ptr& pos, + const_twa_graph_ptr neg, + bool local) + { + std::vector res(pos->num_states(), true); + if (pos->prop_stutter_invariant().is_true()) + return res; + + if (neg == nullptr) + { + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + neg = dualize(p.run(std::const_pointer_cast(pos))); + } + + auto product_states = [](const const_twa_graph_ptr& a) + { + return (a->get_named_prop>> + ("product-states")); + }; + + // Get the set of states (x,y) that appear in the product P1=pos*neg. + std::set> pairs = [&]() + { + twa_graph_ptr prod = spot::product(pos, neg); + auto goodstates = product_states(prod); + std::set> pairs(goodstates->begin(), + goodstates->end()); + return pairs; + }(); + + // Compute P2=cl(pos)*cl(neg). A state x of pos is stutter-sensitive + // if there exists a state (x,y) in both P1 and P2 that as a successor + // in the useful part of P2 and that is not in P1. + twa_graph_ptr prod = spot::product(closure(pos), closure(neg)); + auto prod_pairs = product_states(prod); + scc_info si(prod, scc_info_options::TRACK_SUCCS + | scc_info_options::TRACK_STATES_IF_FIN_USED); + si.determine_unknown_acceptance(); + unsigned n = prod->num_states(); + bool sinv = true; + + for (unsigned s = 0; s < n; ++s) + { + if (!si.is_useful_scc(si.scc_of(s))) + continue; + if (pairs.find((*prod_pairs)[s]) == pairs.end()) + continue; + for (auto& e: prod->out(s)) + if (si.is_useful_scc(si.scc_of(e.dst))) + if (!local || pairs.find((*prod_pairs)[e.dst]) == pairs.end()) + res[(*prod_pairs)[s].first] = sinv = false; + } + std::const_pointer_cast(pos)->prop_stutter_invariant(sinv); + std::const_pointer_cast(neg)->prop_stutter_invariant(sinv); + return res; + } + + namespace + { + static + void highlight_vector(const twa_graph_ptr& aut, + const std::vector& v, + unsigned color) + { + // Create the highlight-states property only if it does not + // exist already. + auto hs = + aut->get_named_prop>("highlight-states"); + if (!hs) + { + hs = new std::map; + aut->set_named_prop("highlight-states", hs); + } + + unsigned n = v.size(); + for (unsigned i = 0; i < n; ++i) + if (v[i]) + hs->emplace(i, color); + } + } + + void + highlight_stutter_invariant_states(const twa_graph_ptr& pos, + formula f, unsigned color, + bool local) + { + highlight_vector(pos, stutter_invariant_states(pos, f, local), color); + } + + void + highlight_stutter_invariant_states(const twa_graph_ptr& pos, + const_twa_graph_ptr neg, + unsigned color, bool local) + { + highlight_vector(pos, stutter_invariant_states(pos, neg, local), color); + } } diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index b494ed134..ba2bf9099 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2014-2017 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -73,4 +73,44 @@ namespace spot check_stutter_invariance(const twa_graph_ptr& aut, formula f = nullptr, bool do_not_determinize = false); + + + ///@{ + /// \brief Determinate the states that are stutter-invariant in \a pos. + /// + /// 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, + 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, + bool local = false); + ///@} + + ///@{ + /// \brief Highlight the states of \a pos that are stutter-invariant. + /// + /// 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. + /// + /// The \a color argument is an index in a predefined set of colors. + /// + /// This function simply works by calling + /// 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, + formula f_pos, unsigned color = 0, + bool local = false); + SPOT_API void + highlight_stutter_invariant_states(const 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 522e76675..42dc36dfe 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -332,6 +332,7 @@ TESTS_ipython = \ python/product.ipynb \ python/randaut.ipynb \ python/randltl.ipynb \ + python/stutter-inv-states.ipynb \ python/testingaut.ipynb \ python/word.ipynb diff --git a/tests/python/stutter-inv-states.ipynb b/tests/python/stutter-inv-states.ipynb new file mode 100644 index 000000000..5fe738bb1 --- /dev/null +++ b/tests/python/stutter-inv-states.ipynb @@ -0,0 +1,1765 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.4" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "spot.setup(show_default='.ba')\n", + "from IPython.display import display" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Detecting stutter-invariant states\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." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')\n", + "f2 = spot.formula('F(a & Xa & XXa & G!b)')\n", + "f = spot.formula_Or([f1, f2])\n", + "\n", + "print(spot.is_stutter_invariant(f1))\n", + "print(spot.is_stutter_invariant(f2))\n", + "print(spot.is_stutter_invariant(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "True\n", + "False\n", + "False\n" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "pos = spot.translate(f)\n", + "display(pos)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1b58d0> >" + ] + } + ], + "prompt_number": 3 + }, + { + "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", + "\n", + "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.stutter_invariant_states(pos, f)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "text": [ + "(False, True, False, True, True, True, True, True)" + ] + } + ], + "prompt_number": 4 + }, + { + "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.)" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.highlight_stutter_invariant_states(pos, f, 5)\n", + "display(pos)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1b58d0> >" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "heading", + "level": 1, + "metadata": {}, + "source": [ + "Another test case" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The union of two stutter-sensitive formulas can be stutter-invariant. Let's make sure that our checks agree." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "g1 = spot.formula('GF(a & Xa) & GF!a')\n", + "g2 = spot.formula('!GF(a & Xa) & GF!a')\n", + "g = spot.formula_Or([g1, g2])" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 6 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.is_stutter_invariant(g1))\n", + "print(spot.is_stutter_invariant(g2))\n", + "print(spot.is_stutter_invariant(g))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "False\n", + "False\n", + "True\n" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut1 = spot.translate(g1)\n", + "aut2 = spot.translate(g2)\n", + "aut = spot.product_or(aut1, aut2)\n", + "spot.highlight_stutter_invariant_states(aut1, g1, 5)\n", + "display(aut1)\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())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "[gen. B\u00fcchi 2]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1b5660> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1ce720> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")) | Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "0,1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\u2776\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", + "\n", + "1->1\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\u2777\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2777\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", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\u24ff\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", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1b5810> >" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "heading", + "level": 1, + "metadata": {}, + "source": [ + "Global vs Local stuttering" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "h = spot.formula('F(a & X(!a & X(b & Xb)))')\n", + "aut = spot.translate(h)\n", + "spot.highlight_stutter_invariant_states(aut, h, 5)\n", + "display(aut)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1ce8a0> >" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "markdown", + "metadata": {}, + "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." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n", + "display(aut)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f0b7c1ce8a0> >" + ] + } + ], + "prompt_number": 10 + }, + { + "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." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.translate(h, 'deterministic')\n", + "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n", + "display(aut.show('.abs'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u24ff\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "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." + ] + } + ], + "metadata": {} + } + ] +}