diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index efd22b9ba..233fb7fb9 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -454,7 +454,7 @@ namespace { assert(std::all_of(strategies.begin(), strategies.end(), [](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; for (size_t i = 1; i < strategies.size(); ++i) tot_strat = spot::product(tot_strat, strategies[i].strat_like); diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index 63d46762f..558349534 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -156,7 +156,7 @@ namespace spot /// acceptance condition /// /// \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 /// \pre Relies on the named properties "state-player" /// \post The named properties "strategy" and "state-winner" are set diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 6392b537e..22f74f934 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -103,7 +103,7 @@ namespace{ spot::acc_cond::mark_t acc; 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 // outgoing edges struct less_info_t @@ -1769,13 +1769,7 @@ namespace spot f = extract_and(f, outs_set); if (!(f.is(op::And))) - { - auto [_, outs_f] = aps_of(f, outs_set); - return { - {f}, - {outs_f} - }; // todo this is not nice, change style?! - } + return { {f}, { aps_of(f, outs_set).second } }; // Atomics prop of children std::vector> children_outs; // Independent formulas