TLA+ and Reals

[John Baugh]

I'm reading "Real Time is Really Simple" and attempting to reproduce the results in section 6.3 (Model Checking Our Specifications):

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-30.pdf

When doing so I get the following error (below and attached) when I try to initialize Delta to 5:

Evaluating assumption line 8, col 8 to line 10, col 26 of module FischerPreface failed.

Attempted to check if the value:

5

is an element of the string "Reals"

Perhaps I haven't properly configured the toolbox?  I'm doing this under Mac OS X:

This is Version 1.5.3 of 14 April 2017 and includes:

  - SANY Version 2.1 of 10 February 2016

  - TLC Version 2.09 of 10 March 2017

  - PlusCal Version 1.8 of 07 December 2015

  - TLATeX Version 1.0 of 04 August 2015

Oh, I've modified Tick as suggested in 6.3.1:

Tick == LET d == 1 IN ...

Thanks,

John

[Leslie Lamport]

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

[John Baugh]

Thanks for the quick response, Leslie.

John

[Chris Ortiz]

Hi John,

I am also trying to follow that paper and trying to model check it. I encountered the same problem. What specifically did you do to make the example to work on TLC?

Thanks,

Zitro