Unbounded CHOOSE while using Standard Module Reals

50 views
Skip to first unread message

Felipe Lisboa

unread,
Mar 4, 2021, 11:42:19 AM3/4/21
to tlaplus
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,


Felipe Lisboa

unread,
Mar 4, 2021, 11:47:36 AM3/4/21
to tlaplus
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.

Andrew Helwer

unread,
Mar 4, 2021, 9:01:05 PM3/4/21
to tlaplus
You need to override the definition of both Real and Infinity. For my spec, I defined Infinity to be the value 100 and Real to be the set 0 ..10 \cup {Infinity}. If you're expected your clock or timers to go above 10 you'll need to increase the size of the Real set as necessary.

If you're using the set Real in other contexts in the spec that require a different override, you can solve this problem by writing something like the following definitions:

\* Possible values for a clock to take, in arbitrary units.
Time == {t \in Real : t >= 0}
\* A time window of nonzero length.
TimeSpan == {t \in Time : t > 0}


Then you can override the definitions of Time and TimeSpan specifically instead of Real generally.

Andrew

Felipe Lisboa

unread,
Mar 5, 2021, 7:19:43 AM3/5/21
to tlaplus
Hey, thanks again Andrew. Very useful answer. Problem solved.
Reply all
Reply to author
Forward
0 new messages