Updated spec and invariant, working for N=3,4

[jasperjiaguo]

1. msgSentNotTainted initialization msgSentNotTainted = [ n \in Node |-> IF n=0 THEN TRUE ELSE FALSE ]
2. bring back the safety and liveness check to the EWD998 file as I'm suspecting terminationDetected is not properly initialized
3. changed the invariant to EWD840's as we are implementing a variant of EWD840 here

Also works for N=4