Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
synthesis:ltlformat [2011/04/19 15:32] – jobstmansynthesis:ltlformat [2011/04/19 15:34] (current) – jobstman
Line 2: Line 2:
  
 This notes are based on a discussion with  This notes are based on a discussion with 
-Viktor Schuppan, Rüiger , and Barbara Jobstmann.+Viktor Schuppan, Rüdiger Ehlers, and Barbara Jobstmann.
  
 In order to obtain a common format, we have to discuss the following topics: In order to obtain a common format, we have to discuss the following topics:
Line 12: Line 12:
   - Title and Meta-information about case studies   - Title and Meta-information about case studies
   - Information about the target: Mealy, Moore, realizability   - Information about the target: Mealy, Moore, realizability
-  - Regular expressions?+  - Regular expressions or automata?
   - How to embed controller synthesis? Ways to specify partial models (see NuGat/NuSMV)   - How to embed controller synthesis? Ways to specify partial models (see NuGat/NuSMV)
  
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 **define** to 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 **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)+  * 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)