Examples using Reals?

[Brian Beckman <bc.be...@xxxxxxxxx>]

I'm seeking some example specifications using Reals (from Figure 18.8 in "Specifying Systems.")  I'd be especially interested in models that can be checked by TLC, though I understand that because the Reals are not enumerable, it won't be possible to enumerate states that include Real values in any trivial way.