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

[tlaplus] timers

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.