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

minimize_wdba: fix nondeterministic execution

Browse source 
Fixes core/readsave.test and python/automata.ipython
with gcc-snapshot (future gcc 7).

* spot/twaalgos/minimize.cc: Here.
* NEWS: Mention the change.
* tests/core/acc_word.test: Adjust test case.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-25 12:00:30 +02:00
parent 20cf43b3ea
commit d7d6b40926
3 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -180,6 +180,9 @@ New in spot 2.0.3a (not yet released)
automata, the error message would report "Comp(Ni)*Comp(Pj)" as automata, the error message would report "Comp(Ni)*Comp(Pj)" as
non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)". non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)".
* Fix some non-deterministic execution of minimize_wdba(), causing
test-suite failures with the future G++ 7, and clang 3.9.
New in spot 2.0.3 (2016-07-11) New in spot 2.0.3 (2016-07-11)
Bug fixes: Bug fixes:

6
spot/twaalgos/minimize.cc
View file

@ -49,9 +49,9 @@
namespace spot namespace spot
{ {
// FIXME: do we really want to use unordered_set instead of set here? // This is called hash_set for historical reason, but we need the
// This calls for benchmarking. // order inside hash_set to be deterministic.
typedef state_set hash_set; typedef std::set<const state*, state_ptr_less_than> hash_set;
typedef state_map<unsigned> hash_map; typedef state_map<unsigned> hash_map;
namespace namespace

14
tests/core/acc_word.test
View file

@ -99,13 +99,13 @@ cat >expected <<EOF
HOA: v1.1 HOA: v1.1
name: "Fa & Fb" name: "Fa & Fb"
States: 4 States: 4
Start: 2 Start: 3
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant terminal properties: deterministic stutter-invariant terminal
spot.highlight.edges: 1 3 2 3 5 3 6 3 7 2 8 2 spot.highlight.edges: 1 3 2 3 4 2 7 3 8 2 9 3
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[t] 0 [t] 0
@ -113,13 +113,13 @@ State: 1
[1] 0 [1] 0
[!1] 1 [!1] 1
State: 2 State: 2
[0] 0
[!0] 2
State: 3
[0&1] 0 [0&1] 0
[0&!1] 1 [0&!1] 1
[!0&!1] 2 [!0&1] 2
[!0&1] 3 [!0&!1] 3
State: 3
[0] 0
[!0] 3
--END-- --END--
EOF EOF
diff expected out diff expected out