[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Fri, 28 Oct 2022 08:03:36 -0700 (PDT)*References*: <57ba9669-3f80-b725-a7d4-6e4daf3b6d33@kit.edu> <b6e2ff30-aee1-4704-adb3-9e3f1238c882n@googlegroups.com>

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

On Friday, October 28, 2022 at 10:51:14 AM UTC-4 Andrew Helwer wrote:

Not sure I follow. YourRandomHmodule parameterizesCounterUpwith the variableh, not the variablechoice. And inRandomHthe variablehis updated in the same waychoiceis updated inCounterUp. So of courseRandomH!SpecHis an implementation ofCounterUp!Spec,becauseRandomHis justCounterUpwith an extra variable (calledchoicewhich might be confusing) that does random stuff.AndrewOn Friday, October 28, 2022 at 9:44:34 AM UTC-4 Matthias Grundmann wrote: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/6f6e0812-a798-4c0f-8f15-f04e19c425ccn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Re: Meaning of "equivalence" of specifications***From:*Grundmann, Matthias (KASTEL)

**Re: [tlaplus] Re: Meaning of "equivalence" of specifications***From:*Hemanth Kapila

**References**:**[tlaplus] Meaning of "equivalence" of specifications***From:*Grundmann, Matthias (KASTEL)

**[tlaplus] Re: Meaning of "equivalence" of specifications***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: Meaning of "equivalence" of specifications** - Next by Date:
**Re: [tlaplus] Re: Meaning of "equivalence" of specifications** - Previous by thread:
**[tlaplus] Re: Meaning of "equivalence" of specifications** - Next by thread:
**Re: [tlaplus] Re: Meaning of "equivalence" of specifications** - Index(es):