[tlaplus] Re: timers

Real-time spec models work fine when using natural numbers. Just think of 1 as the smallest time resolution you care about. You don't actually need Reals to represent time in any real-world system, because real-world systems don't care about an infinite number of decimal places in the elapsed time.

When you quantify over Int or Nat like that you are quantifying over an infinite set, which TLC can't handle (since it is a finite model checker). You have to use a definition override in your model to restrict Int or Nat to something like 0 .. 10 or whatever. Since this affects all usage of Int or Nat in your spec that can be a bit annoying, so you might want to define something like TimeIncrement == Real in your spec then override TimeIncrement == 0 .. 10 in your model, then use \E d \in TimeIncrement instead of \E d \in Real.

On Tuesday, January 16, 2024 at 11:07:12 AM UTC-5 Andrew Samokish wrote:

Hello everyone,
I`m trying to understand if I can emulate some timers with TLA,
practically, i would like to study some requirements like
'if A stays for 200 ms'
in the context of some other triggers depending on time.
There is a nice book 'Real Time is Really Simple' by Leslie Lamport, but when I tried to rewrite the proposed example with TLA+ toolbox, I found that Real numbers are not really supported with TLA , yet mentioned in the book (btw, it is interesting if code sources for this book are available somewhere..).

for example, here is the Tick definition:
Tick == \E d \in Real: d > 0
/\ \A t \in Thread : ubTimer[t] > d
/\ now' = now + d
/\ (ubTimer' = [ta \in Thread |->
IF ubTimer[ta] = 2147483647 THEN 2147483647
ELSE ubTimer[ta] - d])
/\ (lbTimer' = [tb \in Thread |-> Max(0, lbTimer[tb] -d)])
/\ UNCHANGED << x, PC>>
Can you please tell me if I can substitute Reals with Integers without losing consistency? Also, with \E d \in Int TLA reports, that i`m using uncountable definitions....
And, in general, is it possible to implement a timer reacting at the exact time?

Thanks for the help in advance
Sincerely yours, Andrei