Small examples in Lustre
- DurationThm
- The Lustre
file contains 3 theorems of the duration calculus, submitted by
Paritosh Pandya who wrote the
DCVALID verification tool for Duration Calculus. The advantage of NBac is the
ability to prove theorems for any values of the parameters, whereas DCVALID
uses more classical finite-state techniques.
The two first theorems are easy, the last theorem is becoming tricky.
Bertrand Jeannet, February 10, 2011
