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 -- 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/E12608A4-5B86-413A-8B31-A91822D31703%40gmail.com.
Attachment:
ChargingCounter.cfg
Description: Binary data
Attachment:
ChargingCounter.tla
Description: Binary data
Attachment:
SimpleCounter.tla
Description: Binary data
> On 12 May 2023, at 10:43, Grundmann, Matthias (KASTEL) <matthias.grundmann@xxxxxxx> 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/ea647b0f-e091-2049-9c76-e0c1ccd81f8b%40kit.edu. -- 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/E12608A4-5B86-413A-8B31-A91822D31703%40gmail.com.