[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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:

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?


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/78dc63ed-d4a5-4d56-a6b5-0fac83290053n%40googlegroups.com.