This is the JuliaReach repeatability evaluation (RE) package for the ARCH-COMP 2018 category report: Continuous and Hybrid Systems with Linear Continuous Dynamics of the 2nd International Competition on Verifying Continuous and Hybrid Systems (ARCH-COMP '18).
🏆 🤓 The Best Result Award of the ARCH 2018 Friendly Competition was given to JuliaReach. See the announcement here.
To cite the work, you can use:
@inproceedings{AlthoffB0FFFKLM18,
author = {Matthias Althoff and
Stanley Bak and
Xin Chen and
Chuchu Fan and
Marcelo Forets and
Goran Frehse and
Niklas Kochdumper and
Yangge Li and
Sayan Mitra and
Rajarshi Ray and
Christian Schilling and
Stefan Schupp},
editor = {Goran Frehse and
Matthias Althoff and
Sergiy Bogomolov and
Taylor T. Johnson},
title = {{ARCH-COMP18} Category Report: Continuous and Hybrid Systems with
Linear Continuous Dynamics},
booktitle = {{ARCH}},
series = {EPiC Series in Computing},
volume = {54},
pages = {23--52},
publisher = {EasyChair},
year = {2018},
url = {https://doi.org/10.29007/73mb},
doi = {10.29007/73mb}
}
Instructions are provided for installing and running the benchmarks.
Note. ARCH18_RE.jl
is just a "wrapper" module for running the benchmarks of this RE.
The actual algorithms belong to the package Reachability.jl.
This year we have considered purely continuous models only. These are:
- International Space Station (ISS) alias
SpaceStation
. - Building model alias
Building
.
Overview. To install and run the benchmarks, basically these three steps are needed:
- Download and install Julia v0.6.4 using the official download links.
- Clone this repository and run the script
install.jl
to install the required Julia packages and dependencies. - Run the benchmarks to obtain results using the script
run.jl
; the reuslts are stored inresults.md
.
Below we explain these steps in some detail. A section on known issues is given in the end. If you still have problems or questions, do contact us in our gitter channel or via email.
JuliaReach is a software framework for reachability computations of dynamical systems, available at the JuliaReach github project website. It is written in Julia, a modern high-level language for scientific computing. Currently JuliaReach can handle continuous affine systems. The reachability algorithm uses a block decomposition technique presented in DBLP:conf/hybrid/BogomolovFFVPS18. Here we partition the state space, project the initial states to subspaces, and propagate these low-dimensional sets in time. This allows us to perform otherwise expensive set operations in low dimensions. Furthermore, if the output does not depend on all dimensions, we can effectively skip the reach set computation for the respective dimensions. In the evaluation we used two-dimensional blocks, for which our implementation supports epsilon-close approximation; for box approximation we can handle arbitrary partitions. For the set computations we use the LazySets library, which is also part of the JuliaReach framework. LazySets exploits the principle of lazy (on-demand) evaluation and uses support functions to represent lazy sets. JuliaReach also comes with SX, a parser for SX (SpaceEx format) model files. For next year we plan to add support for hybrid dynamics, which will require a careful balance between low- and high-dimensional computations and adaptive choice of the partition.
IMPORTANT NOTE. The master
branch in this repository and the installation
script install.jl
are meant to be a "screenshot" of the packages ecosystem for
this RE. If you intend to use JuliaReach for other purposes than RE, we strongly recommend
that you use instead the currently long-term support Julia version, and follow the installation
instructions in Reachability.jl.
Moreover, the ReachabilityBenchmarks
project contains updated model files for the latest package versions.
This RE requires Julia v0.6.4
. Refer to the official documentation
on how to install and run Julia in your system. As of 05/04/2019, Julia version
v0.6.4
is found under the older releases page.
This RE does not work with Julia v1.0 or higher (see note above).
After installing Julia, the REPL (read-evaluate-print-loop) welcome message should look like:
$ julia
_
_ _ _(_)_ | A fresh approach to technical computing
(_) | (_) (_) | Documentation: https://docs.julialang.org
_ _ _| |_ __ _ | Type "?help" for help.
| | | | | | |/ _` | |
| | |_| | | | (_| | | Version 0.6.4 (2018-07-09 19:09 UTC)
_/ |\__'_|_|_|\__'_| | Official http://julialang.org/ release
|__/ | x86_64-apple-darwin14.5.0
julia>
Clone this repository and then install this RE and dependencies with the
self-contained script install.jl
.
$ git clone https://github.com/JuliaReach/ARCH2018_RE.git
$ cd ARCH2018_RE/
$ julia --color=yes install.jl
Note. The installation and compilation of dependencies, with an average internet connection and machine, may take around 15-30 minutes.
To run the benchmarks, execute the run.jl
script provided in this package:
$ julia --color=yes run.jl
A results.md
file containing the results for each benchmark in tabular format is
saved in your current working directory.
Note. To obtain statistically meaningful performance measures, each reachability
computation is performed several times. The script can take several minutes. The
time displayed in the tables is the minimum time for the given trials. If you are
interested in other statistics, such as mean or median, these can be found by
looking at the entries of the results
object.
For more advanced testing settings we refer to the official BenchmarkTools documentation.
-
If running one of the scripts fails, try running it a second time.
-
See also the installation instructions of the LazySets.jl library.
-
If you still have trouble, don't hesitate to contact us in our gitter channel.