# Re: [tlaplus] Re: Check eventual consistency

Thanks. That fixed the issue.

Trying to understand this better, related to seq.

1. If I remove seq, it still works, as long as I have either WF_vars(Tick) or SF_vars(Tick). Without it, if seq is not present, it doesn't work.
2. Once I add WF_vars(Tick), even if I remove the Tick from next, Next == Add \/ Remove, it always passes, and never fails. Even worse, if I remove count'=Cardinality(elements) in tick, it still passes.
For example, this code should NEVER pass because the count is never updated. However it passes.

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

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS, BUFFER_SIZE

VARIABLES elements, count, seq

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

Init == /\ elements = {}

/\ count = 0

/\ seq = 0

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

/\ e \notin elements

\*     /\ seq < BUFFER_SIZE

/\ elements' = elements \union {e}

/\ seq' =  1

/\ UNCHANGED count

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

/\ Cardinality(elements) > 0

\*       /\ seq < BUFFER_SIZE

/\ elements' = elements \ {e}

/\ seq' =  1

/\ UNCHANGED count

Tick == /\ seq' = 0      \* NOT UPDATING THE COUNT

/\ UNCHANGED <<elements,count>>

ConsistencyInvariant == \/ seq > 0

\/ (count = Cardinality(elements))

IsCountCorrect == (count = Cardinality(elements))

\/ Remove

\*  \/ Tick

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

THEOREM Spec => []<>IsCountCorrect

On Friday, January 6, 2023 at 8:47:31 AM UTC-8 hwa...@xxxxxxxxx wrote:

Hi,

Your problem is that <>[]IsCountCorrect says that eventually, the count is correct and never becomes incorrect again. What you actually want is []<>IsCountCorrect: the count, if incorrect, will always become correct again. Making this change (and removing seq) makes the spec pass.

H

On 1/5/2023 5:42 PM, jayaprabhakar k wrote:
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,
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,
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

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))

\/ 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+u...@xxxxxxxxxxxxxxxx.