diff --git a/NEWS b/NEWS index 7e6bd6a40..77c4e081f 100644 --- a/NEWS +++ b/NEWS @@ -117,6 +117,17 @@ New in spot 2.10.6.dev (not yet released) to obtain a simple model checker (that returns true or false, without counterexample). + Python bindings: + + - The to_str() method of automata can now export a parity game into + the PG-Solver format by passing option 'pg'. See + https://spot.lrde.epita.fr/ipynb/games.html for an example. + + Deprectation notice: + + - spot::pg_print() has been deprecated in favor of spot::print_pg() + for consistency with the rest of the API. + Bugs fixed: - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index bcd9d41d9..06c29db88 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -400,7 +400,7 @@ namespace [](const spot::twa_graph_ptr& game)->void { if (opt_print_pg) - spot::pg_print(std::cout, game); + spot::print_pg(std::cout, game); else spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n'; } @@ -785,7 +785,7 @@ namespace if (opt_print_pg || opt_print_hoa) { if (opt_print_pg) - spot::pg_print(std::cout, arena); + spot::print_pg(std::cout, arena); else spot::print_hoa(std::cout, arena, opt_print_hoa_args) << '\n'; return 0; diff --git a/python/spot/__init__.py b/python/spot/__init__.py index a351e9c54..340eba00a 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2014-2021 Laboratoire de +# Copyright (C) 2014-2022 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -261,6 +261,12 @@ class twa: ostr = ostringstream() print_lbtt(ostr, a, opt) return ostr.str() + if format == 'pg': + if opt is not None: + raise ValueError("print_pg() has no option") + ostr = ostringstream() + print_pg(ostr, a) + return ostr.str() raise ValueError("unknown string format: " + format) def save(a, filename, format='hoa', opt=None, append=False): diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 419b33fe3..ccb3b818e 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018, 2020-2021 Laboratoire de Recherche et +// Copyright (C) 2017-2018, 2020-2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,7 +23,7 @@ #include #include -#include +#include #include namespace spot @@ -834,66 +834,71 @@ namespace spot return solve_parity_game(arena); } + // backward compatibility void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) { - ensure_parity_game(arena, "pg_print"); + print_pg(os, arena); + } - auto do_print = [&os](const const_twa_graph_ptr& arena) - { - const region_t& owner = get_state_players(arena); - - unsigned ns = arena->num_states(); - unsigned init = arena->get_init_state_number(); - os << "parity " << ns - 1 << ";\n"; - std::vector seen(ns, false); - std::vector todo({init}); - while (!todo.empty()) - { - unsigned src = todo.back(); - todo.pop_back(); - if (seen[src]) - continue; - seen[src] = true; - os << src << ' '; - os << arena->out(src).begin()->acc.max_set() - 1 << ' '; - os << owner[src] << ' '; - bool first = true; - for (auto& e: arena->out(src)) - { - if (!first) - os << ','; - first = false; - os << e.dst; - if (!seen[e.dst]) - todo.push_back(e.dst); - } - if (src == init) - os << " \"INIT\""; - os << ";\n"; - } - }; - // Ensure coloring - // PGSolver format expects max odd and colored + std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena) + { bool is_par, max, odd; is_par = arena->acc().is_parity(max, odd, true); - assert(is_par && "pg_printer needs parity condition"); - bool is_colored = (max & odd) ? std::all_of(arena->edges().begin(), - arena->edges().end(), - [](const auto& e) - { - return (bool) e.acc; - }) - : false; - if (is_colored) - do_print(arena); - else + if (!is_par) + throw std::runtime_error("print_pg: arena must have a parity acceptance"); + const region_t& owner = *ensure_game(arena, "print_pg"); + + bool max_odd_colored = + max && odd && std::all_of(arena->edges().begin(), + arena->edges().end(), + [](const auto& e) + { + return (bool) e.acc; + }); + const_twa_graph_ptr towork = arena; + if (!max_odd_colored) { - auto arena2 = change_parity(arena, parity_kind_max, parity_style_odd); - colorize_parity_here(arena2, true); - set_state_players(arena2, - get_state_players(arena)); - do_print(arena2); + twa_graph_ptr tmp = + change_parity(arena, parity_kind_max, parity_style_odd); + colorize_parity_here(tmp, true); + towork = tmp; } + + auto sn = arena->get_named_prop>("state-names"); + unsigned ns = towork->num_states(); + unsigned init = towork->get_init_state_number(); + os << "parity " << ns - 1 << ";\n"; + std::vector seen(ns, false); + std::vector todo({init}); + while (!todo.empty()) + { + unsigned src = todo.back(); + todo.pop_back(); + if (seen[src]) + continue; + seen[src] = true; + os << src << ' '; + os << towork->out(src).begin()->acc.max_set() - 1 << ' '; + os << owner[src] << ' '; + bool first = true; + for (auto& e: arena->out(src)) + { + if (!first) + os << ','; + first = false; + os << e.dst; + if (!seen[e.dst]) + todo.push_back(e.dst); + } + if (sn && sn->size() > src && !(*sn)[src].empty()) + { + os << " \""; + escape_str(os, (*sn)[src]); + os << '"'; + } + os << ";\n"; + } + return os; } void alternate_players(spot::twa_graph_ptr& arena, diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index 64f8d52c8..df5d27439 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -112,10 +112,26 @@ namespace spot /// \ingroup games - /// \brief Print a max odd parity game using PG-solver syntax + /// \brief Print a parity game using PG-solver syntax + /// + /// The input automaton should have parity acceptance and should + /// define state owner. Since the PG solver format want player 1 to + /// solve a max odd condition, the acceptance condition will be + /// adapted to max odd if necessary. + /// + /// The output will list the initial state as first state (because + /// that is the convention of our parser), and list only reachable + /// states. + /// + /// If states are named, the names will be output as well. + /// @{ + SPOT_API + std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena); + + SPOT_DEPRECATED("use print_pg() instead") SPOT_API void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); - + /// @} /// \ingroup games /// \brief Highlight the edges of a strategy on an automaton. diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 95e0bf4d7..33369dcde 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -24,7 +24,7 @@ set -e cat >exp < GFo1)" --outs="o1,o2" --verbose\ --bypass=yes 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx -diff outx exp \ No newline at end of file +diff outx exp diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index fcc2bf12c..a6168b07e 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -897,7 +897,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f8f1861bd20> >" + " *' at 0x7feee9b0ebb0> >" ] }, "execution_count": 8, @@ -1224,7 +1224,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f8f187f5ef0> >" + " *' at 0x7fef001c87b0> >" ] }, "execution_count": 11, @@ -1240,7 +1240,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Input in PGSolver format\n", + "# Input/Output in PGSolver format\n", "\n", "The automaton parser is also able to parse the [PGSolver](https://github.com/tcsprojects/pgsolver) format. Here are two examples from the manual of PGSolver. The support for C-style comments is not part of the PGSolver format.\n", "\n", @@ -1623,6 +1623,45 @@ "display(a.show('.g'), b.show('.g'))" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To output a parity-game in PG-solver format, use `to_str('pg')`." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "parity 4;\n", + "0 6 1 4,2 \"Africa\";\n", + "2 7 0 3,1,0,4 \"Asia\";\n", + "4 5 1 0 \"Antarctica\";\n", + "1 8 1 2,4,3 \"America\";\n", + "3 6 0 4,2 \"Australia\";\n", + "parity 7;\n", + "0 0 0 1,2;\n", + "2 0 0 3,4;\n", + "4 0 0 5,6;\n", + "6 0 0 7,0;\n", + "7 1 1 0,1;\n", + "1 1 1 2,3;\n", + "3 1 1 4,5;\n", + "5 1 1 6,7;\n", + "\n" + ] + } + ], + "source": [ + "print(a.to_str('pg') + b.to_str('pg'))" + ] + }, { "cell_type": "code", "execution_count": null,