diff --git a/stl/__init__.py b/stl/__init__.py index a3574eb..fc7e15e 100644 --- a/stl/__init__.py +++ b/stl/__init__.py @@ -1,4 +1,5 @@ from stl.utils import terms_lens, lineq_lens, walk, tree, and_or_lens +from stl.utils import alw, env, andf, orf from stl.ast import dt_sym, t_sym from stl.ast import LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var, AtomicPred from stl.parser import parse diff --git a/stl/utils.py b/stl/utils.py index 83628c5..de7560f 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -1,5 +1,7 @@ from typing import List, Type, Dict, Mapping, T from collections import deque +import operator as op +from functools import reduce from lenses import lens, Lens import funcy as fn @@ -127,3 +129,19 @@ def to_mtl(phi:STL) -> MTL: def from_mtl(phi:MTL, ap_map:Dict[AtomicPred, LinEq]) -> STL: focus = AP_lens(phi) return focus.modify(ap_map.get) + + +def alw(phi, *, lo, hi): + return G(Interval(lo, hi), phi) + +def env(phi, *, lo, hi): + return F(Interval(lo, hi), phi) + +def until(phi, *, lo, hi): + raise NotImplementedError + +def andf(*args): + return reduce(op.and_, args) + +def orf(): + return reduce(op.or_, args)