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?