# [tlaplus] Re: Unbounded CHOOSE while using Standard Module Reals

Edited the message and forgot to change the subject. However, to explain the problem related to the subject, a similar problem comes up when trying to init uper-bound timers with Infinity. In this case, TLC gives an error of the type : Error while evaluating unbounded CHOOSE _expression_.

Em quinta-feira, 4 de março de 2021 às 17:42:19 UTC+1, Felipe Lisboa escreveu:
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.