[tlaplus] timers

[Andrew Samokish <asam.mail@xxxxxxxxx>]

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

-- 
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/ae8ae8c1-0036-4a7d-ad3e-458676c81b99n%40googlegroups.com.