Instructions for LaRA
=====================

L. Jezequel & D. Lime
May 2017


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-T, 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-T 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:

critReg.xml: constant N (currently set to 5)
fddi.xml: constant N (currently set to 10)
fischer.xml: type id_t upper bound (currently set to 6)
fischer2.xml: type id_t uppper bound (currently set to 6)
trains1.xml: constant N (currently set to 6)
trains2.xml: constant N (currently set to 10)
trains3.xml: constant N (currently set to 6)