Make the repository pip install-able

demo.ipynb

@@ -18,9 +18,9 @@
    "outputs": [],
    "source": [
     "import stlcg\n",
-    "import stlviz as viz\n",
+    "import stlcg.stlviz as viz\n",
     "from stlcg import Expression\n",
-    "from utils import print_learning_progress"
+    "from stlcg.utils import print_learning_progress"
    ]
   },
   {

examples/VAE.ipynb

@@ -16,7 +16,7 @@
     "import numpy as np\n",
     "from abc import ABC, abstractmethod\n",
     "import stlcg \n",
-    "import stlviz \n",
+    "import stlcg.stlviz as stlviz \n",
     "\n",
     "import matplotlib.pyplot as plt\n",
     "from ipywidgets import interact, interactive, fixed, interact_manual\n",

examples/pstl.py

@@ -1,39 +1,43 @@
 import sys
-sys.path.append('../src')
-import matplotlib.pyplot as plt
-import numpy as np
+
+sys.path.append("../src")
 import os
 import pickle
-import torch
-import stlcg
 
+import matplotlib.pyplot as plt
+import numpy as np
 import scipy.io
+import torch
+
+import stlcg
 
-mat = scipy.io.loadmat('models/clustering_data.mat')
+mat = scipy.io.loadmat("models/clustering_data.mat")
 
-ys_ = mat['ys']
+ys_ = mat["ys"]
 ys = np.zeros(ys_.shape)
-ys[:,:] = np.fliplr(ys_)
-t = mat['T'][0,:]
+ys[:, :] = np.fliplr(ys_)
+t = mat["T"][0, :]
 N = ys.shape[0]
 
+
 def run_multiple_times(num, func, ys):
     for i in range(num):
         func(ys, save_filename=None)
 
+
 def binary_search_settling(ys, save_filename="models/pstl_settling_binary_search.npy"):
     ϵ_list = []
     N = ys.shape[0]
     for i in range(N):
-        y = torch.as_tensor(ys[i:i+1,:]).float().unsqueeze(-1)
-        s = stlcg.Expression('s', torch.abs(y - 1))
+        y = torch.as_tensor(ys[i : i + 1, :]).float().unsqueeze(-1)
+        s = stlcg.Expression("s", torch.abs(y - 1))
         ϵL = torch.as_tensor(np.zeros([1, 1, 1])).float().requires_grad_(True)
         ϵU = torch.as_tensor(np.ones([1, 1, 1])).float().requires_grad_(True)
         ϵ = torch.as_tensor(np.ones([1, 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) > 5*1E-3:
+        ϕ = stlcg.Always(subformula=(s < ϵ), interval=[50, 100])
+        while torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5 * 1e-3:
             ϵ = 0.5 * (ϕU.subformula.val + ϕL.subformula.val)
             ϕ.subformula.val = ϵ
             r = ϕ.robustness(s).squeeze()
@@ -47,29 +51,39 @@ 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))
+    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:
+    ϕ = 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)
+        ϕ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
     N = ys.shape[0]
     y = torch.as_tensor(ys).float().unsqueeze(-1)
-    s = stlcg.Expression('s', torch.abs(y - 1))
+    s = stlcg.Expression("s", torch.abs(y - 1))
     ϵ = torch.as_tensor(np.zeros([N, 1, 1])).float().requires_grad_(True)
     ϕ = stlcg.Always(subformula=(s < ϵ), interval=[50, 100])
 
@@ -79,7 +93,7 @@ def stlcg_settling(ys, save_filename="models/pstl_settling_stlcg.npy"):
         loss.backward()
 
         with torch.no_grad():
-            ϵ -= 0.005* ϵ.grad
+            ϵ -= 0.005 * ϵ.grad
 
         ϵ.grad.zero_()
         if loss == 0:
@@ -89,19 +103,21 @@ def stlcg_settling(ys, save_filename="models/pstl_settling_stlcg.npy"):
     np.save(save_filename, ϵ.squeeze().detach().numpy())
 
 
-def binary_search_overshoot(ys, save_filename="models/pstl_overshoot_binary_search.npy"):
+def binary_search_overshoot(
+    ys, save_filename="models/pstl_overshoot_binary_search.npy"
+):
     ϵ_list = []
     N = ys.shape[0]
     for i in range(N):
-        y = torch.as_tensor(ys[i:i+1,:]).float().unsqueeze(-1)
-        s = stlcg.Expression('s', y)
+        y = torch.as_tensor(ys[i : i + 1, :]).float().unsqueeze(-1)
+        s = stlcg.Expression("s", y)
         ϵL = torch.as_tensor(np.zeros([1, 1, 1])).float().requires_grad_(True)
-        ϵU = torch.as_tensor(2*np.ones([1, 1, 1])).float().requires_grad_(True)
+        ϵU = torch.as_tensor(2 * np.ones([1, 1, 1])).float().requires_grad_(True)
         ϵ = torch.as_tensor(np.ones([1, 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) > 5*1E-3:
+        ϕ = stlcg.Always(subformula=(s < ϵ))
+        while torch.abs(ϕU.subformula.val - ϕL.subformula.val) > 5 * 1e-3:
             ϵ = 0.5 * (ϕU.subformula.val + ϕL.subformula.val)
             ϕ.subformula.val = ϵ
             r = ϕ.robustness(s).squeeze()
@@ -114,30 +130,40 @@ 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)
+    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)
+    ϵ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:
+    ϕ = 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)
+        ϕ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]
     max_epoch = 1000
     y = torch.as_tensor(ys).float().unsqueeze(-1)
-    s = stlcg.Expression('s', y)
+    s = stlcg.Expression("s", y)
     ϵ = torch.as_tensor(np.zeros([N, 1, 1])).float().requires_grad_(True)
     ϕ = stlcg.Always(subformula=(s < ϵ))
     for epoch in range(max_epoch):
@@ -146,7 +172,7 @@ def stlcg_overshoot(ys, save_filename="models/pstl_overshoot_stlcg.npy"):
         loss.backward()
 
         with torch.no_grad():
-            ϵ -= 0.005* ϵ.grad
+            ϵ -= 0.005 * ϵ.grad
         if loss == 0:
             break
         ϵ.grad.zero_()
@@ -160,18 +186,17 @@ def stlcg_gpu_settling(ys, save_filename="models/pstl_settling_stlcg_gpu.npy"):
     max_epoch = 1000
     N = ys.shape[0]
     y = torch.as_tensor(ys).float().unsqueeze(-1).cuda()
-    s = stlcg.Expression('s', torch.abs(y - 1))
+    s = stlcg.Expression("s", torch.abs(y - 1))
     ϵ = torch.as_tensor(np.zeros([N, 1, 1])).float().cuda().requires_grad_(True)
     ϕ = stlcg.Always(subformula=(s < ϵ), interval=[50, 100])
 
-
     for epoch in range(max_epoch):
 
         loss = torch.relu(-ϕ.robustness(s).squeeze()).sum()
         loss.backward()
 
         with torch.no_grad():
-            ϵ -= 0.005* ϵ.grad
+            ϵ -= 0.005 * ϵ.grad
 
         ϵ.grad.zero_()
         if loss == 0:
@@ -180,11 +205,12 @@ def stlcg_gpu_settling(ys, save_filename="models/pstl_settling_stlcg_gpu.npy"):
         return ϵ.squeeze().cpu().detach().numpy()
     np.save(save_filename, ϵ.squeeze().cpu().detach().numpy())
 
+
 def stlcg_gpu_overshoot(ys, save_filename="models/pstl_overshoot_stlcg_gpu.npy"):
     N = ys.shape[0]
     max_epoch = 1000
     y = torch.as_tensor(ys).float().unsqueeze(-1).cuda()
-    s = stlcg.Expression('s', y)
+    s = stlcg.Expression("s", y)
     ϵ = torch.as_tensor(np.zeros([N, 1, 1])).float().cuda().requires_grad_(True)
     ϕ = stlcg.Always(subformula=(s < ϵ))
     for epoch in range(max_epoch):
@@ -193,7 +219,7 @@ def stlcg_gpu_overshoot(ys, save_filename="models/pstl_overshoot_stlcg_gpu.npy")
         loss.backward()
 
         with torch.no_grad():
-            ϵ -= 0.005* ϵ.grad
+            ϵ -= 0.005 * ϵ.grad
         if loss == 0:
             break
         ϵ.grad.zero_()
@@ -203,26 +229,30 @@ def stlcg_gpu_overshoot(ys, save_filename="models/pstl_overshoot_stlcg_gpu.npy")
     np.save(save_filename, ϵ.squeeze().cpu().detach().numpy())
 
 
-
 if __name__ == "__main__":
     arguments = sys.argv[1:]
     # func_i, M, num
     M = 500  # batch size
     num = 1  # number of repetitions
     func_i = int(sys.argv[1])
-    func_map = {1: stlcg_settling, 2: binary_search_settling, 3: stlcg_overshoot, 4: binary_search_overshoot, 5: stlcg_gpu_settling, 6: stlcg_gpu_overshoot}
+    func_map = {
+        1: stlcg_settling,
+        2: binary_search_settling,
+        3: stlcg_overshoot,
+        4: binary_search_overshoot,
+        5: stlcg_gpu_settling,
+        6: stlcg_gpu_overshoot,
+    }
     if len(arguments) == 2:
         M = int(sys.argv[2])
     elif len(arguments) == 3:
         M = int(sys.argv[2])
         num = int(sys.argv[3])
     # print(func_map[func_i].__name__, "  M=%i   num=%i"%(M,num))
 
-    mat = scipy.io.loadmat('models/clustering_data.mat')
+    mat = scipy.io.loadmat("models/clustering_data.mat")
 
-    ys_ = np.concatenate([mat['ys'], mat['ys'], mat['ys']], axis=0)[:M,:]
+    ys_ = np.concatenate([mat["ys"], mat["ys"], mat["ys"]], axis=0)[:M, :]
     ys = np.zeros(ys_.shape)
-    ys[:,:] = np.fliplr(ys_)
+    ys[:, :] = np.fliplr(ys_)
     run_multiple_times(num, func_map[func_i], ys)
-
-

pyproject.toml

@@ -0,0 +1,31 @@
+[build-system]
+requires = ["setuptools"]
+build-backend = "setuptools.build_meta"
+
+[project]
+name = "stlcg"
+version = "0.0.1"
+authors = [
+  { name = "Karen Leung", email = "[email protected]" },
+  { name = "Nikos Arechiga", email = "[email protected]" },
+]
+description = "A toolbox to compute the robustness of STL formulas using computations graphs (PyTorch)."
+readme = "README.md"
+
+classifiers = [
+  "Programming Language :: Python :: 3",
+  "License :: OSI Approved :: MIT License",
+  "Operating System :: OS Independent",
+]
+
+[project.urls]
+repository = "https://github.com/StanfordASL/stlcg"
+
+[tool.setuptools.packages.find]
+where = ["src"]
+
+[tool.isort]
+profile = "black"
+line_length = 88
+skip_gitignore = false
+group_by_package = true

src/stlcg/__init__.py

@@ -0,0 +1,41 @@
+from .stlcg import (
+    Always,
+    And,
+    Equal,
+    Eventually,
+    Expression,
+    GreaterThan,
+    Identity,
+    Implies,
+    Integral1d,
+    LessThan,
+    Maxish,
+    Minish,
+    Negation,
+    Or,
+    STL_Formula,
+    Temporal_Operator,
+    Then,
+    Until,
+)
+
+__all__ = [
+    "Always",
+    "And",
+    "Equal",
+    "Eventually",
+    "Expression",
+    "GreaterThan",
+    "Identity",
+    "Implies",
+    "Integral1d",
+    "LessThan",
+    "Maxish",
+    "Minish",
+    "Negation",
+    "Or",
+    "STL_Formula",
+    "Temporal_Operator",
+    "Then",
+    "Until",
+]