From 72f7dd2386b643ec6a371880b7fa11e35f5d11bc Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Sun, 9 Oct 2016 00:19:34 -0700
Subject: [PATCH] first draft of python implementation of lexicographic
 parameter synth

---
 robustness.py | 40 +++++++++++++++++++++++++++++-----------
 1 file changed, 29 insertions(+), 11 deletions(-)

diff --git a/robustness.py b/robustness.py
index 127395f..77943e7 100644
--- a/robustness.py
+++ b/robustness.py
@@ -4,6 +4,7 @@ from operator import sub, add
 from lenses import lens
 
 import stl.ast
+from stl.utils import set_params, param_lens
 
 
 @singledispatch
@@ -24,15 +25,15 @@ def _(stl):
 @pointwise_robustness.register(stl.F)
 def _(stl):
     lo, hi = stl.interval
-    return lambda x, t: max(pointwise_robustness(stl.arg)(x, t + t2) 
-                            for t2 in x[lo:hi].index)
+    return lambda x, t: max((pointwise_robustness(stl.arg)(x, t + t2) 
+                            for t2 in x[lo:hi].index), default=float('inf'))
 
 
 @pointwise_robustness.register(stl.G)
 def _(stl):
     lo, hi = stl.interval
-    return lambda x, t: min(pointwise_robustness(stl.arg)(x, t + t2) 
-                            for t2 in x[lo:hi].index)
+    return lambda x, t: min((pointwise_robustness(stl.arg)(x, t + t2) 
+                            for t2 in x[lo:hi].index), default=-float('inf'))
 
 
 @pointwise_robustness.register(stl.Neg)
@@ -64,16 +65,22 @@ def eval_term(x, t):
     return lambda term: term.coeff*x[term.id.name][t]
 
 
-def binsearch(stleval, *, tol=1e-3, lo, hi):
+def binsearch(stleval, *, tol=1e-3, lo, hi, polarity):
     """Only run search if tightest robustness was positive."""
     # Only check low since hi taken care of by precondition.
     r = stleval(lo)
-    if r > 0 or abs(r) < tol: 
-        return r, lo
 
-    while abs(r) < tol:
+    # TODO: early termination by bounds checks
+    mid = lo
+    if abs(r) < tol: 
+        return r, mid
+
+    while abs(r) > tol and hi - lo > tol:
         mid = lo + (hi - lo) / 2
         r = stleval(mid)
+        print(lo, mid, hi, r)
+        if polarity: # swap direction
+            r *= -1
         if r < 0:
             lo, hi = mid, hi
         else:
@@ -82,9 +89,20 @@ def binsearch(stleval, *, tol=1e-3, lo, hi):
 
 
 def lex_param_project(stl, x, *, order, polarity, ranges, tol=1e-3):
-    val = {var: (ranges[0] if polarity[var] else ranges[1]) for var in order}
+    val = {var: (ranges[var][0] if polarity[var] else ranges[var][1]) for var in order}
     # TODO: evaluate top paramater
+    p_lens = param_lens(stl)
+    
+    def stleval_fact(var, val):
+        l = lens(val)[var]
+        return lambda p: pointwise_robustness(set_params(stl, l.set(p)))(x, 0)
+        
+    
     for var in order:
-        r, param = binsearch() #TODO
-        # TODO: update val
+        print(val)
+        stleval = stleval_fact(var, val)
+        lo, hi = ranges[var]
+        _, param = binsearch(stleval, lo=lo, hi=hi, tol=tol, polarity=polarity[var])
+        val[var] = param
+
     return val