This repository contains the main implementation of "Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees", which is submitted to NeurIPS 2021.
Please refer to ReachNN to set up the environment. Addtionally, you need to set up cnpy, which is a C++ library save vector into numpy array.
To run the controller synthesis for Adaptive Crucise Control(ACC), please do
./example_acc.shTo run the controller synthesis for non-linear Van der Pol's Oscillator system, please do
cd Bernstein_Polynomial_Approximation
make name=nn_os_relu_tanh
python controller_approximation_lib.py -flag 1
To run the controller synthesis for the 3-dimensional numerical example, please do
cd Bernstein_Polynomial_Approximation
make name=nn_3d_relu_tanh
python controller_approximation_lib_3dsysPlease open an issue if there is any problem you encounter with.
Organize the code.