A prototype learner-verifier for dynamical systems.
This project is no longer maintained actively. Please don't use it as a reference for your work.
Most of the code here is written experimentally. Some modules are stale, and will not work. Some modules are duplicates of other modules. My suggestion is to look at the drafts; at commit a1830c1, all drafts work.
We use the Marabou verifier via its Python interface.
To build Marabou (and Maraboupy),
follow the instructions on
the Marabou installation page
at this link.
Before compiling,
make sure to change
the parameter INTERVAL_SPLITTING_FREQUENCY
(in this file)
to 1
.
This might cause some tests to fail; it is OK.
After building Marabou, make a link to the maraboupy
directory, like the following:
ln -s /path/to/Marabou/maraboupy .
This lets us use maraboupy
as a module in this project.
The project neural_clbf
is available at
this page.
Follow the instructions on their page.
You might want to make a link to neural_clbf
.
Steps are the same as the case with maraboupy
.
As the name suggests, it is only a playground. All useful things from the playground are already implemented in the source files (or drafts).