README.md

# JANI2PINS

[![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/)

> The JANI front-end module for the LTSmin toolset

## Table of Contents

- [Installation](#installation)
- [Usage](#usage)
- [Interaction Protocol](#protocol)
- [Contact](#contact)
- [License](#license)

---

## Installation

JANI2PINS requires the following dependencies to work correctly.

### Python 3.8

Install at least Python 3.8  from <https://www.python.org/>

### LTSmin Toolset v3.0.2

Download and install the toolset from <https://ltsmin.utwente.nl/>

### pytest 5.4.3

Install the test libraries  with

```shell
pip install pytest==6.0.1
pip install pytest-cov==2.10.0
```

### jsonschema 3.2.0

Install the JSON schema validator with

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

### websockets 8.1

Install the websockets library  with

```shell
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 tests directory

```shell
sh tests/downloadModels.sh
```

---

## Usage

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.

### --input PATH

Provide the path to the input file containing the jani-model

### --output PATH

(default: CWD)

Provide the path to PINS model implementation

### --strategy {FLATTEN,MIXED,SYMBOLIC}

(default: SYMBOLIC)

The grouping strategy for synchronising automaton instances

### --ltsmin PATH

(default: "/usr/local/include/ltsmin/")

Location of LTSmin header files

### --compile

Compile PINS model after creation in the filesystem (Linux/macOS)

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

### --experiment EXPERIMENT

Add values to uninitialized constants in jani-model, e.g. --experiment "C=42, D=612"

### --real2int

Cast real variables in jani-model to integer (Warning: Can break model behaviour)

### --disableCheck

Disable time-consuming jani-model syntax check

---

## Protocol

Additionally, the JANI specification defines a WebSocket network protocol.

### --server

Run JANI2PINS as a server on a Linux/macOS system using the interactive protocol

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

---

## Contact

If you need support, have a question or find a bug, don't hesitate to contact me via email:
lars.schieffer@protonmail.com

---

## 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.