README.md 1.33 KB
Newer Older
Sayan Mitra's avatar
Sayan Mitra committed
1
2
3
4
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.

Please find the documentation at 
navidmokh's avatar
navidmokh committed
5
6
7

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

chsieh16's avatar
chsieh16 committed
8

navidmokh's avatar
navidmokh committed
9
10
Installation
==================
chsieh16's avatar
chsieh16 committed
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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 \
    sympy z3-solver
```
navidmokh's avatar
navidmokh committed
27
28
29
30
31


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

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

for example:

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

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