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

[tlaplus] Composing multiple instances of a clock specification

Hello all,

Currently researching module composition on TLA+. 
Suppose we have a parametrized Clock specification like the one we see in Lamport's Specifying Systems:

-------------- MODULE Clock ------------------


Init(h) == h \in 1..12
Next(h) == h' = IF h # 12 THEN h + 1 ELSE 1
Spec(h) == Init(h) /\ [][Next(h)]_h /\ WF_h(Next(h))


Now, say i want to compose two clocks outside:
---------------------- MODULE OtherPlace --------------------------------


, y

\* Composing two clocks
TwoClocks1 == C!Spec(x) /\ C!Spec(y)

\* The same as before but in "canonical form", so TLC can understand it
TwoClocks2 == /\ C!Init(x) /\ C!Init(y)
/\ [][ \/ C!Next(x) /\ C!Next(y)
\/ C!Next(x) /\ y' = y
                     \/ C!Next(y) /\ x'
= x
/\ WF_x(C!Next(x)) /\ WF_y(C!Next(y))

Now there are two (independent) clocks as a no-interleaving specification. 
For interleaving we can get ride of the  C!Next(x) /\ C!Next(y) action.

But suppose i want an arbitrary number of clocks. The book have an example with an array of clocks. 
I will try to reproduce something similar here:

---------------------- MODULE OtherPlace --------------------------------


\in Nat

Clock == 1..N

\* supposed to be in [c \in Clock |-> 1..12]

\* Composing every clock in the array
AnyClocks1 == \A c \in Clock : C!Spec(hr[c])      

\* This should be the same as before but in "canonical form", so TLC can understand it
AnyClocks2 == /\ \A c \in Clock : C!Init(hr[c])
\ [][ \/ \E i,j \in Clock : i # j /\ C!Next(hr[i]) /\ C!Next(hr[j])
\/ \E c \in Clock : C!Next(hr[c]) /\ \A i \in Clock\{c} : hr[i]' = hr[i]

This fails on TLC with "hr is undefined". Even if we state it is a function on the initial predicate, 
and state hr[c]' for every c is not enough, it looks like we cant guarantee hr will be a function forever.
This is addressed in the book with a couple of suggestions. 

Currently to make this work i need to redefine the clock specification, for example with:
CNext(c) == hr' = [hr EXCEPT ![c]= IF hr[c] # 12 THEN hr[c] + 1 ELSE 1]
However, i think this will force an interleaving specification because is saying only one component will change, 
so the first action in the Next disjunction cant be taken. So i guess this can be a solution for interleaving.

I cant redefine it like
CNext(c) == hr[c]' = IF hr[c] # 12 THEN hr[c] + 1 ELSE 1
because it causes the same problem that "hr is undefined".

But... i dont really want to redefine the clock specification to make this work. I would like to use the Clock module as it is,
just like in the two clocks version. Is this possible?.


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/837b0340-ae10-4762-afa3-0a428bdfbd7a%40googlegroups.com.