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

Re: 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.

(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.)