Programming Assignment 3: Byzantine Agreement

Total: 20 points

(5) Submitted HW3ByzantineAgreement.mac compiles
(5) Demonstrated proof of correctness with 0 malicious nodes.  Discussion of
correctness of proof.
(5) Correct protocol for 1 malicious node and 4 total nodes.  Model checker
should terminate without finding errors.
(5) Description of sequence of steps causing protocol to fail when M=1, but
there are actually 2 malicious nodes.  Follow discussion directions on
assignment.

Possible Deduction:
(-5) Submitted code should not print additional messages during the
    modelchecking search.

Extra Credit:
(5) Correct protocol for M=2 and N=7.  Tested to exhaustion.  
(5) Demonstrated correctness of M=3 and N=10.  Tested to work for a
"substantial" number of paths.  (Yet to be determined).