{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"spot.setup(show_default='.ba')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"These test cases for the `remove_alternation()` algorithm."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut = spot.automaton('''\n",
"HOA: v1\n",
"tool: \"ltl3ba\" \"1.1.3\"\n",
"name: \"VWAA for FGa && GFb\"\n",
"States: 6\n",
"Start: 0\n",
"acc-name: co-Buchi\n",
"Acceptance: 1 Fin(0)\n",
"AP: 2 \"a\" \"b\"\n",
"properties: trans-labels explicit-labels state-acc univ-branch very-weak\n",
"--BODY--\n",
"State: 0 \"(FG(a) && GF(b))\"\n",
" [t] 3&1\n",
"State: 1 \"GF(b)\"\n",
" [(1)] 1\n",
" [(!1)] 2&1\n",
"State: 2 \"F(b)\" {0}\n",
" [(1)] 5\n",
" [(!1)] 2\n",
"State: 3 \"FG(a)\" {0}\n",
" [(0)] 4\n",
" [t] 3\n",
"State: 4 \"G(a)\"\n",
" [(0)] 4\n",
"State: 5 \"t\"\n",
" [t] 5\n",
"--END--\n",
"'''); aut.show('.1ab')"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74000699f0> >"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut2 = spot.remove_alternation(aut, True); aut2"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74001bff30> >"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.scc_filter(aut2, True)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# Example from ADL's PSL2TGBA talk.\n",
"aut = spot.automaton('''\n",
"HOA: v1\n",
"States: 3\n",
"Start: 0\n",
"acc-name: co-Buchi\n",
"Acceptance: 1 Fin(0)\n",
"AP: 3 \"a\" \"b\" \"p\"\n",
"--BODY--\n",
"State: 0 \"(a;a*;b)*\" {0}\n",
" [0] 1\n",
" [!0] 2\n",
"State: 1 \"a*;b;(a;a*;b)*\" {0}\n",
" [0&1&2] 0&1\n",
" [!1&2] 1\n",
" [!0&!1] 2\n",
" [!0&1&2] 0\n",
"State: 2\n",
" [t] 2\n",
"--END--\n",
"'''); aut.show('.1ab')"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f7400069900> >"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.remove_alternation(aut, True)"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut = spot.automaton('''\n",
"HOA: v1\n",
"States: 5\n",
"Start: 3\n",
"acc-name: co-Buchi\n",
"Acceptance: 1 Fin(0)\n",
"AP: 3 \"a\" \"b\" \"p\"\n",
"--BODY--\n",
"State: 0 \"(a;a*;b)*\" {0}\n",
" [0] 1\n",
" [!0] 2\n",
"State: 1 \"a*;b;(a;a*;b)*\" {0}\n",
" [0&1&2] 0&1\n",
" [!1&2] 1\n",
" [!0&!1] 2\n",
" [!0&1&2] 0\n",
"State: 2\n",
" [t] 2\n",
"State: 3\n",
" [0] 4&0\n",
"State: 4\n",
" [t] 3\n",
"--END--\n",
"'''); aut.show('.1ab')"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f7400079150> >"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.remove_alternation(aut, True)"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# Example from ADL's PSL2TGBA talk.\n",
"aut = spot.automaton('''\n",
"HOA: v1\n",
"States: 6\n",
"Start: 0&3\n",
"Acceptance: 1 Fin(0)\n",
"AP: 3 \"a\" \"b\" \"p\"\n",
"--BODY--\n",
"State: 0 \"(a;a*;b)*\" {0}\n",
" [0] 1\n",
" [!0] 2\n",
"State: 1 \"a*;b;(a;a*;b)*\" {0}\n",
" [0&1&2] 0&1\n",
" [!1&2] 1\n",
" [!0&!1] 2\n",
" [!0&1&2] 0\n",
"State: 2\n",
" [t] 2\n",
"State: 3\n",
" [0] 3\n",
" [!0] 3&4\n",
"State: 4 {0}\n",
" [!0] 4\n",
" [0] 5\n",
"State: 5\n",
" [t] 5\n",
"--END--\n",
"'''); aut.show('.1ab')"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f7400069c90> >"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.remove_alternation(aut, True)"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f740008b360> >"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a = spot.automaton('''\n",
"HOA: v1\n",
"tool: \"ltl3dra\" \"0.2.2\"\n",
"name: \"VWAA for GFa\"\n",
"States: 3\n",
"Start: 0\n",
"acc-name: co-Buchi\n",
"Acceptance: 1 Fin(0)\n",
"AP: 1 \"a\"\n",
"properties: trans-labels explicit-labels state-acc univ-branch very-weak\n",
"--BODY--\n",
"State: 0 \"GF(a)\"\n",
" [t] 1&0\n",
"State: 1 \"F(a)\" {0}\n",
" [(0)] 2\n",
" [t] 1\n",
"State: 2 \"t\"\n",
" [t] 2\n",
"--END--\n",
"'''); a"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f7400150090> >"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.remove_alternation(a, True)"
]
}
],
"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.6.5"
}
},
"nbformat": 4,
"nbformat_minor": 2
}