teaching/mtl-aas
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

correct lipshitz bound for stl predicates

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2017-03-20 11:59:34 -07:00
parent 6489667970
commit 0d4a703dcc
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
stl/utils.py
View file

@ -121,12 +121,12 @@ def from_mtl(phi:MTL, ap_map:Dict[AtomicPred, LinEq]) -> STL:
focus = AP_lens(phi)
return focus.modify(ap_map.get)
def _lineq_lipschitz(lineq):
return sum(map(abs, lens(lineq).terms.each_().coeff.get_all()))
def linear_stl_lipschitz(phi):
r = max(abs(c) for c in terms_lens(phi).coeff.get_all())
try:
return float(r)
except TypeError:
return r
"""Infinity norm lipschitz bound of linear inequality predicate."""
return float(max(map(_lineq_lipschitz, lineq_lens(phi).get_all())))
# EDSL