Additional material to the GandALF paper "LTL to Deterministic Emerson-Lei Automata"
# 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

You can find a zip of Delag here. Please note the README file in the top directory (and ignore the README.md file).
Shortly, 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.