notebooks: correction of typos
* tests/python/_partitioned_relabel.ipynb, tests/python/_product_weak.ipynb, tests/python/acc_cond.ipynb, tests/python/aliases.ipynb, tests/python/automata.ipynb, tests/python/cav22-figs.ipynb, tests/python/contains.ipynb, tests/python/decompose.ipynb, tests/python/formulas.ipynb, tests/python/games.ipynb, tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb, tests/python/parity.ipynb, tests/python/product.ipynb, tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb, tests/python/synthesis.ipynb, tests/python/twagraph-internals.ipynb, tests/python/word.ipynb, tests/python/zlktree.ipynb: here
This commit is contained in:
Florian Renkin
parent
858629dd3a
commit
6dc11b4715
20 changed files with 242 additions and 82 deletions
|
|
@ -12,17 +12,19 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Stutter-invariant languages\n",
|
||||
"\n",
|
||||
"A language $L$ is said to be _stutter-invariant_ iff $\\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_{i+1}\\ldots\\in L \\iff \\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_i\\ell_{i+1}\\ldots\\in L$, i.e., if duplicating a letter in a word or removing a duplicated letter does not change the membership of that word to $L$. These languages are also called _stutter-insensitive_. We use the adjective _sutter-sensitive_ to describe a language that is not stutter-invariant. Of course we can extend this vocabulary to LTL formulas or automata that represent stutter-invariant languages.\n",
|
||||
"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 _stutter-sensitive_ to describe a language that is not stutter-invariant. Of course we can extend this vocabulary to LTL formulas or automata that represent stutter-invariant languages.\n",
|
||||
"\n",
|
||||
"Stutter-invariant languages play an important role in model checking. When verifying a stutter-invariant specification against a system, we know that we have some freedom in how we discretize the time in the model: as long as we do not hide changes of model variables that are observed by the specification, we can merge multiple steps of the model. This, combined by careful analysis of actions of the model that are independent, is the basis for a set of techniques known as _partial-order reductions_ (POR) that postpone the visit of some successors in the model, because we know we can always visit them later."
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -68,6 +70,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -95,13 +98,15 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Of course this `is_stutter_invariant()` function first checks whether the formula is `X`-free before wasting time building automata, so if you want to detect stutter-invariant formulas in your model checker, this is the only function to use. Also, if you hapen to already have an automaton `aut_g` for `g`, you should pass it as a second argument to avoid it being recomputed: `spot.is_stutter_invariant(g, aut_g)`."
|
||||
"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 happen 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)`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -132,6 +137,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -139,10 +145,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Similarly to formulas, automata use a few bits to store some known properties about themselves, like whether they represent a stutter-invariant language. This property can be checked with the `prop_stutter_invariant()` method, but that returns a `trival` instance (i.e., yes, no, or maybe). Some algorithms will update that property whenever that is cheap or expliclitely asked for. For instance `spot.translate()` only sets the property if the translated formula is `X`-free."
|
||||
"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 explicitly asked for. For instance `spot.translate()` only sets the property if the translated formula is `X`-free."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -164,6 +171,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -188,10 +196,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Note that `prop_stutter_invariant()` was updated as a side-effect so that any futher call to `is_stutter_invariant()` with this automaton will be instantaneous."
|
||||
"Note that `prop_stutter_invariant()` was updated as a side-effect so that any further call to `is_stutter_invariant()` with this automaton will be instantaneous."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -212,10 +221,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"You have to be aware of this property being set in your back because if while playing with `is_stutter_invariant()` you the incorrect formula for an automaton by mistake, the automaton will have its property set incorrectly, and running `is_stutter_inariant()` with the correct formula will simply return the cached property.\n",
|
||||
"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_invariant()` with the correct formula will simply return the cached property.\n",
|
||||
"\n",
|
||||
"In doubt, you can always reset the property as follows:"
|
||||
]
|
||||
|
|
@ -239,6 +249,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -331,17 +342,19 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Explaining why a formula is not sutter-invariant"
|
||||
"## Explaining why a formula is not stutter-invariant"
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"As explained in our [Spin'15 paper](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) the sutter-invariant checks are implemented using simple operators suchs as `spot.closure(aut)`, that augment the language of L by adding words that can be obtained by removing duplicated letters, and `spot.sl(aut)` or `spot.sl2(aut)` that both augment the language that L by adding words that can be obtained by duplicating letters. The default `is_stutter_invariant()` function is implemented as `spot.product(spot.closure(aut), spot.closure(neg_aut)).is_empty()`, but that is just one possible implementation selected because it was more efficient.\n",
|
||||
"As explained in our [Spin'15 paper](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) the stutter-invariant checks are implemented using simple operators such as `spot.closure(aut)`, that augment the language of L by adding words that can be obtained by removing duplicated letters, and `spot.sl(aut)` or `spot.sl2(aut)` that both augment the language that L by adding words that can be obtained by duplicating letters. The default `is_stutter_invariant()` function is implemented as `spot.product(spot.closure(aut), spot.closure(neg_aut)).is_empty()`, but that is just one possible implementation selected because it was more efficient.\n",
|
||||
"\n",
|
||||
"Using these bricks, we can modify the original algorithm so it uses a counterexample to explain why a formula is stutter-sensitive."
|
||||
]
|
||||
|
|
@ -394,22 +407,25 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Note that a variant of the above explanation procedure is already integerated in our [on-line LTL translator tool](https://spot.lrde.epita.fr/app/) (use the <i>study</i> tab)."
|
||||
"Note that a variant of the above explanation procedure is already integrated in our [on-line LTL translator tool](https://spot.lrde.epita.fr/app/) (use the <i>study</i> tab)."
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Detecting stutter-invariant states\n",
|
||||
"\n",
|
||||
"Even if the language of an automaton is not sutter invariant, some of its states may recognize a stutter-invariant language. (We assume the language of a state is the language the automaton would have when starting from this state.)"
|
||||
"Even if the language of an automaton is not stutter 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.)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -616,6 +632,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -645,10 +662,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"For convenience, the `highligh_...()` version colors the stutter-invariant states of the automaton for display.\n",
|
||||
"For convenience, the `highlight_...()` version colors the stutter-invariant states of the automaton for display.\n",
|
||||
"(That 5 is the color number for red in Spot's hard-coded palette.)"
|
||||
]
|
||||
},
|
||||
|
|
@ -825,6 +843,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -832,6 +851,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -839,10 +859,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"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`."
|
||||
"This second example illustrates the fact that a state can be marked if it is not stutter-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 stutter-invariant formula `GF!a`."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -878,6 +899,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1082,6 +1104,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1286,11 +1309,12 @@
|
|||
"spot.highlight_stutter_invariant_states(aut, g, 5)\n",
|
||||
"display(aut)\n",
|
||||
"# The stutter_invariant property is set on AUT as a side effect\n",
|
||||
"# of calling sutter_invariant_states() or any variant of it.\n",
|
||||
"# of calling stutter_invariant_states() or any variant of it.\n",
|
||||
"assert(aut.prop_stutter_invariant().is_true())"
|
||||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1415,6 +1439,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1422,10 +1447,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Sutter-invariance at the letter level\n",
|
||||
"## Stutter-invariance at the letter level\n",
|
||||
"\n",
|
||||
"Instead of marking each state as stuttering or not, we can list the letters that we can stutter in each state.\n",
|
||||
"More precisely, a state $q$ is _stutter-invariant for letter $a$_ if the membership to $L(q)$ of any word starting with $a$ is preserved by the operations that duplicate letters or remove duplicates. \n",
|
||||
|
|
@ -1547,12 +1573,13 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"The `stutter_invariant_letters()` functions returns a vector of BDDs indexed by state numbers. The BDD at index $q$ specifies all letters $\\ell$ for which state $q$ would be stuttering. Note that if $q$ is stutter-invariant or reachable from a stutter-invariant state, the associated BDD will be `bddtrue` (printed as `1` below).\n",
|
||||
"\n",
|
||||
"This interface is a bit inconveniant to use interactively, due to the fact that we need a `spot.bdd_dict` object to print a BDD."
|
||||
"This interface is a bit inconvenient to use interactively, due to the fact that we need a `spot.bdd_dict` object to print a BDD."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -1578,6 +1605,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1585,7 +1613,7 @@
|
|||
"\n",
|
||||
"Consider the following automaton, which is a variant of our second example above. \n",
|
||||
"\n",
|
||||
"The language accepted from state (2) is `!GF(a & Xa) & GF!a` (this can be simplified to `FG(!a | X!a)`), while the language accepted from state (0) is `GF(a & Xa) & GF!a`. Therefore. the language accepted from state (5) is `a & X(GF!a)`. Since this is equivalent to `a & GF(!a)` state (5) recognizes stutter-invariant language, but as we can see, it is not the case that all states below (5) are also marked. In fact, states (0) can also be reached via states (7) and (6), recognizing respectively `(a & X(a & GF!a)) | (!a & X(!a & GF(a & Xa) & GF!a))` and `!a & GF(a & Xa) & GF!a))`, i.e., two stutter-sentive languages."
|
||||
"The language accepted from state (2) is `!GF(a & Xa) & GF!a` (this can be simplified to `FG(!a | X!a)`), while the language accepted from state (0) is `GF(a & Xa) & GF!a`. Therefore. the language accepted from state (5) is `a & X(GF!a)`. Since this is equivalent to `a & GF(!a)` state (5) recognizes stutter-invariant language, but as we can see, it is not the case that all states below (5) are also marked. In fact, states (0) can also be reached via states (7) and (6), recognizing respectively `(a & X(a & GF!a)) | (!a & X(!a & GF(a & Xa) & GF!a))` and `!a & GF(a & Xa) & GF!a))`, i.e., two stutter-sensitive languages."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -1817,6 +1845,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -1845,11 +1874,12 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"In cases where we prefer to have a forward-closed set of stutter-invariant states, it is always possible to duplicate\n",
|
||||
"the problematic states. The `make_stutter_invariant_foward_closed_inplace()` modifies the automaton in place, and also returns an updated copie of the vector of stutter-invariant states."
|
||||
"the problematic states. The `make_stutter_invariant_forward_closed_inplace()` modifies the automaton in place, and also returns an updated copy of the vector of stutter-invariant states."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2128,10 +2158,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Now, state 0 is no longuer a problem."
|
||||
"Now, state 0 is no longer a problem."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2155,10 +2186,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Let's see how infrequently the set of stutter-invarant states is not closed."
|
||||
"Let's see how infrequently the set of stutter-invariant states is not closed."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -2277,6 +2309,7 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
|
|
@ -2304,10 +2337,11 @@
|
|||
]
|
||||
},
|
||||
{
|
||||
"attachments": {},
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Here is the percentage of stutter-invarant states."
|
||||
"Here is the percentage of stutter-invariant states."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue