# [tlaplus] Meaning of "equivalence" of specifications

• From: "Grundmann, Matthias (KASTEL)" <matthias.grundmann@xxxxxxx>
• Date: Fri, 28 Oct 2022 15:44:28 +0200
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.4.1

Hello,

I'm trying to understand what exactly it means if two specifications are "equivalent". As an example, I've created two specifications and, as far as I understand the method presented in [1], we can show that these specifications are equivalent although my intuition says that they are not. The first specification (CounterUp) models a simple counter that always increments a variable by 1 and the second specification (Random) sets a variable in each step to a random value.

The two specifications are defined as follows:

----------------------------- MODULE CounterUp -----------------------------
EXTENDS Integers
VARIABLE counter
CONSTANT max
Init == counter = 0
Next == counter' = IF counter < max THEN counter + 1 ELSE
Spec == Init /\ [][Next]_counter
=============================================================================

------------------------------- MODULE Random -------------------------------
EXTENDS Integers
VARIABLE choice
CONSTANT max
Init == choice \in 0..max
Next == choice' \in 0..max
Spec == Init /\ [][Next]_choice
=============================================================================

It is intuitive that CounterUp!Spec => Random!Spec as incrementing a value by 1 is a special case of choosing the next value arbitrarily.
To show this implication, we add "Random == INSTANCE Random WITH choice <- counter" to the module CounterUp. Now, we can show "THEOREM CounterUp!Spec => Random!Spec" by running TLC for a model for CounterUp with the temporal formula "Spec" checking the property "Random!Spec".

To show Random!Spec => CounterUp!Spec, we introduce a new specification RandomH defined as follows (along the lines of [1, Section 3.1]):

------------------------------ MODULE RandomH ------------------------------
EXTENDS Random
VARIABLE h
varsH == <<choice, h>>
InitH == Init /\ h = 0
NextH == Next /\ h' = IF h < max THEN h + 1 ELSE 0
SpecH == InitH /\ [][NextH]_varsH

CounterUp == INSTANCE CounterUp WITH counter <- h
THEOREM SpecH => CounterUp!Spec
=============================================================================

According to Theorem 1 of [1], Random!Spec is equivalent to \EE h : RandomH!SpecH (1).
Using the definition "CounterUp == INSTANCE CounterUp WITH counter <- h" (second last line of module RandomH), we can show that RandomH!SpecH => CounterUp!Spec (2).
According to [1, Section 3.4], it follows from (1) and (2) that Random!Spec => CounterUp!Spec (or maybe Random!Spec => \EE h : CounterUp!Spec ???).

Having shown the two implications, we have shown that Random!Spec is equivalent to CounterUp!Spec.
I conclude that a system that counts is equivalent to a system that chooses values arbitrarily. This result contradicts my intuition which says that counting is not equivalent to choosing values arbitrarily. -- It might be that my intuition is wrong. It might be that my conclusion is wrong as I might have misunderstood what "equivalence" means in this context. It might be that I have included a methodological flaw above (see the "???"). What are your thoughts? What does it mean for one specification to be equivalent to another specification?

Thanks!

Matthias

[1] Lamport, Leslie, and Stephan Merz. “Auxiliary Variables in TLA+”. https://lamport.azurewebsites.net/pubs/auxiliary.pdf

--
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/57ba9669-3f80-b725-a7d4-6e4daf3b6d33%40kit.edu.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature