Hello,
In the following toy example I fail to show with TLC that one spec refines the other when using weak fairness:
The spec consists of three files:
- Counter.tla (overview)
- SimpleCounter.tla (a simple counter)
- ChargingCounter.tla (a slightly less simple counter)
SimpleCounter increments a variable Counter from 0 up to 200. Weak fairness guarantees that the counter counts at least up to 100:
--------------------------- MODULE SimpleCounter ---------------------------
EXTENDS Naturals
VARIABLES
Counter
Init ==
/\ Counter = 0
Next ==
/\ Counter < 200
/\ Counter' = Counter + 1
Spec ==
/\ Init
/\ [][Next]_Counter
/\ Counter < 100 => WF_Counter(Next)
=============================================================================
The ChargingCounter basically does the same but, before incrementing the counter, an internal variable is first "charged" and then added to the counter:
-------------------------- MODULE ChargingCounter --------------------------
EXTENDS Naturals
VARIABLES
Counter,
Internal
vars == <<Counter, Internal>>
Init ==
/\ Counter = 0
/\ Internal = 0
Count ==
/\ Counter < 200
/\ Counter' = Counter + Internal
/\ Internal' = 0
Charge ==
/\ Internal = 0
/\ Internal' = 1
/\ UNCHANGED Counter
Next ==
\/ Count
\/ Charge
Spec ==
/\ Init
/\ [][Next]_vars
/\ Counter < 100 => WF_vars(Next)
=============================================================================
As far as I understand, ChargingCounter is a refinement of SimpleCounter: For every behavior of ChargingCounter there exists a behavior of SimpleCounter in which the Charge step is replaced by a stuttering step.
Without the fairness requirement of SimpleCounter, TLC confirms the refinement relation. However, with the fairness requirement, TLC outputs a trace with just the initial state and the error message "Temporal properties were violated.".
My setup:
------------------------------ MODULE Counter ------------------------------
EXTENDS Naturals
VARIABLES
Counter,
Internal
vars == <<Counter, Internal>>
SimpleCounter == INSTANCE SimpleCounter
ChargingCounter == INSTANCE ChargingCounter ============================================================================= The model uses ChargingCounter!Spec as temporal formula and SimpleCounter!Spec as property. My understanding is that this checks the refinement relation. If I use the property "<>[] (Counter >= 100)" in the model, TLC confirms that the counter reaches 100. Therefore, I expect that ChargingCounter also fulfills the fairness requirement of SimpleCounter and TLC should be able to show that. Where is my misconception? Thank you! Matthias -- 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/ea647b0f-e091-2049-9c76-e0c1ccd81f8b%40kit.edu.
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature