vectorized binary search

StanfordASL · Nov 6, 2021 · abd16c9 · abd16c9
1 parent 1af626f
commit abd16c9
Showing 1 changed file with 35 additions and 0 deletions.
diff --git a/examples/pstl.py b/examples/pstl.py
@@ -47,6 +47,23 @@ def binary_search_settling(ys, save_filename="models/pstl_settling_binary_search
         return np.stack(ϵ_list)
     np.save(save_filename, np.stack(ϵ_list))
 
+def binary_search_settling_vectorize(ys):
+    N = ys.shape[0]
+    y = torch.as_tensor(ys).float().unsqueeze(-1)
+    s = stlcg.Expression('s', torch.abs(y - 1))
+    ϵL = torch.as_tensor(np.zeros([N, 1, 1])).float().requires_grad_(True)
+    ϵU = torch.as_tensor(np.ones([N, 1, 1])).float().requires_grad_(True)
+    ϵ = torch.as_tensor(np.ones([N, 1, 1])).float().requires_grad_(True)
+    ϕL = stlcg.Always(subformula=(s < ϵL), interval=[50, 100])
+    ϕU = stlcg.Always(subformula=(s < ϵU), interval=[50, 100])
+    ϕ =  stlcg.Always(subformula=(s < ϵ), interval=[50, 100])
+    while torch.abs(ϕU.subformula.val - ϕL.subformula.val).max() > 5*1E-3:
+        ϵ = 0.5 * (ϕU.subformula.val + ϕL.subformula.val)
+        ϕ.subformula.val = ϵ
+        r = ϕ.robustness(s)
+        ϕU.subformula.val = torch.where(torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5*1E-3, torch.where(r > 0, ϵ, ϕU.subformula.val), ϕU.subformula.val)
+        ϕL.subformula.val = torch.where(torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5*1E-3, torch.where(r <= 0, ϵ, ϕL.subformula.val), ϕL.subformula.val)
+    return ϵ.squeeze().detach().numpy()
 
 def stlcg_settling(ys, save_filename="models/pstl_settling_stlcg.npy"):
     max_epoch = 1000
@@ -97,6 +114,24 @@ def binary_search_overshoot(ys, save_filename="models/pstl_overshoot_binary_sear
     if save_filename is None:
         return np.stack(ϵ_list)
     np.save(save_filename, np.stack(ϵ_list))
+
+def binary_search_overshoot_vectorize(ys):
+    N = ys.shape[0]
+    y = torch.as_tensor(ys).float().unsqueeze(-1)
+    s = stlcg.Expression('s', y)
+    ϵL = torch.as_tensor(np.zeros([N, 1, 1])).float().requires_grad_(True)
+    ϵU = torch.as_tensor(2*np.ones([N, 1, 1])).float().requires_grad_(True)
+    ϵ = torch.as_tensor(np.ones([N, 1, 1])).float().requires_grad_(True)
+    ϕL = stlcg.Always(subformula=(s < ϵL))
+    ϕU = stlcg.Always(subformula=(s < ϵU))
+    ϕ =  stlcg.Always(subformula=(s < ϵ))
+    while torch.abs(ϕU.subformula.val - ϕL.subformula.val).max() > 5*1E-3:
+        ϵ = 0.5 * (ϕU.subformula.val + ϕL.subformula.val)
+        ϕ.subformula.val = ϵ
+        r = ϕ.robustness(s)
+        ϕU.subformula.val = torch.where(torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5*1E-3, torch.where(r > 0, ϵ, ϕU.subformula.val), ϕU.subformula.val)
+        ϕL.subformula.val = torch.where(torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5*1E-3, torch.where(r <= 0, ϵ, ϕL.subformula.val), ϕL.subformula.val)
+    return ϵ.squeeze().detach().numpy()
 
 def stlcg_overshoot(ys, save_filename="models/pstl_overshoot_stlcg.npy"):
     N = ys.shape[0]