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