README.md 1.72 KB
Newer Older
Sayan Mitra's avatar
Sayan Mitra committed
1
2
3
DryVR 2.0 is a software tool for verifying hybrid systems. It supports reachability analysis of _gray-box_ systems,
that is, systems that are described in part as a transition system and in part as a black-box simulator.

sibai2's avatar
sibai2 committed
4
5
Please note that there are three branches: master: it is based on Python 2.7 and supports hybrid models; symmetries: it is the modification of the master branch created to support symmetry-based acceleration for reachtube computations created for this ATVA 2019 paper: "Using symmetry transformations in equivariant dynamical systems for their safety verification" by Hussein Sibai, Navid Mokhlesi, and Sayan Mitra, however it does not support hybrid models; dryvr3: it is a Python 3.6 version of the master branch which support all features of DryVR 2.0.

Sayan Mitra's avatar
Sayan Mitra committed
6
Please find the documentation at 
navidmokh's avatar
navidmokh committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

http://dryvr-02.readthedocs.io/en/latest/

Installation
==================
To install the required packages, please run:
-------------------------------------------------------------
sudo ./installRequirement.sh

The current version of installation file has been tested on a clean install of Ubuntu 16.04. 

Quick Start
==================
To run verification examples, please run 
-------------------------------------------------------------
python main.py input/[input_file]

for example:

python main.py input/daginput/input_thermo.json

The examples descriptions can be found in the documentation. Please note that as the verification algorithm uses probabilistic method, the verification result may vary for different runs.


To run controller synthesis, please run:
------------------------------------------------------------
python graphSearch.py input/[input_file]

for example:

python graphSearch.py input/rrtinput/mazefinder.json