{
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.5.4"
},
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"spot.setup(show_default='.ba')\n",
"from IPython.display import display"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Detecting stutter-invariant states\n",
"\n",
"Spot can easily check whether a formula is stutter invariant. The check is automaton-based, so it can detect stutter invariant formulas even if they use the `X` operator as `f1` below."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')\n",
"f2 = spot.formula('F(a & Xa & XXa & G!b)')\n",
"f = spot.formula_Or([f1, f2])\n",
"\n",
"print(spot.is_stutter_invariant(f1))\n",
"print(spot.is_stutter_invariant(f2))\n",
"print(spot.is_stutter_invariant(f))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"True\n",
"False\n",
"False\n"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"pos = spot.translate(f)\n",
"display(pos)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1b58d0> >"
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"While the automaton as a whole is stutter-sensitive, but we can see that eventually we will enter a sub-automaton that is stutter-invariant.\n",
"\n",
"The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.stutter_invariant_states(pos, f)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"text": [
"(False, True, False, True, True, True, True, True)"
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `highligh_...()` version colors the stutter-invariant states of the automaton for display.\n",
"(That 5 is the color number for red.)"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.highlight_stutter_invariant_states(pos, f, 5)\n",
"display(pos)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1b58d0> >"
]
}
],
"prompt_number": 5
},
{
"cell_type": "heading",
"level": 1,
"metadata": {},
"source": [
"Another test case"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The union of two stutter-sensitive formulas can be stutter-invariant. Let's make sure that our checks agree."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"g1 = spot.formula('GF(a & Xa) & GF!a')\n",
"g2 = spot.formula('!GF(a & Xa) & GF!a')\n",
"g = spot.formula_Or([g1, g2])"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.is_stutter_invariant(g1))\n",
"print(spot.is_stutter_invariant(g2))\n",
"print(spot.is_stutter_invariant(g))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"False\n",
"False\n",
"True\n"
]
}
],
"prompt_number": 7
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"aut1 = spot.translate(g1)\n",
"aut2 = spot.translate(g2)\n",
"aut = spot.product_or(aut1, aut2)\n",
"spot.highlight_stutter_invariant_states(aut1, g1, 5)\n",
"display(aut1)\n",
"spot.highlight_stutter_invariant_states(aut2, g2, 5)\n",
"display(aut2)\n",
"# At this point it is unknown if AUT is stutter-invariant\n",
"assert(aut.prop_stutter_invariant().is_maybe())\n",
"spot.highlight_stutter_invariant_states(aut, g, 5)\n",
"display(aut)\n",
"# The stutter_invariant property is set on AUT as a side effect\n",
"# of calling sutter_invariant_states() or some variant of it.\n",
"assert(aut.prop_stutter_invariant().is_true())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1b5660> >"
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1ce720> >"
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1b5810> >"
]
}
],
"prompt_number": 8
},
{
"cell_type": "heading",
"level": 1,
"metadata": {},
"source": [
"Global vs Local stuttering"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"h = spot.formula('F(a & X(!a & X(b & Xb)))')\n",
"aut = spot.translate(h)\n",
"spot.highlight_stutter_invariant_states(aut, h, 5)\n",
"display(aut)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1ce8a0> >"
]
}
],
"prompt_number": 9
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above result uses a natural definition of \"stutter-invariant state\": a state is stutter-invariant if the language accepted from this state is.\n",
"\n",
"We can also have a \"local\" variant of the stutter invariance check that considers the state as stutter invariant if you can stutter on (or remove duplicates of) the first letter read from that state, but not necessary do the same operations on a different letter that follows. Just pass `True` as the last optional parameter, as below."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.highlight_stutter_invariant_states(aut, h, 5, True)\n",
"display(aut)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c1ce8a0> >"
]
}
],
"prompt_number": 10
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Note that an SCC can contain a mix of locally stutter-invariant and local stutter-sensitive states. So probably POR should be applied between two locally stutter-invariant states? Here is the deterministic version of the above automaton for example."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"aut = spot.translate(h, 'deterministic')\n",
"spot.highlight_stutter_invariant_states(aut, h, 5, True)\n",
"display(aut.show('.abs'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 11
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Support for more complex acceptance conditions\n",
"\n",
"This also works, although it's not clear how useful that is."
]
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"m = spot.formula('F(a & Xa & Gb) | GF!b')\n",
"aut = spot.translate(m, 'deterministic', 'generic')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 12
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.highlight_stutter_invariant_states(aut, m, 5, True)\n",
"display(aut)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c15f600> >"
]
}
],
"prompt_number": 13
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Checking an automaton without formula\n",
"\n",
"The check can also be applied on an automaton for which the formula is unknown, but in the case the input automaton will be complemented via determinization, so this is costlier."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"aut = spot.automaton('genaut --ks-nca=2 |')\n",
"spot.highlight_stutter_invariant_states(aut, None, 5, True)\n",
"display(aut)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f0b7c13e660> >"
]
}
],
"prompt_number": 44
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If the negated automaton is already known, it can be passed as second argument (instead of the positive formula) to avoid unnecessary work."
]
}
],
"metadata": {}
}
]
}