[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 ------------------INSTANCE TLCINSTANCE NaturalsInit(h) == h \in 1..12 Next(h) == h' = IF h # 12 THEN h + 1 ELSE 1Spec(h) == Init(h) /\ [][Next(h)]_h /\ WF_h(Next(h))=============================================

Now, say i want to compose two clocks outside:
---------------------- MODULE OtherPlace --------------------------------C == INSTANCE ClockVARIABLES x, y \* Composing two clocks TwoClocks1 == C!Spec(x) /\ C!Spec(y)\* The same as before but in "canonical form", so TLC can understand itTwoClocks2 == /\ 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 ClockCONSTANT NASSUME N \in NatClock == 1..NVARIABLES hr   \* supposed to be in [c \in Clock |-> 1..12]\* Composing every clock in the arrayAnyClocks1 == \A c \in Clock : C!Spec(hr[c])       \* This should be the same as before but in "canonical form", so TLC can understand itAnyClocks2 == /\ \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.

--
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.