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.
(I have not the answer to that question but I'm afraid that anything in computer science is numerable even reals.)
I take this opportunity to say that current number management in TLC might be a bit improved. On a 32-bit machine it is impossible to use the quantity
2 ^ 32 -1 in a ASSUMPTION for instance. I understand that ints are used behind the scene and that I would be answered that one can use another value.
All that is true. But well in computer engineering 2 ^32 - 1 makes senses and you can expect to be able to introduce such a calculation in a specification.
So if it is possible to change, without too much fuss, the way TLC manages numbers it would avoid bafflement to users. (No need for gigantic
values. Only those that are at the limits of the 32 bits or 64 bits would suffice.)
(Another improvement that I would suggest to language designers. Commas in numbers help the imperfect machine called (wo)man reading them.)
--
FL