Thanks. I'll try to read Specifying Systems. In any case, I assume I should not add WF_vars(Tick). To make things work, I removed the WF_vars(Tick), made the correct tick. And used a seq < BUFFER_SIZE as a precondition to Add/Remove. Then it all worked.I assume that is the correct way to model. For the record, this is my final working model. Please correct me if I'm wrong.
-------------------------- 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' = seq + 1
/\ UNCHANGED count
Remove == /\ \E e \in elements:
/\ seq < BUFFER_SIZE
/\ seq > 0
/\ elements' = elements \ {e}
/\ seq' = seq + 1
/\ UNCHANGED count
Tick == /\ count' = Cardinality(elements)
/\ seq' = 0
/\ UNCHANGED <<elements>>
ConsistencyInvariant == \/ seq > 0
\/ (count = Cardinality(elements))
IsCountCorrect == (count = Cardinality(elements))
Next == \/ Add
\/ Remove
\/ Tick
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
THEOREM Spec => []<>IsCountCorrect
-On Fri, 6 Jan 2023 at 14:37, Hillel Wayne <hwayne@xxxxxxxxx> wrote:You're running into a fairly niche issue called "Machine Closure", where the action in your fairness condition isn't a subset of your Next formula. WF(Tick) says that if []ENABLED Tick, then Tick eventually happens. Since Tick doesn't have any unprimed variables in it, it's always enabled, but since it's not part of Next, it can never happen. So the Spec formula evaluates to false.
You should see that no initial states are generated in the output.
I actually see Init state generated.--It's a bit unintuitive, I know; see section 8.9 of Specifying Systems for a formal treatment.
H
On 1/6/2023 12:20 PM, jayaprabhakar k wrote:
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 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/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.
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/8068e6ef-e001-29c3-0554-5a668366e6fd%40gmail.com.
On Fri, 6 Jan 2023 at 14:37, Hillel Wayne <hwayne@xxxxxxxxx> wrote:--You're running into a fairly niche issue called "Machine Closure", where the action in your fairness condition isn't a subset of your Next formula. WF(Tick) says that if []ENABLED Tick, then Tick eventually happens. Since Tick doesn't have any unprimed variables in it, it's always enabled, but since it's not part of Next, it can never happen. So the Spec formula evaluates to false. You should see that no initial states are generated in the output.
It's a bit unintuitive, I know; see section 8.9 of Specifying Systems for a formal treatment.
H
On 1/6/2023 12:20 PM, jayaprabhakar k wrote:
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 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/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.
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/8068e6ef-e001-29c3-0554-5a668366e6fd%40gmail.com.