From e491ac70432cb34d1a233d973c83357115203f9b Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Wed, 22 Nov 2017 11:56:23 -0800 Subject: [PATCH] added code for discretizing bounded stl --- stl/ast.py | 10 ++------ stl/parser.py | 4 ++-- stl/test_utils.py | 26 ++++++++++++++++++++- stl/utils.py | 58 +++++++++++++++++++++++++++++++++++++++++++---- 4 files changed, 82 insertions(+), 16 deletions(-) diff --git a/stl/ast.py b/stl/ast.py index e875df2..b64325a 100644 --- a/stl/ast.py +++ b/stl/ast.py @@ -1,5 +1,4 @@ # -*- coding: utf-8 -*- -# TODO: supress + given a + (-b). i.e. want a - b from collections import deque, namedtuple from functools import lru_cache @@ -265,7 +264,7 @@ class Next(namedtuple('Next', ['arg']), AST): __slots__ = () def __repr__(self): - return f"X({self.arg})" + return f"◯({self.arg})" @property def children(self): @@ -291,13 +290,8 @@ def ast_lens(phi, bind=True, *, pred=lambda _: False, - focus_lens=None, + focus_lens=lambda _: [lens], getter=False): - if focus_lens is None: - - def focus_lens(_): - return [lens] - child_lenses = _ast_lens(phi, pred=pred, focus_lens=focus_lens) phi = lenses.bind(phi) if bind else lens return (phi.Tuple if getter else phi.Fork)(*child_lenses) diff --git a/stl/parser.py b/stl/parser.py index 993d70d..76c71c9 100644 --- a/stl/parser.py +++ b/stl/parser.py @@ -2,7 +2,6 @@ # TODO: allow multiplication to be distributive # TODO: support variables on both sides of ineq -# TODO: Allow -x = -1*x from functools import partialmethod @@ -24,12 +23,13 @@ iff = paren_phi _ ("⇔" / "<->" / "iff") _ (and / paren_phi) xor = paren_phi _ ("⊕" / "^" / "xor") _ (and / paren_phi) neg = ("~" / "¬") paren_phi -next = "X" paren_phi +next = next_sym paren_phi f = F interval? phi g = G interval? phi until = paren_phi __ U __ paren_phi timed_until = paren_phi __ U interval __ paren_phi +next_sym = "X" / "◯" F = "F" / "◇" G = "G" / "□" U = "U" diff --git a/stl/test_utils.py b/stl/test_utils.py index 845b1b7..e02324c 100644 --- a/stl/test_utils.py +++ b/stl/test_utils.py @@ -4,7 +4,6 @@ from stl.hypothesis import SignalTemporalLogicStrategy from hypothesis import given from pytest import raises - CONTEXT = { stl.parse('AP1'): stl.parse('F(x > 4)'), stl.parse('AP2'): stl.parse('(AP1) U (AP1)'), @@ -61,3 +60,28 @@ def test_linear_stl_lipschitz(phi1, phi2): @given(SignalTemporalLogicStrategy, SignalTemporalLogicStrategy) def test_timed_until_smoke_test(phi1, phi2): stl.utils.timed_until(phi1, phi2, lo=2, hi=20) + + +def test_discretize(): + dt = 0.3 + + phi = stl.parse('X(AP1)') + assert stl.utils.is_discretizable(phi, dt) + phi2 = stl.utils.discretize(phi, dt) + phi3 = stl.utils.discretize(phi2, dt) + assert phi2 == phi3 + + phi = stl.parse('G[0.3, 1.2](F[0.6, 1.5](AP1))') + assert stl.utils.is_discretizable(phi, dt) + phi2 = stl.utils.discretize(phi, dt) + phi3 = stl.utils.discretize(phi2, dt) + assert phi2 == phi3 + + phi = stl.parse('G[0.3, 1.4](F[0.6, 1.5](AP1))') + assert not stl.utils.is_discretizable(phi, dt) + + phi = stl.parse('G[0.3, 1.2](F(AP1))') + assert not stl.utils.is_discretizable(phi, dt) + + phi = stl.parse('G[0.3, 1.2]((AP1) U (AP2))') + assert not stl.utils.is_discretizable(phi, dt) diff --git a/stl/utils.py b/stl/utils.py index e65598f..c2b8bb4 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -1,16 +1,16 @@ import operator as op from functools import reduce +from math import isfinite import traces +import numpy as np from lenses import bind import stl.ast -from stl.ast import (And, F, G, Interval, LinEq, Neg, - Or, Next, Until, AtomicPred, - _Top, _Bot) +from stl.ast import (And, F, G, Interval, LinEq, Neg, Or, Next, Until, + AtomicPred, _Top, _Bot) from stl.types import STL - oo = float('inf') @@ -67,7 +67,7 @@ def const_trace(x, start=0): def eval_lineq(lineq, x, domain, compact=True): - lhs = sum(const_trace(term.coeff)*x[term.id] for term in lineq.terms) + lhs = sum(const_trace(term.coeff) * x[term.id] for term in lineq.terms) compare = op_lookup.get(lineq.op) output = lhs.operation(const_trace(lineq.const), compare) output.domain = domain @@ -98,6 +98,48 @@ def implicit_validity_domain(phi, trace): return oracle, order +# Code to discretize a bounded STL formula + + +def discretize(phi, dt): + assert is_discretizable(phi, dt) + return _discretize(phi, dt) + + +def _discretize(phi, dt): + if isinstance(phi, (LinEq, AtomicPred)): + return phi + + children = tuple(_discretize(arg, dt) for arg in phi.children) + if isinstance(phi, (And, Or)): + return bind(phi).args.set(children) + elif isinstance(phi, (Neg, Next)): + return bind(phi).arg.set(children[0]) + + # Only remaining cases are G and F + psi = children[0] + l, u = round(phi.interval.lower / dt), round(phi.interval.upper / dt) + psis = (next(psi, i) for i in range(l, u + 1)) + opf = andf if isinstance(phi, G) else orf + return opf(*psis) + + +def _interval_discretizable(itvl, dt): + l, u = itvl.lower / dt, itvl.upper / dt + if not (isfinite(l) and isfinite(u)): + return False + return np.isclose(l, round(l)) and np.isclose(u, round(u)) + + +def is_discretizable(phi, dt): + if any(c for c in phi.walk() if isinstance(c, Until)): + return False + + return all( + _interval_discretizable(c.interval, dt) for c in phi.walk() + if isinstance(c, (F, G))) + + # EDSL @@ -129,5 +171,11 @@ def iff(x, y): return (x & y) | (~x & ~y) +def next(phi, i=1): + for _ in range(i): + phi = Next(phi) + return phi + + def timed_until(phi, psi, lo, hi): return env(psi, lo=lo, hi=hi) & alw(stl.ast.Until(phi, psi), lo=0, hi=lo)