Step
*
1
of Lemma
rsc4-vote
.....failed RWconcl.....
1. Cmd : {T:Type| valueall-type(T)}
2. clients : bag(Id)
3. cmdeq : EqDecider(Cmd)
4. coeff : 
5. flrs :
6. locs : bag(Id)
7. es : EO'
8. e : E
9. i : Id
10. k :
11. k1 :
12. v : Cmd
13. i1 : Id
14. loc(e) 
locs 
loc(e) locs
15. e' : {e':E| e' 
loc e }
16. a :
17. b : Cmd
18. <a, b> Base([propose]; 
Cmd)(e')
(
b1:. b3:Id. <<<a, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e'))
<a, b> Base([propose]; Cmd)(e')
(b1:. b3:Id. <<<a, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e'))
19. (((i locs 
(((k = a) (k1 = 0)) (v = b)) (i1 = loc(e))) (e = e'))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
(i = loc(e))
(a1:
(False
(b1:
b2:Cmd
b3:Id
(<<<a1, b1>, b2>, b3> Base(``rsc4 vote``; Cmd Id)(e)
(a2:Cmd List
(((||a2|| = (coeff * flrs))
(((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))
(
((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))))
(b4:Id List
(<a2, b4> Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init()
<[], []>;rsc4_vote'base(Cmd))(e)
(
(rsc4_newvote(Cmd) <a, 0> <<<a1, b1>, b2>, b3> <a2, b4>))))))))))))
False
(((i locs
(make-Msg(``rsc4 vote``; Cmd Id;<<<k, k1>, v>, i1>)
= make-Msg(``rsc4 vote``; Cmd Id;<<<a, 0>, b>, loc(e)>)))
(e = e'))
((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
<i, make-Msg(``rsc4 vote``; Cmd Id;<<<k, k1>, v>, i1>)>
{rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0>}(e)))
((no rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)| between e' and e)
<i, make-Msg(``rsc4 vote``; Cmd Id;<<<k, k1>, v>, i1>)>
{rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e))
20. (no rsc4_Notify(Cmd;clients) a between e' and e) (no rsc4_Notify(Cmd;clients) a between e' and e)
21. e1 : {e1:E| e1 loc e }
22. b1 :
23. b1@0 : Cmd
24. i locs i locs
25. (((k = a) (k1 = b1)) (v = b1@0)) (i1 = loc(e)) 
'
26. <<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)> '
27. (((k = a) (k1 = b1)) (v = b1@0)) (i1 = loc(e))
<<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)>
BY
{ ILFInstanceF "vote" "rsc4" }
.....failed RWconcl.....
1. Cmd : \{T:Type| valueall-type(T)\}
2. clients : bag(Id)
3. cmdeq : EqDecider(Cmd)
4. coeff : \mBbbZ{}
5. flrs : \mBbbZ{}
6. locs : bag(Id)
7. es : EO'
8. e : E
9. i : Id
10. k : \mBbbZ{}
11. k1 : \mBbbZ{}
12. v : Cmd
13. i1 : Id
14. loc(e) \mdownarrow{}\mmember{} locs \mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs
15. e' : \{e':E| e' \mleq{}loc e \}
16. a : \mBbbZ{}
17. b : Cmd
18. <a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e'))
\mLeftarrow{}{}\mRightarrow{} <a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e'))
19. (((i \mdownarrow{}\mmember{} locs \mwedge{} (((k = a) \mwedge{} (k1 = 0)) \mwedge{} (v = b)) \mwedge{} (i1 = loc(e))) \mwedge{} (e = e'))
\mdownarrow{}\mvee{} ((no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
\mwedge{} (i = loc(e))
\mwedge{} (\mdownarrow{}\mexists{}a1:\mBbbZ{}
(False
\mwedge{} (\mexists{}b1:\mBbbZ{}
\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<a1, b1>, b2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} (\mexists{}a2:Cmd List
(((||a2|| = (coeff * flrs))
\mwedge{} (((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))
\mvee{} (\mneg{}((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))))
\mwedge{} (\mexists{}b4:Id List
(<a2, b4> \mmember{} Memory-class(rsc4\_add\_to\_quorum(Cmd)
<a, 0>rsc4\_init() <[], []>rsc4\_vote'base(Cmd))(
e)
\mwedge{} (\muparrow{}(rsc4\_newvote(Cmd) <a, 0> <<<a1, b1>, b2>, b3> <a2, b4>))))))))))))
\mvee{} False
\mLeftarrow{}{}\mRightarrow{} (((i \mdownarrow{}\mmember{} locs
\mwedge{} (make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<k, k1>, v>, i1>)
= make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<a, 0>, b>, loc(e)>)))
\mwedge{} (e = e'))
\mdownarrow{}\mvee{} ((no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
\mwedge{} <i, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<k, k1>, v>, i1>)> \mmember{}
\{rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0>\}(e)))
\mvee{} ((no rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)| between e' and e)
\mwedge{} <i, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<k, k1>, v>, i1>)> \mmember{}
\{rsc4\_decision(Cmd;clients) a@|Loc, rsc4\_decided'base(Cmd)|\}(e))
20. (no rsc4\_Notify(Cmd;clients) a between e' and e)
\mLeftarrow{}{}\mRightarrow{} (no rsc4\_Notify(Cmd;clients) a between e' and e)
21. e1 : \{e1:E| e1 \mleq{}loc e \}
22. b1 : \mBbbZ{}
23. b1@0 : Cmd
24. i \mdownarrow{}\mmember{} locs \mLeftarrow{}{}\mRightarrow{} i \mdownarrow{}\mmember{} locs
25. (((k = a) \mwedge{} (k1 = b1)) \mwedge{} (v = b1@0)) \mwedge{} (i1 = loc(e)) \mmember{} \mBbbP{}'
26. <<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)> \mmember{} \mBbbP{}'
27. (((k = a) \mwedge{} (k1 = b1)) \mwedge{} (v = b1@0)) \mwedge{} (i1 = loc(e))
\mvdash{} <<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)>
By
ILFInstanceF "vote" "rsc4"
Home
Index