[tlaplus] Re: Check eventual consistency

[jayaprabhakar k <jayaprabhakar@xxxxxxxxx>]

I found what to do for this simple model. Added a definition,

IsCountCorrect == (count = Cardinality(elements))

In the model I set the temporal property as `<>[]IsCountCorrect`. With this, the temporal check seems to work. Removing the Tick, ensures it works as well. I believe this correct.

Now, extending the model to Remove, breaks the model. 

Remove == /\ \E e \in elements:

              /\ elements' = elements \ {e}

              /\ dirty' = 1

              /\ UNCHANGED count

Next == Add \/ REMOVE \/ Tick 

.

Now, the temporal property is violated, because,  removing an element puts it back to an existing state, so the state is deduplicated and Tick will not run in this case.

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 count |-> 0,
 dirty |-> 0,
 elements |-> {}
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "Add",
   location |-> "line 15, col 8 to line 20, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {2}
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Remove",
   location |-> "line 22, col 11 to line 26, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {}
]
>>

---

I tried adding a seq number that keeps incrementing with Add/Remove explodes the state space and the model checker goes on for ever without ever stopping.

---

So I tried resetting seq after a Tick. And still get a similar error. 

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 count |-> 0,
 dirty |-> 0,
 elements |-> {},
 seq |-> 0
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "Add",
   location |-> "line 15, col 8 to line 20, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {3},
 seq |-> 1
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Tick",
   location |-> "line 28, col 9 to line 31, col 29 of module EventualCounter"
 ],
 count |-> 1,
 dirty |-> 0,
 elements |-> {3},
 seq |-> 0
],
[
 _TEAction |-> [
   position |-> 4,
   name |-> "Remove",
   location |-> "line 22, col 11 to line 26, col 32 of module EventualCounter"
 ],
 count |-> 1,
 dirty |-> 1,
 elements |-> {},
 seq |-> 1
]
>>

The corresponding full code is,

-------------------------- MODULE EventualCounter --------------------------

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS

VARIABLES elements, count, dirty, seq

vars == <<elements, count, dirty, seq>>

Init == /\ elements = {}

        /\ count = 0

        /\ dirty = 0

        /\ seq = 0

 

Add == /\ \E e \in 1..MAX_ELEMENTS:

              /\ e \notin elements

              /\ elements' = elements \union {e}

              /\ dirty' = 1

              /\ seq' = seq + 1

              /\ UNCHANGED count

Remove == /\ \E e \in elements:

              /\ elements' = elements \ {e}

              /\ dirty' = 1

              /\ seq' = seq + 1

              /\ UNCHANGED count

Tick == /\ count' = Cardinality(elements)

        /\ dirty' = 0

        /\ seq' = 0

        /\ UNCHANGED elements 

IsCountCorrect == (count = Cardinality(elements))

ConsistencyInvariant == \/ dirty = 1

                        \/ IsCountCorrect

                

EventualConsistencyInvariant == IsCountCorrect

Change == Add \/ Remove        

Next == Change \/ Tick  

Spec == Init /\ [][Next]_vars /\ SF_vars(Tick)

How do I resolve this? 

On Thursday, January 5, 2023 at 2:32:22 PM UTC-8 jayaprabhakar k wrote:

Hi,

I am new to TLA+. I am trying to design a simple eventually consistent counter. 

Elements are added to a set. It could optionally, increment the counter. To ensure, the count becomes eventually consistent, there will be a separate ticker that periodically update the count.

-------------------------- MODULE EventualCounter --------------------------
EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS

VARIABLES elements, count, dirty

vars == <<elements, count, dirty>>

Init == /\ elements = {}
        /\ count = 0
        /\ dirty = 0

Add == /\ \E e \in 1..MAX_ELEMENTS:
              /\ e \notin elements
              /\ elements' = elements \union {e}
              /\ dirty' = 1
              /\ \/ count' = count + 1
                 \/ UNCHANGED count

Tick == /\ count' = Cardinality(elements)
        /\ dirty' = 0
        /\ UNCHANGED elements

ConsistencyInvariant == \/ dirty = 1
             \/ (count = Cardinality(elements))
               
             
Next == \/ Add
        \/ Tick  

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

=============================================================================

How do I add an invariant or temporal property that confirms the count will be eventually consistent with the real count?

If I simply add count = Cardinality(elements), that would fail after each Add/Insert. To pass the invariant, I added a dirty bit. But the, in this case, even if the Tick is never triggered, the invariant will pass.

What should I do to prove or verify, the count will be eventually consistent?

 

-- 
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/afdae50c-9f3d-48b5-84b7-c7aa3ba561a9n%40googlegroups.com.