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

[tlaplus] Unbounded CHOOSE while using Standard Module Reals


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/bd69edf1-dc54-4afc-84e7-bb7536cc6e0bn%40googlegroups.com.