tulip-control/tulip-control — pull request #110 by johnyf (2014-10-04 09:00:28+00:00)
Title: Lily

Adds interface to the full LTL synthesis tool [`Lily`](http://www.iaik.tugraz.at/content/research/design_verification/lily/) and thus close #32. The available choices of LTL solvers are listed [here](https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md#full-ltl-games) (so excluding parity game solvers for this).

From these:

- `GAVS+` is `Java`, GUI-oriented, and a bit too feature-full
- `GASt` is not really open-source
- `Unbeast` has obfuscated source code
- `Acacia` and `Alaska` have been superseded by `Acacia+`

so these are not candidates.

The remaining contenders are `Acacia+` and `Lily`. `Acacia+` has the advantages that:

- it is `python` on the surface
- currently maintained.

But it:

- includes `C`, so it needs compilation
- requires (a patched) `Lily`, so it is at least as difficult to install as `Lily`.

For this reason, as a first choice `Lily` was selected, even though it is the oldest (apparently the first LTL synthesizer) and recently updated. It's installation is easy and cross-platform, because it is written in `Perl`.