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.Leslie