Update README.md

parent 0f9e8f86
......@@ -11,15 +11,12 @@ upon compilation so that no steps other than compiling them need to be taken.
##### A note on CArL and HyPro versions
Not all versions of CArl and HyPro work with each other or with HPnmG. Unfortunately, it is not always so clear which
*do*. Symptoms of bad versions include:
- HyPro refusing to compile because of C++17 features in CArl. CArl offers a C++14 branch `master14`, HyPro offers
`c++14-support`.
- HPnmG or targets thereof refusing to compile because of changed include paths, classes or signatures in HyPro
- Some targets of HPnmG refusing to *link* because of undefined symbols from `libgmp` in `libhypro.so`
As of now (2019-07-22), you should be able to use [this revision](https://github.com/smtrat/carl/commit/ace90eb5daad)
for CArl and [this one](https://github.com/hypro/hypro/commit/9d26f57b5f62) for HyPro.
For the Projektseminar, you should be able to use [this revision](https://github.com/smtrat/carl/commit/112ab9ffec0ce2252aec641c72905771c4729223)
for CArl and the [provided HyPro Version](https://zivgitlab.uni-muenster.de/ag-sks/teaching/projektseminars/2020-21-winter-stochastic-hybrid-systems/2020-21-winter-stochastic-hybrid-systems-student-access/hypro).
For some branches (`integrationOnPolytopes`, `nondeterministicRates`, `hybridAutomata`) you need the C++17 features of CArl. You should then use [this revision](https://github.com/smtrat/carl/commit/112ab9ffec0ce2252aec641c72905771c4729223) of CArl and [this one](https://github.com/hypro/hypro/commit/0754e84580dc0da450e809698f176a02e18bee25) for HyPro.
#### Dependencies
0. Install CMake.
......@@ -76,9 +73,9 @@ command should include lines similar to these:
Build carl with `make carl`. This may take a minute.
#### HyPro
Download [HyPro](https://github.com/hypro/hypro) and pick a [version](#a-note-on-carl-and-hypro-versions)
Download HyPro.
```
$ git clone https://github.com/hypro/hypro && cd hypro && git checkout <XYZ>
$ git clone git@zivgitlab.uni-muenster.de:ag-sks/teaching/projektseminars/2020-21-winter-stochastic-hybrid-systems/2020-21-winter-stochastic-hybrid-systems-student-access/hypro.git && cd hypro
$ mkdir build && cd build && cmake ..
```
If your dependencies are installed correctly and if CArl registered itself correctly with CMake, the output of the
......@@ -87,14 +84,33 @@ latter command should include lines like these:
-- Use system version of CArL
-- Found Java: ...
```
Build HyPro's resources and HyPro itself with `make resources && make hypro`. This may take 10 minutes.
## Instructions
Replication of results for HSCC 2020 Submission "Classic and Non-Prophetic Model Checking for Hybrid Petri Nets with Stochastic Firings":
The GoogleTest file `test/testNondeterministicConflicts.cpp` holds tests for all versions of the case study used in the HSCC 2020 submission, for both nonprophetic and prophetic scheduling. The core algorithms presented in the submission can be found inside the file: `src/hpnmg/NondeterminismSolver.cpp`.
The model files can be found in the folder `/test/testfiles/nondeterministicModelsCharging/`. This folder also includes a PDF file `PLTsHSCC.pdf` that shows the Parametric Location Trees of the models presented in the submission.
Build HyPro's resources and HyPro itself with `make resources && make hypro`.
To build the tests for hypro, just run `make`. After building, run the tests with `make test`.
#### hpnmg
Download hpnmg.
```
$ git clone git@zivgitlab.uni-muenster.de:ag-sks/teaching/projektseminars/2020-21-winter-stochastic-hybrid-systems/2020-21-winter-stochastic-hybrid-systems-student-access/hpnmg.git && cd hpnmg
$ mkdir build && cd build && cmake ..
```
If your dependencies are installed correctly and if HyPro registered itself correctly with CMake, the output of the
latter command should include lines like these:
```
--
```
Build hpnmg with `make main`.
To build the tests for hpnmg, just run `make testAllQuick` or `make testAllExtensive`.
To run the tests, change directory to `build/test` and run the compiled binaries, e.g. `testAllQuick` and `testAllExtensive`:
```
$ make main
$ make testAllQuick && make testAllExtensive
$ cd build/test
$ ./testAllQuick
```
This should take between 30 seconds and two minutes, depending on your machine and the build type (debug or release).
Continuing:
```
$ ./testAllExtensive
```
This should take between 30 seconds and 13 minutes.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment