document utilities and python api
This commit is contained in:
Marcell Vazquez-Chanlatte
parent
aa6ebbfc67
commit
7002246850
6 changed files with 139 additions and 76 deletions
92
README.md
92
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
11
mtl/ast.py
11
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 _: ())
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
42
mtl/utils.py
42
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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue