Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
synthesis:ltlformat [2011/04/19 17:32]
jobstman
synthesis:ltlformat [2011/04/19 17:32]
jobstman
Line 27: Line 27:
 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 ​*defineto avoid writing the same formula multiple times.\\
  
 Extensions in Lily: Extensions in Lily:
   * A formula can range over several lines. A semi-colon indicates the end of the formula.   * 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" +  * Each formula can be prefixed with the keyword ​*assumeor *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)+  * 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.,​\\ ​*assumeG(a=1);​\\ ​*assumeG(b=1);​\\ ​*assertG(c=1);\\ corresponds to (G(a=1) * G(b=1)) -> G(c=1)