From 70022468508fe2935ed12a576d76b3bfe7b315e6 Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Mon, 24 Sep 2018 17:11:24 -0700 Subject: [PATCH] document utilities and python api --- README.md | 92 +++++++++++++++++++++++++++++++++++++++++++++-- mtl/__init__.py | 1 - mtl/ast.py | 11 ++++++ mtl/parser.py | 19 +++++----- mtl/test_utils.py | 50 +++++++++++++------------- mtl/utils.py | 42 +++------------------- 6 files changed, 139 insertions(+), 76 deletions(-) diff --git a/README.md b/README.md index 118f2ee..3597e83 100644 --- a/README.md +++ b/README.md @@ -71,16 +71,102 @@ phi2 = mtl.parse('G(x & y)') # Note that since `U` is binary, it requires parens. phi3 = mtl.parse('(x U y)') +# Weak until (`y` never has to hold). +phi4 = mtl.parse('(x W y)') + # Whenever `x` holds, then `y` holds in the next two time units. -phi4 = mtl.parse('G(x -> F[0, 2] y)') +phi5 = mtl.parse('G(x -> F[0, 2] y)') # We also support timed until. -phi5 = mtl.parse('(a U[0, 2] b)') +phi6 = mtl.parse('(a U[0, 2] b)') # Finally, if time is discretized, we also support the next operator. # Thus, LTL can also be modeled. # `a` holds in two time steps. -phi6 = mtl.parse('XX a') +phi7 = mtl.parse('XX a') +``` + +## Modal Logic (using python syntax) + +```python +a, b = mtl.parse('a'), mtl.parse('b') + +# Eventually `a` will hold. +phi1 = a.eventually() + +# `a & b` will always hold. +phi2 = (a & b).always() + +# `a` until `b` +phi3 = a.until() + +# `a` weak until `b` +phi4 = a.weak_until(b) + +# Whenever `a` holds, then `b` holds in the next two time units. +phi5 = (a.implies(b.eventually(lo=0, hi=2))).always() + +# We also support timed until. +phi6 = a.timed_until(b, lo=0, hi=2) + +# `a` holds in two time steps. +phi7 = a >> 2 +``` + +## Boolean Evaluation +```python +# Assumes piece wise constant interpolation. +data = { + 'a': [(0, True), (1, False), (3, False)] + 'b': [(0, False), (0.2, True), (4, False)] +} + +phi = mtl.parse('F(a | b)') +print(phi(data, quantitative=False)) +# output: True + +# Evaluate at t=3 +print(phi(data, t=3, quantitative=False)) +# output: False + +# Evaluate with discrete time +phi = mtl.parse('X b') +print(phi(data, dt=0.2, quantitative=False)) +# output: True +``` + +## Quantitative Evaluate +```python +# Assumes piece wise constant interpolation. +data = { + 'a': [(0, 100), (1, -1), (3, -2)] + 'b': [(0, 20), (0.2, 2), (4, -10)] +} + +phi = mtl.parse('F(a | b)') +print(phi(data)) +# output: 100 + +# Evaluate at t=3 +print(phi(data, t=3)) +# output: 2 + +# Evaluate with discrete time +phi = mtl.parse('X b') +print(phi(data, dt=0.2)) +# output: 2 +``` + +## Utilities +```python +import mtl +from mtl import utils + +print(utils.scope(mtl.parse('XX a'), dt=0.1)) +# output: 0.2 + +print(utils.discretize(mtl.parse('F[0, 0.2] a'), dt=0.1)) +# output: (a | X a | XX a) ``` [1]: https://link.springer.com/chapter/10.1007/BFb0031988 diff --git a/mtl/__init__.py b/mtl/__init__.py index a739cbd..aaf4863 100644 --- a/mtl/__init__.py +++ b/mtl/__init__.py @@ -3,4 +3,3 @@ from mtl.ast import TOP, BOT from mtl.ast import (Interval, And, G, Neg, AtomicPred, WeakUntil, Next) from mtl.parser import parse -from mtl.utils import alw, env, andf, orf, until diff --git a/mtl/ast.py b/mtl/ast.py index 2abc84d..8550837 100644 --- a/mtl/ast.py +++ b/mtl/ast.py @@ -6,6 +6,8 @@ import attr import funcy as fn from lenses import bind +from mtl import sugar + def flatten_binary(phi, op, dropT, shortT): def f(x): @@ -109,6 +111,7 @@ class Param(NamedTuple): def ast_class(cls): + cls.__xor__ = sugar.xor cls.__or__ = _or cls.__and__ = _and cls.__invert__ = _neg @@ -119,6 +122,14 @@ def ast_class(cls): cls.params = property(_params) cls.atomic_predicates = property(_atomic_predicates) cls.evolve = attr.evolve + cls.iff = sugar.iff + cls.implies = sugar.implies + # Avoid circular dependence. + cls.weak_until = lambda a, b: WeakUntil(a, b) + cls.until = sugar.until + cls.timed_until = sugar.timed_until + cls.always = sugar.alw + cls.eventually = sugar.env if not hasattr(cls, "children"): cls.children = property(lambda _: ()) diff --git a/mtl/parser.py b/mtl/parser.py index 7ff8b73..2dfc857 100644 --- a/mtl/parser.py +++ b/mtl/parser.py @@ -4,8 +4,7 @@ from functools import partialmethod, reduce from parsimonious import Grammar, NodeVisitor from mtl import ast -from mtl.utils import iff, implies, xor, timed_until, until -from mtl.utils import env, alw +from mtl import sugar MTL_GRAMMAR = Grammar(u''' phi = (neg / paren_phi / next / bot / top @@ -81,10 +80,10 @@ class MTLVisitor(NodeVisitor): visit_xor_inner = binop_inner visit_and_outer = partialmethod(binop_outer, binop=op.and_) - visit_iff_outer = partialmethod(binop_outer, binop=iff) - visit_implies_outer = partialmethod(binop_outer, binop=implies) + visit_iff_outer = partialmethod(binop_outer, binop=sugar.iff) + visit_implies_outer = partialmethod(binop_outer, binop=sugar.implies) visit_or_outer = partialmethod(binop_outer, binop=op.or_) - visit_xor_outer = partialmethod(binop_outer, binop=xor) + visit_xor_outer = partialmethod(binop_outer, binop=sugar.xor) def generic_visit(self, _, children): return children @@ -115,20 +114,20 @@ class MTLVisitor(NodeVisitor): lo, hi = self.default_interval if not i else i[0] return op(phi, lo=lo, hi=hi) - visit_f = partialmethod(unary_temp_op_visitor, op=env) - visit_g = partialmethod(unary_temp_op_visitor, op=alw) + visit_f = partialmethod(unary_temp_op_visitor, op=sugar.env) + visit_g = partialmethod(unary_temp_op_visitor, op=sugar.alw) def visit_weak_until(self, _, children): _, _, phi1, _, _, _, phi2, _, _ = children - return ast.WeakUntil(phi1, phi2) + return phi1.weak_until(phi2) def visit_until(self, _, children): _, _, phi1, _, _, _, phi2, _, _ = children - return until(phi1, phi2) + return phi1.until(phi2) def visit_timed_until(self, _, children): _, _, phi1, _, _, itvl, _, phi2, _, _ = children - return timed_until(phi1, phi2, itvl.lower, itvl.upper) + return phi1.timed_until(phi2, itvl.lower, itvl.upper) def visit_id(self, name, _): return name.text diff --git a/mtl/test_utils.py b/mtl/test_utils.py index 0fe875d..5314572 100644 --- a/mtl/test_utils.py +++ b/mtl/test_utils.py @@ -1,4 +1,6 @@ import mtl +from mtl import utils +from mtl import sugar from mtl.hypothesis import MetricTemporalLogicStrategy from hypothesis import given @@ -28,49 +30,49 @@ def test_inline_context(phi): @given(MetricTemporalLogicStrategy, MetricTemporalLogicStrategy) def test_timed_until_smoke_test(phi1, phi2): - mtl.utils.timed_until(phi1, phi2, lo=2, hi=20) + sugar.timed_until(phi1, phi2, lo=2, hi=20) def test_discretize(): dt = 0.3 phi = mtl.parse('@ ap1') - assert mtl.utils.is_discretizable(phi, dt) - phi2 = mtl.utils.discretize(phi, dt) - phi3 = mtl.utils.discretize(phi2, dt) + assert utils.is_discretizable(phi, dt) + phi2 = utils.discretize(phi, dt) + phi3 = utils.discretize(phi2, dt) assert phi2 == phi3 phi = mtl.parse('G[0.3, 1.2] F[0.6, 1.5] ap1') - assert mtl.utils.is_discretizable(phi, dt) - phi2 = mtl.utils.discretize(phi, dt) - phi3 = mtl.utils.discretize(phi2, dt) + assert utils.is_discretizable(phi, dt) + phi2 = utils.discretize(phi, dt) + phi3 = utils.discretize(phi2, dt) assert phi2 == phi3 phi = mtl.parse('G[0.3, 1.4] F[0.6, 1.5] ap1') - assert not mtl.utils.is_discretizable(phi, dt) + assert not utils.is_discretizable(phi, dt) phi = mtl.parse('G[0.3, 1.2] F ap1') - assert not mtl.utils.is_discretizable(phi, dt) + assert not utils.is_discretizable(phi, dt) phi = mtl.parse('G[0.3, 1.2] (ap1 U ap2)') - assert not mtl.utils.is_discretizable(phi, dt) + assert not utils.is_discretizable(phi, dt) phi = mtl.parse('G[0.3, 0.6] ~F[0, 0.3] a') - assert mtl.utils.is_discretizable(phi, dt) - phi2 = mtl.utils.discretize(phi, dt, distribute=True) - phi3 = mtl.utils.discretize(phi2, dt, distribute=True) + assert utils.is_discretizable(phi, dt) + phi2 = utils.discretize(phi, dt, distribute=True) + phi3 = utils.discretize(phi2, dt, distribute=True) assert phi2 == phi3 phi = mtl.TOP - assert mtl.utils.is_discretizable(phi, dt) - phi2 = mtl.utils.discretize(phi, dt) - phi3 = mtl.utils.discretize(phi2, dt) + assert utils.is_discretizable(phi, dt) + phi2 = utils.discretize(phi, dt) + phi3 = utils.discretize(phi2, dt) assert phi2 == phi3 phi = mtl.BOT - assert mtl.utils.is_discretizable(phi, dt) - phi2 = mtl.utils.discretize(phi, dt) - phi3 = mtl.utils.discretize(phi2, dt) + assert utils.is_discretizable(phi, dt) + phi2 = utils.discretize(phi, dt) + phi3 = utils.discretize(phi2, dt) assert phi2 == phi3 @@ -78,16 +80,16 @@ def test_scope(): dt = 0.3 phi = mtl.parse('@ap1') - assert mtl.utils.scope(phi, dt) == 0.3 + assert utils.scope(phi, dt) == 0.3 phi = mtl.parse('(@@ap1 | ap2)') - assert mtl.utils.scope(phi, dt) == 0.6 + assert utils.scope(phi, dt) == 0.6 phi = mtl.parse('G[0.3, 1.2] F[0.6, 1.5] ap1') - assert mtl.utils.scope(phi, dt) == 1.2 + 1.5 + assert utils.scope(phi, dt) == 1.2 + 1.5 phi = mtl.parse('G[0.3, 1.2] F ap1') - assert mtl.utils.scope(phi, dt) == float('inf') + assert utils.scope(phi, dt) == float('inf') phi = mtl.parse('G[0.3, 1.2] (ap1 U ap2)') - assert mtl.utils.scope(phi, dt) == float('inf') + assert utils.scope(phi, dt) == float('inf') diff --git a/mtl/utils.py b/mtl/utils.py index 28a7fea..e2591b2 100644 --- a/mtl/utils.py +++ b/mtl/utils.py @@ -70,7 +70,7 @@ def _discretize(phi, dt, horizon): upper = min(phi.interval.upper, horizon) l, u = round(phi.interval.lower / dt), round(upper / dt) - psis = (next(_discretize(phi.arg, dt, horizon - i), i) + psis = (_discretize(phi.arg, dt, horizon - i) >> i for i in range(l, u + 1)) opf = andf if isinstance(phi, G) else orf return opf(*psis) @@ -85,7 +85,7 @@ def _interval_discretizable(itvl, dt): def _distribute_next(phi, i=0): if isinstance(phi, AtomicPred): - return mtl.utils.next(phi, i=i) + return phi >> i elif isinstance(phi, Next): return _distribute_next(phi.arg, i=i+1) @@ -105,44 +105,10 @@ def is_discretizable(phi, dt): _interval_discretizable(c.interval, dt) for c in phi.walk() if isinstance(c, G)) -# EDSL - - -def alw(phi, *, lo=0, hi=float('inf')): - return G(Interval(lo, hi), phi) - - -def env(phi, *, lo=0, hi=float('inf')): - return ~alw(~phi, lo=lo, hi=hi) - def andf(*args): - return reduce(op.and_, args) if args else mtl.TOP + return reduce(op.and_, args) if args else ast.TOP def orf(*args): - return reduce(op.or_, args) if args else mtl.TOP - - -def implies(x, y): - return ~x | y - - -def xor(x, y): - return (x | y) & ~(x & y) - - -def iff(x, y): - return (x & y) | (~x & ~y) - - -def next(phi, i=1): - return phi >> i - - -def until(phi, psi): - return mtl.ast.WeakUntil(phi, psi) & env(psi) - - -def timed_until(phi, psi, lo, hi): - return env(psi, lo=lo, hi=hi) & alw(until(phi, psi), lo=0, hi=lo) + return reduce(op.or_, args) if args else ast.TOP