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

[tlaplus] Refinement and Fairness



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