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. Submitted to FORMATS 2017
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).
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.
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
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).
The file uppaal.inputs.tgz contains Uppaal templates for the examples used in the paper.
The size of each example is defined as follows:
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
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)
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.
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
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).
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).
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.