diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 2143408b1..27e53b4d8 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1006,8 +1006,10 @@ namespace spot } twa_graph_ptr - solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi) + solved_game_to_mealy(twa_graph_ptr arena, synthesis_info& gi) { + // This currently always produces either separated or split mealy machines + // if this changes, change also the other functions accordingly assert(arena->get_named_prop("state-player") && "Need prop \"state-player\""); if (!arena) @@ -1032,9 +1034,6 @@ namespace spot else if (gi.minimize_lvl >= 3) m = minimize_mealy(m, gi.minimize_lvl - 4); - if (!do_unsplit) - m = unsplit_mealy(m); - if (gi.bv) { gi.bv->strat2aut_time += sw.stop(); @@ -1042,6 +1041,24 @@ namespace spot gi.bv->nb_strat_edges += m->num_edges(); } + assert(is_mealy(m)); + return m; + } + + twa_graph_ptr + solved_game_to_mealy(twa_graph_ptr arena) + { + synthesis_info dummy; + return solved_game_to_mealy(arena, dummy); + } + + twa_graph_ptr + solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi) + { + auto m = solved_game_to_mealy(arena, gi); + + if (m->get_named_prop("state-player")) + m = unsplit_mealy(m); assert(is_separated_mealy(m)); return m; } @@ -1053,6 +1070,27 @@ namespace spot return solved_game_to_separated_mealy(arena, dummy); } + twa_graph_ptr + solved_game_to_split_mealy(twa_graph_ptr arena, synthesis_info& gi) + { + auto m = solved_game_to_mealy(arena, gi); + + if (!m->get_named_prop("state-player")) + { + assert(is_separated_mealy(m)); + split_separated_mealy_here(m); + } + assert(is_split_mealy(m)); + return m; + } + + twa_graph_ptr + solved_game_to_split_mealy(twa_graph_ptr arena) + { + synthesis_info dummy; + return solved_game_to_split_mealy(arena, dummy); + } + } namespace spot diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 9ecd90e73..44e6ca7dc 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -158,15 +158,25 @@ namespace spot /// @} /// \ingroup synthesis - /// \brief creates a separated mealy machine from a solved game + /// \brief creates a mealy machine from a solved game \a arena /// taking into account the options given in \a gi. /// This concerns in particular whether or not the machine is to be reduced /// and how. + /// solved_game_to_mealy can return any type of mealy machine. In fact it + /// will return the type that necessitates no additional operations /// @{ SPOT_API twa_graph_ptr + solved_game_to_mealy(twa_graph_ptr arena, synthesis_info& gi); + SPOT_API twa_graph_ptr + solved_game_to_mealy(twa_graph_ptr arena); + SPOT_API twa_graph_ptr solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi); SPOT_API twa_graph_ptr solved_game_to_separated_mealy(twa_graph_ptr arena); + SPOT_API twa_graph_ptr + solved_game_to_split_mealy(twa_graph_ptr arena, synthesis_info& gi); + SPOT_API twa_graph_ptr + solved_game_to_split_mealy(twa_graph_ptr arena); /// @} /// \ingroup synthesis diff --git a/tests/Makefile.am b/tests/Makefile.am index febb2184b..60858d9c3 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb new file mode 100644 index 000000000..ee7cd9c1f --- /dev/null +++ b/tests/python/_synthesis.ipynb @@ -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 +}