====== Notes on a common format for LTL Synthesis ======

This notes are based on a discussion with 
Viktor Schuppan, Rüdiger Ehlers, and Barbara Jobstmann.

In order to obtain a common format, we have to discuss the following topics:
  - Subset definitions (e.g., GR-1, Safety, Reachability,...)
  - Necessary abbreviations: assume, assert, define, other shortcuts? (see Lily syntax)
  - Order for BDD-based approaches
  - XML-format (see Unbeast)
  - LTL syntax (e.g., Wring syntax from below)
  - Title and Meta-information about case studies
  - Information about the target: Mealy, Moore, realizability
  - Regular expressions or automata?
  - How to embed controller synthesis? Ways to specify partial models (see NuGat/NuSMV)


===== Wring LTL-Syntax (used by Lily) =====

FORMULA    ::= TERM {BINARYOP TERM}\\
TERM       ::= {ATOM | (FORMULA) | UNARYOP FORMULA | TEMPORALOP (FORMULA)}\\
BINARYOP   ::= * | + | ^ | -> | <-> | U | R | V\\
UNARYOP    ::= !\\
TEMPORALOP ::= G | F | X\\
ATOM       ::= VAR=VALUE\\
VAR        ::= \w+\\
VALUE      ::= 0 | 1\\

Furthermore, Wring allows you to use the keyword **define** to avoid writing the same formula multiple times.\\

Extensions in Lily:
  * A formula can range over several lines. A semi-colon indicates the end of the formula.
  * Each formula can be prefixed with the keyword **assume** or **assert**
  * In general, a semi-colon acts as conjunction between formulas unless the assume/assert keywords are used. Then, the list of formulas corresponds to an implication between a conjunction of all formulas assumed and a conjunction of all formulas asserted. E.g.,\\ **assume** G(a=1);\\ **assume** G(b=1);\\ **assert** G(c=1);\\ corresponds to (G(a=1) * G(b=1)) -> G(c=1)