ewd998 icon indicating copy to clipboard operation
ewd998 copied to clipboard

Published 20 hours ago • verified publisher icon tlaplus-workshops

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

Open jasperjiaguo opened this issue 2 years ago • 0 comments

  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 Screen Shot 2022-07-12 at 7 54 46 PM

jasperjiaguo avatar Jul 13 '22 01:07 jasperjiaguo