<jupyter_start><jupyter_text>[//]:  (Copyright c 2021, <NAME>, <NAME>, <NAME>, <NAME>, <NAME>)[//]:  (All rights reserved.)[//]:  (This source code is licensed under the BSD-style license found in the)[//]:  (LICENSE file in the root directory of this source tree. ) 🐚 Welcome to FOSSIL!            ..\\\\         ..\\\\  ,\    --===)))))))   )         ''////  `/            ''////                                                                                                                      OverviewThis tool uses neural network templates alongside the CEGIS architecture to automatically synthesise sound Lyapunov functions of Barrier Certificates for any N-dimensional system. To use this tool please change the python code in the corresponding cells to input your required dynamical system and domain, then use the correspoding cell to synthise a [Lyapunov function](lyap-synth) of [Barrier function](barrier-synth) respectively.If you would like access to more settings, such as , please use the [advanced-playground](FOSSIL-advanced-playground.ipynb). To see benchmarks and further examples refer to [benchmarks](FOSSIL-benchmarks.ipynb).<jupyter_code># % Imports
import sys
sys.path.append('..')
from experiments.playground_utils import *
#sys.path.append(".")<jupyter_output><empty_output><jupyter_text>Synthesising Lyapunov FunctionsFirst, we demonstrate synthesising Lyapunov functions. Consider the following dynamical system:$$ \begin{cases} \dot{x} = -x + xy \\ \dot{y} = - y \end{cases}$$This system can be instantied as follows, with $x_0 = x $ and $x_1 = y$:<jupyter_code>N_Dimensions = 2

x0, x1 = initialise_states(N_Dimensions)

dynamics = [
    -x0 + x0 * x1,
    -x1
]

# Note, any arbitrary variables can be used here, but internally they will be treated as x_0,...,x_n and the
# returned function will be a function of these parameters.<jupyter_output><empty_output><jupyter_text>This system has an equilibrium point at the origin $(x_0, x_1) = (0, 0)$. We seek to synthesis a Lyapunov function to serve as a certificate of stability of this equilibrium point. This Lyapunov function will be validated in a region around the equilibrium point. This domain is defined as:$$ \mathcal{D}  = \{(x_0, x_1): x_0^2 + x_1^2 < r^2 \} $$for some user-set parameter r. To constrain the domain to a torus shape (i.e., excluding a smaller hypershere around the origin), use the keyword arguement INNER_RADIUS.<jupyter_code>r = 10
mode = PrimerMode.LYAPUNOV
numerical_V, symbolic_V = synthesise(dynamics, mode, OUTER_RADIUS=r, CEGIS_PARAMETERS={CegisConfig.SEED_AND_SPEED.k: True})
# The symbolic function can be printed using print_f
print_f(symbolic_V)<jupyter_output><empty_output><jupyter_text>Barrier CerificatesWe now demonstrate synthesising a barrier certificate. Consider the following dynamical system:$$\begin{cases}\dot{x} = y \\\dot{y} = - 2400y - 576x\end{cases}$$We can initialise this dynamical system as follows, with with $x_0 = x $ and $x_1 = y$.<jupyter_code>N_Dimensions = 2

x0, x1= initialise_states(N_Dimensions)

dynamics = [
    x1,
    -2400*x1 - 576*x0
]<jupyter_output><empty_output><jupyter_text>Domain InitialisationWe define the overall domain as $$\begin{align*}& X = \{x_0^2 + x_1^2 \leq 4\}\\ & X_0 = \{(x_0 - 1)^2+(x_1 - 1)^2 \leq 0.25 \} \\ & X_u  = \{ (x_0 + 2)^2+(x_1 + 2)^2 \leq 0.16 \}\end{align*}$$This can be initialised as follows:<jupyter_code>xd = Sphere([0, 0], 2)
xi = Sphere([1, 1], 0.5)
xu = Sphere([-2, -2], 0.4)

#Hyper cuboids can be generated using Rectangle([lower_bounds], [upper_bounds])<jupyter_output><empty_output><jupyter_text>A barrier function is then synthesised as:<jupyter_code>verifier_type = VerifierType.DREAL
mode = PrimerMode.BARRIER

numerical_B, symbolic_B, = synthesise(dynamics, mode, XD=xd, XI=xi, XU=xu, 
                       CEGIS_PARAMETERS={CegisConfig.VERIFIER.k:VerifierType.DREAL, 
                                         CegisConfig.ACTIVATION.k: [ActivationType.LINEAR] })<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.12031952071892162, 'fraction_numerical': 0.020968547179231155, 'mean_word_length': 3.697538100820633, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 30, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 7, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '6', 'dir': 'jupyter-structured-clean-dedup', 'id': '217823', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 1356, 'n_tokens_neox': 1256, 'n_words': 400, 'path': 'experiments/FOSSIL-playground.ipynb', 'repo_name': 'oxford-oxcav/fossil', 'size': '4045'}