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

Re: TLA+ and Reals

Thanks for the quick response, Leslie.


On Monday, July 24, 2017 at 8:43:51 PM UTC-4, Leslie Lamport wrote:
I don't remember the details of the paper, but its whole point was to do model checking over a set of integers rather than a set of real numbers.  A check of the models I used for those specs indicates that they substituted Nat for Real and .. for RealInterval.