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

Re: TLA+ and Reals

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.