1#!/usr/bin/python3
2# -*- mode: python; coding: utf-8 -*-
3# Copyright (C) 2016 Laboratoire de Recherche et Développement de
4# l'EPITA.
5#
6# This file is part of Spot, a model checking library.
7#
8# Spot is free software; you can redistribute it and/or modify it
9# under the terms of the GNU General Public License as published by
10# the Free Software Foundation; either version 3 of the License, or
11# (at your option) any later version.
12#
13# Spot is distributed in the hope that it will be useful, but WITHOUT
14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
15# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
16# License for more details.
17#
18# You should have received a copy of the GNU General Public License
19# along with this program.  If not, see <http://www.gnu.org/licenses/>.
20
21# Test case reduced from a report by Reuben Rowe <r.rowe@ucl.ac.uk>
22# sent to the Spot mailing list on 2016-10-31.
23
24import spot
25
26a = spot.automaton("""
27HOA: v1
28States: 5
29Start: 4
30AP: 3 "p_0" "p_1" "p_2"
31Acceptance: 1 Inf(0)
32--BODY--
33State: 0
34[0&!1&2] 1
35[!0&!1&2] 2
36State: 1 {0}
37[0&!1&2] 1
38State: 2 {0}
39[!0&!1&2] 2
40State: 3 {0}
41[0&1&!2] 0
42[!0&1&!2] 3
43State: 4
44[!0&1&!2] 3
45--END--
46""")
47
48b = spot.automaton("""
49HOA: v1
50States: 8
51Start: 0
52AP: 3 "p_0" "p_1" "p_2"
53Acceptance: 1 Inf(0)
54--BODY--
55State: 0
56[t] 0
57[!0&!1&2] 1
58[!0&1&!2] 4
59[!0&1&!2] 5
60[!0&1&!2] 6
61State: 1 {0}
62[!0&!1&2] 1
63State: 2
64[0&!1&2] 7
65State: 3
66[!0&!1&2] 1
67State: 4
68[0&1&!2] 2
69State: 5
70[0&1&!2] 3
71State: 6 {0}
72[!0&1&!2] 6
73State: 7 {0}
74[0&!1&2] 7
75--END--
76""")
77
78# In Reuben's report this first block built an incorrect deterministic
79# automaton, which ultimately led to an non-empty product.  The second
80# was fine.
81print("use_simulation=True")
82b1 = spot.tgba_determinize(b, False, True, True, True)
83assert b1.num_states() == 5
84b1 = spot.remove_fin(spot.dualize(b1))
85assert not a.intersects(b1)
86
87print("\nuse_simulation=False")
88b2 = spot.tgba_determinize(b, False, True, False, True)
89assert b2.num_states() == 5
90b2 = spot.remove_fin(spot.dualize(b2))
91assert not a.intersects(b2)
92