demo_v4.ded

member(Node, Other)@next :- member(Node, Other);
log(Node, Message)@next :- log(Node, Message);

log(Other, Message)@async :- bcast(Node, Message), member(Node, Other);

bcast("a", "Hello world!")@1;
bcast(Node, Message)@next :- bcast(Node, Message);
bcast(Node, Message)@next :- log(Node, Message);

// someone (X) has a log, but not A.
missing_log(A, Pl) :- log(X, Pl), member(_, A), notin log(A, Pl);

pre(X, Pl) :- log(X, Pl), notin bcast(X, Pl)@1, notin crash(X, X, _);
post(X, Pl) :- log(X, Pl), notin missing_log(_, Pl);

member("a", "a")@1;
member("a", "b")@1;
member("a", "c")@1;
member("b", "a")@1;
member("b", "b")@1;
member("b", "c")@1;
member("c", "a")@1;
member("c", "b")@1;
member("c", "c")@1;