[tlaplus] Unbounded CHOOSE while using Standard Module Reals

[Felipe Lisboa <lisboafelipe5@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bd69edf1-dc54-4afc-84e7-bb7536cc6e0bn%40googlegroups.com.