Making solved game to mealy more flexible
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Solved game to mealy now also supports the other mealy formats * tests/python/_synthesis.ipynb: Test * tests/Makefile.am: Test
This commit is contained in:
Philipp Schlehuber
philipp
parent
488efee7b3
commit
5b6e2a210a
4 changed files with 469 additions and 5 deletions
|
|
@ -448,6 +448,7 @@ TESTS_python = \
|
|||
python/rs_like.py \
|
||||
python/sum.py \
|
||||
python/synthesis.py \
|
||||
python/_synthesis.ipynb \
|
||||
python/toparity.py \
|
||||
python/trival.py \
|
||||
python/tra2tba.py \
|
||||
|
|
|
|||
415
tests/python/_synthesis.ipynb
Normal file
415
tests/python/_synthesis.ipynb
Normal file
|
|
@ -0,0 +1,415 @@
|
|||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 1,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"import spot\n",
|
||||
"spot.setup()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Additional testing for synthesis"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Testing the different methods to solve"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 2,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 2,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"si = spot.synthesis_info()\n",
|
||||
"si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n",
|
||||
"game = spot.ltl_to_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\n",
|
||||
"spot.solve_game(game)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 3,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"HOA: v1\n",
|
||||
"States: 7\n",
|
||||
"Start: 0\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[!0&!1] 1\n",
|
||||
"[!0&1] 2\n",
|
||||
"[0&!1] 3\n",
|
||||
"[0&1] 4\n",
|
||||
"State: 1\n",
|
||||
"[0&1&!2] 4\n",
|
||||
"[0&!1&!2] 3\n",
|
||||
"[!0&1&!2] 2\n",
|
||||
"[!0&!1&!2] 1\n",
|
||||
"State: 2\n",
|
||||
"[0&!2] 4\n",
|
||||
"[!0&!2] 2\n",
|
||||
"State: 3\n",
|
||||
"[!0&1&2] 5\n",
|
||||
"[0&1&2] 4\n",
|
||||
"[!0&!1&2] 6\n",
|
||||
"[0&!1&2] 3\n",
|
||||
"State: 4\n",
|
||||
"[!0&2] 5\n",
|
||||
"[0&2] 4\n",
|
||||
"State: 5\n",
|
||||
"[!0&!2] 5\n",
|
||||
"[0&!2] 4\n",
|
||||
"State: 6\n",
|
||||
"[!0&1&!2] 5\n",
|
||||
"[0&1&!2] 4\n",
|
||||
"[!0&!1&!2] 6\n",
|
||||
"[0&!1&!2] 3\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 7\n",
|
||||
"Start: 0\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[!0&!1] 1\n",
|
||||
"[!0&1] 2\n",
|
||||
"[0&!1] 3\n",
|
||||
"[0&1] 4\n",
|
||||
"State: 1\n",
|
||||
"[0&1&!2] 4\n",
|
||||
"[0&!1&!2] 3\n",
|
||||
"[!0&1&!2] 2\n",
|
||||
"[!0&!1&!2] 1\n",
|
||||
"State: 2\n",
|
||||
"[0&!2] 4\n",
|
||||
"[!0&!2] 2\n",
|
||||
"State: 3\n",
|
||||
"[!0&1&2] 5\n",
|
||||
"[0&1&2] 4\n",
|
||||
"[!0&!1&2] 6\n",
|
||||
"[0&!1&2] 3\n",
|
||||
"State: 4\n",
|
||||
"[!0&2] 5\n",
|
||||
"[0&2] 4\n",
|
||||
"State: 5\n",
|
||||
"[!0&!2] 5\n",
|
||||
"[0&!2] 4\n",
|
||||
"State: 6\n",
|
||||
"[!0&1&!2] 5\n",
|
||||
"[0&1&!2] 4\n",
|
||||
"[!0&!1&!2] 6\n",
|
||||
"[0&!1&!2] 3\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 21\n",
|
||||
"Start: 0\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"spot-state-player: 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[!0&!1] 7\n",
|
||||
"[!0&1] 8\n",
|
||||
"[0&!1] 9\n",
|
||||
"[0&1] 10\n",
|
||||
"State: 1\n",
|
||||
"[0&1] 11\n",
|
||||
"[0&!1] 12\n",
|
||||
"[!0&1] 13\n",
|
||||
"[!0&!1] 14\n",
|
||||
"State: 2\n",
|
||||
"[0] 11\n",
|
||||
"[!0] 13\n",
|
||||
"State: 3\n",
|
||||
"[!0&1] 15\n",
|
||||
"[0&1] 16\n",
|
||||
"[!0&!1] 17\n",
|
||||
"[0&!1] 18\n",
|
||||
"State: 4\n",
|
||||
"[!0] 15\n",
|
||||
"[0] 16\n",
|
||||
"State: 5\n",
|
||||
"[!0] 19\n",
|
||||
"[0] 11\n",
|
||||
"State: 6\n",
|
||||
"[!0&1] 19\n",
|
||||
"[0&1] 11\n",
|
||||
"[!0&!1] 20\n",
|
||||
"[0&!1] 12\n",
|
||||
"State: 7\n",
|
||||
"[t] 1\n",
|
||||
"State: 8\n",
|
||||
"[t] 2\n",
|
||||
"State: 9\n",
|
||||
"[t] 3\n",
|
||||
"State: 10\n",
|
||||
"[t] 4\n",
|
||||
"State: 11\n",
|
||||
"[!2] 4\n",
|
||||
"State: 12\n",
|
||||
"[!2] 3\n",
|
||||
"State: 13\n",
|
||||
"[!2] 2\n",
|
||||
"State: 14\n",
|
||||
"[!2] 1\n",
|
||||
"State: 15\n",
|
||||
"[2] 5\n",
|
||||
"State: 16\n",
|
||||
"[2] 4\n",
|
||||
"State: 17\n",
|
||||
"[2] 6\n",
|
||||
"State: 18\n",
|
||||
"[2] 3\n",
|
||||
"State: 19\n",
|
||||
"[!2] 5\n",
|
||||
"State: 20\n",
|
||||
"[!2] 6\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 2\n",
|
||||
"Start: 1\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0&1&!2] 1\n",
|
||||
"[0&!1&!2] 1\n",
|
||||
"[!0&1&!2] 0\n",
|
||||
"[!0&!1&!2] 0\n",
|
||||
"State: 1\n",
|
||||
"[!0&1&2] 0\n",
|
||||
"[0&1&2] 1\n",
|
||||
"[!0&!1&2] 0\n",
|
||||
"[0&!1&2] 1\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 2\n",
|
||||
"Start: 1\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0&1&!2] 1\n",
|
||||
"[0&!1&!2] 1\n",
|
||||
"[!0&1&!2] 0\n",
|
||||
"[!0&!1&!2] 0\n",
|
||||
"State: 1\n",
|
||||
"[!0&1&2] 0\n",
|
||||
"[0&1&2] 1\n",
|
||||
"[!0&!1&2] 0\n",
|
||||
"[0&!1&2] 1\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 6\n",
|
||||
"Start: 1\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"spot-state-player: 0 0 1 1 1 1\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0&1] 2\n",
|
||||
"[0&!1] 2\n",
|
||||
"[!0&1] 3\n",
|
||||
"[!0&!1] 3\n",
|
||||
"State: 1\n",
|
||||
"[!0&1] 4\n",
|
||||
"[0&1] 5\n",
|
||||
"[!0&!1] 4\n",
|
||||
"[0&!1] 5\n",
|
||||
"State: 2\n",
|
||||
"[!2] 1\n",
|
||||
"State: 3\n",
|
||||
"[!2] 0\n",
|
||||
"State: 4\n",
|
||||
"[2] 0\n",
|
||||
"State: 5\n",
|
||||
"[2] 1\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 6\n",
|
||||
"Start: 1\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"spot-state-player: 0 0 1 1 1 1\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0] 3\n",
|
||||
"[!0] 4\n",
|
||||
"State: 1\n",
|
||||
"[0] 2\n",
|
||||
"[!0] 5\n",
|
||||
"State: 2\n",
|
||||
"[2] 1\n",
|
||||
"State: 3\n",
|
||||
"[!2] 1\n",
|
||||
"State: 4\n",
|
||||
"[!2] 0\n",
|
||||
"State: 5\n",
|
||||
"[2] 0\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 2\n",
|
||||
"Start: 0\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0&2] 0\n",
|
||||
"[!0&2] 1\n",
|
||||
"State: 1\n",
|
||||
"[0&!2] 0\n",
|
||||
"[!0&!2] 1\n",
|
||||
"--END--\n",
|
||||
"HOA: v1\n",
|
||||
"States: 6\n",
|
||||
"Start: 1\n",
|
||||
"AP: 3 \"i1\" \"i0\" \"o0\"\n",
|
||||
"acc-name: all\n",
|
||||
"Acceptance: 0 t\n",
|
||||
"properties: trans-labels explicit-labels state-acc deterministic\n",
|
||||
"spot-state-player: 0 0 1 1 1 1\n",
|
||||
"--BODY--\n",
|
||||
"State: 0\n",
|
||||
"[0] 3\n",
|
||||
"[!0] 4\n",
|
||||
"State: 1\n",
|
||||
"[0] 2\n",
|
||||
"[!0] 5\n",
|
||||
"State: 2\n",
|
||||
"[2] 1\n",
|
||||
"State: 3\n",
|
||||
"[!2] 1\n",
|
||||
"State: 4\n",
|
||||
"[!2] 0\n",
|
||||
"State: 5\n",
|
||||
"[2] 0\n",
|
||||
"--END--\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"si.minimize_lvl = 0\n",
|
||||
"mm0 = spot.solved_game_to_mealy(game, si)\n",
|
||||
"msep0 = spot.solved_game_to_separated_mealy(game, si)\n",
|
||||
"msplit0 = spot.solved_game_to_split_mealy(game, si)\n",
|
||||
"assert(spot.is_separated_mealy(mm0)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n",
|
||||
"assert(spot.is_separated_mealy(msep0))\n",
|
||||
"assert(spot.is_split_mealy(msplit0))\n",
|
||||
"print(mm0.to_str(\"hoa\"))\n",
|
||||
"print(msep0.to_str(\"hoa\"))\n",
|
||||
"print(msplit0.to_str(\"hoa\"))\n",
|
||||
"si.minimize_lvl = 2\n",
|
||||
"mm2 = spot.solved_game_to_mealy(game, si)\n",
|
||||
"msep2 = spot.solved_game_to_separated_mealy(game, si)\n",
|
||||
"msplit2 = spot.solved_game_to_split_mealy(game, si)\n",
|
||||
"assert(spot.is_separated_mealy(mm2)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n",
|
||||
"assert(spot.is_separated_mealy(msep2))\n",
|
||||
"assert(spot.is_split_mealy(msplit2))\n",
|
||||
"print(mm2.to_str(\"hoa\"))\n",
|
||||
"print(msep2.to_str(\"hoa\"))\n",
|
||||
"print(msplit2.to_str(\"hoa\"))\n",
|
||||
"si.minimize_lvl = 3\n",
|
||||
"mm3 = spot.solved_game_to_mealy(game, si)\n",
|
||||
"msep3 = spot.solved_game_to_separated_mealy(game, si)\n",
|
||||
"msplit3 = spot.solved_game_to_split_mealy(game, si)\n",
|
||||
"assert(spot.is_split_mealy(mm3)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\n",
|
||||
"assert(spot.is_separated_mealy(msep3))\n",
|
||||
"assert(spot.is_split_mealy(msplit3))\n",
|
||||
"print(mm3.to_str(\"hoa\"))\n",
|
||||
"print(msep3.to_str(\"hoa\"))\n",
|
||||
"print(msplit3.to_str(\"hoa\"))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 4,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"mus0 = spot.unsplit_mealy(msplit0)\n",
|
||||
"mus2 = spot.unsplit_mealy(msplit2)\n",
|
||||
"mus3 = spot.unsplit_mealy(msplit3)\n",
|
||||
"mmus3 = spot.unsplit_mealy(mm3)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 5,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"assert(mm0.equivalent_to(msep0))\n",
|
||||
"assert(mm0.equivalent_to(mus0))\n",
|
||||
"assert(mm2.equivalent_to(msep2))\n",
|
||||
"assert(mm2.equivalent_to(mus2))\n",
|
||||
"assert(mmus3.equivalent_to(msep3))\n",
|
||||
"assert(mmus3.equivalent_to(mus3))"
|
||||
]
|
||||
}
|
||||
],
|
||||
"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.8.10"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue