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

*From*: John Baugh <jwb...@xxxxxxxxx>*Date*: Tue, 25 Jul 2017 06:32:58 -0700 (PDT)*References*: <4b855f06-b297-42fb-8896-5f627b8502aa@googlegroups.com> <cf0406de-2f4a-42ea-a83e-5b1a7e696c21@googlegroups.com>

Thanks for the quick response, Leslie.

On Monday, July 24, 2017 at 8:43:51 PM UTC-4, Leslie Lamport wrote:

John

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

**References**:**TLA+ and Reals***From:*John Baugh

**Re: TLA+ and Reals***From:*Leslie Lamport

- Prev by Date:
**Re: TLA+ and Reals** - Next by Date:
**New to TLA, Can't figure out the example work** - Previous by thread:
**Re: TLA+ and Reals** - Next by thread:
**New to TLA, Can't figure out the example work** - Index(es):