<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!                                                         ___._                                                       .'  '-.._                                                      /  /.--.____")                                                     |   \   __.-'~                                                     |  :  -'/                                                    /:.  :.-'    __________                                     | : '. |    '--.____  '--------.______       _.----.-----./      :/            '--.__            `'----/       '-.      __ :/                  '-.___           :           \   .'  )/                        '---._           _.-'   ] /  _/                             '-._      _/     _/ / _/                                 \_ .-'____.-'__< |  \___                                   <_______.\    \_\_---.7                                  |   /'=r_.-'     _\\ =/                              .--'   /            ._/'>                            .'   _.-'                           / .--'                          /,/                          |/`)                          'c=, OverviewThis tool uses neural networks alongside the CEGIS architecture to automatically synthesise sound Lyapunov functions of Barrier Certificates for any N-dimensional system.This notebook provides access to the following settings:1.  [Verifier Type](verifier-type)1.  [Neural Network Structure](nn-structure)     i)  Activation functions \    ii) Layer structure (number of neurons, number of layers)1.  [Factorisation](factorisation)1.  [Last Layer of Ones](ll1)1.  [Barrier Function Sythesis Settings](barrier-settings)1.  [Sympy Settings](sympy-settings)1.  [Further CEGIS Settings](further-settings)     i)   Learning Rate \    ii)  Batch size \    iii) Maximum number of CEGIS iterations \    iv)  Rounding 1.  [Primer Settings](primer-settings)    i)   Seed and Speed \    ii)  Positive Domain \    iii)  Interactive Domain      [Running the tool with custom settings](running) [Advanced Functionality](advanced)If you would like to use a more simple interface to the tool with just defualt settings, please use the [playground](FOSSIL-playground.ipynb).<jupyter_code># % Imports
import sys
sys.path.append('..')
from experiments.playground_utils import *<jupyter_output><empty_output><jupyter_text>1. Verifier Type (*CegisConfig.VERIFIER.k*)The tool has inbuilt support for both Z3 and Dreal4, and either can be selected as the backend to the verification. Please note that certain functionality cannot be used with Z3 as the verifier, though this is the default verifier.**To specify the verifier, change the following variable to either VerifierType.Z3 or VerifierType.DREAL**<jupyter_code>verifier_type = VerifierType.Z3<jupyter_output><empty_output><jupyter_text>2. Neural Network Structure Activations (*CegisConfig.ACTIVATION.k*)The following activation functions are available:*  Linear or identity:$$\sigma(x) = x $$___*  Square:$$\sigma(x) = x^2 $$___*  Mixed $n^{th}$ order Polynomial:$$ \sigma(x) = \sum_{i=1}^{n}x_i ^i, $$ where $x_i$ represents the i^th neurons in the layer, giving a mixed layer of activations. For more details on this please see [mixed_activation_functions]___*  RELU:$$ \sigma(x) = \max(0,x) $$___*  RELU-Square:$$\sigma(x) = x_1^2 + \max(0, x_2), $$where x_1 denotes the the first half of the neurons in the layer and x_2 denotes the second half. ___*  REQU:$$ \sigma(x) = x \cdot \max(0,x)$$___*  Sigmoid (requires Dreal):$$ \sigma(x) = \frac{\text{e}^{x}}{\text{e}^{x} +1}$$___*  Tanh (requires Dreal):$$\sigma(x) = \tanh(x) $$ Neuron Structure  (*CegisConfig.N_HIDDEN_NEURONS.k*)The tool supports any number of layers each with any number of neurons and activation function. However, it should be noted that larger networks will have longer verification times. The desired activation functions for each should be inlcuded as a list with each element representing the activation function for that layer. Similarly, the number of neurons in each layer should be inlcuded as a list.For example, for a network structure with two hidden layers, one with 50 and one with 20 neurons, the first of which has mixed second-order polynomial (LIN_SQUARE)  activations and the second with relu (RELU) activations.activations = \[ ActivationType.LIN_SQUARE, ActivationType.RELU \] neurons     = \[ 50, 20 \]The default parameters are given in the cell below and can be changed freely.<jupyter_code>activations = [ActivationType.SQUARE]
neurons = [10]<jupyter_output><empty_output><jupyter_text>3. Factorisation  (*CegisConfig.FACTORS.k*)In order to help ensure that $V(x^*) = 0$ when synthesising Lyapunov r functions, the learner can be augmented with a quadratic term as $$ V(x) = (x-x^*)^2 \cdot \text{n}(x), $$  where $n(x)$ is the original neural network.  **To use quadratic factors, set the following variable to LearningFactors.QUADRATIC.** \**To not use any factors (the defualt setting), set the following variable to None**<jupyter_code>factors = None<jupyter_output><empty_output><jupyter_text>4. Last Layer of Ones (Lyapunov Only) (*CegisConfig.LLO.k*)llo(*boolean, defualt True*): This constrains the last layer of the neural network to be all ones. This can improve synthesise by helping ensure the positive definiteness (V(x) > 0) condition holds for the learner and verifier.**To constrain the last layer to be all ones, set the following variable to True.**<jupyter_code>llo = False<jupyter_output><empty_output><jupyter_text>5. Symmetric Belt (Barrier Only) (*CegisConfig.SYMMETRIC_BELT.k*)*symmetric_belt (boolean, default=False)*: defines whether the belt for the derivative barrier condition is symmetric around zero (if so, we consider $|B(x)| \leq 0.5$) or not (if so, the we consider $B(x) \geq -0.1$). **To constrain the belt to be symmetric, set the following variable to True.**<jupyter_code>symmetric_belt = False<jupyter_output><empty_output><jupyter_text>6. Sympy SettingsThese settings determine the usage of sympy within the CEGIS object.sp_handle (*boolean, default True*): determines whether expressions are handled using the python symbolic library *sympy*. (*CegisConfig.SP_HANDLE.k*)sp_simplify (*boolean, default True*): determines whether expressions are simplified using the *sympy* (potentially costly operation). (*CegisConfig.SP_SIMPLIFY.k*)**To disable sympy handling and simplification, set the following variables to False.**<jupyter_code>sp_handle = True

sp_simplify = True<jupyter_output><empty_output><jupyter_text>7. Further CEGIS Settings* Learning Rate (*positive float, default = 0.1*): sets the learning rate of the neural network. (*CegisConfig.LEARNING_RATE.k*)* Batch Size (*int, defualt = 500*): defines the number of data points initially generated. (*CegisConfig.BATCH_SIZE*)* Max Iterations (*int, default = 10*): sets the maximum number of CEGIS loops before termination. (*CegisConfig.CEGIS_MAX_ITERS.k*)* Rounding (*int, default = 3*): sets the rounding precision used in the Translator. (*CegisConfig.ROUNDING.k*)<jupyter_code>learning_rate = 0.1

batch_size = 500

max_iterations = 10

rounding = 3<jupyter_output><empty_output><jupyter_text>8. Primer SettingsThese settings affect how CEGIS is called and interacted with.* Seed and Speed (*boolean, default=False*): if *Seed and Speed* is True, then a CEGIS object is repeatedly instantiated on a short timeout until the procedure is successful. (*CegisConfig.SEED_AND_SPEED.k*)* Interactive Domain (*boolean, default=False*) : determines whether the user can adjust the domain size if CEGIS fails. Cannot be used in conjunction with *Seed and Speed*. (*CegisConfig.INTERACTIVE_DOMAIN.k*)* Positive Domain (*boolean, defualt=False*): Lyapunov only. If True, then the verification domain for Lyapunov conditions is constrained to the positive orthant. (*CegisConfig.POSITIVE_DOMAIN.k*)<jupyter_code>seed_and_speed = False

positive_domain = False

domain_mode = False<jupyter_output><empty_output><jupyter_text>Running with custom settingsOnce you have set custom settings using the cells above, use the following cell to instantiate a dynamical system and to synthesise either a Lyapunov or Barrier Certificate. The settings are placed into the Cegis_Parameters dictionary as shown.<jupyter_code>N_Dimensions = 2

x0, x1 = initialise_states(N_Dimensions)

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

mode = PrimerMode.LYAPUNOV

parameters = {CegisConfig.VERIFIER.k: verifier_type,         CegisConfig.ACTIVATION.k: activations,
              CegisConfig.N_HIDDEN_NEURONS.k: neurons,       CegisConfig.FACTORS.k: factors, 
              CegisConfig.LLO.k: llo,                        CegisConfig.LEARNING_RATE.k: learning_rate, 
              CegisConfig.BATCH_SIZE.k: batch_size,          CegisConfig.CEGIS_MAX_ITERS.k: max_iterations,
              CegisConfig.SP_HANDLE.k: sp_handle,            CegisConfig.SP_SIMPLIFY.k: sp_simplify, 
              CegisConfig.SEED_AND_SPEED.k: seed_and_speed,  CegisConfig.POSITIVE_DOMAIN.k: positive_domain,
              CegisConfig.INTERACTIVE_DOMAIN.k: domain_mode,}
f_n, f_s = synthesise(dynamics, mode, 
           CEGIS_PARAMETERS=parameters)<jupyter_output><empty_output><jupyter_text>Advanced FunctionalityUsers are able to define custom systems (dynamics + domains) for either Lyapunov synthesis or Barrier synthesis. These should be in the form of the python functions shown below, including routines for generating the system dynamics, symbolic domains and data generation in the domains. Note that for Lyapunov synthesis, the equilibrium point to perform analysis on must lie at the origin.For generating data within domains, users are encouraged to user the existing functions in experiments/benchmarks/domains_fcns.py when possible.These functions can be passed to *synthesise* or to *Primer.create_Primer* as the argument f. In this case, the CegisConfig.N_VARS parameter must be passed in cegis_parameters.<jupyter_code>from experiments.benchmarks.domain_fcns import *

#Lyapunov Example
def lyap_hybrid(batch_size, functions, inner, outer):
    # example of 2-d hybrid sys
    _And = functions['And']

    def f(functions, v):
        _If = functions['If']
        x0, x1 = v
        _then = - x1 - 0.5*x0**3
        _else = - x1 - x0**2 - 0.25*x1**3
        _cond = x1 >= 0
        return [-x0, _If(_cond, _then, _else)]

    def XD(_, v):
        x0, x1 = v
        return _And(inner**2 < x0**2 + x1**2,
                               x0**2 + x1**2 <= outer**2)

    def SD():
        return circle_init_data((0., 0.), outer**2, batch_size)

    return f, XD, SD()

# Barrier Example
def obstacle_avoidance(batch_size, functions):
    _And = functions['And']
    velo = 1

    def f(functions, v):
        x, y, phi = v
        return [
            velo * functions['sin'](phi), velo * functions['cos'](phi),
            - functions['sin'](phi) + 3 * (x * functions['sin'](phi) + y * functions['cos'](phi)) / (0.5 + x ** 2 + y ** 2)
        ]

    def XD(_, v):
        x, y, phi = v
        return _And(-2 <= x, y <= 2, -1.57 <= phi, phi <= 1.57)

    def XI(_, v):
        x, y, phi = v
        return _And(-0.1 <= x, x <= 0.1, -2 <= y, y <= -1.8, -0.52 <= phi, phi <= 0.52)

    def XU(_, v):
        x, y, _phi = v
        return x**2 + y**2 <= 0.04

    def SD():
        x_comp = -2 + torch.randn(batch_size, 1)**2
        y_comp = 2 - torch.randn(batch_size, 1)**2
        phi_comp = segment([-1.57, 1.57], batch_size)
        dom = torch.cat([x_comp, y_comp, phi_comp], dim=1)
        return dom

    def SI():
        x = segment([-0.1, 0.1], batch_size)
        y = segment([-2.0, -1.8], batch_size)
        phi = segment([-0.52, 0.52], batch_size)
        return torch.cat([x, y, phi], dim=1)

    def SU():
        xy = circle_init_data((0., 0.), 0.04, batch_size)
        phi = segment([-0.52, 0.52], batch_size)
        return torch.cat([xy, phi], dim=1)

    bounds = inf_bounds_n(2)
    pi = math.pi
    bounds.append([-pi/2, pi/2])
    return f, XD, XI, XU, SD(), SI(), SU(), bounds<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.11386660183159089, 'fraction_numerical': 0.015155198962638788, 'mean_word_length': 2.8550452983442676, 'pattern_counts': {'":': 0, '<': 65, '<?xml version=': 0, '>': 53, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 1, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '11', 'dir': 'jupyter-structured-clean-dedup', 'id': '598707', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 3920, 'n_tokens_neox': 3673, 'n_words': 1208, 'path': 'experiments/FOSSIL-advanced-playground.ipynb', 'repo_name': 'oxford-oxcav/fossil', 'size': '12378'}