Additional material to the GandALF paper "LTL to Deterministic Emerson-Lei Automata"

On this home page you find the implementation of Delag and PRISM to reproduce the experiments of the paper.

Delag

Delag is now a part of Owl, a library for LTL and omega-automata. You can find the newest version of Delag here.
To obtain the version on which the submission is based, please unpack this zip file. Please note the README file in the top directory (and ignore the README.md file).
Independently of the version you use, you can translate an LTL formula by giving them just as a parameter:


    ./delag '(F G a) | (F G b)'

LTL formulae

For your convenice, we have also added the LTL formulas. The mapping of the files is as follows

File	Description
literature.ltl	Literature formulas of [29,7,10]
alternating.ltl	Formula phi_{R,n} for n from 0 to 8
historyVsAfter.ltl	Formula phi_{H,n} for n from 0 to 10

Please note, that these formula are in prefix normal form of LBT. You can convert them using SPOT. For example, to convert
| F G a F G b
please use:
ltlfilt --full-parentheses --lbt-input --unabbreviate="MRW" -f '| F G a F G b'

PRISM

Our PRISM implementation based on PRISM 4.3.1 dev can be found here. To compile PRISM change into the prism/prism subdirectory and run make. A binary prism will be placed in prism/prism/bin To execute PRISM, we refer to README file contained in the top directory.

PRISM material

The material for PRISM can be found here. It contains the IEEE 802.11 model (wlan2.pm) and the properties (wlanX.pctl). Please note, since we reused some properties for maximal and minimal probabilities, the mapping is as follows:

File	Description
wlan1.pctl	Pmin(varphi1)
wlan2.pctl	Pmin(varphi2)
wlan3.pctl	Pmin(varphi3)
wlan4.pctl	Pmin(varphi4)
wlan5.pctl	Pmax(varphi4)
wlan6.pctl	Pmin(varphi5)
wlan7.pctl	Pmax(varphi5)
wlan8.pctl	Pmin(varphi6)
wlan9.pctl	Pmin(varphi7)

SPOT

We use SPOT (version 2.3.8) for some LTL formula format translations. To install SPOT, please follow the instructions here. We configured and compiled SPOT with the options --disable-devel and --disable-debug.