rename pg_print() as print_pg() and add it to to_str()
* NEWS: Mention those change. * spot/twaalgos/game.hh (print_pg): New function. (pg_print): Mark as deprecated. * spot/twaalgos/game.cc (pg_print): Redirect to print_pg(). (print_pg): Update to output state names. * python/spot/__init__.py: Teach to_str() about print_pg(). * bin/ltlsynt.cc: Adjust to call print_pg(). * tests/python/games.ipynb: Add an example. * tests/core/ltlsynt.test: Adjust to remove the "INIT" note.
This commit is contained in:
Alexandre Duret-Lutz
parent
b3e994c249
commit
8b93b6967d
7 changed files with 145 additions and 68 deletions
11
NEWS
11
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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -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 <spot/misc/timer.hh>
|
||||
#include <spot/twaalgos/game.hh>
|
||||
#include <spot/misc/bddlt.hh>
|
||||
#include <spot/misc/escape.hh>
|
||||
#include <spot/twaalgos/sccinfo.hh>
|
||||
|
||||
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<bool> seen(ns, false);
|
||||
std::vector<unsigned> 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<std::vector<std::string>>("state-names");
|
||||
unsigned ns = towork->num_states();
|
||||
unsigned init = towork->get_init_state_number();
|
||||
os << "parity " << ns - 1 << ";\n";
|
||||
std::vector<bool> seen(ns, false);
|
||||
std::vector<unsigned> 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,
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ set -e
|
|||
|
||||
cat >exp <<EOF
|
||||
parity 17;
|
||||
0 1 0 7,8 "INIT";
|
||||
0 1 0 7,8;
|
||||
8 1 1 2;
|
||||
2 3 0 11,12;
|
||||
12 3 1 2,3;
|
||||
|
|
@ -43,7 +43,7 @@ parity 17;
|
|||
11 3 1 1,4;
|
||||
7 1 1 1,2;
|
||||
parity 13;
|
||||
0 1 0 1,2 "INIT";
|
||||
0 1 0 1,2;
|
||||
2 1 1 3;
|
||||
3 3 0 5,4;
|
||||
4 2 1 12,3;
|
||||
|
|
@ -58,7 +58,7 @@ parity 13;
|
|||
13 1 1 6,10;
|
||||
1 1 1 6,3;
|
||||
parity 5;
|
||||
0 1 0 2,3 "INIT";
|
||||
0 1 0 2,3;
|
||||
3 3 1 1;
|
||||
1 1 0 4,5;
|
||||
5 2 1 1,1;
|
||||
|
|
|
|||
|
|
@ -897,7 +897,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8f1861bd20> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7feee9b0ebb0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 8,
|
||||
|
|
@ -1224,7 +1224,7 @@
|
|||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8f187f5ef0> >"
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' 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,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue