LaRA ideas in Romeo

L. Jezequel, D. Lime & B. Serée
March 2021

This tool is presented in the following paper:
Loïg Jezequel, Didier Lime, and Bastien Serée: A lazy query scheme for reachability analysis in Petri nets. Petri nets 2021

Files

Usage

At the moment, we provide only Linux 64 bits binaries of all the tools.

To get the CTS representation of a PNML model: ./pnml2cts model.pnml > model.cts
To get the CTS representation of a formula from the MCC: ./formula2cts CTLReachability.xml X > formula.cts where X is the number of the formula to convert
To get the CTS representation of the full problem (model and formula): cat model.cts formula.cts > problem.cts
To execute romeo-cli on this problem: ./romeo-cli problem.cts

LaRA-T

L. Jezequel & D. Lime
May 2017

This tool is presented in the following paper:
Loïg Jezequel and Didier Lime: Let’s Be Lazy, We Have Time or, Lazy Reachability Analysis for Timed Automata. FORMATS 2017

Files

Dependencies

LaRA-T is written in Haskell and compiles (at least) with GHC v8.0.1. In addition to standard containers, LaRA-T uses the Parsec parsing library (tested with v3.1.11).

Compilation

To compile LaRA, execute: ghc --make lara.hs (with Mac OS X, you may have to rename lara.hs to something else as otherwise the binary will be name lara, the same -- Mac OS' filesystem is not case-sensitive -- as the subdirectory Lara/ containing sources).

Experiments presented in the paper were done by printing only "True" instead of the whole trace when the property is indeed true. This behavior can be replicated by commenting in/out the adequate lines in lara.hs.

Execution

We provide a Linux 64 bits binary (lara-linux) and a Mac OS X binary (lara-macosx), for the sake of convenience.

To execute LaRA with a system description contained in a file named, e.g., fddi.noa : ./lara fddi.noa

Case-studies for LaRA

The file lara-t.generators.tgz contains example generator sources (again written in Haskell and to be compiled with, e.g., ghc --make fddi.hs) as well as corresponding Linux 64 bits binaries.

To generate a system description of size s using generator xxx: ./xxx s
For example, fddi of size 3 as used in the paper is generated by: ./fddi 3

Already generated examples of the sizes used in the paper are also provided for the sake of convenience (files called lara-t.input.xxx.tgz).

Case-studies for Uppaal

The file uppaal.inputs.tgz contains Uppaal templates for the examples used in the paper.

The size of each example is defined as follows:

LaRA

L. Jezequel & D. Lime
Feb. 2016

This tool has been presented in the following paper:
Loïg Jezequel and Didier Lime: Lazy Reachability Analysis in Distributed Systems. CONCUR 2016: 17:1-17:14

Files

Dependencies

LaRA is written in Haskell and compiles (at least) with GHC v7.10.3. In addition to standard containers, LaRA uses the Parsec parsing library (tested with v3.1.9) and fgl graph library (tested with v5.5.2.3)

Compilation

To compile LaRA, execute: ghc --make lara.hs

Experiments presented in the paper were done by printing only "True" instead of the whole trace when the property is indeed true. This behavior can be replicated by commenting in/out the adequate lines in lara.hs.

Execution

We provide a Linux 64 bits binary (lara-linux), for the sake of convenience.

To execute LaRA with a system description contained in a file named, e.g., philo.noa : ./lara philo.noa

Case-studies for LaRA

The file lara.generators.tgz contains example generator sources (again written in Haskell and to be compiled with, e.g., ghc --make philo.hs) as well as corresponding Linux 64 bits binaries.

To generate a system description of size s with formula parameter k using generator xxx: ./xxx s k.
For example, Philo of size 15 as used in the paper is generated by: ./philo 15 2

The formula paramater k's meaning is:

Already generated examples of the sizes used in the paper are also provided for the sake of convenience (files called lara.input.xxx.tgz).

Case-studies for LoLA

The file lola.generators.tgz contains example generator sources (again written in Haskell and to be compiled with, e.g., ghc --make philo.hs) as well as corresponding Linux 64 bits binaries.

To generate a system description of size s using generator xxx: lola.generator.xxx/gensys s
To generate the corresponding formula with parameter k: lola.generator.xxx/genformula s k
For example, Philo of size 15 as used in the paper is generated by: lola.generator.philo/gensys 15 followed by lola.generator.philo/genformula 15 2

The formula paramater k's meaning is the same as for LaRA.

Already generated examples of the sizes used in the paper are also provided for the sake of convenience (files called lola.input.xxx.tgz).

Case-studies for CADP

The file cadp.generators.tgz contains example generator sources (again written in Haskell and to be compiled with, e.g., ghc --make philo.hs) as well as corresponding Linux 64 bits binaries.

To generate a system description of size s using generator xxx: cd capd.generator.xxx followed by ./gencomponents s > xxx.lnt then ./genproduct s > xxx.svl and finally svl xxx.svl
To generate the corresponding formula with parameter k: ./genformula s k > prop.mcl
The formula can then be verified with CADP: svl verif.svl

The formula paramater k's meaning is the same as for LaRA.