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:32] jobstman |
synthesis:ltlformat [2011/04/19 17:33] 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 **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) |