diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 78571fe50..09bbe02fb 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -184,55 +184,8 @@ ARGMATCH_VERIFY(solver_args, solver_types); static solver opt_solver = SPLIT_DET; static bool verbose = false; - namespace { - - // Ensures that the game is complete for player 0. - // Also computes the owner of each state (false for player 0, i.e. env). - // Initial state belongs to Player 0 and the game is turn-based. - static std::vector* - complete_env(spot::twa_graph_ptr& arena) - { - unsigned sink_env = arena->new_state(); - unsigned sink_con = arena->new_state(); - - auto um = arena->acc().unsat_mark(); - if (!um.first) - throw std::runtime_error("game winning condition is a tautology"); - arena->new_edge(sink_con, sink_env, bddtrue, um.second); - arena->new_edge(sink_env, sink_con, bddtrue, um.second); - - std::vector seen(arena->num_states(), false); - unsigned init = arena->get_init_state_number(); - std::vector todo({init}); - auto owner = new std::vector(arena->num_states(), false); - (*owner)[init] = false; - (*owner)[sink_env] = true; - while (!todo.empty()) - { - unsigned src = todo.back(); - todo.pop_back(); - seen[src] = true; - bdd missing = bddtrue; - for (const auto& e: arena->out(src)) - { - if (!(*owner)[src]) - missing -= e.cond; - - if (!seen[e.dst]) - { - (*owner)[e.dst] = !(*owner)[src]; - todo.push_back(e.dst); - } - } - if (!(*owner)[src] && missing != bddfalse) - arena->new_edge(src, sink_con, missing, um.second); - } - - return owner; - } - static spot::twa_graph_ptr to_dpa(const spot::twa_graph_ptr& split) { @@ -548,8 +501,7 @@ namespace nb_states_dpa = dpa->num_states(); if (want_time) sw.start(); - auto owner = complete_env(dpa); - dpa->set_named_prop("state-player", owner); + propagate_players(dpa, false, true); if (want_time) bgame_time = sw.stop(); if (verbose) diff --git a/spot/misc/game.cc b/spot/misc/game.cc index a21feface..f4a4cd21a 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -247,4 +247,61 @@ namespace spot solve_rec(arena, owner, states_, m.max_set(), w, s); } + + void propagate_players(spot::twa_graph_ptr& arena, + bool first_player, bool complete0) + { + auto um = arena->acc().unsat_mark(); + if (!um.first) + throw std::runtime_error("game winning condition is a tautology"); + + unsigned sink_env = 0; + unsigned sink_con = 0; + + std::vector seen(arena->num_states(), false); + unsigned init = arena->get_init_state_number(); + std::vector todo({init}); + auto owner = new std::vector(arena->num_states(), false); + (*owner)[init] = first_player; + while (!todo.empty()) + { + unsigned src = todo.back(); + todo.pop_back(); + seen[src] = true; + bdd missing = bddtrue; + for (const auto& e: arena->out(src)) + { + bool osrc = (*owner)[src]; + if (complete0 && !osrc) + missing -= e.cond; + + if (!seen[e.dst]) + { + (*owner)[e.dst] = !osrc; + todo.push_back(e.dst); + } + else if ((*owner)[e.dst] == osrc) + { + delete owner; + throw + std::runtime_error("propagate_players(): odd cycle detected"); + } + } + if (complete0 && !(*owner)[src] && missing != bddfalse) + { + if (sink_env == 0) + { + sink_env = arena->new_state(); + sink_con = arena->new_state(); + owner->push_back(true); + owner->push_back(false); + arena->new_edge(sink_con, sink_env, bddtrue, um.second); + arena->new_edge(sink_env, sink_con, bddtrue, um.second); + } + arena->new_edge(src, sink_con, missing, um.second); + } + } + + arena->set_named_prop("state-player", owner); + } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 91c3fbb70..b6cf30d22 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -31,6 +31,22 @@ namespace spot { + + /// \brief Transform an automaton into a parity game by propagating + /// players + /// + /// This propagate state players, assuming the initial state belong + /// to \a first_player, and alternating players on each transitions. + /// If an odd cycle is detected, a runtime_exception is raised. + /// + /// If \a complete0 is set, ensure that states of player 0 are + /// complete. + SPOT_API + void propagate_players(spot::twa_graph_ptr& arena, + bool first_player = false, + bool complete0 = true); + + typedef std::unordered_set region_t; typedef std::unordered_map strategy_t; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 86da4626d..663994c00 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -23,7 +23,7 @@ set -e cat >exp <