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

added stl lipschitz computation bound

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2017-03-18 18:10:51 -07:00
parent 16084f83c0
commit eeb543fa34
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
stl/utils.py
View file

@ -121,6 +121,15 @@ def from_mtl(phi:MTL, ap_map:Dict[AtomicPred, LinEq]) -> STL:
focus = AP_lens(phi) focus = AP_lens(phi)
return focus.modify(ap_map.get) return focus.modify(ap_map.get)
def lineq_lipschitz(lineq):
"""1 norm lipschitz bound of linear inequality predicate."""
return sum(map(abs, lens(lineq).terms.each_().coeff.get_all()))
def linear_stl_lipschitz(phi):
return max(map(lineq_lipschitz, lineq_lens(phi).get_all()))
# EDSL # EDSL
def alw(phi, *, lo, hi): def alw(phi, *, lo, hi):