From 86de4d40529b61cd93bfcbe53ade5fa774c46450 Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber-Caissier Date: Fri, 18 Mar 2022 01:02:45 +0100 Subject: [PATCH] Introduce mealy_prod Product between mealy machines with propagation of synthesis outputs and additional assertions. Currently it only supports input complete machines * spot/twaalgos/mealy_machine.cc, spot/twaalgos/mealy_machine.hh: Here * bin/ltlsynt.cc: Use * tests/python/except.py, tests/python/synthesis.ipynb: Test --- bin/ltlsynt.cc | 3 +- spot/twaalgos/mealy_machine.cc | 54 ++++++++ spot/twaalgos/mealy_machine.hh | 10 ++ tests/python/except.py | 17 +++ tests/python/synthesis.ipynb | 220 ++++++++++++++++++++++++++++++--- 5 files changed, 288 insertions(+), 16 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 73ec6b2b1..4d118dd46 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -545,7 +545,8 @@ namespace && "ltlsynt: Cannot handle TGBA as strategy."); tot_strat = mealy_machines.front().mealy_like; for (size_t i = 1; i < mealy_machines.size(); ++i) - tot_strat = spot::product(tot_strat, mealy_machines[i].mealy_like); + tot_strat = spot::mealy_product(tot_strat, + mealy_machines[i].mealy_like); printer.print(tot_strat, timer_printer_dummy); } diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 99b762f16..36c162402 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -34,6 +34,7 @@ #include #include #include +#include #include #include @@ -55,6 +56,7 @@ namespace { + using namespace spot; bool is_deterministic_(const std::vector& ins) { const unsigned n_ins = ins.size(); @@ -64,6 +66,24 @@ namespace return false; return true; } + + bool is_complete_(const const_twa_graph_ptr& m, + const bdd& outs) + { + auto* sp = m->get_named_prop("state-player"); + const auto N = m->num_states(); + for (auto s = 0u; s < N; ++s) + { + if (sp && sp->at(s)) + continue; // No need tpo check player states + bdd all_cond = bddfalse; + for (const auto& e : m->out(s)) + all_cond |= bdd_exist(e.cond, outs); + if (all_cond != bddtrue) + return false; + } + return true; + } } @@ -3843,4 +3863,38 @@ namespace spot return true; } + twa_graph_ptr + mealy_product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) + { + bdd outs[] = {get_synthesis_outputs(left), + get_synthesis_outputs(right)}; + +#ifndef NDEBUG + for (const auto& [m, n, o] : {std::tuple{left, "left", outs[0]}, + {right, "right", outs[1]}}) + { + if (!is_mealy(m)) + throw std::runtime_error(std::string("mealy_prod(): ") + n + + " is not a mealy machine"); + if (!is_complete_(m, o)) + throw std::runtime_error(std::string("mealy_prod(): ") + n + + " is not input complete"); + } +#endif + + auto p = product(left, right); + bdd pouts = outs[0] & outs[1]; + set_synthesis_outputs(p, pouts); + +#ifndef NDEBUG + if (!is_mealy(p)) + throw std::runtime_error("mealy_prod(): Prooduct is not mealy"); + if (!is_complete_(p, pouts)) + throw std::runtime_error("mealy_prod(): Prooduct is not input complete. " + "Incompatible machines?"); +#endif + + return p; + } } diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh index 139f7cce2..77c3968ab 100644 --- a/spot/twaalgos/mealy_machine.hh +++ b/spot/twaalgos/mealy_machine.hh @@ -128,4 +128,14 @@ namespace spot is_split_mealy_specialization(const_twa_graph_ptr left, const_twa_graph_ptr right, bool verbose = false); + + /// \brief Product between two mealy machines \a left and \a right. + /// \pre The machines have to be both either split or unsplit, + /// input complete and compatible. All of this is check by assertion + /// \result The mealy machine representing the shared behaviour. + /// The resulting machine has the same class (mealy/separated/split) + /// as the input machines + SPOT_API twa_graph_ptr + mealy_product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right); } \ No newline at end of file diff --git a/tests/python/except.py b/tests/python/except.py index 8674721c9..3aeee7a3e 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -331,3 +331,20 @@ except RuntimeError as e: tc.assertIn("already registered", se) else: report_missing_exception() + + +si = spot.synthesis_info() +si.s = spot.synthesis_info.algo_LAR +g1 = spot.ltl_to_game("G((i0 xor i1) <-> o0)", ["o0"], si) +g2 = spot.ltl_to_game("G((i0 xor i1) <-> (!o0 & !o1))", ["o0", "o1"], si) +spot.solve_game(g1) +spot.solve_game(g2) +strat1 = spot.solved_game_to_separated_mealy(g1) +strat2 = spot.solved_game_to_separated_mealy(g2) +try: + stratcomp = spot.mealy_product(strat1, strat2) +except RuntimeError as e: + se = str(e) + tc.assertIn("Incompatible", se) +else: + report_missing_exception() \ No newline at end of file diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 8c706c481..7ec181ebe 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -696,7 +696,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc5ec2bf930> >" + " *' at 0x7f05083f22a0> >" ] }, "metadata": {}, @@ -2714,7 +2714,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3027,7 +3027,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc5dc8463f0> >" + " *' at 0x7f05082c7a20> >" ] }, "metadata": {}, @@ -3102,7 +3102,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc5ec2bf990> >" + " *' at 0x7f05083f2300> >" ] }, "metadata": {}, @@ -3179,7 +3179,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3306,7 +3306,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3327,8 +3327,13 @@ "It can happen that the complete specification of the controller can be separated into sub-specifications with DISJOINT output propositions, see Finkbeiner et al. Specification Decomposition for Reactive Synthesis.\n", "This results in multiple Mealy machines which have to be converted into one single AIG circuit.\n", "\n", - "This can be done using the function `mealy_machines_to_aig()`, which takes a vector of separated Mealy machines as argument.\n", - "In order for this to work, all Mealy machines need to share the same `bdd_dict`. This can be ensured by passing a common options strucuture." + "This can be done in two ways:\n", + "\n", + "1. Using the function `mealy_machines_to_aig()`, which takes a vector of separated mealy machines as argument.\n", + "2. Combine the mealy machines into one before passing it to `mealy_machine_to aig(). This currently only supports input complete machines of the same type (mealy/separated mealy/split mealy)\n", + "\n", + "Note that the method version is usually preferable as it is faster.\n", + "Also note that in order for this to work, all mealy machines need to share the same `bdd_dict`. This can be ensured by passing a common options strucuture." ] }, { @@ -3623,7 +3628,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "Circuit implementing both machines:\n" + "Circuit implementing both machines from a vector of machines:\n" ] }, { @@ -3733,7 +3738,185 @@ "\n" ], "text/plain": [ - " >" + " >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Combining the two machines into one.\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0 & o1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0 & !o1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f05082c7ba0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "8->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o0\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "10->o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o1\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "10->o1:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "i0\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" ] }, "metadata": {}, @@ -3753,9 +3936,16 @@ "strat2 = spot.solved_game_to_separated_mealy(g2)\n", "print(\"Reduced strategies:\")\n", "display_inline(strat1, strat2)\n", - "print(\"Circuit implementing both machines:\")\n", + "#Method 1\n", + "print(\"Circuit implementing both machines from a vector of machines:\")\n", "aig = spot.mealy_machines_to_aig([strat1, strat2], \"isop\")\n", - "display(aig)" + "display(aig)\n", + "#Method 2\n", + "strat_comb = spot.mealy_product(strat1, strat2)\n", + "print(\"Combining the two machines into one.\")\n", + "display(strat_comb)\n", + "aig_comb = spot.mealy_machine_to_aig(strat_comb, \"isop\")\n", + "display(aig_comb)" ] }, { @@ -3906,7 +4096,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4030,7 +4220,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc5dc846690> >" + " *' at 0x7f05082c7690> >" ] }, "execution_count": 16, @@ -4419,7 +4609,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.8.10" } }, "nbformat": 4,