Commit d919b78c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent adc40fdc

NEWS

+4 −0
Changes for NEWS: 4 added lines, 0 removed lines.
Original line number Diff line number Diff line
@@ -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:

THANKS

+1 −0
Changes for THANKS: 1 added line, 0 removed lines.
Original line number Diff line number Diff line
@@ -25,6 +25,7 @@ Michael Tautschnig 
Michael Weber

Ming-Hsien Tsai

Nikos Gorogiannis

Reuben Rowe

Rüdiger Ehlers

Silien Hong

Sonali Dutta

spot/twaalgos/simulation.cc

+6 −0
Changes for spot/twaalgos/simulation.cc: 6 added lines, 0 removed lines.
Original line number Diff line number Diff line
@@ -582,6 +582,12 @@ namespace spot 
              }

          }



        // 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;

tests/Makefile.am

+1 −0
Changes for tests/Makefile.am: 1 added line, 0 removed lines.
Original line number Diff line number Diff line
@@ -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 \

tests/python/bugdet.py

0 → 100644
+91 −0
Changes for tests/python/bugdet.py: 91 added lines, 0 removed lines.
Original line number Diff line number Diff line 
#!/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