Commit fad05632 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: implement the map and transform functions for formulas

* wrap/python/spot.py: Implement them.
* wrap/python/tests/ltlsimple.py: New tests.
parent 23693898
......@@ -116,9 +116,32 @@ def _formula_to_str(self, format = 'spot', parenth = False):
else:
raise ValueError("unknown string format: " + format)
def _formula_traverse(self, func):
if func(self):
return
for f in self:
f.traverse(func)
def _formula_map(self, func):
k = self.kind()
if k in (FalseVal, TrueVal, EmptyWord, AP):
return self;
if k in (Not, X, F, G, Closure, NegClosure, NegClosureMarked):
return formula.unop(k, func(self[0]))
if k in (Xor, Implies, Equiv, U, R, W, M, EConcat,
EConcatMarked, UConcat):
return formula.binop(k, func(self[0]), func(self[1]))
if k in (Or, OrRat, And, AndRat, AndNLM, Concat, Fusion):
return formula.multop(k, [func(x) for x in self])
if k in (Star, FStar):
return formula.bunop(k, func(self[0]), self.min(), self.max())
raise ValueError("unknown type of formula")
formula.__init__ = _formula_str_ctor
formula.to_str = _formula_to_str
formula.show_ast = _render_formula_as_svg
formula.traverse = _formula_traverse
formula.map = _formula_map
def _twa_to_str(a, format='hoa', opt=None):
format = format.lower()
......
......@@ -74,3 +74,22 @@ assert spot.fnode_instances_check()
#----------------------------------------------------------------------
assert str([x for x in spot.formula('a &b & c')]) == '[a, b, c]'
def switch_g_f(x):
if x._is(spot.G):
return spot.formula.F(switch_g_f(x[0]))
if x._is(spot.F):
return spot.formula.G(switch_g_f(x[0]))
return x.map(switch_g_f)
f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)')
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):
x += 1
f.traverse(count_g)
assert x == 3
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment