1#!/usr/bin/python3 2# -*- mode: python; coding: utf-8 -*- 3# Copyright (C) 2018 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 21import spot 22 23aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)') 24si = spot.scc_info(aut) 25s = "" 26for aut2 in si.split_on_sets(0, [0]): 27 # This call to to_str() used to fail because split_on_sets had not 28 # registered the atomic propositions of aut 29 s += aut2.to_str() 30assert spot.automaton(s).num_states() == 8 31