Meaning of "equivalence" of specifications

[Grundmann, Matthias (KASTEL)]

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

[Andrew Helwer]

Not sure I follow. Your RandomH module parameterizes CounterUp with the variable h, not the variable choice. And in RandomH the variable h is updated in the same way choice is updated in CounterUp. So of course RandomH!SpecH is an implementation of CounterUp!Spec, because RandomH is just CounterUp with an extra variable (called choice which might be confusing) that does random stuff.

Andrew

[Andrew Helwer]

Oops forgot to also say the definition of spec equivalence. Two specs are equivalent if they generate the same set of behaviours, optionally with consistent renaming of variables. Saying that spec A implies spec B  (so A implements B) is saying that if you take the set of behaviours generated by A, and project those behaviours to a subset of A's variables (optionally with consistent renaming), then it is the same set of behaviours as generated by B. So if you have A => B and B => A, then A and B are equivalent, because if two sets are subsets of each other then they must be equivalent - so the behaviors of A and B are equivalent when looking at all variables.

Andrew

[Hemanth Kapila]

On Fri, Oct 28, 2022 at 8:33 PM Andrew Helwer <andrew...@gmail.com> wrote:
>
> Oops forgot to also say the definition of spec equivalence. Two specs are equivalent if they generate the same set of behaviours, optionally with consistent renaming of variables. Saying that spec A implies spec B (so A implements B) is saying that if you take the set of behaviours generated by A, and project those behaviours to a subset of A's variables (optionally with consistent renaming), then it is the same set of behaviours as generated by B. So if you have A => B and B => A, then A and B are equivalent, because if two sets are subsets of each other then they must be equivalent - so the behaviors of A and B are equivalent when looking at all variables.
>
> Andrew

Is equivalence the same as Bisimulation [0]?
[0]https://en.wikipedia.org/wiki/Bisimulation

[Grundmann, Matthias (KASTEL)]

Thanks for the reply, Andrew!

> and project those behaviours to a subset of A's variables (optionally with consistent renaming)

This might be the point that I was missing. However, I'm not sure whether I really understand it. Does it mean something like implication and equivalence are "parameterized by a set of variables"? In my initial example, this could mean that CounterUp and RandomH are equivalent with respect to the variable counter and RandomH and Random are equivalent with respect to the variable choice. And because these two equivalences are "two different kinds of equivalence", the equivalence is not transitive and CounterUp is not equivalent to Random? This would intuitively make sense.
Is a formal definition for implication that captures this aspect written up somewhere?

Matthias

[Stephan Merz]

Hello,

two TLA+ formulas F and G (in particular, two specifications) are equivalent if for any sequence of states sigma,

sigma |= F iff sigma |= G.

In other words, the two formulas are satisfied by the same behaviors. Since the formulas Spec from your two modules do not have the same variables (and are both satisfiable but not valid), they cannot be equivalent. For example, a behavior sigma such that

sigma_i(counter) = IF i < max THEN i ELSE max
sigma_i(choice) = -1

satisfies CounterUp!Spec but not Random!Spec.

Instead, what your argument shows is that both

(*) CounterUp!Spec => \EE choice : Random!Spec

and

(**) Random!Spec => \EE counter : CounterUp!Spec

hold, and indeed the use of \EE is important here. It follows that (\EE choice : Random!Spec) and (\EE counter : CounterUp!Spec) are equivalent.

In fact, neither of the two implications above should come as a surprise: the formulas on the right-hand sides of these implications have no free variables (in logicians' terms, they are "closed formulas") and must therefore be equivalent to either TRUE or FALSE, but since the inner formula is satisfiable, they must be equivalent to TRUE.

Had you used the same state variable in specifications CounterUp!Spec and Random!Spec, you could indeed verify that

CounterUp!Spec => Random!Spec

holds. In other words, CounterUp!Spec is a refinement of Random!Spec. The reverse implication does not hold, i.e. here the use of hiding is essential. However, if h were called counter then you could verify

RandomH!Spec => CounterUp!Spec

which again is unsurprising because the history variable mirrors the behavior of the counter.

It is probably somewhat confusing that the TLA+ tools do not support \EE directly. Instead of model checking the implications (**) and (**), you actually check, say,

CounterUp!Spec => (Random!Spec WITH choice <- counter)

where the latter formula is not actual TLA+ syntax but denotes substitution of the term "counter" for the variable "choice". The soundness of adding a history variable cannot be checked using the current TLA+ tools at all.

I do hope this explanation helps more than it adds to the confusion!

Stephan

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57ba9669-3f80-b725-a7d4-6e4daf3b6d33%40kit.edu.

[Hillel Wayne]

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

[Grundmann, Matthias (KASTEL)]

Thank you, Stephan and Hillel, your explanations cleared up my confusion. I think I disregarded the importance of the \EE operator.

Matthias

On 28.10.22 17:55, Hillel Wayne wrote:
> 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.

> --
> 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+u...@googlegroups.com <mailto:tlaplus+u...@googlegroups.com>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/159294fc-925c-d5f3-bf1c-e0d2c3564687%40gmail.com <https://groups.google.com/d/msgid/tlaplus/159294fc-925c-d5f3-bf1c-e0d2c3564687%40gmail.com?utm_medium=email&utm_source=footer>.