rename module to fosco

cegis_cbf/cbf.py → fosco/cbf.py

@@ -5,11 +5,11 @@
 import torch
 from torch.optim import Optimizer
 
-from cegis_cbf.common.domains import Set, Rectangle
-from cegis_cbf.common.consts import DomainNames
-from cegis_cbf.common.utils import _set_assertion
-from cegis_cbf.learner import LearnerNN, LearnerCT
-from cegis_cbf.verifier import SYMBOL
+from fosco.common.domains import Set, Rectangle
+from fosco.common.consts import DomainNames
+from fosco.common.utils import _set_assertion
+from fosco.learner import LearnerNN, LearnerCT
+from fosco.verifier import SYMBOL
 from systems import ControlAffineControllableDynamicalModel
 
 XD = DomainNames.XD.value

cegis_cbf/cegis.py → fosco/cegis.py

@@ -6,19 +6,19 @@
 
 import matplotlib.pyplot as plt
 
-from cegis_cbf.cbf import ControlBarrierFunction
-from cegis_cbf.common.formatter import CustomFormatter
-from cegis_cbf.common.plotting import benchmark_3d
-from cegis_cbf.consolidator import make_consolidator
-from cegis_cbf.common.consts import (
+from fosco.cbf import ControlBarrierFunction
+from fosco.common.formatter import CustomFormatter
+from fosco.common.plotting import benchmark_3d
+from fosco.consolidator import make_consolidator
+from fosco.common.consts import (
     CertificateType,
     TimeDomain,
     ActivationType,
     VerifierType,
 )
-from cegis_cbf.learner import make_learner, LearnerNN
-from cegis_cbf.translator import make_translator
-from cegis_cbf.verifier import make_verifier
+from fosco.learner import make_learner, LearnerNN
+from fosco.translator import make_translator
+from fosco.verifier import make_verifier
 from systems import ControlAffineControllableDynamicalModel
 
 CegisResult = namedtuple("CegisResult", ["found", "net", "infos"])
@@ -32,7 +32,7 @@ class CegisConfig:
     SYSTEM: Type[ControlAffineControllableDynamicalModel] = None
     DOMAINS: dict[str, Any] = None
     TIME_DOMAIN: TimeDomain = TimeDomain.CONTINUOUS
-    # cegis_cbf
+    # fosco
     CERTIFICATE: CertificateType = CertificateType.CBF
     VERIFIER: VerifierType = VerifierType.Z3
     CEGIS_MAX_ITERS: int = 10
@@ -233,5 +233,5 @@ def _assert_state(self):
         assert self.config.CEGIS_MAX_ITERS > 0
         assert (
             self.x is self.verifier.xs
-        ), "expected same variables in cegis_cbf and verifier"
+        ), "expected same variables in fosco and verifier"
         self.certificate._assert_state(self.domains, self.datasets)

cegis_cbf/common/activations.py → fosco/common/activations.py

@@ -1,6 +1,6 @@
 import torch
 
-from cegis_cbf.common import consts
+from fosco.common import consts
 
 
 # Activation function

cegis_cbf/common/activations_symbolic.py → fosco/common/activations_symbolic.py

@@ -7,7 +7,7 @@
 import numpy as np
 import z3
 
-from cegis_cbf.common import consts
+from fosco.common import consts
 
 
 def activation_sym(select, p):

cegis_cbf/common/domains.py → fosco/common/domains.py

@@ -5,9 +5,9 @@
 from matplotlib import pyplot as plt
 from mpl_toolkits.mplot3d import art3d
 
-from cegis_cbf import verifier
-from cegis_cbf.common.plotting import get_plot_colour
-from cegis_cbf.common.utils import round_init_data, square_init_data
+from fosco import verifier
+from fosco.common.plotting import get_plot_colour
+from fosco.common.utils import round_init_data, square_init_data
 
 
 class Set:

cegis_cbf/learner.py → fosco/learner.py

@@ -5,9 +5,9 @@
 import torch
 from torch import nn
 
-from cegis_cbf.common.activations import activation
-from cegis_cbf.common.consts import ActivationType, TimeDomain
-from cegis_cbf.models.network import MLP
+from fosco.common.activations import activation
+from fosco.common.consts import ActivationType, TimeDomain
+from fosco.models.network import MLP
 
 
 class LearnerNN(nn.Module):

cegis_cbf/models/network.py → fosco/models/network.py

@@ -1,7 +1,7 @@
 from torch import nn
 
-from cegis_cbf.common.activations import activation
-from cegis_cbf.common.consts import ActivationType
+from fosco.common.activations import activation
+from fosco.common.consts import ActivationType
 
 
 class MLP(nn.Module):

cegis_cbf/translator.py → fosco/translator.py

@@ -4,10 +4,10 @@
 import numpy as np
 import z3
 
-from cegis_cbf.common.activations_symbolic import activation_sym, activation_der_sym
-from cegis_cbf.common.consts import VerifierType, TimeDomain
-from cegis_cbf.models.network import MLP
-from cegis_cbf.verifier import SYMBOL
+from fosco.common.activations_symbolic import activation_sym, activation_der_sym
+from fosco.common.consts import VerifierType, TimeDomain
+from fosco.models.network import MLP
+from fosco.verifier import SYMBOL
 
 
 class Translator(ABC):

cegis_cbf/verifier.py → fosco/verifier.py

@@ -5,8 +5,8 @@
 import torch
 import z3
 
-from cegis_cbf.common.utils import contains_object
-from cegis_cbf.common.consts import VerifierType
+from fosco.common.utils import contains_object
+from fosco.common.consts import VerifierType
 
 SYMBOL = z3.ArithRef
 INF: float = 1e300

run_example.py

@@ -4,11 +4,11 @@
 import torch
 from matplotlib import pyplot as plt
 
-import cegis_cbf.cegis
-from cegis_cbf.common import domains
-from cegis_cbf.common.consts import ActivationType
-from cegis_cbf.common.consts import CertificateType, TimeDomain, VerifierType
-from cegis_cbf.common.plotting import benchmark_3d
+import fosco.cegis
+from fosco.common import domains
+from fosco.common.consts import ActivationType
+from fosco.common.consts import CertificateType, TimeDomain, VerifierType
+from fosco.common.plotting import benchmark_3d
 from systems import make_system
 
 
@@ -72,7 +72,7 @@ def main():
         "unsafe": lambda n: XU.generate_data(n),
     }
 
-    config = cegis_cbf.cegis.CegisConfig(
+    config = fosco.cegis.CegisConfig(
         SYSTEM=system,
         DOMAINS=sets,
         DATA_GEN=data_gen,
@@ -85,7 +85,7 @@ def main():
         N_DATA=n_data_samples,
         SEED=seed,
     )
-    cegis = cegis_cbf.cegis.Cegis(config=config, verbose=verbose)
+    cegis = fosco.cegis.Cegis(config=config, verbose=verbose)
 
     result = cegis.solve()
 

systems/system.py

@@ -4,7 +4,7 @@
 import torch
 import z3
 
-from cegis_cbf.common.utils import contains_object
+from fosco.common.utils import contains_object
 
 
 class ControlAffineControllableDynamicalModel:

tests/test_cegis.py

@@ -3,9 +3,9 @@
 
 import torch
 
-from cegis_cbf.cegis import CegisConfig, Cegis
-from cegis_cbf.common.domains import Rectangle, Sphere
-from cegis_cbf.common.consts import (
+from fosco.cegis import CegisConfig, Cegis
+from fosco.common.domains import Rectangle, Sphere
+from fosco.common.consts import (
     TimeDomain,
     ActivationType,
     VerifierType,

tests/test_domains.py

@@ -1,6 +1,6 @@
 import unittest
 
-from cegis_cbf.common import domains
+from fosco.common import domains
 
 
 class TestDomains(unittest.TestCase):

tests/test_translator.py

@@ -3,9 +3,9 @@
 import numpy as np
 import torch
 
-from cegis_cbf.models.network import MLP
-from cegis_cbf.translator import MLPZ3Translator, make_translator
-from cegis_cbf.verifier import VerifierZ3
+from fosco.models.network import MLP
+from fosco.translator import MLPZ3Translator, make_translator
+from fosco.verifier import VerifierZ3
 
 
 class TestTranslator(unittest.TestCase):
@@ -70,8 +70,8 @@ def test_separation_symbolic_functions(self):
         ), f"Wrong symbolic formula for Vdot, got {expr_nndot}"
 
     def test_factory(self):
-        from cegis_cbf.common.consts import VerifierType
-        from cegis_cbf.common.consts import TimeDomain
+        from fosco.common.consts import VerifierType
+        from fosco.common.consts import TimeDomain
 
         translator = make_translator(
             verifier_type=VerifierType.Z3, time_domain=TimeDomain.CONTINUOUS

tests/test_verifier.py

@@ -1,8 +1,8 @@
 import unittest
 
 
-from cegis_cbf.common.consts import VerifierType
-from cegis_cbf.verifier import make_verifier, Verifier, SYMBOL
+from fosco.common.consts import VerifierType
+from fosco.verifier import make_verifier, Verifier, SYMBOL
 
 
 class TestVerifier(unittest.TestCase):