diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 3bfeba5b7..c0a655d73 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -354,7 +354,7 @@ namespace spot dst_cond_color_t key{std::make_pair(dst, ocond.id()), color}; auto [it, inserted] = - player_map.try_emplace(key, aut->num_states() + 1); + player_map.try_emplace(key, aut->num_states()); if (!inserted) return it->second; unsigned ns = aut->new_state(); diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index d2427ea1a..4fbba5fd8 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -421,6 +421,12 @@ ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2' ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2' ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4' +# The following used to raise an exception because of a bug in +# split_2step_fast_here(). +for i in 0 1 2 3 4 5; do + ltlsynt --ins=a -f 'GFa <-> GFb' --simplify=$i | grep 'States: 1' +done + cat >exp <