% % Note this version is matches the discussion in the report as far as page 14. % After that, you need to make some changes (see the comments below) % om1: CONTEXT = BEGIN stage: TYPE = [1..5]; n: NATURAL = 3; k: NATURAL = 2; relays: TYPE = [1..n]; receivers: TYPE = [1..k]; vals: TYPE = [0..n+1]; missing_v: vals = 0; correct_v: vals = n+1; faults: TYPE = {arbitrary, symmetric, manifest, none}; controller: MODULE = BEGIN OUTPUT pc: stage, sf: faults, rf: ARRAY relays OF faults INITIALIZATION pc = 1; sf IN {v: faults | TRUE}; rf IN {a: ARRAY relays OF faults | FORALL (i:relays): IF sf = arbitrary THEN a[i] /= arbitrary ELSE TRUE ENDIF }; TRANSITION [ pc <= 4 --> pc' = pc+1 [] ELSE --> ] END; rvec: TYPE = ARRAY relays OF vals; vvec: TYPE = ARRAY receivers OF vals; source: MODULE = BEGIN OUTPUT s_out: rvec INPUT pc: stage, sf: faults TRANSITION [ pc = 1 AND (sf = none OR sf = symmetric) --> s_out' = [[i:relays] correct_v] [] pc = 1 AND sf = manifest --> s_out' = [[i:relays] missing_v] [] pc = 1 AND sf = arbitrary --> s_out' IN {a: rvec | TRUE} [] ELSE --> ] END; relay[i: relays]: MODULE = BEGIN INPUT pc: stage, r_in: vals, rf: faults OUTPUT r_out: vvec TRANSITION [ pc = 2 AND rf = none --> r_out' = [[p:receivers] r_in] [] pc = 2 AND rf = manifest --> r_out' = [[p:receivers] missing_v] [] ([] (x:vals): pc = 2 AND rf = symmetric --> r_out' = [[p:receivers] x]) [] pc = 2 AND rf = arbitrary --> r_out' IN {a: vvec | TRUE} [] ELSE --> ] END; all: TYPE = [0..n]; count_h(a: rvec, v: vals, acc: all, i: relays): all = LET this_one: [0..1] = IF a[i]=v THEN 1 ELSE 0 ENDIF IN IF i=1 THEN acc + this_one ELSE count_h(a, v, acc + this_one, i-1) ENDIF; count(a: rvec, v: vals): all = count_h(a, v, 0, n); receiver[p:receivers]: MODULE = BEGIN INPUT vecs: ARRAY relays OF vvec, pc: stage LOCAL inv: rvec OUTPUT vote: vals DEFINITION inv = [[i:relays] vecs[i][p]] TRANSITION [ ([] (i: vals): pc = 3 AND 2*count(inv, i) > n --> vote' = i) % Comment out the two lines above and uncomment the three lines below % to switch to a hybrid majority vote % ([] (i: [1..n+1]): % pc = 3 AND % 2*count(inv, i) > n - count(inv, missing_v) --> vote' = i) [] ELSE --> vote' = missing_v ] END; system: MODULE = controller || source || (WITH OUTPUT vecs: ARRAY relays OF vvec WITH INPUT s_out: rvec WITH INPUT rf: ARRAY relays OF faults (|| (i:relays): RENAME r_in TO s_out[i], r_out TO vecs[i], rf TO rf[i] IN relay[i])) || (WITH OUTPUT votes: vvec (|| (x:receivers): RENAME vote TO votes[x] IN receiver[x])); live_0: THEOREM system |- F(pc=4); live_1: THEOREM system |- G(F(pc=5)); live_2: THEOREM system |- F(G(pc=5)); fc: TYPE = [0..3*(n+1)]; fcount_h(a: ARRAY relays OF faults, acc: all, i: relays, weights: [faults -> [0..3]]): fc = IF i=1 THEN acc + weights(a[i]) ELSE fcount_h(a, acc + weights(a[i]), i-1, weights) ENDIF; fcount(a: ARRAY relays OF faults, s: faults, weights: [faults ->[0..3]]): fc = fcount_h(a, weights(s), n, weights); wts(x: faults): [0..3] = IF x=arbitrary THEN 3 ELSIF x=symmetric THEN 2 ELSIF x=manifest THEN 1 ELSE 0 ENDIF; validity: THEOREM system |- G(pc=4 AND sf=none AND fcount(rf, sf, wts) < n => FORALL (x:receivers): votes[x]=correct_v); agreement: THEOREM system |- G(pc=4 AND fcount(rf, sf, wts) < n => FORALL (x,y:receivers): votes[x]=votes[y]); END