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