Differences

This shows you the differences between two versions of the page.

--- synthesis:ltlformat [2011/04/19 17:30]
jobstman created
+++ synthesis:ltlformat [2011/04/19 17:32]
jobstman
@@ Line 18: / Line 18: @@
 ===== Wring LTL-Syntax (used by Lily) =====
-FORMULA    ::= TERM {BINARYOP TERM}
+FORMULA    ::= TERM {BINARYOP TERM}\\
-TERM       ::= {ATOM | (FORMULA) | UNARYOP FORMULA | TEMPORALOP (FORMULA)}
+TERM       ::= {ATOM | (FORMULA) | UNARYOP FORMULA | TEMPORALOP (FORMULA)}\\
-BINARYOP   ::= * | + | ^ | -> | <-> | U | R | V
+BINARYOP   ::= * | + | ^ | -> | <-> | U | R | V\\
-UNARYOP    ::= !
+UNARYOP    ::= !\\
-TEMPORALOP ::= G | F | X
+TEMPORALOP ::= G | F | X\\
-ATOM       ::= VAR=VALUE
+ATOM       ::= VAR=VALUE\\
-VAR        ::= \w+
+VAR        ::= \w+\\
-VALUE      ::= 0 | 1
+VALUE      ::= 0 | 1\\
-Furthermore, Wring allows you to use the keyword "define" to avoid writing the same formula multiple times
+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); assume G(b); assert G(c);" corresponds to "(G(a) * G(b)) -> G(b)".
+  * 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)