[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Examples using Reals?

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.