# [tlaplus] Unbounded CHOOSE while using Standard Module Reals

Hey,

In the context of writing a DRAM controller spec, I followed Lamport's procedure described in "Real Time is Really Simple", which consists of using countdown timers to model my timing constraints.

I added a type invariant predicate to check type-check my timers (see below) and I am initializing them with 0. But TLC gives me:

Attempted to check if the value 0 is an element of the string "Reals".

TimeTypeOK ==
/\ cmds_lbtimer \in [Banks \X CMDS] -> Real]
/\ arvl_lbtimer \in [Requestors -> Real]
/\ chsl_lbtimer \in Real
/\ now \in {r \in Real : r =< maxtime}

Why is this ? Is there something wrong with the standard module Reals?

Thanks,

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.