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

*From*: JosEdu Solsona <josedusolsona@xxxxxxxxx>*Date*: Tue, 26 May 2020 23:13:14 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] Composing multiple instances of a clock specification***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: TLC Java exception** - Next by Date:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Previous by thread:
**Re: [tlaplus] Re: TLC Java exception** - Next by thread:
**Re: [tlaplus] Composing multiple instances of a clock specification** - Index(es):