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. H On 10/28/2022 8:44 AM, Grundmann, Matthias (KASTEL) 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 <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. 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>.
-- 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/6506cd45-510c-271c-1ccb-9bc7d01a1964%40kit.edu.
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature