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