Commit 0175bb7c authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update README

parent 7df229a9
......@@ -56,10 +56,10 @@ pip install websockets==8.1
### QCOMP
For testing purposes, you can download more JANI models from the [QCOMP Benchmark Set](http://qcomp.org/benchmarks/index.html) by executing the following shell script in the mdp directory
For testing purposes, you can download more jani-models from the [QCOMP Benchmark Set](http://qcomp.org/benchmarks/index.html) by executing the following shell script in the tests directory
```shell
cd JANI2PINS/tests/res/mdp/
cd JANI2PINS/tests/
sh downloadModels.sh
```
......@@ -69,83 +69,57 @@ sh downloadModels.sh
In general, JANI2PINS creates the source code implementation of the dl-open API of LTSmin, according to its input in the [JANI]("http://www.jani-spec.org/") model format. Therefore, you have the following option to adjust the creation of the plugin implementation.
### Required
### --input PATH
#### --input PATH
Provide path to the input file, containing the jani-model
Provide the path to the input file, which contains the JANI model
### Optional
#### --output PATH
### --output PATH
(default: CWD)
Create the source code at PATH location
#### --experiment EXPERIMENT
Add values to uninitialized constants in JANI model, e.g. --experiment "C=42, D=612"
Provide path of location for creating PINS model implementation
#### --syncMode MODE
### --ltsmin PATH
(default: FLATTEN)
Handle synchronized nondeterministic actions either with mode FLATTEN or POSTPONE.
#### --real2int
(default: "/usr/local/include/ltsmin/")
Cast real constants in JANI model to integer
Location of LTSmin headers
#### --compile
### --compile
Let JANI2PINS compile the plugin implementation after creation
(Important: --ltsmin has to link to correct header location)
#### --ltsmin PATH
### --experiment EXPERIMENT
(default: "/usr/local/include/ltsmin/")
Add values to uninitialized constants in jani-model, e.g. --experiment "C=42, D=612"
LTSmin header file location
### --real2int
#### --recursionLimit INTEGER
Cast real variables in jani-model to integer (Warning: Can produce wrong models)
(default: 1000)
### --disableCheck
Set recursion limit for jani2pins execution
Disable time consuming jani-model syntax check
---
## Protocol
## Interactive - Protocol
Additionally, the JANI specification defines a WebSocket network protocol.
### Required
#### --ltsmin PATH
LTSmin header file location directory
#### --jani2pins PATH
Path of JANI2PINS installation location
(Example: /Users/lars/jani2pins/JANI2PINS/jani2pins.py)
### Optional
#### --port INTEGER
### --server
(default: 15291)
Run JANI2PINS as server, implementing interactive protocol
Port of WebSocket connection
(Important: --ltsmin has to link to correct header location)
#### --address PATH
### --address ADDRESS
(default: "localhost")
(default: "localhost:15291")
Address of server, used in WebSocket connection
Adjust web address of server
---
......
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