From a331d90b44379375803f06b26aba0a0d3f5d1ba4 Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Thu, 15 Dec 2016 20:56:44 -0800
Subject: [PATCH] implemented f,neg,or canonical form and fixed bug in Or rule

---
 stl/smooth_robustness.py | 12 ++++--------
 stl/utils.py             | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/stl/smooth_robustness.py b/stl/smooth_robustness.py
index 5e24858..25ef934 100644
--- a/stl/smooth_robustness.py
+++ b/stl/smooth_robustness.py
@@ -10,7 +10,7 @@ from lenses import lens
 
 import stl.ast
 from stl.ast import t_sym
-from stl.utils import walk
+from stl.utils import walk, f_neg_or_canonical_form
 from stl.robustness import op_lookup
 
 Param = namedtuple("Param", ["L", "h", "B", "eps"])
@@ -40,10 +40,6 @@ def admissible_params(phi, eps, L):
     B = max(node_base(n, eps, L) for n in walk(phi))
     return B, h
 
-def new_symbol_set(ss):
-    indices = set(ss[id_map].keys())
-    non_indicies = set(v.name for k, v in ss.items() if v != "id_map")
-    return indices | non_indicies
 
 def symbolic_params(phi, eps, L):
     return Param(
@@ -53,8 +49,8 @@ def symbolic_params(phi, eps, L):
         eps=sym.Dummy("eps"),
     )
 
-
 def smooth_robustness(phi, *, L=None, eps=None):
+    phi = f_neg_or_canonical_form(phi)
     p = symbolic_params(phi, eps, L)
     lo, hi = beta(phi, p), alpha(phi, p)
     subs = {}
@@ -96,7 +92,7 @@ def _(phi, p):
 
 @alpha.register(stl.Neg)
 def _(phi, p):
-    return 1/beta(phi, p)
+    return 1/beta(phi.arg, p)
 
 
 @alpha.register(stl.Or)
@@ -128,7 +124,7 @@ beta.register(stl.LinEq)(alpha)
 
 @beta.register(stl.Neg)
 def _(phi, p):
-    return 1/alpha(phi, p)
+    return 1/alpha(phi.arg, p)
 
 
 @beta.register(stl.Or)
diff --git a/stl/utils.py b/stl/utils.py
index 40d0ea3..e14eeea 100644
--- a/stl/utils.py
+++ b/stl/utils.py
@@ -85,3 +85,26 @@ def symbol_lens(phi):
 def set_params(stl_or_lens, val):
     l = stl_or_lens if isinstance(stl_or_lens, Lens) else param_lens(stl_or_lens)
     return l.modify(lambda x: val[str(x)] if str(x) in val else x)
+
+
+def f_neg_or_canonical_form(phi):
+    if isinstance(phi, stl.LinEq):
+        return phi
+
+    children = [f_neg_or_canonical_form(s) for s in phi.children()]
+    if isinstance(phi, (stl.And, stl.G)):
+        children = [stl.ast.Neg(s) for s in children]
+    children = tuple(children)
+
+    if isinstance(phi, stl.Or):
+        return stl.Or(children)
+    elif isinstance(phi, stl.And):
+        return stl.Neg(stl.Or(children))
+    elif isinstance(phi, stl.Neg):
+        return stl.Neg(children[0])
+    elif isinstance(phi, stl.F):
+        return stl.F(phi.interval, children[0])
+    elif isinstance(phi, stl.G):
+        return stl.Neg(stl.F(phi.interval, children[0]))
+    else:
+        raise NotImplementedError