Section 3.4 is about history variables, which track prior states
of the spec. In this case RandomH isn't actually using a history
variable.
I intuitively think of Spec1 => \EE x: Spec2 as
saying that Spec1 refines an aspect of Spec2. We might use
it, for example, if Spec1 is a detailed server model and spec2 is
the high level interactions of a server and a client. then we'd
use this refinement to say that Spec1 refines the behavior of the
server in Spec2, if we hide all the behavior of the client.
In your case, you're showing that Random!Spec accurately
represents the part of RandomH related to a random
choice, if you hide all the behavior of the incrementing counter.
H
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