From bdd20bd1a1b4eaae113a231b0b50ab4c6a184796 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Oct 2021 22:51:10 +0200 Subject: [PATCH] rename game_info to synthesis_info; move it with the synthesis code * spot/twaalgos/game.cc, spot/twaalgos/game.hh (game_info): Move... * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh (synthesis_info): ... here, because this structure contains only synthesis stuff. Also rename "solver" to "algo" to match the ltlsynt option. (solve_game): Move the two argument version of this function here, since that's the only game-related generic function that use synthesis_info. * bin/ltlsynt.cc, tests/core/ltlsynt.test, tests/python/games.ipynb, tests/python/synthesis.py, NEWS: Adjust all uses and mentions. --- NEWS | 8 +-- bin/ltlsynt.cc | 30 +++++------ spot/twaalgos/game.cc | 73 +++---------------------- spot/twaalgos/game.hh | 77 --------------------------- spot/twaalgos/synthesis.cc | 106 +++++++++++++++++++++++++++++-------- spot/twaalgos/synthesis.hh | 78 +++++++++++++++++++++++++-- tests/core/ltlsynt.test | 2 +- tests/python/games.ipynb | 64 +++++++++++----------- tests/python/synthesis.py | 4 +- 9 files changed, 217 insertions(+), 225 deletions(-) diff --git a/NEWS b/NEWS index 022609fa9..2cf1a36aa 100644 --- a/NEWS +++ b/NEWS @@ -57,10 +57,10 @@ New in spot 2.9.8.dev (not yet released) - autfilt learned a --kill-states=NUM[,NUM...] option. Library: - - Spot now provides convenient function to create and solve game. - The functions are located in twaalgos/game.hh and - twaalgos/synthesis.hh. Moreover a new structure holding - all the necessary options called game_info is now available. + - Spot now provides convenient function to create and solve games. + The functions are located in twaalgos/game.hh. Additional + functions related to the application to reactive synthesis are + in twaalgos/synthesis.hh. - A new class called aig is introduced to represent and-inverter-graphs, which is useful for synthesis. diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 29dd5ce0c..a1eee92d8 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -145,9 +145,9 @@ static bool opt_real = false; static bool opt_do_verify = false; static const char* opt_print_aiger = nullptr; -static spot::game_info* gi; +static spot::synthesis_info* gi; -static char const *const solver_names[] = +static char const *const algo_names[] = { "ds", "sd", @@ -156,7 +156,7 @@ static char const *const solver_names[] = "lar.old" }; -static char const *const solver_args[] = +static char const *const algo_args[] = { "detsplit", "ds", "splitdet", "sd", @@ -165,15 +165,15 @@ static char const *const solver_args[] = "lar.old", nullptr }; -static spot::game_info::solver const solver_types[] = +static spot::synthesis_info::algo const algo_types[] = { - spot::game_info::solver::DET_SPLIT, spot::game_info::solver::DET_SPLIT, - spot::game_info::solver::SPLIT_DET, spot::game_info::solver::SPLIT_DET, - spot::game_info::solver::DPA_SPLIT, spot::game_info::solver::DPA_SPLIT, - spot::game_info::solver::LAR, - spot::game_info::solver::LAR_OLD, + spot::synthesis_info::algo::DET_SPLIT, spot::synthesis_info::algo::DET_SPLIT, + spot::synthesis_info::algo::SPLIT_DET, spot::synthesis_info::algo::SPLIT_DET, + spot::synthesis_info::algo::DPA_SPLIT, spot::synthesis_info::algo::DPA_SPLIT, + spot::synthesis_info::algo::LAR, + spot::synthesis_info::algo::LAR_OLD, }; -ARGMATCH_VERIFY(solver_args, solver_types); +ARGMATCH_VERIFY(algo_args, algo_types); static const char* const decompose_args[] = { @@ -256,7 +256,7 @@ namespace std::ostringstream os; os << f; spot::escape_rfc4180(out << '"', os.str()); - out << "\",\"" << solver_names[(int) gi->s] + out << "\",\"" << algo_names[(int) gi->s] << "\"," << bv->total_time << ',' << bv->trans_time << ',' << bv->split_time @@ -601,12 +601,12 @@ parse_opt(int key, char *arg, struct argp_state *) switch (key) { case OPT_ALGO: - gi->s = XARGMATCH("--algo", arg, solver_args, solver_types); + gi->s = XARGMATCH("--algo", arg, algo_args, algo_types); break; case OPT_CSV: opt_csv = arg ? arg : "-"; if (not gi->bv) - gi->bv = spot::game_info::bench_var(); + gi->bv = spot::synthesis_info::bench_var(); break; case OPT_DECOMPOSE: opt_decompose_ltl = XARGMATCH("--decompose", arg, @@ -655,7 +655,7 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_VERBOSE: gi->verbose_stream = &std::cerr; if (not gi->bv) - gi->bv = spot::game_info::bench_var(); + gi->bv = spot::synthesis_info::bench_var(); break; case OPT_VERIFY: opt_do_verify = true; @@ -678,7 +678,7 @@ main(int argc, char **argv) return protected_main(argv, [&] { // Create gi_ as a local variable, so make sure it is destroyed // before all global variables. - spot::game_info gi_; + spot::synthesis_info gi_; gi = &gi_; //gi_.opt.set("simul", 0); // no simulation, except... //gi_.opt.set("dpa-simul", 1); // ... after determinization diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 545c5d89b..cfb839bcb 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2017-2018, 2020-2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -768,80 +768,21 @@ namespace spot } // anonymous - std::ostream& operator<<(std::ostream& os, game_info::solver s) - { - using solver = game_info::solver; - switch (s) - { - case (solver::DET_SPLIT): - os << "ds"; - break; - case (solver::SPLIT_DET): - os << "sd"; - break; - case (solver::DPA_SPLIT): - os << "ps"; - break; - case (solver::LAR): - os << "lar"; - break; - case (solver::LAR_OLD): - os << "lar.old"; - break; - } - return os; -} - - std::ostream& - operator<<(std::ostream& os, const game_info& gi) - { - os << "force sbacc: " << gi.force_sbacc << '\n' - << "solver: " << gi.s << '\n' - << "minimization-lvl: " << gi.minimize_lvl << '\n' - << (gi.verbose_stream ? "Is verbose\n" : "Is not verbose\n") - << "the bdd_dict used is " << gi.dict.get(); - return os; - } - bool solve_parity_game(const twa_graph_ptr& arena) { parity_game pg; return pg.solve(arena); } - bool solve_game(twa_graph_ptr arena, game_info& gi) + bool solve_game(twa_graph_ptr arena) { - stopwatch sw; - if (gi.bv) - sw.start(); bool dummy1, dummy2; - bool ret; - - if (arena->acc().is_parity(dummy1, dummy2, true)) - { - if (gi.verbose_stream) - *(gi.verbose_stream) << "Identified as parity game.\n"; - ret = solve_parity_game(arena); - } - else - throw std::runtime_error("No solver available for this arena due to its" - "acceptance condition."); - if (gi.bv) - gi.bv->solve_time += sw.stop(); - if (gi.verbose_stream) - *(gi.verbose_stream) << "game solved in " - << gi.bv->solve_time << " seconds\n"; - return ret; + if (!arena->acc().is_parity(dummy1, dummy2, true)) + throw std::runtime_error + ("solve_game(): unsupported acceptance condition."); + return solve_parity_game(arena); } - bool - solve_game(twa_graph_ptr arena) - { - game_info dummy1; - return solve_game(arena, dummy1); - } - - void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) { auto owner = ensure_parity_game(arena, "pg_print"); diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index add0325a6..e65b48f18 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -95,83 +95,6 @@ namespace spot SPOT_API bool solve_safety_game(twa_graph_ptr game); - /// \ingroup games - /// \brief Benchmarking and options structure for games and synthesis - /// - /// \note This structure is designed to interface with the algorithms - /// found in spot/twaalgos/synthesis.hh and spot/twaalgos/game.hh - struct SPOT_API game_info - { - enum class solver - { - DET_SPLIT=0, - SPLIT_DET, - DPA_SPLIT, - LAR, - LAR_OLD, - }; - - struct bench_var - { - double total_time = 0.0; - double trans_time = 0.0; - double split_time = 0.0; - double paritize_time = 0.0; - double solve_time = 0.0; - double strat2aut_time = 0.0; - double aig_time = 0.0; - unsigned nb_states_arena = 0; - unsigned nb_states_arena_env = 0; - unsigned nb_strat_states = 0; - unsigned nb_strat_edges = 0; - unsigned nb_latches = 0; - unsigned nb_gates = 0; - bool realizable = false; - }; - - game_info() - : force_sbacc{false}, - s{solver::LAR}, - minimize_lvl{2}, - bv{}, - verbose_stream{nullptr}, - dict(make_bdd_dict()) - { - } - - bool force_sbacc; - solver s; - int minimize_lvl; - std::optional bv; - std::ostream* verbose_stream; - option_map opt; - bdd_dict_ptr dict; - }; - - /// \ingroup games - /// \brief Stream solvers - SPOT_API std::ostream& - operator<<(std::ostream& os, game_info::solver s); - - /// \ingroup games - /// \brief Stream benchmarks and options - SPOT_API std::ostream & - operator<<(std::ostream &os, const game_info &gi); - - /// \ingroup games - /// \brief Generic interface for game solving - /// - /// Calls the most suitable solver, depending on the type of game/ - /// acceptance condition - /// - /// \param arena The game arena - /// \param gi struct for options and benchmarking - /// \return Whether the initial state is won by player or not - /// \pre Relies on the named properties "state-player" - /// \post The named properties "strategy" and "state-winner" are set - SPOT_API bool - solve_game(twa_graph_ptr arena, game_info& gi); - /// \ingroup games /// \brief Generic interface for game solving /// diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index e655edab5..57d6d541c 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2020 Laboratoire de Recherche et +// Copyright (C) 2020, 2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -771,12 +771,49 @@ namespace spot return strat_split; } + std::ostream& operator<<(std::ostream& os, synthesis_info::algo s) + { + using algo = synthesis_info::algo; + const char* name = nullptr; + switch (s) + { + case (algo::DET_SPLIT): + name = "ds"; + break; + case (algo::SPLIT_DET): + name = "sd"; + break; + case (algo::DPA_SPLIT): + name = "ps"; + break; + case (algo::LAR): + name = "lar"; + break; + case (algo::LAR_OLD): + name = "lar.old"; + break; + } + return os << name; +} + + std::ostream& + operator<<(std::ostream& os, const synthesis_info& gi) + { + os << "force sbacc: " << gi.force_sbacc << '\n' + << "solver: " << gi.s << '\n' + << "minimization-lvl: " << gi.minimize_lvl << '\n' + << (gi.verbose_stream ? "Is verbose\n" : "Is not verbose\n") + << "the bdd_dict used is " << gi.dict.get(); + return os; + } + + namespace // Anonymous create_game { static translator - create_translator(game_info& gi) + create_translator(synthesis_info& gi) { - using solver = game_info::solver; + using algo = synthesis_info::algo; option_map& extra_options = gi.opt; auto sol = gi.s; @@ -793,19 +830,19 @@ namespace spot translator trans(dict, &extra_options); switch (sol) { - case solver::LAR: + case algo::LAR: SPOT_FALLTHROUGH; - case solver::LAR_OLD: + case algo::LAR_OLD: trans.set_type(postprocessor::Generic); trans.set_pref(postprocessor::Deterministic); break; - case solver::DPA_SPLIT: + case algo::DPA_SPLIT: trans.set_type(postprocessor::ParityMaxOdd); trans.set_pref(postprocessor::Deterministic | postprocessor::Colored); break; - case solver::DET_SPLIT: + case algo::DET_SPLIT: SPOT_FALLTHROUGH; - case solver::SPLIT_DET: + case algo::SPLIT_DET: break; } return trans; @@ -838,9 +875,9 @@ namespace spot twa_graph_ptr create_game(const formula& f, const std::vector& all_outs, - game_info& gi) + synthesis_info& gi) { - using solver = game_info::solver; + using algo = synthesis_info::algo; [](std::vector sv, std::string msg) { @@ -901,7 +938,7 @@ namespace spot switch (gi.s) { - case solver::DET_SPLIT: + case algo::DET_SPLIT: { if (bv) sw.start(); @@ -930,7 +967,7 @@ namespace spot << tmp->num_states() << " states\n"; break; } - case solver::DPA_SPLIT: + case algo::DPA_SPLIT: { if (bv) sw.start(); @@ -953,7 +990,7 @@ namespace spot << dpa->num_states() << " states\n"; break; } - case solver::SPLIT_DET: + case algo::SPLIT_DET: { sw.start(); auto split = split_2step(aut, outs, true); @@ -983,13 +1020,13 @@ namespace spot alternate_players(dpa); break; } - case solver::LAR: + case algo::LAR: SPOT_FALLTHROUGH; - case solver::LAR_OLD: + case algo::LAR_OLD: { if (bv) sw.start(); - if (gi.s == solver::LAR) + if (gi.s == algo::LAR) { dpa = to_parity(aut); // reduce_parity is called by to_parity(), @@ -1034,7 +1071,7 @@ namespace spot create_game(const formula& f, const std::vector& all_outs) { - game_info dummy; + synthesis_info dummy; return create_game(f, all_outs, dummy); } @@ -1048,7 +1085,7 @@ namespace spot twa_graph_ptr create_game(const std::string& f, const std::vector& all_outs, - game_info& gi) + synthesis_info& gi) { return create_game(parse_formula(f), all_outs, gi); } @@ -1119,7 +1156,7 @@ namespace spot } twa_graph_ptr - create_strategy(twa_graph_ptr arena, game_info& gi) + create_strategy(twa_graph_ptr arena, synthesis_info& gi) { if (!arena) throw std::runtime_error("Arena can not be null"); @@ -1158,7 +1195,7 @@ namespace spot twa_graph_ptr create_strategy(twa_graph_ptr arena) { - game_info dummy; + synthesis_info dummy; return create_strategy(arena, dummy); } @@ -1210,7 +1247,7 @@ namespace spot strategy_like_t try_create_direct_strategy(formula f, const std::vector& output_aps, - game_info &gi) + synthesis_info &gi) { formula_2_inout_props form2props(output_aps); auto vs = gi.verbose_stream; @@ -1303,7 +1340,7 @@ namespace spot bool is_ok = ((is_gf_bool_right && left.is_syntactic_recurrence()) || (is_fg_bool_right && left.is_syntactic_guarantee())); - // TODO: game_info not updated + // TODO: synthesis_info not updated // TODO: Verbose auto& bv = gi.bv; stopwatch sw; @@ -1820,4 +1857,29 @@ namespace spot return split_independant_formulas(parse_formula(f), outs); } + bool + solve_game(twa_graph_ptr arena, synthesis_info& gi) + { + stopwatch sw; + if (gi.bv) + sw.start(); + if (gi.verbose_stream) + { + *(gi.verbose_stream) << "solving game with acceptance: "; + std::string name = arena->acc().name(); + if (!name.empty()) + *(gi.verbose_stream) << name; + else + *(gi.verbose_stream) << arena->get_acceptance(); + *(gi.verbose_stream) << '\n'; + } + bool res = solve_game(arena); + if (gi.bv) + gi.bv->solve_time += sw.stop(); + if (gi.verbose_stream) + *(gi.verbose_stream) << "game solved in " + << gi.bv->solve_time << " seconds\n"; + return res; + } + } // spot diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index a540cfc11..f42d7370e 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -85,6 +85,66 @@ namespace spot SPOT_API twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut); + /// \ingroup synthesis + /// \brief Benchmarking data and options for synthesis + struct SPOT_API synthesis_info + { + enum class algo + { + DET_SPLIT=0, + SPLIT_DET, + DPA_SPLIT, + LAR, + LAR_OLD, + }; + + struct bench_var + { + double total_time = 0.0; + double trans_time = 0.0; + double split_time = 0.0; + double paritize_time = 0.0; + double solve_time = 0.0; + double strat2aut_time = 0.0; + double aig_time = 0.0; + unsigned nb_states_arena = 0; + unsigned nb_states_arena_env = 0; + unsigned nb_strat_states = 0; + unsigned nb_strat_edges = 0; + unsigned nb_latches = 0; + unsigned nb_gates = 0; + bool realizable = false; + }; + + synthesis_info() + : force_sbacc{false}, + s{algo::LAR}, + minimize_lvl{2}, + bv{}, + verbose_stream{nullptr}, + dict(make_bdd_dict()) + { + } + + bool force_sbacc; + algo s; + int minimize_lvl; + std::optional bv; + std::ostream* verbose_stream; + option_map opt; + bdd_dict_ptr dict; + }; + + /// \ingroup synthesis + /// \brief Stream algo + SPOT_API std::ostream& + operator<<(std::ostream& os, synthesis_info::algo s); + + /// \ingroup synthesis + /// \brief Stream benchmarks and options + SPOT_API std::ostream & + operator<<(std::ostream &os, const synthesis_info &gi); + /// \ingroup synthesis /// \brief Creates a game from a specification and a set of @@ -92,13 +152,13 @@ namespace spot /// /// \param f The specification given as LTL/PSL formula /// \param all_outs The names of all output propositions - /// \param gi game_info structure + /// \param gi synthesis_info structure /// \note All propositions in the formula that do not appear in all_outs /// arer treated as input variables. SPOT_API twa_graph_ptr create_game(const formula& f, const std::vector& all_outs, - game_info& gi); + synthesis_info& gi); /// \ingroup synthesis /// \brief create_game called with default options @@ -111,7 +171,7 @@ namespace spot SPOT_API twa_graph_ptr create_game(const std::string& f, const std::vector& all_outs, - game_info& gi); + synthesis_info& gi); /// \ingroup synthesis /// \brief create_game called with default options @@ -159,7 +219,7 @@ namespace spot /// options given in \a gi /// @{ SPOT_API twa_graph_ptr - create_strategy(twa_graph_ptr arena, game_info& gi); + create_strategy(twa_graph_ptr arena, synthesis_info& gi); SPOT_API twa_graph_ptr create_strategy(twa_graph_ptr arena); /// @} @@ -215,6 +275,14 @@ namespace spot SPOT_API strategy_like_t try_create_direct_strategy(formula f, const std::vector& output_aps, - game_info& gi); + synthesis_info& gi); + + /// \ingroup synthesis + /// \brief Solve a game, and update synthesis_info + /// + /// This is just a wrapper around the solve_game() function with a + /// single argument. This one measure the runtime and update \a gi. + SPOT_API bool + solve_game(twa_graph_ptr arena, synthesis_info& gi); } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 37c5f46e0..f27b7280c 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -233,7 +233,7 @@ LAR construction done in X seconds DPA has 4 states, 3 colors split inputs and outputs done in X seconds automaton has 12 states -Identified as parity game. +solving game with acceptance: parity max odd 5 game solved in X seconds EOF ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \ diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 299a5e06d..571184ae7 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -676,7 +676,7 @@ "- Solving the game\n", "- Obtaining the strategy\n", "\n", - "Each of these steps is parametrized by the same options structure called game_info." + "Each of these steps is parametrized by the same option structure called `synthesis_info`." ] }, { @@ -688,8 +688,8 @@ "name": "stdout", "output_type": "stream", "text": [ - "game has 29 states, and 55 edges.\n", - "output propositions are ('o0',)\n" + "game has 29 states and 55 edges\n", + "output propositions are: o0\n" ] }, { @@ -1340,7 +1340,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc16bd50> >" + " *' at 0x7f78f67a4450> >" ] }, "metadata": {}, @@ -1349,13 +1349,12 @@ ], "source": [ "#Create the game\n", - "gi = spot.game_info()\n", - "gi.s = spot.game_info.solver_LAR #Use lar solver\n", + "gi = spot.synthesis_info()\n", + "gi.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n", "\n", - "#Todo arena changes when executed multiple times\n", "game = spot.create_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], gi)\n", - "print(\"game has \", game.num_states(), \" states, and \", game.num_edges(), \" edges.\")\n", - "print(\"output propositions are \", spot.get_synthesis_output_aps(game))\n", + "print(\"game has\", game.num_states(), \"states and\", game.num_edges(), \"edges\")\n", + "print(\"output propositions are:\", \", \".join(spot.get_synthesis_output_aps(game)))\n", "display(game)" ] }, @@ -1368,7 +1367,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "Found a solution: True\n" + "Found a solution: True\n" ] }, { @@ -1974,7 +1973,7 @@ ], "source": [ "#Solve the game\n", - "print(\"Found a solution: \", spot.solve_game(game))\n", + "print(\"Found a solution:\", spot.solve_game(game))\n", "spot.highlight_strategy(game)\n", "game.show('.g')" ] @@ -1988,7 +1987,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 0\n" + "simplification lvl 0\n" ] }, { @@ -2223,7 +2222,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 1\n" + "simplification lvl 1\n" ] }, { @@ -2364,7 +2363,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 2\n" + "simplification lvl 2\n" ] }, { @@ -2471,7 +2470,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 3\n" + "simplification lvl 3\n" ] }, { @@ -2550,7 +2549,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 4\n" + "simplification lvl 4\n" ] }, { @@ -2629,7 +2628,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 5\n" + "simplification lvl 5\n" ] }, { @@ -2707,16 +2706,16 @@ ], "source": [ "# Create the strategy\n", - "# We have different strategies for minimization:\n", - "# 0 : No minimizaiton\n", - "# 1 : DFA minimization\n", - "# 2 : Inclusion based minimization with output assignement\n", - "# 3 : SAT based exact minimization\n", + "# We have different levels of simplification:\n", + "# 0 : No simplification\n", + "# 1 : bisimulation-based reduction\n", + "# 2 : bisimulation-based reduction with output output assignement\n", + "# 3 : SAT-based exact minimization\n", "# 4 : First 1 then 3 (exact)\n", "# 5 : First 2 then 3 (not exact)\n", "for i in range(6):\n", - " print(\"minimization lvl \", i)\n", - " gi.minimize_lvl = i #Use inclusion with output assignement to minimize the strategy\n", + " print(\"simplification lvl\", i)\n", + " gi.minimize_lvl = i\n", " strat = spot.create_strategy(game, gi)\n", " display(strat.show())" ] @@ -3130,7 +3129,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc16b720> >" + " *' at 0x7f78f67a4c90> >" ] }, "execution_count": 11, @@ -3139,8 +3138,7 @@ } ], "source": [ - "gi.minimize_lvl = 0\n", - "spot.apply_strategy(game, False, False)\n" + "spot.apply_strategy(game, False, False)" ] }, { @@ -3409,7 +3407,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc16bf30> >" + " *' at 0x7f78f67a4330> >" ] }, "execution_count": 12, @@ -3772,7 +3770,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc30cab0> >" + " *' at 0x7f79040eeed0> >" ] }, "execution_count": 15, @@ -4074,7 +4072,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc26b480> >" + " *' at 0x7f78f67b83c0> >" ] }, "metadata": {}, @@ -4201,7 +4199,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0ddc26bea0> >" + " *' at 0x7f78f67b8c00> >" ] }, "execution_count": 22, @@ -4255,7 +4253,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 23, @@ -4328,7 +4326,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 24, diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index da72b9868..f824288ff 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -22,8 +22,8 @@ import spot # A shared variable caused the 2nd call to create_game to give an incorrect # result. for i in range(0, 2): - gi = spot.game_info() - gi.s = spot.game_info.solver_LAR + gi = spot.synthesis_info() + gi.s = spot.synthesis_info.algo_LAR game = spot.create_game("(Ga) <-> (Fb)", ["b"], gi) assert not spot.solve_game(game)