Em sexta-feira, 5 de março de 2021 às 03:01:05 UTC+1, andrew...@xxxxxxxxx escreveu:
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
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?