diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index f3eb97417..72005e475 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1627,23 +1627,30 @@ namespace spot } else if (like_names) { - std::vector r_pairs; - bool r_like = is_rabin_like(r_pairs); - unsigned rsz = r_pairs.size(); - std::vector s_pairs; - bool s_like = is_streett_like(s_pairs); - unsigned ssz = s_pairs.size(); - if (r_like && (!s_like || (rsz <= ssz))) + if (!uses_fin_acceptance()) { - os << "Rabin-like"; - if (!no_main_param) - os << ' ' << rsz; + os << "Fin-less" << sets(); } - else if (s_like && (!r_like || (ssz < rsz))) + else { - os << "Streett-like"; - if (!no_main_param) - os << ' ' << ssz; + std::vector r_pairs; + bool r_like = is_rabin_like(r_pairs); + unsigned rsz = r_pairs.size(); + std::vector s_pairs; + bool s_like = is_streett_like(s_pairs); + unsigned ssz = s_pairs.size(); + if (r_like && (!s_like || (rsz <= ssz))) + { + os << "Rabin-like"; + if (!no_main_param) + os << ' ' << rsz; + } + else if (s_like && (!r_like || (ssz < rsz))) + { + os << "Streett-like"; + if (!no_main_param) + os << ' ' << ssz; + } } } } diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index c35c748b1..89272b53a 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.3" }, "name": "" }, @@ -177,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1786450> >" + " *' at 0x7fb1043b73f0> >" ] } ], @@ -570,7 +570,7 @@ "\n" ], "text": [ - " *' at 0x7f23c17168d0> >" + " *' at 0x7fb1042bc900> >" ] } ], @@ -640,7 +640,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716330> >" + " *' at 0x7fb1042ce7b0> >" ] } ], @@ -716,7 +716,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716180> >" + " *' at 0x7fb1043b7390> >" ] } ], @@ -1176,7 +1176,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716b10> >" + " *' at 0x7fb1042ce870> >" ] } ], @@ -1277,7 +1277,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716990> >" + " *' at 0x7fb1042bc660> >" ] } ], @@ -1395,7 +1395,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716960> >" + " *' at 0x7fb1042ce6c0> >" ] } ], @@ -1494,7 +1494,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716b40> >" + " *' at 0x7fb1043dd600> >" ] } ], @@ -1964,7 +1964,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716ba0> >" + " *' at 0x7fb1042ce600> >" ] } ], @@ -2168,19 +2168,20 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ") | Inf(\n", - "\u2776\n", - ") | (Inf(\n", - "\u2777\n", - ")&Inf(\n", - "\u2778\n", - "))\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ") | (Inf(\n", + "\u2777\n", + ")&Inf(\n", + "\u2778\n", + "))\n", + "[Fin-less 4]\n", "\n", "\n", "0\n", @@ -2580,7 +2581,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716bd0> >" + " *' at 0x7fb1042bc8d0> >" ] } ], @@ -2736,7 +2737,7 @@ "\n" ], "text": [ - " *' at 0x7f23c17164e0> >" + " *' at 0x7fb1042ce780> >" ] } ], @@ -2806,7 +2807,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716900> >" + " *' at 0x7fb1042ce8a0> >" ] } ], @@ -3237,7 +3238,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716bd0> >" + " *' at 0x7fb1042ce810> >" ] }, { @@ -3406,7 +3407,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716a20> >" + " *' at 0x7fb1042ce7e0> >" ] } ], @@ -3495,7 +3496,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716a20> >" + " *' at 0x7fb1042ce7e0> >" ] } ], @@ -3584,7 +3585,7 @@ "\n" ], "text": [ - " *' at 0x7f23c1716a20> >" + " *' at 0x7fb1042ce7e0> >" ] } ], diff --git a/tests/python/randaut.ipynb b/tests/python/randaut.ipynb index 9e1ac5953..128aa0f96 100644 --- a/tests/python/randaut.ipynb +++ b/tests/python/randaut.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.3" }, "name": "" }, @@ -35,7 +35,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 2 + "prompt_number": 1 }, { "cell_type": "markdown", @@ -584,17 +584,18 @@ "!p0 & !p1\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u2776\n", - ") | (Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2777\n", - "))\n", + "\n", + "Inf(\n", + "\u2776\n", + ") | (Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2777\n", + "))\n", + "[Fin-less 3]\n", "\n", "\n", "0\n", @@ -2277,13 +2278,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 3, + "prompt_number": 2, "text": [ "" ] } ], - "prompt_number": 3 + "prompt_number": 2 } ], "metadata": {} diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index a86cf9d79..b1373a9db 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -354,7 +354,7 @@ "\n" ], "text": [ - " *' at 0x7f71841135d0> >" + " *' at 0x7f399007b4b0> >" ] }, { @@ -626,7 +626,7 @@ "\n" ], "text": [ - " *' at 0x7f71840b9b40> >" + " *' at 0x7f399007b660> >" ] } ], @@ -816,7 +816,7 @@ "\n" ], "text": [ - " *' at 0x7f71840b9b40> >" + " *' at 0x7f399007b660> >" ] } ], @@ -979,7 +979,7 @@ "\n" ], "text": [ - " *' at 0x7f7184113480> >" + " *' at 0x7f3981fdfab0> >" ] }, { @@ -1066,7 +1066,7 @@ "\n" ], "text": [ - " *' at 0x7f71841135a0> >" + " *' at 0x7f3981fdfa20> >" ] } ], @@ -1105,18 +1105,19 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")) | Inf(\n", - "\u2777\n", - ")\n", + "\n", + "(Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")) | Inf(\n", + "\u2777\n", + ")\n", + "[Fin-less 3]\n", "\n", "\n", "5\n", @@ -1259,7 +1260,7 @@ "\n" ], "text": [ - " *' at 0x7f71840b9a80> >" + " *' at 0x7f3981fdfba0> >" ] } ], @@ -1373,7 +1374,7 @@ "\n" ], "text": [ - " *' at 0x7f7184137690> >" + " *' at 0x7f3981fdf390> >" ] } ], @@ -1496,7 +1497,7 @@ "\n" ], "text": [ - " *' at 0x7f71840b9b70> >" + " *' at 0x7f3981fdfa80> >" ] } ],