VoteFor(a, b, v) ==
/\ maxBal[a] =< b
/\ \A vt \in votes[a] : vt[1] /= b
/\ \A c \in Acceptor \ {a} :
\A vt \in votes[c] : (vt[1] = b) => (vt[2] = v)
/\ \E Q \in Quorum : ShowsSafeAt(Q, b, v)
/\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<<b, v>>}]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
(***************************************************************************)
(* The rest of the spec is straightforward. *)
(***************************************************************************)
Next == \E a \in Acceptor, b \in Ballot :
\/ IncreaseMaxBal(a, b)
\/ \E v \in Value : VoteFor(a, b, v)
Spec == Init /\ [][Next]_<<votes, maxBal>>
related code:
VoteFor(a, b, v) ==
/\ maxBal[a] =< b
/\ \A vt \in votes[a] : vt[1] /= b
/\ \A c \in Acceptor \ {a} :
\A vt \in votes[c] : (vt[1] = b) => (vt[2] = v)
/\ \E Q \in Quorum : ShowsSafeAt(Q, b, v)
/\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<<b, v>>}]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
If VoteFor specifies maxBal', and IncreaseMaxBal specifies maxBal', then they can only be true that the same time if there is some value for maxBal' that satisfies both actions.
Given TLC isn't giving you an error, I'm guessing you also have UNCHANGED
votes in IncreaseMaxBal? Then they definitely
both can't be true at the same time, as VoteFor would
specify that votes changes and IncreaseMaxBal
does not.
H
--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a970adcf-3791-4835-b6c8-ac024b5c9cef%40googlegroups.com.
Hi Shiyao
related code:
VoteFor(a, b, v) ==
/\ maxBal[a] =< b
/\ \A vt \in votes[a] : vt[1] /= b
/\ \A c \in Acceptor \ {a} :
\A vt \in votes[c] : (vt[1] = b) => (vt[2] = v)
/\ \E Q \in Quorum : ShowsSafeAt(Q, b, v)
/\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<<b, v>>}]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
If VoteFor specifies maxBal', and IncreaseMaxBal specifies maxBal', then they can only be true that the same time if there is some value for maxBal' that satisfies both actions.
Given TLC isn't giving you an error, I'm guessing you also have UNCHANGED votes in IncreaseMaxBal? Then they definitely both can't be true at the same time, as VoteFor would specify that votes changes and IncreaseMaxBal does not.
H
--
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 tla...@googlegroups.com.
I'm having some trouble coming up with a valid spec where that
would matter. You're saying that OP1, OP2, and
OP1 /\ OP2 are all valid actions, but also that the
conjunction includes transitions that aren't included in either
individual action. As far as I know, the semantics of TLA+, in
particular that the next-state relation must completely specify
all variables, make that impossible. But I'd be happy to be proven
wrong on this!
With that in mind, I suspect that TLC doesn't check those
transitions. You'd have to ask Markus to know for sure, though.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/18c0b8b6-1fe6-40b8-8560-d808d6bc7dc6%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4e8eaa89-0e5c-8d82-2982-105426e39f84%40gmail.com.
On 23 Sep 2019, at 04:35, Shiyao MA <i...@introo.me> wrote:Hi Merz,What I understand from Hillel's reply is that,If Post(s, A) /= Post(s, B).Then Post(s, A/\B) = φBest,
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/18c0b8b6-1fe6-40b8-8560-d808d6bc7dc6%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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4e8eaa89-0e5c-8d82-2982-105426e39f84%40gmail.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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/396b14f6-bfa6-4a25-86a4-06099ecc80e0%40googlegroups.com.