alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Adept ltlsynt pgame to new solver

Browse source 
* bin/ltlsynt.cc: Remove change/colorize_parity, check alternating
This commit is contained in:
Philipp Schlehuber-Caissier 2022-06-29 01:21:00 +02:00
parent 6bc1dd0467
commit ddbdcd39cb
1 changed files with 36 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

42
bin/ltlsynt.cc
View file

@ -736,12 +736,42 @@ namespace
} }
if (!arena->get_named_prop<std::vector<bool>>("state-player")) if (!arena->get_named_prop<std::vector<bool>>("state-player"))
arena = spot::split_2step(arena, true); arena = spot::split_2step(arena, true);
// FIXME: If we do not split the game, we should check that it is else
// alternating. {
spot::change_parity_here(arena, // Check if the game is alternating and fix trivial cases
spot::parity_kind_max, const unsigned N = arena->num_states();
spot::parity_style_odd); // Can not use get_state_players because we need a non-const version
spot::colorize_parity_here(arena, true); auto spptr =
arena->get_named_prop<std::vector<bool>>("state-player");
assert(spptr);
const bdd& outs = get_synthesis_outputs(arena);
for (unsigned n = 0; n < N; ++n)
{
const bool p = (*spptr)[n];
for (auto& e : arena->out(n))
{
if (p != (*spptr)[e.dst])
continue; // All good
// Check if the condition is a simply conjunction of input and
// output. If so insert an intermediate state
// This also covers trivial self-loops
bdd cond = e.cond;
bdd i_cond = bdd_exist(cond, outs);
bdd o_cond = bdd_existcomp(cond, outs);
if ((i_cond & o_cond) == cond)
{
unsigned inter = arena->new_state();
spptr->push_back(!p);
e.cond = p ? o_cond : i_cond;
e.dst = inter;
arena->new_edge(inter, e.dst, !p ? o_cond : i_cond);
}
else
throw std::runtime_error("ltlsynt: given parity game is not"
"alternating and not trivially fixable!");
}
}
}
if (gi->bv) if (gi->bv)
{ {
gi->bv->split_time += sw_local.stop(); gi->bv->split_time += sw_local.stop();