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

Small examples in Lustre |