[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Check eventual consistency

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


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.