README.md 3.04 KB
Newer Older
Lars Schieffer's avatar
Lars Schieffer committed
1
2
# JANI2PINS

Lars Schieffer's avatar
Lars Schieffer committed
3
4
5
6
[![License](https://img.shields.io/badge/license-GNU%20LGPL%20v3-brightgreen)](https://www.gnu.org/licenses/lgpl-3.0.en.html)
[![Python](https://img.shields.io/badge/python-3.8-important)](https://www.python.org/)
[![Coverage](https://img.shields.io/badge/coverage-90%25-green)](https://github.com/)

Lars Schieffer's avatar
Lars Schieffer committed
7
> The JANI front-end module for the LTSmin toolset
Lars Schieffer's avatar
Lars Schieffer committed
8
9
10
11
12

## Table of Contents

- [Installation](#installation)
- [Usage](#usage)
13
- [Interaction Protocol](#protocol)
Lars Schieffer's avatar
Lars Schieffer committed
14
15
16
17
18
19
20
- [Contact](#contact)
- [License](#license)

---

## Installation

Lars Schieffer's avatar
Lars Schieffer committed
21
JANI2PINS requires the following dependencies to work correctly.
Lars Schieffer's avatar
Lars Schieffer committed
22
23
24

### Python 3.8

Lars Schieffer's avatar
Lars Schieffer committed
25
Install at least Python 3.8  from <https://www.python.org/>
Lars Schieffer's avatar
Lars Schieffer committed
26
27
28

### LTSmin Toolset v3.0.2

Lars Schieffer's avatar
Lars Schieffer committed
29
Download and install the toolset from <https://ltsmin.utwente.nl/>
Lars Schieffer's avatar
Lars Schieffer committed
30
31
32
33
34
35

### pytest 5.4.3

Install the test libraries  with

```shell
Lars Schieffer's avatar
Lars Schieffer committed
36
pip install pytest==6.0.1
Lars Schieffer's avatar
Lars Schieffer committed
37
38
39
pip install pytest-cov==2.10.0
```

40
41
42
43
44
45
46
47
### jsonschema 3.2.0

Install the JSON schema validator with

```shell
pip install jsonschema==3.2.0
```

Lars Schieffer's avatar
Lars Schieffer committed
48
49
50
51
52
53
54
55
56
57
### websockets 8.1

Install the websockets library  with

```shell
pip install websockets==8.1
```

### QCOMP

Lars Schieffer's avatar
Lars Schieffer committed
58
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
Lars Schieffer's avatar
Lars Schieffer committed
59
60

```shell
Lars Schieffer's avatar
Lars Schieffer committed
61
sh tests/downloadModels.sh
Lars Schieffer's avatar
Lars Schieffer committed
62
63
64
65
66
67
```

---

## Usage

Lars Schieffer's avatar
Lars Schieffer committed
68
In general, JANI2PINS creates the source code implementation of the LTSmin's dl-open API, according to its input [jani-model]("http://www.jani-spec.org/"). Therefore, you have the following options to adjust the creation of the plugin implementation.
Lars Schieffer's avatar
Lars Schieffer committed
69

Lars Schieffer's avatar
Lars Schieffer committed
70
### --input PATH
Lars Schieffer's avatar
Lars Schieffer committed
71

Lars Schieffer's avatar
Lars Schieffer committed
72
Provide the path to the input file containing the jani-model
Lars Schieffer's avatar
Lars Schieffer committed
73

Lars Schieffer's avatar
Lars Schieffer committed
74
### --output PATH
Lars Schieffer's avatar
Lars Schieffer committed
75
76
77

(default: CWD)

Lars Schieffer's avatar
Lars Schieffer committed
78
Provide the path to PINS model implementation
Lars Schieffer's avatar
Lars Schieffer committed
79

Lars Schieffer's avatar
Lars Schieffer committed
80
81
82
83
84
85
### --strategy {FLATTEN,MIXED,SYMBOLIC}

(default: SYMBOLIC)

The grouping strategy for synchronising automaton instances

Lars Schieffer's avatar
Lars Schieffer committed
86
### --ltsmin PATH
Lars Schieffer's avatar
Lars Schieffer committed
87

Lars Schieffer's avatar
Lars Schieffer committed
88
(default: "/usr/local/include/ltsmin/")
Lars Schieffer's avatar
Lars Schieffer committed
89

Lars Schieffer's avatar
Lars Schieffer committed
90
Location of LTSmin header files
Lars Schieffer's avatar
Lars Schieffer committed
91

Lars Schieffer's avatar
Lars Schieffer committed
92
### --compile
Lars Schieffer's avatar
Lars Schieffer committed
93

94
Compile PINS model after creation in the filesystem (Linux/macOS)
Lars Schieffer's avatar
Lars Schieffer committed
95
96
97

(Important: --ltsmin has to link to correct header location)

Lars Schieffer's avatar
Lars Schieffer committed
98
### --experiment EXPERIMENT
Lars Schieffer's avatar
Lars Schieffer committed
99

Lars Schieffer's avatar
Lars Schieffer committed
100
Add values to uninitialized constants in jani-model, e.g. --experiment "C=42, D=612"
Lars Schieffer's avatar
Lars Schieffer committed
101

Lars Schieffer's avatar
Lars Schieffer committed
102
### --real2int
Lars Schieffer's avatar
Lars Schieffer committed
103

Lars Schieffer's avatar
Lars Schieffer committed
104
Cast real variables in jani-model to integer (Warning: Can break model behaviour)
Lars Schieffer's avatar
Lars Schieffer committed
105

Lars Schieffer's avatar
Lars Schieffer committed
106
### --disableCheck
Lars Schieffer's avatar
Lars Schieffer committed
107

Lars Schieffer's avatar
Lars Schieffer committed
108
Disable time-consuming jani-model syntax check
Lars Schieffer's avatar
Lars Schieffer committed
109
110
111

---

112
## Protocol
Lars Schieffer's avatar
Lars Schieffer committed
113
114
115

Additionally, the JANI specification defines a WebSocket network protocol.

Lars Schieffer's avatar
Lars Schieffer committed
116
### --server
117

Lars Schieffer's avatar
Lars Schieffer committed
118
Run JANI2PINS as a server on a Linux/macOS system using the interactive protocol
Lars Schieffer's avatar
Lars Schieffer committed
119

Lars Schieffer's avatar
Lars Schieffer committed
120
(Important: --ltsmin has to link to correct header location)
Lars Schieffer's avatar
Lars Schieffer committed
121
122
123
124
125

---

## Contact

Lars Schieffer's avatar
Lars Schieffer committed
126
If you need support, have a question or find a bug, don't hesitate to contact me via email:
127
lars.schieffer@protonmail.com
Lars Schieffer's avatar
Lars Schieffer committed
128
129
130
131
132
133
134
135
136

---

## License

[![License](https://img.shields.io/badge/license-GNU%20LGPL%20v3-brightgreen)](https://www.gnu.org/licenses/lgpl-3.0.en.html)

- [GNU Lesser General Public License v3](https://www.gnu.org/licenses/lgpl-3.0.en.html)
- Copyright © 2019-2020 Lars Schieffer, Saarland University.