From 6464324a2c17eab0abc059f50cc92aa60ed7ab03 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Oct 2021 22:34:06 +0200 Subject: [PATCH] ltlsynt: fix a bug in split_2step_fast_here * spot/twaalgos/synthesis.cc (split_2step_fast_here::get_ps): Fix the state number recorded in the map. * tests/core/ltlsynt.test: Add test case. --- spot/twaalgos/synthesis.cc | 2 +- tests/core/ltlsynt.test | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) 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 <