[tlaplus] Re: Translational Symmetry for Model Checking

[Willy Schultz <will62794@xxxxxxxxx>]

Thanks, that thread is helpful! I was thinking about it in the context of distributed protocols that utilize various types of logical version numbers. One thought was to define a VIEW function that looks at all version values in the current state, and shifts them all downward so the smallest version in that state is sent to zero e.g.

View(1,1,1) == (0,0,0) 

View(1,2,1) == (0,1,0)

View(1,2,4) == (0,1,3) 

I attached a simple experiment of this for a toy quorum based election protocol based on monotonically increasing terms/epochs. The VIEW _expression_ in TLA+ is written as:

MinTerm == Min(Range(currentTerm))

currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]

View == <<currentTermsShifted, state>>

where currentTerm is variable that maps from server identifiers to natural numbers. 

Without the view _expression_ and setting a state constraint of MaxTerm=10, TLC finds 631 reachable states for the SimpleElection spec and attached config. With the VIEW _expression_ enabled it finds 118 reachable states. For a MaxTerm=20 it finds 2461 states without the view, and 238 states with the view. For a MaxTerm=50 it finds 15151 states without the view and 598 states with it. I wonder if this approach would help reduce model checking burden for some real world specs, or if the gains in most cases wouldn't be significant enough to warrant it.

I suppose it may be sound in some cases to abstract further and have the view _expression_ only look at the ordering relationships between counter values in a state. This seems like a kind of manual predicate abstraction i.e. if a protocol only depends on the fact that one value is <,>,= another, but doesn't care about the concrete values. This seems to echo some of Ron's comments in the linked thread.

Will

-- 
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/004d850e-5165-43aa-8e6d-04d025d16aefn%40googlegroups.com.
---- MODULE SimpleElection ----
EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC

CONSTANTS Server
CONSTANTS Secondary, Primary, Nil
CONSTANT InitTerm

VARIABLE currentTerm
VARIABLE state

vars == <<currentTerm, state>>

\* The set of all quorums in a given set.
Quorums == {i \in SUBSET Server : Cardinality(i) * 2 > Cardinality(Server)}

\* Node 'i' gets elected as a primary.
BecomeLeader(i, voteQuorum) == 
    LET newTerm == currentTerm[i] + 1 IN
    /\ i \in voteQuorum \* The new leader should vote for itself.
    /\ \A v \in voteQuorum : currentTerm[v] < newTerm
    \* Update the terms of each voter.
    /\ currentTerm' = [s \in Server |-> IF s \in voteQuorum THEN newTerm ELSE currentTerm[s]]
    /\ state' = [s \in Server |->
                    IF s = i THEN Primary
                    ELSE IF s \in voteQuorum THEN Secondary \* All voters should revert to secondary state.
                    ELSE state[s]]    \* Allow new leaders to write a no-op on step up if they want to. It is optional, but permissible.

Init == 
    /\ currentTerm = [i \in Server |-> InitTerm]
    /\ state       = [i \in Server |-> Secondary]

Next == \E s \in Server : \E Q \in Quorums : BecomeLeader(s, Q)

Spec == Init /\ [][Next]_vars

UniqueLeader == \A s,t \in Server : 
    (/\ state[s] = Primary 
     /\ state[t] = Primary
     /\ currentTerm[s] = currentTerm[t]) => (s = t)

------------------------------------------------

CONSTANTS MaxTerm

StateConstraint == \A s \in Server : currentTerm[s] <= MaxTerm

Range(T) == { T[x] : x \in DOMAIN T }
Min(S) == CHOOSE x \in S: \A y \in S \ {x}: y > x

\*
\* Define a view expression that shifts all terms so 
\* that the minimum term value in the current state is shifted
\* down to zero.
\*

MinTerm == Min(Range(currentTerm))

currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]

View == <<currentTermsShifted, state>>

=============================================================================

INIT Init
NEXT Next

CONSTANTS 
Nil = Nil
Server = {n1,n2,n3}
Secondary = Secondary
Primary = Primary
MaxTerm = 50
InitTerm = 0
CONSTRAINT StateConstraint
INVARIANT UniqueLeader
VIEW View