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

Re: [tlaplus] Composing multiple instances of a clock specification



Hello,

I recall that Leslie at some point wrote a note about exactly the issue that you mention, but I don't seem to be able to find it on the TLA Web site.

In essence the problem is that writing something like

(1)  \A x \in S : f[x] = e

is weaker than writing

(2)  f = [x \in S |-> e]

because (1) doesn't tell us that the domain of f is S, or in fact that f is a function. You can strengthen (2) by writing

(3) f \in [S -> T] /\ \A x \in S : f[x] = e

for some suitable set T. Applying this line of thought to your clock specification you could write

AnyClocks1 ==
  /\ [](hr \in [Clock -> 1 .. 12])
  /\ \A c \in Clock : C!Spec(hr[c])

or, in a form suitable for TLC,

AnyClocks2 == 
  /\ \A c \in Clock : (hr \in [Clock -> 1 .. 12]) /\ C!Init(hr[c])
  /\ [][ /\ hr' \in [Clock -> 1 .. 12]
         /\ \A c \in Clock : [C!Next(hr[c])]_<<hr[c]>>
       ]_<<hr>>

and these are perfectly fine TLA+ specifications. The downside is that TLC will enumerate the set of all functions of the given shape and then filter out those that satisfy the initial and next-state conditions, so this approach will not scale for TLC. (It's not an issue when you write proofs using TLAPS.)

If I recall correctly, Leslie's conclusion was that it wasn't worth composing components in this way but better to start with a specification of an array of components in the first place.

Stephan


On 27 May 2020, at 08:13, JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:

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.


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

--
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/E46A7913-D473-4058-8AC3-3158353CC898%40gmail.com.