[tlaplus] Re: Refinement and Fairness

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hi Matthias,

I think you and I hit similar problems [1]. By adding a condition before some temporal property (including weak and strong fairness), we get some unusual behaviors.

I thought the problem was the deadlock in both SimpleCounter.tla and ChargingCounter.tla. I fixed the deadlocks, checked the refinement property again, but I still got the "Temporal properties were violated." message and the initial predicate as a counterexample, just like you.

PS: FYI, instead of using the Counter.tla file, I checked refinement by writing this in ChargingCounter.tla:

SC == INSTANCE SimpleCounter

Refinement == SC!Spec

And this in ChargingCounter.cfg:

PROPERTY Refinement

In summary, I can't help you, but I'm listening to the thread in case someone has an answer.

Best,

Jones

[1]: https://groups.google.com/g/tlaplus/c/EO9ff0OBqtA

On Friday, 12 May 2023 at 05:43:41 UTC-3 Grundmann, Matthias (KASTEL) wrote:

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/41789992-0530-4e33-90c3-094f5390a450n%40googlegroups.com.