README.md 2.6 KB
Newer Older
Sayan Mitra's avatar
Sayan Mitra committed
1
2
DryVR 2.0 is a software tool for verifying cyber-physical and autonomoous systems. A key feature of DryVR is that it supports reachability analysis of _gray-box_ systems, that is, systems that are described in part as a white box transition system or a program and in part as a black-box simulator as shown in the figure below.

Sayan Mitra's avatar
Sayan Mitra committed
3
<img src="figures/dryvrmodel.png" style="float: left; margin-right: 10px;" />
Sayan Mitra's avatar
Sayan Mitra committed
4

sibai2's avatar
sibai2 committed
5
6
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
7
Please find the documentation at 
navidmokh's avatar
navidmokh committed
8
9
10

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

chsieh16's avatar
chsieh16 committed
11

navidmokh's avatar
navidmokh committed
12
13
Installation
==================
chsieh16's avatar
chsieh16 committed
14
15
16
17
18
19
20
21
22
23
24
25
26
27
Following installation instructions has been tested with Python 2.7.12 on
Ubuntu 16.04.

Install System dependencies:

```bash
$ sudo apt-get install python-pip python-cairo python-tk python-pygraphviz \
    libglpk-dev
```

Install PyPi dependencies using `pip`:
```bash
$ pip2 install --user --upgrade pip  # Upgrade pip first
$ pip2 install --user glpk networkx python-igraph matplotlib numpy scipy \
chsieh16's avatar
chsieh16 committed
28
    sympy z3-solver six
chsieh16's avatar
chsieh16 committed
29
```
navidmokh's avatar
navidmokh committed
30

31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
For Python 3.5 or above on Ubuntu 16.04, try the following instructions.

```bash
$ sudo apt-get install python3-pip python3-cairo python3-tk python3-pygraphviz \
    libglpk-dev
$ pip3 install --user --upgrade pip  # Upgrade pip first
$ pip3 install --user -r requirements.txt
```

If using Python 3 `venv` virtual environment on Ubuntu 16.04, try the following instructions.
```bash
$ sudo apt-get install python3-pip libcairo2-dev libgraphviz-dev libglpk-dev
$ pip3 install --upgrade pip  # Upgrade pip first
$ pip3 install -r requirements.txt
```
navidmokh's avatar
navidmokh committed
46
47
48
49

Quick Start
==================
To run verification examples, please run 
chsieh16's avatar
chsieh16 committed
50
51

```bash
navidmokh's avatar
navidmokh committed
52
python main.py input/[input_file]
chsieh16's avatar
chsieh16 committed
53
```
navidmokh's avatar
navidmokh committed
54
55
56

for example:

chsieh16's avatar
chsieh16 committed
57
```bash
navidmokh's avatar
navidmokh committed
58
python main.py input/daginput/input_thermo.json
chsieh16's avatar
chsieh16 committed
59
```
navidmokh's avatar
navidmokh committed
60
61
62
63
64
65
66
67
68
69
70
71

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