Refinement and Fairness

50 views
Skip to first unread message

Grundmann, Matthias (KASTEL)

unread,
May 12, 2023, 4:43:41 AM5/12/23
to tla...@googlegroups.com
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

Message has been deleted

Stephan Merz

unread,
May 13, 2023, 10:35:12 AM5/13/23
to tla...@googlegroups.com
I don't understand why your specifications include the conjunct

Counter < 100 => WF_Counter(Next)

Note that this implication is evaluated in the initial state of a behavior because it is not in the scope of a temporal operator. Since Counter is initialized to 0, the formula is simply equivalent to

WF_Counter(Next)

But perhaps you meant to assert that the counter should eventually be incremented in states where the counter value is less than 100. This is expressed by the fairness condition

WF_Counter(Counter < 100 /\ Next)

Anyway, for me TLC successfully checks refinement using either your original specs or the ones where your fairness condition is replaced with either of the above ones (and inconsistent replacements of fairness conditions show the expected counter-examples). I am using TLC from the VS/Code extension with the modules / configuration file attached to this message and deadlock checking disabled. The version of TLC is identified as

TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)

Stephan

ChargingCounter.cfg
ChargingCounter.tla
SimpleCounter.tla

Grundmann, Matthias (KASTEL)

unread,
May 16, 2023, 3:20:36 AM5/16/23
to tla...@googlegroups.com
Hello,

> Note that this implication is evaluated in the initial state of a behavior because it is not in the scope of a temporal operator. Since Counter is initialized to 0, the formula is simply equivalent to
>
> WF_Counter(Next)
>
> But perhaps you meant to assert that the counter should eventually be incremented in states where the counter value is less than 100. This is expressed by the fairness condition
>
> WF_Counter(Counter < 100 /\ Next)

Thank you, for the explanation! That was what I actually wanted to express.
After changing this line, everything works as I expect.


Btw, when checking which version of TLC I have, I found that the toolbox reports inconsistent information:
Help -> About shows

> This is Version 1.8.0 of Day Month Year and includes:
> - SANY Version 2.2 of 20 April 2020
> - TLC Version 2.15 of 20 April 2020

While TLC Model Checker -> TLC Console shows in the first line

> TLC2 Version 2.18 of Day Month 20?? (rev: ca5ad64)

I'm running the latest release of the toolbox from Github (https://github.com/tlaplus/tlaplus/releases#latest-tla-files).

Matthias
Reply all
Reply to author
Forward
0 new messages