diff --git a/mtl/sugar.py b/mtl/sugar.py new file mode 100644 index 0000000..54db20d --- /dev/null +++ b/mtl/sugar.py @@ -0,0 +1,29 @@ +from mtl import ast + + +def alw(phi, *, lo=0, hi=float('inf')): + return ast.G(ast.Interval(lo, hi), phi) + + +def env(phi, *, lo=0, hi=float('inf')): + return ~alw(~phi, lo=lo, hi=hi) + + +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 until(phi, psi): + return 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) diff --git a/mtl/test_boolean_eval.py b/mtl/test_boolean_eval.py index 7c5ed64..fb4cbad 100644 --- a/mtl/test_boolean_eval.py +++ b/mtl/test_boolean_eval.py @@ -55,5 +55,5 @@ def test_temporal_identity4(phi): @given(MetricTemporalLogicStrategy) def test_temporal_identity5(phi): - assert mtl.until(mtl.TOP, phi)(x, 0, quantitative=False) \ - == mtl.env(phi)(x, 0, quantitative=False) + assert mtl.TOP.until(phi)(x, 0, quantitative=False) \ + == phi.eventually()(x, 0, quantitative=False) diff --git a/mtl/utils.py b/mtl/utils.py index e2591b2..25e5da0 100644 --- a/mtl/utils.py +++ b/mtl/utils.py @@ -5,8 +5,8 @@ from math import isfinite from discrete_signals import signal import numpy as np -import mtl.ast -from mtl.ast import (And, G, Interval, Neg, Next, WeakUntil, +from mtl import ast +from mtl.ast import (And, G, Neg, Next, WeakUntil, AtomicPred, _Bot) oo = float('inf')