* bin/ltlsynt.cc, spot/twaalgos/game.hh,
spot/twaalgos/synthesis.cc: here
This commit is contained in:
Florian Renkin 2021-09-13 15:28:39 +02:00
parent 7d908b9320
commit b9ec16f9c2
3 changed files with 4 additions and 10 deletions

View file

@ -454,7 +454,7 @@ namespace
{ {
assert(std::all_of(strategies.begin(), strategies.end(), assert(std::all_of(strategies.begin(), strategies.end(),
[](const auto& sl){return sl.success == 1; }) [](const auto& sl){return sl.success == 1; })
&& "ltlsynt: Can not handle GTBA as strategy."); && "ltlsynt: Can not handle TGBA as strategy.");
tot_strat = strategies.front().strat_like; tot_strat = strategies.front().strat_like;
for (size_t i = 1; i < strategies.size(); ++i) for (size_t i = 1; i < strategies.size(); ++i)
tot_strat = spot::product(tot_strat, strategies[i].strat_like); tot_strat = spot::product(tot_strat, strategies[i].strat_like);

View file

@ -156,7 +156,7 @@ namespace spot
/// acceptance condition /// acceptance condition
/// ///
/// \param arena The game arena /// \param arena The game arena
/// \param gi struct ofr options and benchmarking /// \param gi struct for options and benchmarking
/// \return Whether the initial state is won by player or not /// \return Whether the initial state is won by player or not
/// \pre Relies on the named properties "state-player" /// \pre Relies on the named properties "state-player"
/// \post The named properties "strategy" and "state-winner" are set /// \post The named properties "strategy" and "state-winner" are set

View file

@ -103,7 +103,7 @@ namespace{
spot::acc_cond::mark_t acc; spot::acc_cond::mark_t acc;
size_t pre_hash; size_t pre_hash;
}; };
// We define a order between the edges to avoid creating multiple // We define an order between the edges to avoid creating multiple
// states that in fact correspond to permutations of the order of the // states that in fact correspond to permutations of the order of the
// outgoing edges // outgoing edges
struct less_info_t struct less_info_t
@ -1769,13 +1769,7 @@ namespace spot
f = extract_and(f, outs_set); f = extract_and(f, outs_set);
if (!(f.is(op::And))) if (!(f.is(op::And)))
{ return { {f}, { aps_of(f, outs_set).second } };
auto [_, outs_f] = aps_of(f, outs_set);
return {
{f},
{outs_f}
}; // todo this is not nice, change style?!
}
// Atomics prop of children // Atomics prop of children
std::vector<std::set<formula>> children_outs; std::vector<std::set<formula>> children_outs;
// Independent formulas // Independent formulas