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

ltlsynt: fix a bug in split_2step_fast_here

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-24 22:34:06 +02:00
parent 1df5f0e2c7
commit 6464324a2c
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/synthesis.cc
View file

@ -354,7 +354,7 @@ namespace spot
dst_cond_color_t key{std::make_pair(dst, ocond.id()), dst_cond_color_t key{std::make_pair(dst, ocond.id()),
color}; color};
auto [it, inserted] = auto [it, inserted] =
player_map.try_emplace(key, aut->num_states() + 1); player_map.try_emplace(key, aut->num_states());
if (!inserted) if (!inserted)
return it->second; return it->second;
unsigned ns = aut->new_state(); unsigned ns = aut->new_state();

6
tests/core/ltlsynt.test
View file

@ -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=bisim-sat | grep 'States: 2'
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4' 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 <<EOF cat >exp <<EOF
REALIZABLE REALIZABLE
aag 34 4 3 2 27 aag 34 4 3 2 27