diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index ec2defb4f..6d4537206 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -974,16 +974,13 @@ namespace spot
if (gi.s == algo::LAR)
{
dpa = to_parity(aut);
- // reduce_parity is called by to_parity(),
- // but with colorization turned off.
- colorize_parity_here(dpa, true);
+ // reduce_parity is called by to_parity()
}
else
{
dpa = to_parity_old(aut);
dpa = reduce_parity_here(dpa, true);
}
- change_parity_here(dpa, parity_kind_max, parity_style_odd);
if (bv)
bv->paritize_time += sw.stop();
if (vs)
@@ -995,6 +992,7 @@ namespace spot
if (bv)
sw.start();
dpa = split_2step(dpa, outs, true);
+ change_parity_here(dpa, parity_kind_max, parity_style_odd);
colorize_parity_here(dpa, true);
if (bv)
bv->split_time += sw.stop();
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 24a53556a..215143df2 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -59,11 +59,11 @@ parity 13;
1 1 1 6,3;
parity 5;
1 1 0 4,5 "INIT";
-5 4 1 1,1;
-4 5 1 0,1;
+5 2 1 1,1;
+4 3 1 0,1;
0 1 0 2,3;
-3 5 1 1;
-2 3 1 0,0;
+3 3 1 1;
+2 1 1 0,0;
EOF
: > out
@@ -230,10 +230,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 3 colors
LAR construction done in X seconds
-DPA has 4 states, 3 colors
+DPA has 4 states, 1 colors
split inputs and outputs done in X seconds
automaton has 12 states
-solving game with acceptance: parity max odd 5
+solving game with acceptance: parity max odd 3
game solved in X seconds
EOF
ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \
@@ -569,10 +569,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 2 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
EOF
ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out
@@ -646,10 +646,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 4 states and 1 colors
LAR construction done in X seconds
-DPA has 4 states, 4 colors
+DPA has 4 states, 1 colors
split inputs and outputs done in X seconds
automaton has 9 states
-solving game with acceptance: parity max odd 6
+solving game with acceptance: Streett 1
game solved in X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF
@@ -663,20 +663,20 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 2 colors
+DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
trying to create strategy directly for (a | x) -> x
direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 2 colors
+DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF
@@ -692,20 +692,20 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 2 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
trying to create strategy directly for Gy
direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 2 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF
@@ -720,10 +720,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: parity max odd 3
game solved in X seconds
EOF
ltlsynt -f '!F(a|b)' --outs=b --decompose=yes --aiger --verbose 2> out || true
@@ -737,10 +737,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: parity max odd 3
game solved in X seconds
EOF
ltlsynt -f 'G!(a -> b)' --outs=b --decompose=yes --aiger\
@@ -755,10 +755,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 4 colors
+DPA has 2 states, 1 colors
split inputs and outputs done in X seconds
automaton has 5 states
-solving game with acceptance: parity max odd 6
+solving game with acceptance: Streett 1
game solved in X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF
@@ -775,30 +775,30 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 2 colors
+DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
trying to create strategy directly for a -> c
direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 2 colors
+DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
trying to create strategy directly for a -> d
direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 2 states and 1 colors
LAR construction done in X seconds
-DPA has 2 states, 2 colors
+DPA has 2 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: Streett 1
game solved in X seconds
AIG circuit was created in X seconds and has 0 latches and 0 gates
EOF
@@ -814,10 +814,10 @@ direct strategy might exist but was not found.
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
-DPA has 1 states, 2 colors
+DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 4 states
-solving game with acceptance: parity max odd 4
+solving game with acceptance: parity max odd 3
game solved in X seconds
EOF
ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \
diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb
index 0fbad3d08..4e7374852 100644
--- a/tests/python/_mealy.ipynb
+++ b/tests/python/_mealy.ipynb
@@ -3,6 +3,7 @@
{
"cell_type": "code",
"execution_count": 1,
+ "id": "8bca10b8",
"metadata": {},
"outputs": [],
"source": [
@@ -12,6 +13,7 @@
},
{
"cell_type": "markdown",
+ "id": "c73e997a",
"metadata": {},
"source": [
"Test the Mealy printer."
@@ -20,6 +22,7 @@
{
"cell_type": "code",
"execution_count": 2,
+ "id": "f8eff7ed",
"metadata": {},
"outputs": [],
"source": [
@@ -29,6 +32,7 @@
{
"cell_type": "code",
"execution_count": 3,
+ "id": "ad3c80bc",
"metadata": {},
"outputs": [
{
@@ -49,6 +53,7 @@
{
"cell_type": "code",
"execution_count": 4,
+ "id": "50130d85",
"metadata": {},
"outputs": [
{
@@ -60,82 +65,78 @@
"\n",
"\n",
- "\n"
],
"text/plain": [
- " *' at 0x7f300c179300> >"
+ " *' at 0x7f32ec571c30> >"
]
},
"execution_count": 6,
@@ -228,6 +231,7 @@
{
"cell_type": "code",
"execution_count": 7,
+ "id": "88f2c0e0",
"metadata": {},
"outputs": [],
"source": [
@@ -237,6 +241,7 @@
{
"cell_type": "code",
"execution_count": 8,
+ "id": "e626997e",
"metadata": {},
"outputs": [
{
@@ -285,7 +290,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f300c179300> >"
+ " *' at 0x7f32ec571c30> >"
]
},
"execution_count": 8,
@@ -300,7 +305,7 @@
],
"metadata": {
"kernelspec": {
- "display_name": "Python 3",
+ "display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
@@ -314,7 +319,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
- "version": "3.8.10"
+ "version": "3.9.2"
}
},
"nbformat": 4,
diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb
index 324aab546..028ed0372 100644
--- a/tests/python/games.ipynb
+++ b/tests/python/games.ipynb
@@ -693,18 +693,14 @@
" viewBox=\"0.00 0.00 566.58 353.20\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"\n",
"\n",
- "Fin(\n",
- "❹\n",
- ") & (Inf(\n",
- "❸\n",
- ") | (Fin(\n",
- "❷\n",
- ") & (Inf(\n",
- "❶\n",
- ") | Fin(\n",
- "⓿\n",
- "))))\n",
- "[parity max odd 5]\n",
+ "Fin(\n",
+ "❷\n",
+ ") & (Inf(\n",
+ "❶\n",
+ ") | Fin(\n",
+ "⓿\n",
+ "))\n",
+ "[parity max odd 3]\n",
"\n",
"\n",
"\n",
@@ -786,7 +782,7 @@
"\n",
"\n",
"1\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -800,7 +796,7 @@
"\n",
"\n",
"1\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -830,7 +826,7 @@
"\n",
"\n",
"1\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -858,7 +854,7 @@
"\n",
"\n",
"1\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -886,7 +882,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -894,7 +890,7 @@
"\n",
"\n",
"b\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -902,7 +898,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -910,7 +906,7 @@
"\n",
"\n",
"b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -918,7 +914,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -926,13 +922,13 @@
"\n",
"\n",
"b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n"
],
"text/plain": [
- " *' at 0x7f5c143ec630> >"
+ " *' at 0x7f80642eee70> >"
]
},
"execution_count": 8,
@@ -967,8 +963,8 @@
"States: 12\n",
"Start: 4\n",
"AP: 2 \"b\" \"a\"\n",
- "acc-name: parity max odd 5\n",
- "Acceptance: 5 Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))\n",
+ "acc-name: parity max odd 3\n",
+ "Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))\n",
"properties: trans-labels explicit-labels trans-acc colored complete\n",
"properties: deterministic\n",
"spot-state-player: 0 0 0 0 0 1 1 1 1 1 1 1\n",
@@ -988,22 +984,22 @@
"[!1] 10 {1}\n",
"[1] 11 {1}\n",
"State: 5\n",
- "[t] 0 {3}\n",
+ "[t] 0 {1}\n",
"State: 6\n",
- "[t] 1 {4}\n",
+ "[t] 1 {2}\n",
"State: 7\n",
- "[t] 0 {4}\n",
+ "[t] 0 {2}\n",
"State: 8\n",
- "[t] 2 {3}\n",
+ "[t] 2 {1}\n",
"State: 9\n",
- "[!0] 2 {3}\n",
- "[0] 3 {4}\n",
+ "[!0] 2 {1}\n",
+ "[0] 3 {2}\n",
"State: 10\n",
- "[!0] 0 {3}\n",
- "[0] 3 {3}\n",
+ "[!0] 0 {1}\n",
+ "[0] 3 {1}\n",
"State: 11\n",
- "[!0] 1 {3}\n",
- "[0] 3 {3}\n",
+ "[!0] 1 {1}\n",
+ "[0] 3 {1}\n",
"--END--\n"
]
}
@@ -1057,18 +1053,14 @@
" viewBox=\"0.00 0.00 566.58 353.20\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"\n",
"\n",
- "Fin(\n",
- "❹\n",
- ") & (Inf(\n",
- "❸\n",
- ") | (Fin(\n",
- "❷\n",
- ") & (Inf(\n",
- "❶\n",
- ") | Fin(\n",
- "⓿\n",
- "))))\n",
- "[parity max odd 5]\n",
+ "Fin(\n",
+ "❷\n",
+ ") & (Inf(\n",
+ "❶\n",
+ ") | Fin(\n",
+ "⓿\n",
+ "))\n",
+ "[parity max odd 3]\n",
"\n",
"\n",
"\n",
@@ -1150,7 +1142,7 @@
"\n",
"\n",
"1\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1164,7 +1156,7 @@
"\n",
"\n",
"1\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -1194,7 +1186,7 @@
"\n",
"\n",
"1\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -1222,7 +1214,7 @@
"\n",
"\n",
"1\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1250,7 +1242,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1258,7 +1250,7 @@
"\n",
"\n",
"b\n",
- "❹\n",
+ "❷\n",
"\n",
"\n",
"\n",
@@ -1266,7 +1258,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1274,7 +1266,7 @@
"\n",
"\n",
"b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1282,7 +1274,7 @@
"\n",
"\n",
"!b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n",
@@ -1290,13 +1282,13 @@
"\n",
"\n",
"b\n",
- "❸\n",
+ "❶\n",
"\n",
"\n",
"\n"
],
"text/plain": [
- " *' at 0x7f5c143fdf30> >"
+ " *' at 0x7f806443b1b0> >"
]
},
"execution_count": 11,
@@ -1307,11 +1299,18 @@
"source": [
"spot.highlight_strategy(game)"
]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
}
],
"metadata": {
"kernelspec": {
- "display_name": "Python 3",
+ "display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
@@ -1325,7 +1324,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
- "version": "3.7.3"
+ "version": "3.9.2"
}
},
"nbformat": 4,
diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb
index e290f02b5..8c706c481 100644
--- a/tests/python/synthesis.ipynb
+++ b/tests/python/synthesis.ipynb
@@ -3,6 +3,7 @@
{
"cell_type": "code",
"execution_count": 1,
+ "id": "1b9b5964",
"metadata": {},
"outputs": [],
"source": [
@@ -13,6 +14,7 @@
},
{
"cell_type": "markdown",
+ "id": "b465c6ba",
"metadata": {},
"source": [
"This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n",
@@ -37,6 +39,7 @@
{
"cell_type": "code",
"execution_count": 2,
+ "id": "8576bdad",
"metadata": {},
"outputs": [
{
@@ -53,649 +56,647 @@
"\n",
"\n",
- "\n",
"\n",
- "