<!-- Adapted from: https://www.writethedocs.org/guide/writing/beginners-guide-to-docs/ -->

# Lola2

## User Guide

_Lola2_ adds support for [Lola](https://theo.informatik.uni-rostock.de/theo-forschung/tools/lola/) to Renew. Lola can be helpful when you want to analyse Petri Nets.

### Features

- Analyse Petri Nets with the State-of-the-art tool Lola

### Example Usage

1. Open a net in the graphical editor.
2. Analyse it with Lola via Tools -> Lola2 Integration

### Provided Commands

- "Show Lola GUI": Starts up the graphical user interface, from which all functionality of the
  plugin can be accessed.
- "Check all verification tasks" - checks all Lola tasks found in the current drawing i.e. all
  TextFigures that start with "ANALYSE" or "ASSERT" (upper case required). Depending on the result
  it creates a colored frame around the task text.
- "Check selected request" - checks a single selected verification task and colors the frame.
- "Check selected Transitions" - checks if selected transitions are dead. In this case, they are
  colored red, otherwise (non-dead) they are colored green.
- "Check selected Places" - checks if selected places are bounded. In this case, they are
  colored green, otherwise (unbounded) they are colored red.
- "Check all places and transitions" - checks and colors all places and transitions.


### Installation

Old:
- You will need a working build environment (configure, make, gcc)
  => install the package 'build-essential'
  (sudo apt-get install build-essential)
- to draw reachability graphs you will need the package 'graphviz'
- run the compile-lola.sh shell script, it will download the lola sources,
  compile the different required lola binaries to the lib folder
- run ant, this will compile the plugin and copy it to ../dist/plugins

New:
- Just build Lola using gradle with Lola2:plugin

### Dependencies

This plugin depends on the following plugins and external libraries:

- `Gui`

### Configuration

**NAME**| **TYPE** | **DESCRIPTION**          |**DEFAULT**
:-----|:--------:|:-------------------------|:-----
`de.renew.lola.tmpdir`| `String` | Name of the Lola binary. | "lola"


## Developer Guide

### Core Classes

- `LolaAnalyzer`: This class is responsible for calling Lola and producing a LolaResult.
- `LolaFileCreator`: Is responsible for creating Lola net files, which allow the analysis of Renew Nets in Lola.
- `LolaTask`: represents a verification request. Can determine it's type, check itself and color
  it's corresponding figure.

- `LolaResult`: Represents the result of a lola call.

- `LolaGUI`: The graphical user interface.

- `LolaHelper`: Provides a method to find the used temporary directory and provides the Lola call command.

### How to Extend

_Lola_ exposes the LolaResult interface. You can implement this interface to add additional functionality to Lola.

- `de.renew.lola.analysis.LolaResult` - contains all information about the Result the Lola binary produced.

### Additional Information

<!-- Common issues, explanations for inconsistencies, etc. -->

<!-- Contribution Info -->

<!-- License -->
