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

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