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

fix ignored aborter in WDBA-minimization

Browse source 
Fixes #443, reported by Roei Nahum.  (However the fix
only works for the development version, where wdba-det-max
was introduced to work around that kind of problem.)

* spot/twaalgos/minimize.cc: Avoid aborter being implicitly
converted to Boolean.
* tests/core/ltl2tgba2.test: Add test case.
* THANKS: Add Roei Nahum.
This commit is contained in:
Alexandre Duret-Lutz 2020-12-08 11:56:29 +01:00
parent 9da0b3a1c4
commit eeaed5592f
3 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
THANKS
View file

@ -40,6 +40,7 @@ Ming-Hsien Tsai
Nikos Gorogiannis Nikos Gorogiannis
Paul Guénézan Paul Guénézan
Reuben Rowe Reuben Rowe
Roei Nahum
Rüdiger Ehlers Rüdiger Ehlers
Silien Hong Silien Hong
Simon Jantsch Simon Jantsch

3
spot/twaalgos/minimize.cc
View file

@ -386,7 +386,6 @@ namespace spot
twa_graph_ptr det_a; twa_graph_ptr det_a;
{ {
power_map pm;
bool input_is_det = is_deterministic(a); bool input_is_det = is_deterministic(a);
if (input_is_det) if (input_is_det)
{ {
@ -394,7 +393,7 @@ namespace spot
} }
else else
{ {
det_a = tgba_powerset(a, pm, aborter); det_a = tgba_powerset(a, aborter);
if (!det_a) if (!det_a)
return nullptr; return nullptr;
} }

4
tests/core/ltl2tgba2.test
View file

@ -474,3 +474,7 @@ test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d`
# Issue #418. # Issue #418.
f='(G!a | G!b | G!c) & (FG!a2 | GFb2 | GFc2) & (GFc2 | FG!b2 | GFa2)' f='(G!a | G!b | G!c) & (FG!a2 | GFb2 | GFc2) & (GFc2 | FG!b2 | GFa2)'
test 28 = `ltl2tgba -D -G -S --stats=%s "$f"` test 28 = `ltl2tgba -D -G -S --stats=%s "$f"`
# Issue #443. This used to be too long.
f='(!(G({(a)} |=> {(b)[*32]})))'
test 34 = `ltl2tgba -B --stats=%s "$f"`