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

python: implicit str->formula conversion

Browse source 
* python/spot/impl.i, python/spot/__init__.py: Implement it.
* NEWS: Mention it.
* tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb,
tests/python/ltsmin-pml.ipynb, tests/python/stutter-inv.ipynb,
doc/org/tut02.org: Modernize.
This commit is contained in:
Alexandre Duret-Lutz 2018-05-15 16:07:14 +02:00
parent 5c1d9c492c
commit 6a808492c1
10 changed files with 168 additions and 210 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -81,6 +81,10 @@ New in spot 2.5.3.dev (not yet released)
See https://spot.lrde.epita.fr/ipynb/alternation.html for some See https://spot.lrde.epita.fr/ipynb/alternation.html for some
examples. examples.
- Strings are now implicitely converted into formulas when passed
as arguments to functions that expect formulas. Previously this
was done only for a few functions.
Bugs fixed: Bugs fixed:
- print_dot() will correctly escape strings containing \n in HTML - print_dot() will correctly escape strings containing \n in HTML

9
doc/org/tut02.org
View file

@ -62,18 +62,17 @@ pairs of atomic propositions of the form (new-name, old-name).
#+BEGIN_SRC python :results output :exports both #+BEGIN_SRC python :results output :exports both
import spot import spot
f = spot.formula('"Proc@Here" U ("var > 10" | "var < 4")')
m = spot.relabeling_map() m = spot.relabeling_map()
g = spot.relabel(f, spot.Pnn, m) g = spot.relabel('"Proc@Here" U ("var > 10" | "var < 4")', spot.Pnn, m)
for newname, oldname in m.items(): for newname, oldname in m.items():
print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True))) print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True)))
print(g.to_str('spin', True)) print(g.to_str('spin', True))
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: #define p0 ((Proc@Here)) : #define p0 (Proc@Here)
: #define p1 ((var < 4)) : #define p1 (var < 4)
: #define p2 ((var > 10)) : #define p2 (var > 10)
: (p0) U ((p1) || (p2)) : (p0) U ((p1) || (p2))
* C++ * C++

28
python/spot/__init__.py
View file

@ -675,26 +675,18 @@ def translate(formula, *args, dict=_bdd_dict):
formula.translate = translate formula.translate = translate
def contains(left, right): # Wrap C++-functions into lambdas so that they get converted into
from spot.impl import contains as contains_impl # instance methods (i.e., self passed as first argument
if type(left) is str: # automatically), because only user-defined functions are converted as
left = formula(left) # instance methods.
if type(right) is str: def _add_formula(meth, name = None):
right = formula(right) setattr(formula, name or meth, (lambda self, *args, **kwargs:
return contains_impl(left, right) globals()[meth](self, *args, **kwargs)))
def are_equivalent(left, right):
from spot.impl import are_equivalent as equiv
if type(left) is str:
left = formula(left)
if type(right) is str:
right = formula(right)
return equiv(left, right)
formula.contains = contains _add_formula('contains')
formula.equivalent_to = are_equivalent _add_formula('are_equivalent', 'equivalent_to')
twa.contains = contains
twa.equivalent_to = are_equivalent
def postprocess(automaton, *args, formula=None): def postprocess(automaton, *args, formula=None):
"""Post process an automaton. """Post process an automaton.

9
python/spot/impl.i
View file

@ -365,7 +365,8 @@ namespace swig
// default to None on the Python side. // default to None on the Python side.
%typemap(in) spot::formula { %typemap(in) spot::formula {
void *tmp; void *tmp;
int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*), 0); int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*),
SWIG_POINTER_IMPLICIT_CONV);
if (!SWIG_IsOK(res)) { if (!SWIG_IsOK(res)) {
%argument_fail(res, "spot::formula", $symname, $argnum); %argument_fail(res, "spot::formula", $symname, $argnum);
} }
@ -377,9 +378,10 @@ namespace swig
// if tmp == nullptr, then the default value of $1 is fine. // if tmp == nullptr, then the default value of $1 is fine.
} }
%typemap(typecheck) spot::formula { %typemap(typecheck, precedence=2000) spot::formula {
$1 = SWIG_CheckState(SWIG_ConvertPtr($input, nullptr, $1 = SWIG_CheckState(SWIG_ConvertPtr($input, nullptr,
$descriptor(spot::formula*), 0)); $descriptor(spot::formula*),
SWIG_POINTER_IMPLICIT_CONV));
} }
%typemap(out) spot::formula { %typemap(out) spot::formula {
@ -427,6 +429,7 @@ namespace swig
%include <spot/misc/trival.hh> %include <spot/misc/trival.hh>
%implicitconv std::vector<spot::formula>; %implicitconv std::vector<spot::formula>;
%implicitconv spot::formula;
%include <spot/tl/formula.hh> %include <spot/tl/formula.hh>

8
tests/python/atva16-fig2a.ipynb
View file

@ -4,7 +4,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"." "This example is the left part of Fig.2 in our ATVA'16 paper titled [\"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"](https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf), slightly updated to the current version of Spot."
] ]
}, },
{ {
@ -14,7 +14,7 @@
"outputs": [], "outputs": [],
"source": [ "source": [
"import spot\n", "import spot\n",
"spot.setup(show_default='.abr')" "spot.setup(show_default='.b')"
] ]
}, },
{ {
@ -155,7 +155,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3264654bd0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f81a85ea1e0> >"
] ]
}, },
"execution_count": 3, "execution_count": 3,
@ -175,7 +175,7 @@
"source": [ "source": [
"def implies(f, g):\n", "def implies(f, g):\n",
" f = spot.formula(f)\n", " f = spot.formula(f)\n",
" g = spot.formula_Not(spot.formula(g))\n", " g = spot.formula.Not(g)\n",
" return spot.product(f.translate(), g.translate()).is_empty()\n", " return spot.product(f.translate(), g.translate()).is_empty()\n",
"def equiv(f, g):\n", "def equiv(f, g):\n",
" return implies(f, g) and implies(g, f)" " return implies(f, g) and implies(g, f)"

25
tests/python/atva16-fig2b.ipynb
View file

@ -4,7 +4,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"." "This example is the right part of Fig.2 in our ATVA'16 paper titled [\"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"](https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf) slightly updated to benefit from improvements in more recent versions of Spot."
] ]
}, },
{ {
@ -15,8 +15,8 @@
"source": [ "source": [
"import spot\n", "import spot\n",
"import spot.ltsmin\n", "import spot.ltsmin\n",
"spot.setup(show_default='.abr', max_states=10)\n", "spot.setup(show_default='.Ab', max_states=10)\n",
"# This extra line ensures that our test-suite skips this test if divine is not installed.\n", "# This extra line ensures that our test suite skips this test if divine is not installed.\n",
"spot.ltsmin.require('divine')" "spot.ltsmin.require('divine')"
] ]
}, },
@ -82,12 +82,10 @@
"<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n", " -->\n",
"<!-- Pages: 1 -->\n", "<!-- Pages: 1 -->\n",
"<svg width=\"734pt\" height=\"177pt\"\n", "<svg width=\"734pt\" height=\"156pt\"\n",
" viewBox=\"0.00 0.00 734.00 177.35\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", " viewBox=\"0.00 0.00 734.00 156.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(.5617 .5617) rotate(0) translate(4 311.7401)\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(.5617 .5617) rotate(0) translate(4 273.7401)\">\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-311.7401 1302.7729,-311.7401 1302.7729,4 -4,4\"/>\n", "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-273.7401 1302.7729,-273.7401 1302.7729,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"646.3864\" y=\"-292.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">t</text>\n",
"<text text-anchor=\"start\" x=\"638.3864\" y=\"-277.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[all]</text>\n",
"<!-- I -->\n", "<!-- I -->\n",
"<!-- 0 -->\n", "<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n", "<g id=\"node2\" class=\"node\">\n",
@ -289,7 +287,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f7cac317630> >" "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f4dc45626f0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
@ -308,10 +306,9 @@
"outputs": [], "outputs": [],
"source": [ "source": [
"def model_check(model, f):\n", "def model_check(model, f):\n",
" f = spot.formula(f)\n", " nf = spot.formula.Not(f)\n",
" ss = model.kripke(spot.atomic_prop_collect(f))\n", " ss = model.kripke(spot.atomic_prop_collect(nf))\n",
" nf = spot.formula_Not(f).translate()\n", " return not ss.intersects(nf.translate())"
" return spot.otf_product(ss, nf).is_empty()"
] ]
}, },
{ {

102
tests/python/formulas.ipynb
View file

@ -11,9 +11,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 1, "execution_count": 1,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [], "outputs": [],
"source": [ "source": [
"import spot" "import spot"
@ -29,9 +27,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 2, "execution_count": 2,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -55,9 +51,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 3, "execution_count": 3,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -87,9 +81,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 4, "execution_count": 4,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -119,9 +111,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 5, "execution_count": 5,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -152,9 +142,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 6, "execution_count": 6,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -181,9 +169,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 7, "execution_count": 7,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"name": "stdout", "name": "stdout",
@ -214,9 +200,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 8, "execution_count": 8,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"name": "stdout", "name": "stdout",
@ -251,9 +235,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 9, "execution_count": 9,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"name": "stdout", "name": "stdout",
@ -316,9 +298,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 10, "execution_count": 10,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -338,9 +318,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 11, "execution_count": 11,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -367,9 +345,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 12, "execution_count": 12,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -389,9 +365,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 13, "execution_count": 13,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -411,9 +385,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 14, "execution_count": 14,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -440,9 +412,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 15, "execution_count": 15,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -465,9 +435,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 16, "execution_count": 16,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -490,9 +458,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 17, "execution_count": 17,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -522,9 +488,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 18, "execution_count": 18,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"name": "stdout", "name": "stdout",
@ -661,9 +625,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 19, "execution_count": 19,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -709,9 +671,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 20, "execution_count": 20,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -731,9 +691,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 21, "execution_count": 21,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -763,9 +721,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 22, "execution_count": 22,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -795,9 +751,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 23, "execution_count": 23,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -821,9 +775,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 24, "execution_count": 24,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"data": { "data": {
@ -853,9 +805,7 @@
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 25, "execution_count": 25,
"metadata": { "metadata": {},
"collapsed": false
},
"outputs": [ "outputs": [
{ {
"name": "stdout", "name": "stdout",
@ -898,7 +848,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.6.4" "version": "3.6.5"
} }
}, },
"nbformat": 4, "nbformat": 4,

29
tests/python/ltsmin-dve.ipynb
View file

@ -436,7 +436,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f77f84535a0> >" "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f2214652270> >"
] ]
}, },
"execution_count": 9, "execution_count": 9,
@ -1194,6 +1194,13 @@
"k.show('.<0') # unlimited output" "k.show('.<0') # unlimited output"
] ]
}, },
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If we have an LTL proposition to check, we can convert it into an automaton using `spot.translate()`, and synchronize that automaton with the Kripke structure using `spot.otf_product()`. This `otf_product()` function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm \"consumes\" it (here the display routine). "
]
},
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 12, "execution_count": 12,
@ -1258,7 +1265,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f83e2ae0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f22145bdb40> >"
] ]
}, },
"execution_count": 12, "execution_count": 12,
@ -1446,7 +1453,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f77f84536f0> >" "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f221462dae0> >"
] ]
}, },
"execution_count": 13, "execution_count": 13,
@ -1495,10 +1502,9 @@
"outputs": [], "outputs": [],
"source": [ "source": [
"def model_check(f, m):\n", "def model_check(f, m):\n",
" f = spot.formula(f)\n", " nf = spot.formula.Not(f)\n",
" ss = m.kripke(spot.atomic_prop_collect(f))\n", " ss = m.kripke(spot.atomic_prop_collect(nf))\n",
" nf = spot.formula_Not(f).translate()\n", " return spot.otf_product(ss, nf.translate()).is_empty() "
" return spot.otf_product(ss, nf).is_empty() "
] ]
}, },
{ {
@ -1535,10 +1541,9 @@
"outputs": [], "outputs": [],
"source": [ "source": [
"def model_debug(f, m):\n", "def model_debug(f, m):\n",
" f = spot.formula(f)\n", " nf = spot.formula.Not(f)\n",
" ss = m.kripke(spot.atomic_prop_collect(f))\n", " ss = m.kripke(spot.atomic_prop_collect(nf))\n",
" nf = spot.formula_Not(f).translate()\n", " return ss.intersecting_run(nf.translate())"
" return ss.intersecting_run(nf)"
] ]
}, },
{ {
@ -1660,7 +1665,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f83ee270> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f221464a870> >"
] ]
}, },
"execution_count": 19, "execution_count": 19,

12
tests/python/ltsmin-pml.ipynb
View file

@ -38,8 +38,8 @@
"SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n", "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n",
"(C) University of Twente, Formal Methods and Tools group\n", "(C) University of Twente, Formal Methods and Tools group\n",
"\n", "\n",
"Parsing tmp_kk6cvzf.pml...\n", "Parsing tmps8i1kbv6.pml...\n",
"Parsing tmp_kk6cvzf.pml done (0.0 sec)\n", "Parsing tmps8i1kbv6.pml done (0.0 sec)\n",
"\n", "\n",
"Optimizing graphs...\n", "Optimizing graphs...\n",
" StateMerging changed 0 states/transitions.\n", " StateMerging changed 0 states/transitions.\n",
@ -225,8 +225,8 @@
" Found 2 / 2 (100.0%) Commuting actions \n", " Found 2 / 2 (100.0%) Commuting actions \n",
"Generating guard dependency matrices done (0.0 sec)\n", "Generating guard dependency matrices done (0.0 sec)\n",
"\n", "\n",
"Written C code to /home/adl/git/spot/tests/python/tmp_kk6cvzf.pml.spins.c\n", "Written C code to /home/adl/git/spot/tests/python/tmps8i1kbv6.pml.spins.c\n",
"Compiled C code to PINS library tmp_kk6cvzf.pml.spins\n", "Compiled C code to PINS library tmps8i1kbv6.pml.spins\n",
"\n" "\n"
] ]
} }
@ -560,7 +560,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fa8d4065b40> >" "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f44743b5ae0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
@ -603,7 +603,7 @@
"<!-- 0 -->\n", "<!-- 0 -->\n",
"<g class=\"node\" id=\"node2\">\n", "<g class=\"node\" id=\"node2\">\n",
"<title>0</title>\n", "<title>0</title>\n",
"<g id=\"a_node2\"><a xlink:title=\"P_0._pc=1, P_0.a=0, P_0.b=0\n", "<g id=\"a_node2\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=0\n",
"&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n", "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
"<ellipse cx=\"55\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n", "<ellipse cx=\"55\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"55\" y=\"-113.3\">0</text>\n", "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"55\" y=\"-113.3\">0</text>\n",

152
tests/python/stutter-inv.ipynb
View file

@ -7,7 +7,7 @@
"outputs": [], "outputs": [],
"source": [ "source": [
"import spot\n", "import spot\n",
"spot.setup(show_default='.ban')\n", "spot.setup(show_default='.bn')\n",
"from IPython.display import display" "from IPython.display import display"
] ]
}, },
@ -302,7 +302,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa2444ce810> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642b47b0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -355,7 +355,7 @@
"def explain_stut(f):\n", "def explain_stut(f):\n",
" f = spot.formula(f)\n", " f = spot.formula(f)\n",
" pos = spot.translate(f)\n", " pos = spot.translate(f)\n",
" neg = spot.translate(spot.formula_Not(f))\n", " neg = spot.translate(spot.formula.Not(f))\n",
" word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word()\n", " word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word()\n",
" if word is None:\n", " if word is None:\n",
" print(f, \"is stutter invariant\")\n", " print(f, \"is stutter invariant\")\n",
@ -428,7 +428,7 @@
"source": [ "source": [
"f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')\n", "f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')\n",
"f2 = spot.formula('F(a & Xa & XXa & G!b)')\n", "f2 = spot.formula('F(a & Xa & XXa & G!b)')\n",
"f = spot.formula_Or([f1, f2])\n", "f = spot.formula.Or([f1, f2])\n",
"\n", "\n",
"print(spot.is_stutter_invariant(f1))\n", "print(spot.is_stutter_invariant(f1))\n",
"print(spot.is_stutter_invariant(f2))\n", "print(spot.is_stutter_invariant(f2))\n",
@ -595,7 +595,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24445d270> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642c22d0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -804,7 +804,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24445d270> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642c22d0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -845,7 +845,7 @@
"source": [ "source": [
"g1 = spot.formula('GF(a & Xa) & GF!a')\n", "g1 = spot.formula('GF(a & Xa) & GF!a')\n",
"g2 = spot.formula('!GF(a & Xa) & GF!a')\n", "g2 = spot.formula('!GF(a & Xa) & GF!a')\n",
"g = spot.formula_Or([g1, g2])" "g = spot.formula.Or([g1, g2])"
] ]
}, },
{ {
@ -963,7 +963,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa2444ce8a0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642b4750> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1062,7 +1062,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446e5d0> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d26c0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1279,7 +1279,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446e660> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d2720> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1408,7 +1408,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244d50270> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1643175a0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1539,7 +1539,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446eb70> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d2ea0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1799,7 +1799,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244480540> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642e62a0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1819,7 +1819,7 @@
"State: 6 [!0] 0\n", "State: 6 [!0] 0\n",
"State: 7 [!0] 6 [0] 5\n", "State: 7 [!0] 6 [0] 5\n",
"--END--\"\"\")\n", "--END--\"\"\")\n",
"spot.highlight_stutter_invariant_states(ex1,None, 5)\n", "spot.highlight_stutter_invariant_states(ex1, None, 5)\n",
"display(ex1)" "display(ex1)"
] ]
}, },
@ -2113,7 +2113,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244480540> >" "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642e62a0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2189,69 +2189,69 @@
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"formula states SIstates fwd_closed\n", "formula states SIstates fwd_closed\n",
"(p1 & X(!p0 U p2)) R !p0 3 2 1\n", "Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2))) 3 2 1\n",
"(!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) 4 3 1\n", "Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U 4 3 1\n",
"!p0 | ((p2 & X(!p1 U p3)) R !p1) 4 2 1\n", "G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 4 2 1\n",
"G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U 4 1 1\n", "G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & 4 1 1\n",
"G(!p0 | (!p1 W (p2 | (!p1 & p3 & X(!p1 U 3 0 1\n", "G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & 3 0 1\n",
"(!p0 U p2) | G(!p0 | XG!p1) 3 2 1\n", "F(p0 & XFp1) -> (!p0 U p2) 3 2 1\n",
"G!p0 | ((p0 | !p1 | X(!p2 W p0)) U (p0 | 4 3 1\n", "Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2)) 4 3 1\n",
"!p0 W (p0 & ((!p1 U p3) | G(!p1 | XG!p2) 4 2 1\n", "G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p 4 2 1\n",
"G(!p0 | G!p1 | ((p1 | !p2 | X(!p3 W p1)) 4 1 1\n", "G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (! 4 1 1\n",
"G(!p0 | ((p1 | !p2 | X(!p3 W p1)) U (p1 3 0 1\n", "G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3 3 0 1\n",
"G(!p0 | X(F(p1 & Fp2) | G!p1)) 6 1 1\n", "G((p0 & XFp1) -> XF(p1 & Fp2)) 6 1 1\n",
"G!p0 | ((!p1 | X((!p0 U (p2 & Fp3)) | (p 6 2 1\n", "Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U ( 6 2 1\n",
"G(!p0 | G(!p1 | X(!p2 W (p2 & Fp3)))) 5 0 1\n", "G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & F 5 0 1\n",
"G(!p0 | G!p1 | ((!p2 | X((!p1 U (p3 & Fp 10 2 1\n", "G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> 10 2 1\n",
"G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | ( 10 0 1\n", "G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U 10 0 1\n",
"G(!p0 | F(p1 & XFp2)) 4 0 1\n", "G(p0 -> F(p1 & XFp2)) 4 0 1\n",
"G!p0 | ((!p1 | ((p2 & X(!p0 U p3)) M !p0 4 1 1\n", "Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 4 1 1\n",
"G(!p0 | G(!p1 | (p2 & XFp3))) 3 3 1\n", "G(p0 -> G(p1 -> (p2 & XFp3))) 3 3 1\n",
"G(!p0 | G!p1 | ((!p2 | ((p3 & X(!p1 U p4 4 0 1\n", "G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 4 0 1\n",
"G(!p0 | ((!p1 | ((p3 & X(!p2 U p4)) M !p 6 2 1\n", "G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 6 2 1\n",
"G(!p0 | F(p1 & !p2 & X(!p2 U p3))) 4 0 1\n", "G(p0 -> F(p1 & !p2 & X(!p2 U p3))) 4 0 1\n",
"G!p0 | ((!p1 | ((p2 & !p3 & X((!p0 & !p3 4 1 1\n", "Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & 4 1 1\n",
"G(!p0 | G(!p1 | (p2 & !p3 & X(!p3 U p4)) 3 3 1\n", "G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4)) 3 3 1\n",
"G(!p0 | G!p1 | ((!p2 | ((p3 & !p4 & X((! 4 0 1\n", "G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 4 0 1\n",
"G(!p0 | ((!p1 | ((p3 & !p4 & X((!p2 & !p 6 2 1\n", "G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & 6 2 1\n",
"p0 U (p1 & X(p2 U p3)) 3 2 1\n", "p0 U (p1 & X(p2 U p3)) 3 2 1\n",
"p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & 7 2 1\n", "p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & 7 2 1\n",
"F(p0 & XGp1) 2 2 1\n", "F(p0 & XGp1) 2 2 1\n",
"F(p0 & X(p1 & XFp2)) 4 2 1\n", "F(p0 & X(p1 & XFp2)) 4 2 1\n",
"F(p0 & X(p1 U p2)) 3 1 1\n", "F(p0 & X(p1 U p2)) 3 1 1\n",
"G(p0 & Fp1 & Fp2 & Fp3) 1 1 1\n", "G(p0 & XF(p1 & XF(p2 & XFp3))) 1 1 1\n",
"GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 4 4 1\n", "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0)) 4 4 1\n",
"GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 9 9 1\n", "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 9 9 1\n",
"G(!p0 | !p1 | p2 | X(!p2 | p3 | X(!p1 | 3 0 1\n", "G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 3 0 1\n",
"G(!p0 | !p1 | p2 | X(!p2 | (p2 U (!p2 U 5 5 1\n", "G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 5 5 1\n",
"1 1 1 1\n", "G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U 1 1 1\n",
"G(p0 | !p1 | Xp2) 2 0 1\n", "G((!p0 & p1) -> Xp2) 2 0 1\n",
"G(!p0 | X(p0 | p1)) 2 2 1\n", "G(p0 -> X(p0 | p1)) 2 2 1\n",
"G((((p1 & Xp1) | (!p1 & X!p1)) & ((p0 & 34 34 1\n", "G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 34 34 1\n",
"G(!p0 | p1 | !p2 | X(!p0 | !p1 | p3)) 2 2 1\n", "G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3)) 2 2 1\n",
"G(!p0 | X(!p0 U p1)) 2 0 1\n", "G(p0 -> X(!p0 U p1)) 2 0 1\n",
"G(p0 | X(!p0 | (p0 W p1))) 3 3 1\n", "G((!p0 & Xp0) -> X((p0 U p1) | Gp0)) 3 3 1\n",
"G(p0 | X(!p0 | ((!p1 & X(p0 & p1)) M p0) 4 4 1\n", "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 4 4 1\n",
"G(p0 | X(!p0 | ((!p1 & X(p1 & ((!p1 & X( 6 6 1\n", "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 6 6 1\n",
"G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X( 6 6 1\n", "G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X( 6 6 1\n",
"G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X( 8 8 1\n", "G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X( 8 8 1\n",
"G(p0 | X(!p0 | ((p0 | X!p0) U (!p1 & Xp1 6 6 1\n", "G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & 6 6 1\n",
"G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | 12 0 1\n", "G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | 12 0 1\n",
"G((!p0 & Xp0) | (p1 & Xp1) | (!p1 & X!p1 4 4 1\n", "G((Xp0 -> p0) -> (p1 <-> Xp1)) 4 4 1\n",
"G((!p0 & Xp0) | ((!p1 | Xp1) & (p1 | X!p 4 4 1\n", "G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> 4 4 1\n",
"p0 & XG!p0 2 1 1\n", "p0 & XG!p0 2 1 1\n",
"XG(!p0 | p2 | G!p1 | X(p2 M !p1)) 4 1 1\n", "XG(p0 -> (G!p1 | (!Xp1 U p2))) 4 1 1\n",
"XG(!p0 | p1 | (!p1 W p2)) 3 2 1\n", "XG((p0 & !p1) -> (G!p1 | (!p1 U p2))) 3 2 1\n",
"XG(!p0 | !p1 | (p1 W p2)) 3 2 1\n", "XG((p0 & p1) -> (Gp1 | (p1 U p2))) 3 2 1\n",
"Xp0 & G(p0 | X(!p0 | Xp0)) 5 0 1\n", "Xp0 & G((!p0 & Xp0) -> XXp0) 5 0 1\n",
"1 1 1 1\n", "(Xp0 U Xp1) | !X(p0 U p1) 1 1 1\n",
"1 1 1 1\n", "(Xp0 U p1) | !X(p0 U (p0 & p1)) 1 1 1\n",
"G(!p0 | Fp1) 2 2 1\n", "((Xp0 U p1) | !X(p0 U (p0 & p1))) & G(p0 2 2 1\n",
"G(!p0 | Fp1) 2 2 1\n", "((Xp0 U Xp1) | !X(p0 U p1)) & G(p0 -> Fp 2 2 1\n",
"F(p0 & X(!p1 U !p2)) 3 1 1\n", "!G(p0 -> X(p1 R p2)) 3 1 1\n",
"(p0 & Xp1) R X(p2 R p0) 5 3 1\n", "(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R 5 3 1\n",
"G((p0 | XGp1) & (p2 | XG!p1)) 3 2 1\n", "G(p0 | XGp1) & G(p2 | XG!p1) 3 2 1\n",
"Gp0 1 1 1\n" "G(p0 | (Xp1 & X!p1)) 1 1 1\n"
] ]
} }
], ],
@ -2272,6 +2272,7 @@
"fmt = \"{:40.40} {:>6} {:>8} {:>10}\"\n", "fmt = \"{:40.40} {:>6} {:>8} {:>10}\"\n",
"print(fmt.format(\"formula\", \"states\", \"SIstates\", \"fwd_closed\"))\n", "print(fmt.format(\"formula\", \"states\", \"SIstates\", \"fwd_closed\"))\n",
"for f in formulas:\n", "for f in formulas:\n",
" s = f.to_str()\n",
" aut = spot.translate(f)\n", " aut = spot.translate(f)\n",
" aut_size.append(aut.num_states())\n", " aut_size.append(aut.num_states())\n",
" sistates = spot.stutter_invariant_states(aut, f)\n", " sistates = spot.stutter_invariant_states(aut, f)\n",
@ -2279,7 +2280,7 @@
" sistates_size.append(sisz)\n", " sistates_size.append(sisz)\n",
" fc = spot.is_stutter_invariant_forward_closed(aut, sistates) == -1\n", " fc = spot.is_stutter_invariant_forward_closed(aut, sistates) == -1\n",
" fwd_closed.append(fc)\n", " fwd_closed.append(fc)\n",
" print(fmt.format(f.to_str(), aut.num_states(), sisz, fc))" " print(fmt.format(s, aut.num_states(), sisz, fc))"
] ]
}, },
{ {
@ -2335,6 +2336,13 @@
"source": [ "source": [
"100*sum(sistates_size)/sum(aut_size)" "100*sum(sistates_size)/sum(aut_size)"
] ]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
} }
], ],
"metadata": { "metadata": {