diff --git a/parser.py b/parser.py index c45f9dc..f04500f 100644 --- a/parser.py +++ b/parser.py @@ -49,8 +49,8 @@ prime = "'" pm = "+" / "-" dt = "dt" -unbound = "?" -id = ~r"[a-zA-z\d]*" +unbound = "?" id +id = ~r"[a-zA-z\d]+" const = ~r"[\+\-]?\d*(\.\d+)?" op = ">=" / "<=" / "<" / ">" / "=" _ = ~r"\s"+ diff --git a/robustness.py b/robustness.py index 994303f..aaf5bbe 100644 --- a/robustness.py +++ b/robustness.py @@ -62,3 +62,30 @@ def eval_terms(lineq, x, t): def eval_term(x, t): return lambda term: term.coeff*x[term.id.name][t] + + +def binsearch(stleval, *, tol=1e-3, lo, hi): + """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: + mid = lo + (hi - lo) / 2 + r = stleval(mid) + if r < 0: + lo, hi = mid, hi + else: + lo, hi = lo, mid + return r, mid + + +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} + # TODO: evaluate top paramater + for var in order: + r, param = binsearch() #TODO + # TODO: update val + return val +