From 078eb11b5cdb2b875836a99253efc026ae41cfe4 Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Fri, 23 Dec 2016 18:32:04 -0800 Subject: [PATCH] add helper function for going to an MTL formula --- stl/utils.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/stl/utils.py b/stl/utils.py index 1cdf605..88b0395 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -4,6 +4,7 @@ from lenses import lens, Lens import funcy as fn import sympy +import stl.ast from stl.ast import LinEq, And, Or, NaryOpSTL, F, G, Interval, Neg def walk(stl, bfs=False): @@ -108,3 +109,12 @@ def f_neg_or_canonical_form(phi): return Neg(F(phi.interval, children[0])) else: raise NotImplementedError + + +def to_mtl(phi): + focus = lineq_lens(phi) + to_ap = lambda i: stl.ast.AtomicPred("AP{}".format(i)) + ap_map = {to_ap(i): leq for i, leq in enumerate(focus.get_all())} + lineq_map = {v:k for k,v in ap_map.items()} + return focus.modify(lineq_map.get), ap_map +