From 2c34d9dc7a0816c1870eca6f3a54db141253079d Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Wed, 22 Nov 2017 12:21:44 -0800 Subject: [PATCH] added code to get scope of stl formula --- stl/test_utils.py | 16 ++++++++++++++++ stl/utils.py | 24 ++++++++++++++++++++++-- 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/stl/test_utils.py b/stl/test_utils.py index e02324c..09a7b78 100644 --- a/stl/test_utils.py +++ b/stl/test_utils.py @@ -85,3 +85,19 @@ def test_discretize(): phi = stl.parse('G[0.3, 1.2]((AP1) U (AP2))') assert not stl.utils.is_discretizable(phi, dt) + + +def test_scope(): + dt = 0.3 + + phi = stl.parse('X(AP1)') + assert stl.utils.scope(phi, dt) == 0.3 + + phi = stl.parse('G[0.3, 1.2](F[0.6, 1.5](AP1))') + assert stl.utils.scope(phi, dt) == 1.2 + 1.5 + + phi = stl.parse('G[0.3, 1.2](F(AP1))') + assert stl.utils.scope(phi, dt) == float('inf') + + phi = stl.parse('G[0.3, 1.2]((AP1) U (AP2))') + assert stl.utils.scope(phi, dt) == float('inf') diff --git a/stl/utils.py b/stl/utils.py index c2b8bb4..a9171a6 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -1,5 +1,5 @@ import operator as op -from functools import reduce +from functools import reduce, wraps from math import isfinite import traces @@ -98,11 +98,31 @@ def implicit_validity_domain(phi, trace): return oracle, order +def require_discretizable(func): + @wraps(func) + def _func(phi, dt, *args, **kwargs): + assert is_discretizable(phi, dt) + return func(phi, dt, *args, **kwargs) + + return _func + + +def scope(phi, dt, *, _t=0): + if isinstance(phi, Next): + _t += dt + elif isinstance(phi, (G, F)): + _t += phi.interval.upper + elif isinstance(phi, Until): + _t += float('inf') + + return max((scope(c, dt, _t=_t) for c in phi.children), default=_t) + + # Code to discretize a bounded STL formula +@require_discretizable def discretize(phi, dt): - assert is_discretizable(phi, dt) return _discretize(phi, dt)