diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 17177ebe4..bd2d9049c 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -51,6 +51,21 @@ def setup(**kwargs): d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets os.environ['SPOT_DOTDEFAULT'] = d +# In version 3.0.2, Swig puts strongly typed enum in the main +# namespace without prefixing them. Latter versions fix this. So we +# can remove for following hack once 3.0.2 is no longer used in our +# build farm. +if not 'op_ff' in globals(): + for i in ('ff', 'tt', 'eword', 'ap', 'Not', 'X', 'F', 'G', + 'Closure', 'NegClosure', 'NegClosureMarked', + 'Xor', 'Implies', 'Equiv', 'U', 'R', 'W', 'M', + 'EConcat', 'EConcatMarked', 'UConcat', 'Or', + 'OrRat', 'And', 'AndRat', 'AndNLM', 'Concat', + 'Fusion', 'Star', 'FStar'): + globals()['op_' + i] = globals()[i]; + del globals()[i] + + # Global BDD dict so that we do not have to create one in user code. _bdd_dict = make_bdd_dict() @@ -124,16 +139,18 @@ def _formula_traverse(self, func): def _formula_map(self, func): k = self.kind() - if k in (ff, tt, eword, ap): + if k in (op_ff, op_tt, op_eword, op_ap): return self; - if k in (Not, X, F, G, Closure, NegClosure, NegClosureMarked): + if k in (op_Not, op_X, op_F, op_G, op_Closure, + op_NegClosure, op_NegClosureMarked): return formula.unop(k, func(self[0])) - if k in (Xor, Implies, Equiv, U, R, W, M, EConcat, - EConcatMarked, UConcat): + if k in (op_Xor, op_Implies, op_Equiv, op_U, op_R, op_W, + op_M, op_EConcat, op_EConcatMarked, op_UConcat): return formula.binop(k, func(self[0]), func(self[1])) - if k in (Or, OrRat, And, AndRat, AndNLM, Concat, Fusion): + if k in (op_Or, op_OrRat, op_And, op_AndRat, op_AndNLM, + op_Concat, op_Fusion): return formula.multop(k, [func(x) for x in self]) - if k in (Star, FStar): + if k in (op_Star, op_FStar): return formula.bunop(k, func(self[0]), self.min(), self.max()) raise ValueError("unknown type of formula") diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index ba65aa1b4..10be6e283 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -77,9 +77,9 @@ assert str([x for x in spot.formula('a &b & c')]) == '[a, b, c]' def switch_g_f(x): - if x._is(spot.G): + if x._is(spot.op_G): return spot.formula.F(switch_g_f(x[0])) - if x._is(spot.F): + if x._is(spot.op_F): return spot.formula.G(switch_g_f(x[0])) return x.map(switch_g_f) @@ -89,7 +89,7 @@ assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)' x = 0 def count_g(f): global x - if f._is(spot.G): + if f._is(spot.op_G): x += 1 f.traverse(count_g) assert x == 3