README.md 2.69 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

Sayan Mitra's avatar
Sayan Mitra committed
5
The white-box transition system is specified as a JSON file and the black-box simulator can be written in any language. DryVR uses PAC-learning to learn a sensitivity function for the black-box and combines that with reachanbility analysis on the transition graph. The tool has been used to verify ground and aeiral vehicle models in complex scenarios. You can find more detailed documentation and usages from [this page](https://dryvr.readthedocs.io/en/latest/publications.html). 
Sayan Mitra's avatar
Sayan Mitra committed
6
7


chsieh16's avatar
chsieh16 committed
8
Note that there are three branches: `master`: it is based on Python 3 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; `dryvr2`: it is the deprecated version using Python 2.7 which support all features of DryVR 2.0.
navidmokh's avatar
navidmokh committed
9

chsieh16's avatar
chsieh16 committed
10

navidmokh's avatar
navidmokh committed
11
12
Installation
==================
chsieh16's avatar
chsieh16 committed
13
Following installation instructions has been tested with Python 3 on Ubuntu 16.04 and 20.04.
navidmokh's avatar
navidmokh committed
14

chsieh16's avatar
chsieh16 committed
15
For Python 3.5 or above on Ubuntu 16.04 or 20.04, try the following instructions.
16
17

```bash
chsieh16's avatar
chsieh16 committed
18
$ sudo apt-get install python3-pip python3-cairo python3-tk python3-pygraphviz libglpk-dev
19
20
21
22
$ pip3 install --user --upgrade pip  # Upgrade pip first
$ pip3 install --user -r requirements.txt
```

chsieh16's avatar
chsieh16 committed
23
If using Python 3 `venv` virtual environment on Ubuntu 16.04 or 20.04, try the following instructions.
24
25
26
27
28
```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
29
30
31
32

Quick Start
==================
To run verification examples, please run 
chsieh16's avatar
chsieh16 committed
33
34

```bash
navidmokh's avatar
navidmokh committed
35
python main.py input/[input_file]
chsieh16's avatar
chsieh16 committed
36
```
navidmokh's avatar
navidmokh committed
37
38
39

for example:

chsieh16's avatar
chsieh16 committed
40
```bash
navidmokh's avatar
navidmokh committed
41
python main.py input/daginput/input_thermo.json
chsieh16's avatar
chsieh16 committed
42
```
navidmokh's avatar
navidmokh committed
43
44
45
46
47
48

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:
------------------------------------------------------------
chsieh16's avatar
chsieh16 committed
49
50

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

for example:

chsieh16's avatar
chsieh16 committed
56
```bash
navidmokh's avatar
navidmokh committed
57
python graphSearch.py input/rrtinput/mazefinder.json
chsieh16's avatar
chsieh16 committed
58
```
navidmokh's avatar
navidmokh committed
59