[tlaplus] Re: Translational Symmetry for Model Checking

One interesting thing Leslie talks about a lot in Real Time (and somewhat mentioned in the other thread) is that these sorts of VIEW functions have model checking correctness implications. I wonder whether there is some general way of writing & testing a refinement relation to ensure that reducing all the counters modulo some number maintains all the important invariants of your spec, and no valid behaviors are accidentally removed.

On Thursday, June 17, 2021 at 6:53:09 PM UTC-4 will...@xxxxxxxxx wrote:

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