diff --git a/NEWS b/NEWS
index be25f0deb..af123c2a6 100644
--- a/NEWS
+++ b/NEWS
@@ -33,6 +33,10 @@ New in spot 2.1.2.dev (not yet released)
* Running the LTL parser in debug-mode would crash.
+ * tgba_determinize() could produce incorrect deterministic automata
+ when run with use_simulation (the default) on non-simplified
+ automata.
+
New in spot 2.1.2 (2016-10-14)
Command-line tools:
diff --git a/THANKS b/THANKS
index 0b5832d1a..1cb44319e 100644
--- a/THANKS
+++ b/THANKS
@@ -25,6 +25,7 @@ Michael Tautschnig
Michael Weber
Ming-Hsien Tsai
Nikos Gorogiannis
+Reuben Rowe
Rüdiger Ehlers
Silien Hong
Sonali Dutta
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index 1c4fa474f..97ddcf3a2 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -582,7 +582,13 @@ namespace spot
}
}
- res->purge_unreachable_states();
+ // If we recorded implications for the determinization
+ // procedure, we should not remove unreachable states, as that
+ // will invalidate the contents of the IMPLICATIONS vector.
+ // It's OK not to purge the result, as the determinization
+ // will only explore the reachable part anyway.
+ if (!implications)
+ res->purge_unreachable_states();
delete gb;
res->prop_copy(original_,
diff --git a/tests/Makefile.am b/tests/Makefile.am
index dfe075640..f29445b27 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -321,6 +321,7 @@ TESTS_python = \
python/accparse2.py \
python/alarm.py \
python/bddnqueen.py \
+ python/bugdet.py \
python/implies.py \
python/interdep.py \
python/ltl2tgba.test \
diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py
new file mode 100644
index 000000000..ca619cdc4
--- /dev/null
+++ b/tests/python/bugdet.py
@@ -0,0 +1,91 @@
+#!/usr/bin/python3
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# l'EPITA.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+
+# Test case reduced from a report by Reuben Rowe
+# sent to the Spot mailing list on 2016-10-31.
+
+import spot
+
+a = spot.automaton("""
+HOA: v1
+States: 5
+Start: 4
+AP: 3 "p_0" "p_1" "p_2"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0&!1&2] 1
+[!0&!1&2] 2
+State: 1 {0}
+[0&!1&2] 1
+State: 2 {0}
+[!0&!1&2] 2
+State: 3 {0}
+[0&1&!2] 0
+[!0&1&!2] 3
+State: 4
+[!0&1&!2] 3
+--END--
+""")
+
+b = spot.automaton("""
+HOA: v1
+States: 8
+Start: 0
+AP: 3 "p_0" "p_1" "p_2"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[t] 0
+[!0&!1&2] 1
+[!0&1&!2] 4
+[!0&1&!2] 5
+[!0&1&!2] 6
+State: 1 {0}
+[!0&!1&2] 1
+State: 2
+[0&!1&2] 7
+State: 3
+[!0&!1&2] 1
+State: 4
+[0&1&!2] 2
+State: 5
+[0&1&!2] 3
+State: 6 {0}
+[!0&1&!2] 6
+State: 7 {0}
+[0&!1&2] 7
+--END--
+""");
+
+# In Reuben's report this first block built an incorrect deterministic
+# automaton, which ultimately led to an non-empty product. The second
+# was fine.
+print("use_simulation=True")
+b1 = spot.tgba_determinize(b, False, True, True, True)
+assert b1.num_states() == 5
+b1 = spot.remove_fin(spot.dtwa_complement(b1))
+assert spot.otf_product(a, b1).is_empty() == True
+
+print("\nuse_simulation=False")
+b2 = spot.tgba_determinize(b, False, True, False, True)
+assert b2.num_states() == 5
+b2 = spot.remove_fin(spot.dtwa_complement(b2))
+assert spot.otf_product(a, b1).is_empty() == True