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 ------------------
INSTANCE TLC
INSTANCE Naturals
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 --------------------------------
C == INSTANCE Clock
VARIABLES x, 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
]_<<x,y>>
/\ 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 --------------------------------
C == INSTANCE Clock
CONSTANT N
ASSUME N \in Nat
Clock == 1..N
VARIABLES hr \* 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]
]_<<hr>>
======================================================================
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?.
Thanks.