[tlaplus] Check eventual consistency

[jayaprabhakar k <jayaprabhakar@xxxxxxxxx>]

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/b826786a-53ca-4fe3-af4a-a5c8c934aa37n%40googlegroups.com.