Commit 1fd0aa14 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

multiple adjustments for Debian stable

* tests/python/ipnbdoctest.py: Adjust to Python <3.6.
* tests/python/_autparserr.ipynb: Adjust to older IPython version.
* tests/python/stutter-inv.ipynb: Avoid pandas because its output
varies from version to version.
parent 527c8025
%% Cell type:code id: tags:
``` python
from IPython.display import display
import spot
spot.setup()
```
%% Cell type:markdown id: tags:
Test syntax errors
------------------
%% Cell type:code id: tags:
``` python
%%file _example.aut
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 1
State: 1
[t] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[a] 3
State: 1
[1] 0
[0&!1] 1
--END--
```
%%%% Output: stream
Overwriting _example.aut
Writing _example.aut
%% Cell type:code id: tags:
``` python
for a in spot.automata('_example.aut'):
display(a)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="133pt" height="101pt"viewBox="0.00 0.00 133.00 101.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 97)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-97 129,-97 129,4 -4,4"/><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="107" cy="-42" rx="18" ry="18"/><text text-anchor="middle" x="107" y="-38.3" font-family="Lato" font-size="14.00">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="black" d="M23.0602,-62.9848C24.6706,-62.5773 58.2688,-54.0766 82.2014,-48.0213"/><polygon fill="black" stroke="black" points="89.2724,-46.2323 83.2589,-51.0031 85.8793,-47.0908 82.4862,-47.9493 82.4862,-47.9493 82.4862,-47.9493 85.8793,-47.0908 81.7135,-44.8956 89.2724,-46.2323 89.2724,-46.2323"/></g><!-- 1&#45;&gt;1 --><g id="edge3" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="black" d="M99.9688,-58.6641C98.4062,-68.625 100.75,-78 107,-78 111.688,-78 114.178,-72.7266 114.471,-65.8876"/><polygon fill="black" stroke="black" points="114.031,-58.6641 117.601,-65.4598 114.244,-62.1576 114.456,-65.6511 114.456,-65.6511 114.456,-65.6511 114.244,-62.1576 111.312,-65.8425 114.031,-58.6641 114.031,-58.6641"/><text text-anchor="middle" x="107" y="-81.8" font-family="Lato" font-size="14.00">1</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="22" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="black" cx="22" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="22" y="-18.3" font-family="Lato" font-size="14.00">0</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M43.5169,-26.9438C55.3149,-29.7867 70.1833,-33.3695 82.4561,-36.3268"/><polygon fill="black" stroke="black" points="89.3394,-37.9854 81.7962,-39.4079 85.9368,-37.1655 82.5342,-36.3455 82.5342,-36.3455 82.5342,-36.3455 85.9368,-37.1655 83.2721,-33.2832 89.3394,-37.9854 89.3394,-37.9854"/><text text-anchor="middle" x="66.5" y="-37.8" font-family="Lato" font-size="14.00">1</text></g></g></svg>)
%%%% Output: error
File "<string>", line unknown
SyntaxError:
_example.aut:20.2: syntax error, unexpected identifier
_example.aut:20.1-3: ignoring this invalid label
_example.aut:20.5: state number is larger than state count...
_example.aut:14.1-9: ... declared here.
%% Cell type:code id: tags:
``` python
spot.automaton('_example.aut', timeout=100)
```
%%%% Output: execute_result
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="133pt" height="101pt"viewBox="0.00 0.00 133.00 101.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 97)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-97 129,-97 129,4 -4,4"/><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="107" cy="-42" rx="18" ry="18"/><text text-anchor="middle" x="107" y="-38.3" font-family="Lato" font-size="14.00">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="black" d="M23.0602,-62.9848C24.6706,-62.5773 58.2688,-54.0766 82.2014,-48.0213"/><polygon fill="black" stroke="black" points="89.2724,-46.2323 83.2589,-51.0031 85.8793,-47.0908 82.4862,-47.9493 82.4862,-47.9493 82.4862,-47.9493 85.8793,-47.0908 81.7135,-44.8956 89.2724,-46.2323 89.2724,-46.2323"/></g><!-- 1&#45;&gt;1 --><g id="edge3" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="black" d="M99.9688,-58.6641C98.4062,-68.625 100.75,-78 107,-78 111.688,-78 114.178,-72.7266 114.471,-65.8876"/><polygon fill="black" stroke="black" points="114.031,-58.6641 117.601,-65.4598 114.244,-62.1576 114.456,-65.6511 114.456,-65.6511 114.456,-65.6511 114.244,-62.1576 111.312,-65.8425 114.031,-58.6641 114.031,-58.6641"/><text text-anchor="middle" x="107" y="-81.8" font-family="Lato" font-size="14.00">1</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="22" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="black" cx="22" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="22" y="-18.3" font-family="Lato" font-size="14.00">0</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M43.5169,-26.9438C55.3149,-29.7867 70.1833,-33.3695 82.4561,-36.3268"/><polygon fill="black" stroke="black" points="89.3394,-37.9854 81.7962,-39.4079 85.9368,-37.1655 82.5342,-36.3455 82.5342,-36.3455 82.5342,-36.3455 85.9368,-37.1655 83.2721,-33.2832 89.3394,-37.9854 89.3394,-37.9854"/><text text-anchor="middle" x="66.5" y="-37.8" font-family="Lato" font-size="14.00">1</text></g></g></svg>)
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbec846c5a0> >
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f72fc2ce090> >
%% Cell type:markdown id: tags:
# Error reading from pipe
%% Cell type:code id: tags:
``` python
spot.automaton('non-existing-cmd |')
```
%%%% Output: error
---------------------------------------------------------------------------
CalledProcessError Traceback (most recent call last)
<ipython-input-5-6b4750207d55> in <module>()
----> 1 spot.automaton('non-existing-cmd |')
/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
479 See `spot.automata` for a list of supported formats."""
480 try:
--> 481 return next(automata(filename, **kwargs))
482 except StopIteration:
483 raise RuntimeError("Failed to read automaton from {}".format(filename))
/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
464 del proc
465 if ret:
--> 466 raise subprocess.CalledProcessError(ret, filename[:-1])
467 # deleting o explicitely now prevents Python 3.5 from
468 # reporting the following error: "<built-in function
CalledProcessError: Command 'non-existing-cmd ' returned non-zero exit status 127.
%% Cell type:code id: tags:
``` python
spot.automaton('sleep 3; cat _example.aut |', timeout=1)
```
%%%% Output: error
---------------------------------------------------------------------------
TimeoutExpired Traceback (most recent call last)
<ipython-input-6-e4289051db4c> in <module>()
----> 1 spot.automaton('sleep 3; cat _example.aut |', timeout=1)
/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
479 See `spot.automata` for a list of supported formats."""
480 try:
--> 481 return next(automata(filename, **kwargs))
482 except StopIteration:
483 raise RuntimeError("Failed to read automaton from {}".format(filename))
/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
423 else:
424 try:
--> 425 out, err = proc.communicate(timeout=timeout)
426 except subprocess.TimeoutExpired:
427 # Using subprocess.check_output() with timeout
/usr/lib/python3.6/subprocess.py in communicate(self, input, timeout)
841
842 try:
--> 843 stdout, stderr = self._communicate(input, endtime, timeout)
844 finally:
845 self._communication_started = True
/usr/lib/python3.6/subprocess.py in _communicate(self, input, endtime, orig_timeout)
1513
1514 ready = selector.select(timeout)
-> 1515 self._check_timeout(endtime, orig_timeout)
1516
1517 # XXX Rewrite these to use non-blocking I/O on the file
/usr/lib/python3.6/subprocess.py in _check_timeout(self, endtime, orig_timeout)
869 return
870 if _time() > endtime:
--> 871 raise TimeoutExpired(self.args, orig_timeout)
872
873
TimeoutExpired: Command 'sleep 3; cat _example.aut ' timed out after 1 seconds
%% Cell type:code id: tags:
``` python
for a in spot.automata("ltl2tgba 'a U b'|", 'ltl2tgba "syntax U U error"|'):
display(a)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="171pt" height="85pt"viewBox="0.00 0.00 171.00 85.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 81)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-81 167,-81 167,4 -4,4"/><!-- I --><!-- 1 --><g id="node2" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-22" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-18.3" font-family="Lato" font-size="14.00">1</text></g><!-- I&#45;&gt;1 --><g id="edge1" class="edge"><title>I&#45;&gt;1</title><path fill="none" stroke="black" d="M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22"/><polygon fill="black" stroke="black" points="37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22"/></g><!-- 1&#45;&gt;1 --><g id="edge4" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="black" d="M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433"/><polygon fill="black" stroke="black" points="62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373"/><text text-anchor="start" x="37.5" y="-61.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 0 --><g id="node3" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="141" cy="-22" rx="18" ry="18"/><ellipse fill="none" stroke="black" cx="141" cy="-22" rx="22" ry="22"/><text text-anchor="middle" x="141" y="-18.3" font-family="Lato" font-size="14.00">0</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="black" d="M74.1977,-22C85.0734,-22 99.3874,-22 111.887,-22"/><polygon fill="black" stroke="black" points="118.997,-22 111.997,-25.1501 115.497,-22 111.997,-22.0001 111.997,-22.0001 111.997,-22.0001 115.497,-22 111.997,-18.8501 118.997,-22 118.997,-22"/><text text-anchor="start" x="92" y="-25.8" font-family="Lato" font-size="14.00">b</text></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M132.994,-42.5808C131.886,-52.8447 134.555,-62 141,-62 145.834,-62 148.544,-56.8502 149.129,-49.9451"/><polygon fill="black" stroke="black" points="149.006,-42.5808 152.273,-49.5273 149.065,-46.0803 149.123,-49.5798 149.123,-49.5798 149.123,-49.5798 149.065,-46.0803 145.973,-49.6324 149.006,-42.5808 149.006,-42.5808"/><text text-anchor="middle" x="141" y="-65.8" font-family="Lato" font-size="14.00">1</text></g></g></svg>)
%%%% Output: error
---------------------------------------------------------------------------
CalledProcessError Traceback (most recent call last)
<ipython-input-7-cf613d56390d> in <module>()
----> 1 for a in spot.automata("ltl2tgba 'a U b'|", 'ltl2tgba "syntax U U error"|'):
2 display(a)
/home/adl/git/spot/python/spot/__init__.py in automata(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)
464 del proc
465 if ret:
--> 466 raise subprocess.CalledProcessError(ret, filename[:-1])
467 # deleting o explicitely now prevents Python 3.5 from
468 # reporting the following error: "<built-in function
CalledProcessError: Command 'ltl2tgba "syntax U U error"' returned non-zero exit status 2.
%% Cell type:markdown id: tags:
Reading an empty file with `spot.automaton()` is an error.
%% Cell type:code id: tags:
``` python
spot.automaton('true|')
```
%%%% Output: error
---------------------------------------------------------------------------
StopIteration Traceback (most recent call last)
/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
480 try:
--> 481 return next(automata(filename, **kwargs))
482 except StopIteration:
StopIteration:
During handling of the above exception, another exception occurred:
RuntimeError Traceback (most recent call last)
<ipython-input-8-139f3bb684aa> in <module>()
----> 1 spot.automaton('true|')
/home/adl/git/spot/python/spot/__init__.py in automaton(filename, **kwargs)
481 return next(automata(filename, **kwargs))
482 except StopIteration:
--> 483 raise RuntimeError("Failed to read automaton from {}".format(filename))
484
485
RuntimeError: Failed to read automaton from true|
%% Cell type:code id: tags:
``` python
!rm _example.aut
```
......
......@@ -115,12 +115,9 @@ def canonicalize(s, type, ignores):
s = re.sub(r' fill="black"', '', s)
s = re.sub(r' stroke="transparent"', ' stroke="none"', s)
s = re.sub(r'><title>', '>\n<title>', s)
# Different Pandas versions produce different CSS styles.
s = re.sub(r'<style[ a-z]*>.*</style>',
'<style>...</style>', s, flags=re.DOTALL)
# CalledProcessError message has a final dot in Python 3.6
s = re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', s)
# Different Pandas versions produce different CSS styles (when there is a
# style).
s = re.sub(r'<style[ a-z]*>.*</style>\n', '', s, flags=re.DOTALL)
for n, p in enumerate(ignores):
s = re.sub(p, 'IGN{}'.format(n), s)
......@@ -145,6 +142,12 @@ def canonical_dict(dict, ignores):
# sys.exit(77) is used to Skip the test.
sys.exit(77)
if 'ename' in dict and dict['ename'] == 'CalledProcessError':
# CalledProcessError message has a final dot in Python 3.6
dict['evalue'] = \
re.sub(r"(' returned non-zero exit status \d+)\.", r'\1',
dict['evalue'])
if 'transient' in dict:
del dict['transient']
if 'execution_count' in dict:
......
%% Cell type:code id: tags:
``` python
import spot
spot.setup(show_default='.ban')
from IPython.display import display
```
%% Cell type:markdown id: tags:
# Stutter-invariant languages
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.
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 id: tags:
## Stutter-invariant formulas
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 id: tags:
``` python
f = spot.formula('a U b')
print(f.is_syntactic_stutter_invariant())
```
%%%% Output: stream
True
%% Cell type:code id: tags:
``` python
f = spot.formula('a U Xb')
print(f.is_syntactic_stutter_invariant())
```
%%%% Output: stream
False
%% Cell type:markdown id: tags:
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 id: tags:
``` python
g = spot.formula('F(a & X(!a & Gb))')
print(g.is_syntactic_stutter_invariant())
print(spot.is_stutter_invariant(g))
```
%%%% Output: stream
False
True
%% Cell type:markdown id: tags:
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 id: tags:
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 id: tags:
``` python
spot.remove_x(g)
```
%%%% Output: execute_result
$\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))))$
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))))
%% Cell type:markdown id: tags:
## Stutter-invariant automata
%% Cell type:markdown id: tags:
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 id: tags:
``` python
aut = spot.translate(g)
print(aut.prop_stutter_invariant())
```
%%%% Output: stream
maybe
%% Cell type:markdown id: tags:
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 id: tags:
``` python
print(spot.is_stutter_invariant(g, aut))
```
%%%% Output: stream
True
%% Cell type:markdown id: tags:
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 id: tags:
``` python
print(aut.prop_stutter_invariant())
```
%%%% Output: stream
yes
%% Cell type:markdown id: tags:
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.
In doubt, you can always reset the property as follows:
%% Cell type:code id: tags:
``` python
aut.prop_stutter_invariant(spot.trival_maybe())
print(aut.prop_stutter_invariant())
```
%%%% Output: stream
maybe
%% Cell type:markdown id: tags:
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 id: tags:
``` python
a1 = spot.automaton('''HOA: v1
AP: 1 "a"
States: 2
Start: 0
Acceptance: 0 t
--BODY--
State: 0 [0] 1
State: 1 [t] 0
--END--''')
display(a1)
print(spot.is_stutter_invariant(a1))
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="163pt" height="84pt"viewBox="0.00 0.00 163.00 84.35" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 80.3516)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-80.3516 159,-80.3516 159,4 -4,4"/><text text-anchor="start" x="74.5" y="-61.1516" font-family="Lato" font-size="14.00">t</text><text text-anchor="start" x="66.5" y="-46.1516" font-family="Lato" font-size="14.00">[all]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-20.3516" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-16.6516" font-family="Lato" font-size="14.00">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="black" d="M1.15491,-20.3516C2.79388,-20.3516 17.1543,-20.3516 30.6317,-20.3516"/><polygon fill="black" stroke="black" points="37.9419,-20.3516 30.9419,-23.5017 34.4419,-20.3516 30.9419,-20.3517 30.9419,-20.3517 30.9419,-20.3517 34.4419,-20.3516 30.9418,-17.2017 37.9419,-20.3516 37.9419,-20.3516"/></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="137" cy="-20.3516" rx="18" ry="18"/><text text-anchor="middle" x="137" y="-16.6516" font-family="Lato" font-size="14.00">1</text></g><!-- 0&#45;&gt;1 --><g id="edge2" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M74.1418,-20.3516C85.1153,-20.3516 99.5214,-20.3516 111.67,-20.3516"/><polygon fill="black" stroke="black" points="118.892,-20.3516 111.892,-23.5017 115.392,-20.3516 111.892,-20.3517 111.892,-20.3517 111.892,-20.3517 115.392,-20.3516 111.892,-17.2017 118.892,-20.3516 118.892,-20.3516"/><text text-anchor="start" x="93" y="-24.1516" font-family="Lato" font-size="14.00">a</text></g><!-- 1&#45;&gt;0 --><g id="edge3" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="black" d="M122.524,-9.39411C114.011,-3.78441 102.645,1.35158 92,-1.35158 87.1374,-2.58634 82.2193,-4.64763 77.668,-6.96768"/><polygon fill="black" stroke="black" points="71.3113,-10.4859 75.9105,-4.34007 74.3736,-8.79098 77.4359,-7.09611 77.4359,-7.09611 77.4359,-7.09611 74.3736,-8.79098 78.9613,-9.85216 71.3113,-10.4859 71.3113,-10.4859"/><text text-anchor="middle" x="96.5" y="-5.15158" font-family="Lato" font-size="14.00">1</text></g></g></svg>)
%%%% Output: stream
False
%% Cell type:markdown id: tags:
## Explaining why a formula is not sutter-invariant
%% Cell type:markdown id: tags:
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.
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 id: tags:
``` python
def explain_stut(f):
f = spot.formula(f)
pos = spot.translate(f)
neg = spot.translate(spot.formula_Not(f))
word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word()
if word is None:
print(f, "is stutter invariant")
return
word.simplify()
waut = word.as_automaton()
if waut.intersects(pos):
acc, rej, aut = "accepted", "rejected", neg
else:
acc, rej, aut = "rejected", "accepted", pos
word2 = spot.sl2(waut).intersecting_word(aut)
word2.simplify()
print("""{} is {} by {}
but if we stutter some of its letters, we get
{} which is {} by {}""".format(word, acc, f, word2, rej, f))
```
%% Cell type:code id: tags:
``` python
explain_stut('GF(a & Xb)')
```
%%%% Output: stream
cycle{!a & !b; a & b} is rejected by GF(a & Xb)
but if we stutter some of its letters, we get
cycle{!a & !b; a & b; a & b} which is accepted by GF(a & Xb)
%% Cell type:markdown id: tags:
## Detecting stutter-invariant states
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 id: tags:
### First example
For instance let us build a disjunction of a stutter-invariant formula and a stutter-sensitive one:
%% Cell type:code id: tags:
``` python
f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')
f2 = spot.formula('F(a & Xa & XXa & G!b)')
f = spot.formula_Or([f1, f2])
print(spot.is_stutter_invariant(f1))
print(spot.is_stutter_invariant(f2))
print(spot.is_stutter_invariant(f))
```
%%%% Output: stream
True
False
False
%% Cell type:code id: tags:
``` python
pos = spot.translate(f)
display(pos)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="518pt" height="230pt"viewBox="0.00 0.00 518.00 230.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 226)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-226 514,-226 514,4 -4,4"/><text text-anchor="start" x="234" y="-207.8" font-family="Lato" font-size="14.00">Inf(</text><text text-anchor="start" x="256" y="-207.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="272" y="-207.8" font-family="Lato" font-size="14.00">)</text><text text-anchor="start" x="232" y="-193.8" font-family="Lato" font-size="14.00">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-78" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-74.3" font-family="Lato" font-size="14.00">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="black" d="M1.15491,-78C2.79388,-78 17.1543,-78 30.6317,-78"/><polygon fill="black" stroke="black" points="37.9419,-78 30.9419,-81.1501 34.4419,-78 30.9419,-78.0001 30.9419,-78.0001 30.9419,-78.0001 34.4419,-78 30.9418,-74.8501 37.9419,-78 37.9419,-78"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M49.6208,-95.0373C48.3189,-104.858 50.4453,-114 56,-114 60.166,-114 62.4036,-108.858 62.7128,-102.143"/><polygon fill="black" stroke="black" points="62.3792,-95.0373 65.8541,-101.882 62.5434,-98.5335 62.7076,-102.03 62.7076,-102.03 62.7076,-102.03 62.5434,-98.5335 59.561,-102.177 62.3792,-95.0373 62.3792,-95.0373"/><text text-anchor="start" x="51.5" y="-117.8" font-family="Lato" font-size="14.00">1</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="165" cy="-103" rx="18" ry="18"/><text text-anchor="start" x="160.5" y="-99.3" font-family="Lato" font-size="14.00">1</text></g><!-- 0&#45;&gt;1 --><g id="edge3" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M73.7188,-81.9062C91.6218,-86.0892 120.176,-92.7606 140.371,-97.4793"/><polygon fill="black" stroke="black" points="147.399,-99.1212 139.866,-100.596 143.99,-98.3248 140.582,-97.5285 140.582,-97.5285 140.582,-97.5285 143.99,-98.3248 141.299,-94.4611 147.399,-99.1212 147.399,-99.1212"/><text text-anchor="start" x="107" y="-98.8" font-family="Lato" font-size="14.00">a</text></g><!-- 2 --><g id="node4" class="node"><title>2</title><ellipse fill="#ffffaa" stroke="black" cx="165" cy="-49" rx="18" ry="18"/><text text-anchor="middle" x="165" y="-45.3" font-family="Lato" font-size="14.00">2</text></g><!-- 0&#45;&gt;2 --><g id="edge4" class="edge"><title>0&#45;&gt;2</title><path fill="none" stroke="black" d="M73.7153,-73.1495C79.4994,-71.4909 86.0282,-69.6409 92,-68 108.136,-63.5664 126.361,-58.7589 140.438,-55.0891"/><polygon fill="black" stroke="black" points="147.388,-53.2817 141.406,-58.0921 144.001,-54.1626 140.613,-55.0435 140.613,-55.0435 140.613,-55.0435 144.001,-54.1626 139.82,-51.9949 147.388,-53.2817 147.388,-53.2817"/><text text-anchor="start" x="92" y="-71.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 3 --><g id="node5" class="node"><title>3</title><ellipse fill="#ffffaa" stroke="black" cx="274" cy="-105" rx="18" ry="18"/><text text-anchor="middle" x="274" y="-101.3" font-family="Lato" font-size="14.00">3</text></g><!-- 1&#45;&gt;3 --><g id="edge5" class="edge"><title>1&#45;&gt;3</title><path fill="none" stroke="black" d="M183.191,-103.321C200.897,-103.652 228.648,-104.171 248.616,-104.544"/><polygon fill="black" stroke="black" points="255.851,-104.679 248.794,-107.698 252.352,-104.614 248.852,-104.549 248.852,-104.549 248.852,-104.549 252.352,-104.614 248.911,-101.399 255.851,-104.679 255.851,-104.679"/><text text-anchor="start" x="214" y="-108.8" font-family="Lato" font-size="14.00">!a</text></g><!-- 5 --><g id="node6" class="node"><title>5</title><ellipse fill="#ffffaa" stroke="black" cx="274" cy="-48" rx="18" ry="18"/><text text-anchor="middle" x="274" y="-44.3" font-family="Lato" font-size="14.00">5</text></g><!-- 2&#45;&gt;5 --><g id="edge6" class="edge"><title>2&#45;&gt;5</title><path fill="none" stroke="black" d="M183.191,-48.8393C200.897,-48.6739 228.648,-48.4145 248.616,-48.2279"/><polygon fill="black" stroke="black" points="255.851,-48.1603 248.881,-51.3756 252.351,-48.193 248.852,-48.2258 248.852,-48.2258 248.852,-48.2258 252.351,-48.193 248.822,-45.0759 255.851,-48.1603 255.851,-48.1603"/><text text-anchor="start" x="201" y="-52.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 3&#45;&gt;3 --><g id="edge7" class="edge"><title>3&#45;&gt;3</title><path fill="none" stroke="black" d="M264.767,-120.541C262.169,-130.909 265.246,-141 274,-141 280.702,-141 284.077,-135.085 284.124,-127.659"/><polygon fill="black" stroke="black" points="283.233,-120.541 287.229,-127.095 283.668,-124.014 284.103,-127.487 284.103,-127.487 284.103,-127.487 283.668,-124.014 280.977,-127.879 283.233,-120.541 283.233,-120.541"/><text text-anchor="start" x="269.5" y="-144.8" font-family="Lato" font-size="14.00">1</text></g><!-- 4 --><g id="node7" class="node"><title>4</title><ellipse fill="#ffffaa" stroke="black" cx="383" cy="-120" rx="18" ry="18"/><text text-anchor="middle" x="383" y="-116.3" font-family="Lato" font-size="14.00">4</text></g><!-- 3&#45;&gt;4 --><g id="edge8" class="edge"><title>3&#45;&gt;4</title><path fill="none" stroke="black" d="M292.191,-107.41C309.975,-109.903 337.892,-113.817 357.88,-116.619"/><polygon fill="black" stroke="black" points="364.851,-117.596 357.482,-119.744 361.385,-117.11 357.919,-116.624 357.919,-116.624 357.919,-116.624 361.385,-117.11 358.356,-113.505 364.851,-117.596 364.851,-117.596"/><text text-anchor="start" x="311.5" y="-118.8" font-family="Lato" font-size="14.00">a &amp; b</text></g><!-- 6 --><g id="node9" class="node"><title>6</title><ellipse fill="#ffffaa" stroke="black" cx="383" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="383" y="-14.3" font-family="Lato" font-size="14.00">6</text></g><!-- 5&#45;&gt;6 --><g id="edge10" class="edge"><title>5&#45;&gt;6</title><path fill="none" stroke="black" d="M291.719,-43.3125C309.7,-38.2709 338.426,-30.2169 358.637,-24.5505"/><polygon fill="black" stroke="black" points="365.399,-22.6546 359.509,-27.5774 362.029,-23.5995 358.659,-24.5444 358.659,-24.5444 358.659,-24.5444 362.029,-23.5995 357.808,-21.5114 365.399,-22.6546 365.399,-22.6546"/><text text-anchor="start" x="310" y="-41.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 7 --><g id="node8" class="node"><title>7</title><ellipse fill="#ffffaa" stroke="black" cx="492" cy="-120" rx="18" ry="18"/><text text-anchor="middle" x="492" y="-116.3" font-family="Lato" font-size="14.00">7</text></g><!-- 4&#45;&gt;7 --><g id="edge9" class="edge"><title>4&#45;&gt;7</title><path fill="none" stroke="black" d="M401.191,-120C418.897,-120 446.648,-120 466.616,-120"/><polygon fill="black" stroke="black" points="473.851,-120 466.851,-123.15 470.351,-120 466.851,-120 466.851,-120 466.851,-120 470.351,-120 466.851,-116.85 473.851,-120 473.851,-120"/><text text-anchor="start" x="419" y="-123.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 7&#45;&gt;7 --><g id="edge12" class="edge"><title>7&#45;&gt;7</title><path fill="none" stroke="black" d="M482.767,-135.541C480.169,-145.909 483.246,-156 492,-156 498.702,-156 502.077,-150.085 502.124,-142.659"/><polygon fill="black" stroke="black" points="501.233,-135.541 505.229,-142.095 501.668,-139.014 502.103,-142.487 502.103,-142.487 502.103,-142.487 501.668,-139.014 498.977,-142.879 501.233,-135.541 501.233,-135.541"/><text text-anchor="start" x="488.5" y="-174.8" font-family="Lato" font-size="14.00">a</text><text text-anchor="start" x="484" y="-159.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g><!-- 6&#45;&gt;6 --><g id="edge11" class="edge"><title>6&#45;&gt;6</title><path fill="none" stroke="black" d="M373.767,-33.5414C371.169,-43.9087 374.246,-54 383,-54 389.702,-54 393.077,-48.0847 393.124,-40.6591"/><polygon fill="black" stroke="black" points="392.233,-33.5414 396.229,-40.0955 392.668,-37.0143 393.103,-40.4871 393.103,-40.4871 393.103,-40.4871 392.668,-37.0143 389.977,-40.8788 392.233,-33.5414 392.233,-33.5414"/><text text-anchor="start" x="376.5" y="-72.8" font-family="Lato" font-size="14.00">!b</text><text text-anchor="start" x="375" y="-57.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%% Cell type:markdown id: tags:
While the automaton as a whole is stutter-sensitive, we can see that eventually we will enter a sub-automaton that is stutter-invariant.
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 can only be reached via 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.
%% Cell type:code id: tags:
``` python
spot.stutter_invariant_states(pos, f)
```
%%%% Output: execute_result
(False, True, False, True, True, True, True, True)
%% Cell type:markdown id: tags:
For convenience, the `highligh_...()` version colors the stutter-invariant states of the automaton for display.
(That 5 is the color number for red in Spot's hard-coded palette.)
%% Cell type:code id: tags:
``` python
spot.highlight_stutter_invariant_states(pos, f, 5)
display(pos)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="518pt" height="230pt"viewBox="0.00 0.00 518.00 230.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 226)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-226 514,-226 514,4 -4,4"/><text text-anchor="start" x="234" y="-207.8" font-family="Lato" font-size="14.00">Inf(</text><text text-anchor="start" x="256" y="-207.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="272" y="-207.8" font-family="Lato" font-size="14.00">)</text><text text-anchor="start" x="232" y="-193.8" font-family="Lato" font-size="14.00">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-78" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-74.3" font-family="Lato" font-size="14.00">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="black" d="M1.15491,-78C2.79388,-78 17.1543,-78 30.6317,-78"/><polygon fill="black" stroke="black" points="37.9419,-78 30.9419,-81.1501 34.4419,-78 30.9419,-78.0001 30.9419,-78.0001 30.9419,-78.0001 34.4419,-78 30.9418,-74.8501 37.9419,-78 37.9419,-78"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M49.6208,-95.0373C48.3189,-104.858 50.4453,-114 56,-114 60.166,-114 62.4036,-108.858 62.7128,-102.143"/><polygon fill="black" stroke="black" points="62.3792,-95.0373 65.8541,-101.882 62.5434,-98.5335 62.7076,-102.03 62.7076,-102.03 62.7076,-102.03 62.5434,-98.5335 59.561,-102.177 62.3792,-95.0373 62.3792,-95.0373"/><text text-anchor="start" x="51.5" y="-117.8" font-family="Lato" font-size="14.00">1</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="165" cy="-103" rx="18" ry="18"/><text text-anchor="start" x="160.5" y="-99.3" font-family="Lato" font-size="14.00">1</text></g><!-- 0&#45;&gt;1 --><g id="edge3" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M73.7188,-81.9062C91.6218,-86.0892 120.176,-92.7606 140.371,-97.4793"/><polygon fill="black" stroke="black" points="147.399,-99.1212 139.866,-100.596 143.99,-98.3248 140.582,-97.5285 140.582,-97.5285 140.582,-97.5285 143.99,-98.3248 141.299,-94.4611 147.399,-99.1212 147.399,-99.1212"/><text text-anchor="start" x="107" y="-98.8" font-family="Lato" font-size="14.00">a</text></g><!-- 2 --><g id="node4" class="node"><title>2</title><ellipse fill="#ffffaa" stroke="black" cx="165" cy="-49" rx="18" ry="18"/><text text-anchor="middle" x="165" y="-45.3" font-family="Lato" font-size="14.00">2</text></g><!-- 0&#45;&gt;2 --><g id="edge4" class="edge"><title>0&#45;&gt;2</title><path fill="none" stroke="black" d="M73.7153,-73.1495C79.4994,-71.4909 86.0282,-69.6409 92,-68 108.136,-63.5664 126.361,-58.7589 140.438,-55.0891"/><polygon fill="black" stroke="black" points="147.388,-53.2817 141.406,-58.0921 144.001,-54.1626 140.613,-55.0435 140.613,-55.0435 140.613,-55.0435 144.001,-54.1626 139.82,-51.9949 147.388,-53.2817 147.388,-53.2817"/><text text-anchor="start" x="92" y="-71.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 3 --><g id="node5" class="node"><title>3</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="274" cy="-105" rx="18" ry="18"/><text text-anchor="middle" x="274" y="-101.3" font-family="Lato" font-size="14.00">3</text></g><!-- 1&#45;&gt;3 --><g id="edge5" class="edge"><title>1&#45;&gt;3</title><path fill="none" stroke="black" d="M183.191,-103.321C200.897,-103.652 228.648,-104.171 248.616,-104.544"/><polygon fill="black" stroke="black" points="255.851,-104.679 248.794,-107.698 252.352,-104.614 248.852,-104.549 248.852,-104.549 248.852,-104.549 252.352,-104.614 248.911,-101.399 255.851,-104.679 255.851,-104.679"/><text text-anchor="start" x="214" y="-108.8" font-family="Lato" font-size="14.00">!a</text></g><!-- 5 --><g id="node6" class="node"><title>5</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="274" cy="-48" rx="18" ry="18"/><text text-anchor="middle" x="274" y="-44.3" font-family="Lato" font-size="14.00">5</text></g><!-- 2&#45;&gt;5 --><g id="edge6" class="edge"><title>2&#45;&gt;5</title><path fill="none" stroke="black" d="M183.191,-48.8393C200.897,-48.6739 228.648,-48.4145 248.616,-48.2279"/><polygon fill="black" stroke="black" points="255.851,-48.1603 248.881,-51.3756 252.351,-48.193 248.852,-48.2258 248.852,-48.2258 248.852,-48.2258 252.351,-48.193 248.822,-45.0759 255.851,-48.1603 255.851,-48.1603"/><text text-anchor="start" x="201" y="-52.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 3&#45;&gt;3 --><g id="edge7" class="edge"><title>3&#45;&gt;3</title><path fill="none" stroke="black" d="M264.767,-120.541C262.169,-130.909 265.246,-141 274,-141 280.702,-141 284.077,-135.085 284.124,-127.659"/><polygon fill="black" stroke="black" points="283.233,-120.541 287.229,-127.095 283.668,-124.014 284.103,-127.487 284.103,-127.487 284.103,-127.487 283.668,-124.014 280.977,-127.879 283.233,-120.541 283.233,-120.541"/><text text-anchor="start" x="269.5" y="-144.8" font-family="Lato" font-size="14.00">1</text></g><!-- 4 --><g id="node7" class="node"><title>4</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="383" cy="-120" rx="18" ry="18"/><text text-anchor="middle" x="383" y="-116.3" font-family="Lato" font-size="14.00">4</text></g><!-- 3&#45;&gt;4 --><g id="edge8" class="edge"><title>3&#45;&gt;4</title><path fill="none" stroke="black" d="M292.191,-107.41C309.975,-109.903 337.892,-113.817 357.88,-116.619"/><polygon fill="black" stroke="black" points="364.851,-117.596 357.482,-119.744 361.385,-117.11 357.919,-116.624 357.919,-116.624 357.919,-116.624 361.385,-117.11 358.356,-113.505 364.851,-117.596 364.851,-117.596"/><text text-anchor="start" x="311.5" y="-118.8" font-family="Lato" font-size="14.00">a &amp; b</text></g><!-- 6 --><g id="node9" class="node"><title>6</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="383" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="383" y="-14.3" font-family="Lato" font-size="14.00">6</text></g><!-- 5&#45;&gt;6 --><g id="edge10" class="edge"><title>5&#45;&gt;6</title><path fill="none" stroke="black" d="M291.719,-43.3125C309.7,-38.2709 338.426,-30.2169 358.637,-24.5505"/><polygon fill="black" stroke="black" points="365.399,-22.6546 359.509,-27.5774 362.029,-23.5995 358.659,-24.5444 358.659,-24.5444 358.659,-24.5444 362.029,-23.5995 357.808,-21.5114 365.399,-22.6546 365.399,-22.6546"/><text text-anchor="start" x="310" y="-41.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 7 --><g id="node8" class="node"><title>7</title><ellipse fill="#ffffaa" stroke="#e31a1c" stroke-width="2" cx="492" cy="-120" rx="18" ry="18"/><text text-anchor="middle" x="492" y="-116.3" font-family="Lato" font-size="14.00">7</text></g><!-- 4&#45;&gt;7 --><g id="edge9" class="edge"><title>4&#45;&gt;7</title><path fill="none" stroke="black" d="M401.191,-120C418.897,-120 446.648,-120 466.616,-120"/><polygon fill="black" stroke="black" points="473.851,-120 466.851,-123.15 470.351,-120 466.851,-120 466.851,-120 466.851,-120 470.351,-120 466.851,-116.85 473.851,-120 473.851,-120"/><text text-anchor="start" x="419" y="-123.8" font-family="Lato" font-size="14.00">a &amp; !b</text></g><!-- 7&#45;&gt;7 --><g id="edge12" class="edge"><title>7&#45;&gt;7</title><path fill="none" stroke="black" d="M482.767,-135.541C480.169,-145.909 483.246,-156 492,-156 498.702,-156 502.077,-150.085 502.124,-142.659"/><polygon fill="black" stroke="black" points="501.233,-135.541 505.229,-142.095 501.668,-139.014 502.103,-142.487 502.103,-142.487 502.103,-142.487 501.668,-139.014 498.977,-142.879 501.233,-135.541 501.233,-135.541"/><text text-anchor="start" x="488.5" y="-174.8" font-family="Lato" font-size="14.00">a</text><text text-anchor="start" x="484" y="-159.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g><!-- 6&#45;&gt;6 --><g id="edge11" class="edge"><title>6&#45;&gt;6</title><path fill="none" stroke="black" d="M373.767,-33.5414C371.169,-43.9087 374.246,-54 383,-54 389.702,-54 393.077,-48.0847 393.124,-40.6591"/><polygon fill="black" stroke="black" points="392.233,-33.5414 396.229,-40.0955 392.668,-37.0143 393.103,-40.4871 393.103,-40.4871 393.103,-40.4871 392.668,-37.0143 389.977,-40.8788 392.233,-33.5414 392.233,-33.5414"/><text text-anchor="start" x="376.5" y="-72.8" font-family="Lato" font-size="14.00">!b</text><text text-anchor="start" x="375" y="-57.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%% Cell type:markdown id: tags:
Such a procedure gives us map of where POR can be enabled when model checking using such an automaton.
%% Cell type:markdown id: tags:
### Second example
%% Cell type:markdown id: tags:
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`.
%% Cell type:code id: tags:
``` python
g1 = spot.formula('GF(a & Xa) & GF!a')
g2 = spot.formula('!GF(a & Xa) & GF!a')
g = spot.formula_Or([g1, g2])
```
%% Cell type:code id: tags:
``` python
print(spot.is_stutter_invariant(g1))
print(spot.is_stutter_invariant(g2))
print(spot.is_stutter_invariant(g))
```
%%%% Output: stream
False
False
True
%% Cell type:markdown id: tags:
Here are the automata for `g1` and `g2`, note that none of the states are stutter-invariant.
%% Cell type:code id: tags:
``` python
aut1 = spot.translate(g1)
aut1.set_name(str(g1))
spot.highlight_stutter_invariant_states(aut1, g1, 5)
display(aut1)
aut2 = spot.translate(g2)
aut2.set_name(str(g2))
spot.highlight_stutter_invariant_states(aut2, g2, 5)
display(aut2)
```
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="170pt" height="178pt"viewBox="0.00 0.00 170.00 177.75" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 173.75)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-173.75 166,-173.75 166,4 -4,4"/><text text-anchor="start" x="25" y="-155.55" font-family="Lato" font-size="14.00">G(F(a &amp; Xa) &amp; F!a)</text><text text-anchor="start" x="34" y="-141.55" font-family="Lato" font-size="14.00">Inf(</text><text text-anchor="start" x="56" y="-141.55" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="72" y="-141.55" font-family="Lato" font-size="14.00">)&amp;Inf(</text><text text-anchor="start" x="108" y="-141.55" font-family="Lato" font-size="14.00" fill="#ff4da0">❶</text><text text-anchor="start" x="124" y="-141.55" font-family="Lato" font-size="14.00">)</text><text text-anchor="start" x="37" y="-127.55" font-family="Lato" font-size="14.00">[gen. Büchi 2]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-20.7502" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-17.0502" font-family="Lato" font-size="14.00">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="black" d="M1.15491,-20.7502C2.79388,-20.7502 17.1543,-20.7502 30.6317,-20.7502"/><polygon fill="black" stroke="black" points="37.9419,-20.7502 30.9419,-23.9003 34.4419,-20.7502 30.9419,-20.7503 30.9419,-20.7503 30.9419,-20.7503 34.4419,-20.7502 30.9418,-17.6003 37.9419,-20.7502 37.9419,-20.7502"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M52.7643,-38.5319C52.2144,-48.0651 53.293,-56.7502 56,-56.7502 57.988,-56.7502 59.0977,-52.0663 59.3292,-45.8023"/><polygon fill="black" stroke="black" points="59.2357,-38.5319 62.4756,-45.4908 59.2808,-42.0316 59.3258,-45.5313 59.3258,-45.5313 59.3258,-45.5313 59.2808,-42.0316 56.1761,-45.5719 59.2357,-38.5319 59.2357,-38.5319"/><text text-anchor="start" x="50.5" y="-75.5502" font-family="Lato" font-size="14.00">!a</text><text text-anchor="start" x="48" y="-60.5502" font-family="Lato" font-size="14.00" fill="#ff4da0">❶</text></g><!-- 0&#45;&gt;0 --><g id="edge3" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M50.9906,-38.3273C47.5451,-59.4682 49.2148,-86.7502 56,-86.7502 62.043,-86.7502 64.0285,-65.1097 61.9564,-45.4408"/><polygon fill="black" stroke="black" points="61.0094,-38.3273 65.0556,-44.8504 61.4713,-41.7967 61.9332,-45.2661 61.9332,-45.2661 61.9332,-45.2661 61.4713,-41.7967 58.8107,-45.6818 61.0094,-38.3273 61.0094,-38.3273"/><text text-anchor="start" x="52.5" y="-90.5502" font-family="Lato" font-size="14.00">a</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="144" cy="-20.7502" rx="18" ry="18"/><text text-anchor="middle" x="144" y="-17.0502" font-family="Lato" font-size="14.00">1</text></g><!-- 0&#45;&gt;1 --><g id="edge4" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M74.4034,-20.7502C87.1928,-20.7502 104.732,-20.7502 118.874,-20.7502"/><polygon fill="black" stroke="black" points="125.916,-20.7502 118.916,-23.9003 122.416,-20.7502 118.916,-20.7503 118.916,-20.7503 118.916,-20.7503 122.416,-20.7502 118.916,-17.6003 125.916,-20.7502 125.916,-20.7502"/><text text-anchor="start" x="96.5" y="-39.5502" font-family="Lato" font-size="14.00">a</text><text text-anchor="start" x="92" y="-24.5502" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g><!-- 1&#45;&gt;0 --><g id="edge5" class="edge"><title>1&#45;&gt;0</title><path fill="none" stroke="black" d="M128.689,-10.8844C122.598,-7.25669 115.237,-3.58794 108,-1.75016 101.108,-0 98.8924,-0 92,-1.75016 87.1374,-2.98492 82.2193,-5.0462 77.668,-7.36626"/><polygon fill="black" stroke="black" points="71.3113,-10.8844 75.9105,-4.73864 74.3736,-9.18956 77.4359,-7.49469 77.4359,-7.49469 77.4359,-7.49469 74.3736,-9.18956 78.9613,-10.2507 71.3113,-10.8844 71.3113,-10.8844"/><text text-anchor="start" x="96.5" y="-5.55016" font-family="Lato" font-size="14.00">a</text></g><!-- 1&#45;&gt;1 --><g id="edge6" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="black" d="M136.332,-37.0404C134.483,-47.1393 137.039,-56.7502 144,-56.7502 149.221,-56.7502 151.964,-51.3441 152.229,-44.3805"/><polygon fill="black" stroke="black" points="151.668,-37.0404 155.342,-43.7801 151.935,-40.5303 152.201,-44.0201 152.201,-44.0201 152.201,-44.0201 151.935,-40.5303 149.06,-44.2601 151.668,-37.0404 151.668,-37.0404"/><text text-anchor="start" x="140.5" y="-75.5502" font-family="Lato" font-size="14.00">a</text><text text-anchor="start" x="136" y="-60.5502" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%%%% Output: display_data
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.38.0 (20140413.2041)--><!-- Title: G Pages: 1 --><svg width="253pt" height="172pt"viewBox="0.00 0.00 253.00 172.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 168)"><title>G</title><polygon fill="white" stroke="none" points="-4,4 -4,-168 249,-168 249,4 -4,4"/><text text-anchor="start" x="88.5" y="-149.8" font-family="Lato" font-size="14.00">FG(!a | X!a)</text><text text-anchor="start" x="101.5" y="-135.8" font-family="Lato" font-size="14.00">Inf(</text><text text-anchor="start" x="123.5" y="-135.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text><text text-anchor="start" x="139.5" y="-135.8" font-family="Lato" font-size="14.00">)</text><text text-anchor="start" x="99.5" y="-121.8" font-family="Lato" font-size="14.00">[Büchi]</text><!-- I --><!-- 0 --><g id="node2" class="node"><title>0</title><ellipse fill="#ffffaa" stroke="black" cx="56" cy="-18" rx="18" ry="18"/><text text-anchor="middle" x="56" y="-14.3" font-family="Lato" font-size="14.00">0</text></g><!-- I&#45;&gt;0 --><g id="edge1" class="edge"><title>I&#45;&gt;0</title><path fill="none" stroke="black" d="M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18"/><polygon fill="black" stroke="black" points="37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18"/></g><!-- 0&#45;&gt;0 --><g id="edge2" class="edge"><title>0&#45;&gt;0</title><path fill="none" stroke="black" d="M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433"/><polygon fill="black" stroke="black" points="62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373"/><text text-anchor="start" x="51.5" y="-57.8" font-family="Lato" font-size="14.00">1</text></g><!-- 1 --><g id="node3" class="node"><title>1</title><ellipse fill="#ffffaa" stroke="black" cx="139" cy="-48" rx="18" ry="18"/><text text-anchor="start" x="134.5" y="-44.3" font-family="Lato" font-size="14.00">1</text></g><!-- 0&#45;&gt;1 --><g id="edge3" class="edge"><title>0&#45;&gt;1</title><path fill="none" stroke="black" d="M73.003,-23.927C85.017,-28.3767 101.638,-34.5325 115.064,-39.5053"/><polygon fill="black" stroke="black" points="121.753,-41.9826 114.095,-42.5052 118.471,-40.767 115.189,-39.5513 115.189,-39.5513 115.189,-39.5513 118.471,-40.767 116.283,-36.5974 121.753,-41.9826 121.753,-41.9826"/><text text-anchor="start" x="92" y="-37.8" font-family="Lato" font-size="14.00">!a</text></g><!-- 2 --><g id="node4" class="node"><title>2</title><ellipse fill="#ffffaa" stroke="black" cx="227" cy="-30" rx="18" ry="18"/><text text-anchor="middle" x="227" y="-26.3" font-family="Lato" font-size="14.00">2</text></g><!-- 0&#45;&gt;2 --><g id="edge4" class="edge"><title>0&#45;&gt;2</title><path fill="none" stroke="black" d="M73.3505,-13.1706C93.2093,-7.96467 127.69,-1.04806 157,-6 173.081,-8.71684 190.415,-14.7595 203.687,-20.1014"/><polygon fill="black" stroke="black" points="210.229,-22.8097 202.557,-23.0425 206.995,-21.4709 203.762,-20.1321 203.762,-20.1321 203.762,-20.1321 206.995,-21.4709 204.966,-17.2216 210.229,-22.8097 210.229,-22.8097"/><text text-anchor="start" x="135.5" y="-9.8" font-family="Lato" font-size="14.00">a</text></g><!-- 1&#45;&gt;1 --><g id="edge5" class="edge"><title>1&#45;&gt;1</title><path fill="none" stroke="black" d="M131.969,-64.6641C130.406,-74.625 132.75,-84 139,-84 143.688,-84 146.178,-78.7266 146.471,-71.8876"/><polygon fill="black" stroke="black" points="146.031,-64.6641 149.601,-71.4598 146.244,-68.1576 146.456,-71.6511 146.456,-71.6511 146.456,-71.6511 146.244,-68.1576 143.312,-71.8425 146.031,-64.6641 146.031,-64.6641"/><text text-anchor="start" x="133.5" y="-102.8" font-family="Lato" font-size="14.00">!a</text><text text-anchor="start" x="131" y="-87.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g><!-- 1&#45;&gt;2 --><g id="edge6" class="edge"><title>1&#45;&gt;2</title><path fill="none" stroke="black" d="M155.003,-56.5894C165.311,-61.3438 179.21,-65.4707 191,-61 197.945,-58.3667 204.396,-53.6555 209.82,-48.6883"/><polygon fill="black" stroke="black" points="214.881,-43.7031 212.105,-50.8594 212.388,-46.1591 209.894,-48.6152 209.894,-48.6152 209.894,-48.6152 212.388,-46.1591 207.684,-46.3709 214.881,-43.7031 214.881,-43.7031"/><text text-anchor="start" x="179.5" y="-80.8" font-family="Lato" font-size="14.00">a</text><text text-anchor="start" x="175" y="-65.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g><!-- 2&#45;&gt;1 --><g id="edge7" class="edge"><title>2&#45;&gt;1</title><path fill="none" stroke="black" d="M209.173,-26.2984C199.09,-24.7439 186.112,-23.9222 175,-27 169.835,-28.4305 164.668,-30.8484 159.95,-33.5456"/><polygon fill="black" stroke="black" points="153.837,-37.33 158.131,-30.967 156.813,-35.4876 159.789,-33.6452 159.789,-33.6452 159.789,-33.6452 156.813,-35.4876 161.447,-36.3235 153.837,-37.33 153.837,-37.33"/><text text-anchor="start" x="177.5" y="-45.8" font-family="Lato" font-size="14.00">!a</text><text text-anchor="start" x="175" y="-30.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text></g></g></svg>)
%% Cell type:markdown id: tags:
Now we build the sum of these two 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 id: tags:
``` python
aut = spot.sum(aut1, aut2)
# At this point it is unknown if AUT is stutter-invariant
assert(aut.prop_stutter_invariant().is_maybe())
spot.highlight_stutter_invariant_states(aut, g, 5)