interdep.py 1.66 KB
Newer Older
1 2 3 4 5 6
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement
# de l'EPITA.
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
# Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
#
# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.

25 26 27
# Make sure that interdependencies between the spot and buddy wrappers
# are not problematic.
import buddy
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
28
import spot
29
import sys
30 31 32 33
e = spot.default_environment.instance()
p = spot.empty_parse_error_list()
f = spot.parse('GFa', p, e)
dict = spot.bdd_dict()
34
a = spot.ltl_to_tgba_lacim(f, dict)
35 36
s0 = a.get_init_state()
b = s0.as_bdd()
37
sys.stdout.write("%s\n" % b)
38 39 40 41
iter = a.succ_iter(s0)
iter.first()
while not iter.done():
    c = iter.current_condition()
42
    sys.stdout.write("%s\n" % c)
43 44 45
    b &= c # `&=' is defined only in buddy.  So if this statement works
           # it means buddy can grok spot's objects.
    iter.next()
46
sys.stdout.write("%s\n" % b)