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

TLA+ and Reals

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


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


Attachment: tla-reals.png
Description: PNG image