| Status | Community | License |
|---|---|---|
   |
 |
 |
This is a benchmark suite for reachability computations. It includes the SLICOT models, which reflect real world applications with dimensions ranging from several dozens to over 10.000.
Clone this repository
git clone https://github.com/JuliaReach/ReachabilityBenchmarks.git
You need to have installed the Julia package Reachability.jl, by following the instruction in the installation section.
Some models are stored in MAT files. These can be loaded in Julia using the MAT.jl package. To install this package, do:
julia> import Pkg; Pkg.add("MAT")There are also bash scripts to run SpaceEx for most of the models.
These scripts assume that spaceex (and some other tools for creating plots) are added to the PATH.
The models are given as Julia scripts, which you can run by including them in Julia's REPL, e.g.
julia> include("models/SLICOT/iss/iss.jl")The scripts are accompanied by a function named like the model, which calculates reachable states or checks a safety property, depending on the model's options. To compute the reach set using the default options with a time step of 0.01, do
julia> sol = solve(iss(:mode=>"reach", :T=>20.0, :δ=>0.01)...);More options can be added in the same style.
To plot the reachable states, you can use the function plot from the Plots
package.
julia> using Plots
julia> plot(sol)This repository provides a Julia script that will execute Julia on all existent SLICOT models.
julia -e 'include("src/benchmark_all.jl")'The results are stored in the current folder. There is also a bash script which can be modified (by just uncommenting the respective parts) to run SpaceEx on all the models.
Follow this Jupyter nbviewer link to access the folder of available models, and click on files of type ".ipynb" to open the notebooks.
For example, in models/ARCH2018/SpaceStation you will find a safety property check for the 270-variable structural model of component 1R (Russian service module) of the International Space Station.
