Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
synthesis:ltlformat [2011/04/19 17:30] jobstman |
synthesis:ltlformat [2011/04/19 17: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 19: | Line 19: | ||
| 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: | 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); 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) |