Testing timed automata

[dabd]

How do you go about testing timed automata using scalacheck?

A simple example of a timed automaton is a light switch with a button that if you press once will light up, but if you press it twice quickly, it will light up with a brighter light.

See p. 17 of http://people.cs.aau.dk/~ask/Undervisning/MVP/html/mvp5.pdf

[Martin Mauch]

Do you mean how to explicitly deal with time in Scalacheck?

I guess there isn't something in-built, but you could have a look at stateful testing:

https://github.com/rickynils/scalacheck/blob/master/doc/UserGuide.md#stateful-testing

You could start out like the counter example but incorporate the time of the last press into the State type and then calculate the next state by checking how long ago the last press was.