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))
Next == \/ Add
\/ 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,
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/afdae50c-9f3d-48b5-84b7-c7aa3ba561a9n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/h4nrF-pbor4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.