diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 76389a259..87805801b 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -376,7 +376,7 @@ namespace } case 0: { - auto arena = spot::create_game(*sub_f, *sub_o, *gi); + auto arena = spot::ltl_to_game(*sub_f, *sub_o, *gi); if (gi->bv) { gi->bv->nb_states_arena += arena->num_states(); diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 06bc77b48..e4682ac6b 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -454,7 +454,7 @@ namespace spot /// Unless \a ins and \a outs are specified, only the propositions /// actually used in the strategy appear in the aiger circuit. So it /// can happen that, for instance, propositions marked as output - /// during the call to create_game are absent. + /// during the call to ltl_to_game() are absent. /// If \a ins and \a outs are used, all properties they list are /// guaranteed to appear in the aiger circuit. /// @{ diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 57d6d541c..08cb4264d 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -808,7 +808,7 @@ namespace spot } - namespace // Anonymous create_game + namespace // Anonymous ltl_to_game { static translator create_translator(synthesis_info& gi) @@ -873,7 +873,7 @@ namespace spot } // anonymous twa_graph_ptr - create_game(const formula& f, + ltl_to_game(const formula& f, const std::vector& all_outs, synthesis_info& gi) { @@ -1068,26 +1068,26 @@ namespace spot } twa_graph_ptr - create_game(const formula& f, + ltl_to_game(const formula& f, const std::vector& all_outs) { synthesis_info dummy; - return create_game(f, all_outs, dummy); + return ltl_to_game(f, all_outs, dummy); } twa_graph_ptr - create_game(const std::string& f, + ltl_to_game(const std::string& f, const std::vector& all_outs) { - return create_game(parse_formula(f), all_outs); + return ltl_to_game(parse_formula(f), all_outs); } twa_graph_ptr - create_game(const std::string& f, + ltl_to_game(const std::string& f, const std::vector& all_outs, synthesis_info& gi) { - return create_game(parse_formula(f), all_outs, gi); + return ltl_to_game(parse_formula(f), all_outs, gi); } void diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index f42d7370e..80c8a33eb 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -150,34 +150,28 @@ namespace spot /// \brief Creates a game from a specification and a set of /// output propositions /// - /// \param f The specification given as LTL/PSL formula + /// \param f The specification given as an LTL/PSL formula, or + /// as a string. /// \param all_outs The names of all output propositions /// \param gi synthesis_info structure /// \note All propositions in the formula that do not appear in all_outs - /// arer treated as input variables. + /// are treated as input variables. + /// @{ SPOT_API twa_graph_ptr - create_game(const formula& f, + ltl_to_game(const formula& f, const std::vector& all_outs, synthesis_info& gi); - - /// \ingroup synthesis - /// \brief create_game called with default options SPOT_API twa_graph_ptr - create_game(const formula& f, + ltl_to_game(const formula& f, const std::vector& all_outs); - - /// \ingroup synthesis - /// \brief Like create_game but formula given as string SPOT_API twa_graph_ptr - create_game(const std::string& f, + ltl_to_game(const std::string& f, const std::vector& all_outs, synthesis_info& gi); - - /// \ingroup synthesis - /// \brief create_game called with default options SPOT_API twa_graph_ptr - create_game(const std::string& f, + ltl_to_game(const std::string& f, const std::vector& all_outs); + /// @} /// \ingroup synthesis /// \brief Takes a solved game and restricts the automaton to the diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 24efe9d8e..46e8f6841 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -31,7 +31,7 @@ "\n", "Each of these steps is parametrized by a structure called `synthesis_info`. This structure stores some additional data needed to pass fine-tuning options or to store statistics.\n", "\n", - "The `create_game` function takes the LTL specification, and the list of controlable atomic propositions (or output signals). It returns a two-player game, where player 0 plays the input variables (and wants to invalidate the acceptance condition), and player 1 plays the output variables (and wants to satisfy the output condition). The conversion from LTL to parity automata can use one of many algorithms, and can be specified in the `synthesis_info` structure (this works like the `--algo=` option of `ltlsynt`)." + "The `ltl_to_game` function takes the LTL specification, and the list of controlable atomic propositions (or output signals). It returns a two-player game, where player 0 plays the input variables (and wants to invalidate the acceptance condition), and player 1 plays the output variables (and wants to satisfy the output condition). The conversion from LTL to parity automata can use one of many algorithms, and can be specified in the `synthesis_info` structure (this works like the `--algo=` option of `ltlsynt`)." ] }, { @@ -707,7 +707,7 @@ "si = spot.synthesis_info()\n", "si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n", "\n", - "game = spot.create_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\n", + "game = spot.ltl_to_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\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)" @@ -3141,7 +3141,7 @@ } ], "source": [ - "game = spot.create_game(\"i0 <-> F((Go1 -> Fi1) U o0)\", [\"o0\", \"o1\"])\n", + "game = spot.ltl_to_game(\"i0 <-> F((Go1 -> Fi1) U o0)\", [\"o0\", \"o1\"])\n", "spot.solve_game(game)\n", "spot.highlight_strategy(game)\n", "display(game)\n", diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index f824288ff..87885e6d2 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -19,16 +19,16 @@ import spot -# A shared variable caused the 2nd call to create_game to give an incorrect +# A shared variable caused the 2nd call to ltl_to_game to give an incorrect # result. for i in range(0, 2): gi = spot.synthesis_info() gi.s = spot.synthesis_info.algo_LAR - game = spot.create_game("(Ga) <-> (Fb)", ["b"], gi) + game = spot.ltl_to_game("(Ga) <-> (Fb)", ["b"], gi) assert not spot.solve_game(game) # A game can have only inputs -game = spot.create_game("GFa", []) +game = spot.ltl_to_game("GFa", []) assert(game.to_str() == """HOA: v1 States: 3 Start: 0