From d919b78c890cbdf25ad35706b9427ce1c05c04cf Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 1 Nov 2016 09:03:22 +0100
Subject: [PATCH] simulation: do not purge unreachable states when recording
 implications

This fixes the incorrect output of tgba_determinize() reported yesterday
by Reuben Rowe.

* spot/twaalgos/simulation.cc: Do not purge unreachable states when
recording implications.
* tests/python/bugdet.py: New test case.
* tests/Makefile.am: Add it.
* THANKS: Add Reuben.
* NEWS: Mention the bug.
---
 NEWS                        |  4 ++
 THANKS                      |  1 +
 spot/twaalgos/simulation.cc |  8 +++-
 tests/Makefile.am           |  1 +
 tests/python/bugdet.py      | 91 +++++++++++++++++++++++++++++++++++++
 5 files changed, 104 insertions(+), 1 deletion(-)
 create mode 100644 tests/python/bugdet.py

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 <http://www.gnu.org/licenses/>.
+
+# Test case reduced from a report by Reuben Rowe <r.rowe@ucl.ac.uk>
+# 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