Merge branch 'master'

README.md

@@ -2,22 +2,15 @@
 
 FOSSIL is a software tool for the sound and automated synthesis of Lyapunov functions and Barrier certificates, for the purposes of verifying the stability or safety of continuous-time dynamical systems modelled as differential equations. The tool leverages a CEGIS-based architecture; the verision 1.0 tool is described in detail by a corresponding [tool paper](https://doi.org/10.1145/3447928.3456646) (also [below](#citation)).
 
-*If you are a repeatability reviewer, please see the [repeatability instructions](repeatability_instructions.md).*
-
 ## Requirements
 
-Install:
-
-> python3 python3-pip curl
-
-On Ubuntu 22.04 you can do it with: `sudo apt-get install -y python3 python3-pip curl`
-
+Fossil 2.0 requires Python 3.9 or later.
 We recommend dReal as an SMT solver. Since we rely on dReal's python interface, dReal's prerequisites must be installed as well. These include Bazel, which must be built from source. dReal provide scripts to install the prerequisites on Ubuntu 18.04, 20.04 and 22.04.
 
 dReal instructions available [on their GitHub repository](https://github.com/dreal/dreal4). The prerequisites for Ubuntu 22.04 can be installed with:
 
 ```console
-curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/20.04/install.sh | sudo bash
+curl -fsSL https://raw.githubusercontent.com/dreal/dreal4/master/setup/ubuntu/22.04/install_prereqs.sh | sudo bash
 ```
 
 Once dReal is installed, you can install the python interface for Fossil 2.0 using:
@@ -35,9 +28,64 @@ We provide a Docker image of Fossil 2.0 . Begin by installing Docker on your sys
 # docer run --rm aleccedwards/fossil fossil -h
 ```
 
-## Citation
+## Command-line Interface
+
+Fossil 2.0 provides a command-line interface, which relies on yaml files to specify the configuration of the synthesis problem. The following configuration
+file specifies a stability verification problem for a continuous-time model with two variables, and a neural network with two hidden layers of 5 neurons each.
+It also specifies the synthesis of a controller with one hidden layer of 5 neurons to stabilize the system. Further details on the options available in the configuration file can be found in the [user guide](user-guide.md), and examples found in the [experiments folder](experiments/benchmarks/cli).
+
+```yaml
+N_VARS: 2
+SYSTEM: [x1 - x0**3, u0]
+CERTIFICATE: Lyapunov
+TIME_DOMAIN: CONTINUOUS
+DOMAINS:
+  XD: Torus([0,0], 1.0, 0.01)
+N_DATA:
+  XD: 1000
+N_HIDDEN_NEURONS: [5, 5]
+ACTIVATION: [SIGMOID, SQUARE]
+CTRLAYER: [5,1]
+CTRLACTIVATION: [LINEAR]
+VERIFIER: DREAL
+```
+
+The following command will synthesize a Lyapunov function and a controller for the system specified in the configuration file:
+
+```console
+fossil config.yaml
+```
+
+## Citations
+
+Fossil has been described in the following papers:
+
+### Version 2.0
+
+#### Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
+
+* Counterexampl-Guided synthesis of neural network certificates and controllers
+* Range of properties including stability, safety, reach-while-avoid for continuous-time models
+* Stability and safety for discrete-time models
+* Pythonic and command-line interfaces
+
+```bibtex
+@inproceedings{Edwards_Peruffo_Abate_2024,
+series={HSCC ’24},
+title={Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models}, 
+booktitle={Proceedings of the 27th International Conference on Hybrid Systems: Computation and Control},
+publisher={Association for Computing Machinery},
+author={Edwards, Alec and Peruffo, Andrea and Abate, Alessandro}, year={2021},
+collection={HSCC ’24} }
+```
+
+### Version 1.0
+
+#### FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks
 
-To cite Fossil in publications use the following BibTeX entry:
+* Counterexample-Guided Inductive Synthesis (CEGIS) for Lyapunov functions and Barrier certificates
+* Continuous-time models
+* Leverages neural networks as candidate Lyapunov functions and Barrier certificates
 
 ```bibtex
 @inproceedings{Abate_Ahmed_Edwards_Giacobbe_Peruffo_2021,

experiments/benchmarks/cli/learn.yaml

@@ -0,0 +1,15 @@
+SYSTEM: [x1, -x1 - x0]
+# SYSTEM: [-x1-x0, -x1]
+CERTIFICATE: Lyapunov
+DOMAINS:
+  XD: Sphere([0,0], 1.0)
+TIME_DOMAIN: CONTINUOUS
+VERIFIER: NONE
+N_DATA:
+  XD: 1000
+N_VARS: 2
+N_HIDDEN_NEURONS: [5]
+ACTIVATION: [SQUARE]
+# CTRLAYER: [5,1]
+# CTRLACTIVATION: [LINEAR]
+SEED: 0

experiments/benchmarks/cli/verify.yaml

@@ -0,0 +1,16 @@
+SYSTEM: [-x0, -x1]
+# SYSTEM: [-x1-x0, -x1]
+CERTIFICATE: Lyapunov
+CANDIDATE: [x0**2 + x1**2]
+DOMAINS:
+  XD: Torus([0,0], 1.0, 0.1)
+TIME_DOMAIN: CONTINUOUS
+VERIFIER: DREAL
+N_DATA:
+  XD: 1000
+N_VARS: 2
+N_HIDDEN_NEURONS: [5]
+ACTIVATION: [SQUARE]
+# CTRLAYER: [5,1]
+# CTRLACTIVATION: [LINEAR]
+SEED: 0

experiments/benchmarks/roa/roa_1.py

@@ -21,7 +21,7 @@ def test_lnn(args):
     n_vars = 2
 
     system = models.NonPoly1
-    batch_size = 500
+    batch_size = 1000
 
     XD = domains.Union(
         domains.Sphere([0.75, -0.75], 1), domains.Sphere([-0.75, 0.75], 1)
@@ -39,8 +39,8 @@ def test_lnn(args):
     }
 
     # define NN parameters
-    activations = [ActivationType.SOFTPLUS]
-    n_hidden_neurons = [5] * len(activations)
+    activations = [ActivationType.TANH_SQUARE]
+    n_hidden_neurons = [10] * len(activations)
 
     opts = CegisConfig(
         N_VARS=n_vars,
@@ -53,15 +53,17 @@ def test_lnn(args):
         ACTIVATION=activations,
         N_HIDDEN_NEURONS=n_hidden_neurons,
         CEGIS_MAX_ITERS=25,
+        VERBOSE=0,
         LLO=True,
+        # FACTORS=LearningFactors.QUADRATIC,
     )
 
     main.run_benchmark(
         opts,
         record=args.record,
-        plot=True,
+        plot=False,
         concurrent=args.concurrent,
-        repeat=args.repeat,
+        repeat=10,
     )