MAYBE Time: 0.024726 TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} DP: DP: { sent# up x -> sent# x, rec# sent x -> sent# rec x, rec# sent x -> rec# x, rec# rec x -> sent# rec x, rec# no x -> sent# rec x, rec# no x -> rec# x, rec# up x -> rec# x, rec# bot() -> sent# bot(), no# up x -> no# x, top# sent up x -> rec# x, top# sent up x -> top# check rec x, top# sent up x -> check# rec x, top# rec up x -> rec# x, top# rec up x -> top# check rec x, top# rec up x -> check# rec x, top# no up x -> rec# x, top# no up x -> top# check rec x, top# no up x -> check# rec x, check# sent x -> sent# check x, check# sent x -> check# x, check# rec x -> rec# check x, check# rec x -> check# x, check# no x -> no# check x, check# no x -> check# x, check# up x -> check# x} TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} UR: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} EDG: {(sent# up x -> sent# x, sent# up x -> sent# x) (rec# no x -> rec# x, rec# bot() -> sent# bot()) (rec# no x -> rec# x, rec# up x -> rec# x) (rec# no x -> rec# x, rec# no x -> rec# x) (rec# no x -> rec# x, rec# no x -> sent# rec x) (rec# no x -> rec# x, rec# rec x -> sent# rec x) (rec# no x -> rec# x, rec# sent x -> rec# x) (rec# no x -> rec# x, rec# sent x -> sent# rec x) (no# up x -> no# x, no# up x -> no# x) (top# rec up x -> rec# x, rec# bot() -> sent# bot()) (top# rec up x -> rec# x, rec# up x -> rec# x) (top# rec up x -> rec# x, rec# no x -> rec# x) (top# rec up x -> rec# x, rec# no x -> sent# rec x) (top# rec up x -> rec# x, rec# rec x -> sent# rec x) (top# rec up x -> rec# x, rec# sent x -> rec# x) (top# rec up x -> rec# x, rec# sent x -> sent# rec x) (check# sent x -> check# x, check# up x -> check# x) (check# sent x -> check# x, check# no x -> check# x) (check# sent x -> check# x, check# no x -> no# check x) (check# sent x -> check# x, check# rec x -> check# x) (check# sent x -> check# x, check# rec x -> rec# check x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# sent x -> sent# check x) (check# no x -> check# x, check# up x -> check# x) (check# no x -> check# x, check# no x -> check# x) (check# no x -> check# x, check# no x -> no# check x) (check# no x -> check# x, check# rec x -> check# x) (check# no x -> check# x, check# rec x -> rec# check x) (check# no x -> check# x, check# sent x -> check# x) (check# no x -> check# x, check# sent x -> sent# check x) (top# sent up x -> top# check rec x, top# no up x -> check# rec x) (top# sent up x -> top# check rec x, top# no up x -> top# check rec x) (top# sent up x -> top# check rec x, top# no up x -> rec# x) (top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# no up x -> check# rec x) (top# no up x -> top# check rec x, top# no up x -> top# check rec x) (top# no up x -> top# check rec x, top# no up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# no x -> check# x) (top# sent up x -> check# rec x, check# no x -> no# check x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# no x -> check# x) (top# no up x -> check# rec x, check# no x -> no# check x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# bot() -> sent# bot()) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# no x -> no# check x) (top# rec up x -> check# rec x, check# no x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x) (top# rec up x -> top# check rec x, top# no up x -> rec# x) (top# rec up x -> top# check rec x, top# no up x -> top# check rec x) (top# rec up x -> top# check rec x, top# no up x -> check# rec x) (check# up x -> check# x, check# sent x -> sent# check x) (check# up x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# rec x -> rec# check x) (check# up x -> check# x, check# rec x -> check# x) (check# up x -> check# x, check# no x -> no# check x) (check# up x -> check# x, check# no x -> check# x) (check# up x -> check# x, check# up x -> check# x) (check# rec x -> check# x, check# sent x -> sent# check x) (check# rec x -> check# x, check# sent x -> check# x) (check# rec x -> check# x, check# rec x -> rec# check x) (check# rec x -> check# x, check# rec x -> check# x) (check# rec x -> check# x, check# no x -> no# check x) (check# rec x -> check# x, check# no x -> check# x) (check# rec x -> check# x, check# up x -> check# x) (top# no up x -> rec# x, rec# sent x -> sent# rec x) (top# no up x -> rec# x, rec# sent x -> rec# x) (top# no up x -> rec# x, rec# rec x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> rec# x) (top# no up x -> rec# x, rec# up x -> rec# x) (top# no up x -> rec# x, rec# bot() -> sent# bot()) (top# sent up x -> rec# x, rec# sent x -> sent# rec x) (top# sent up x -> rec# x, rec# sent x -> rec# x) (top# sent up x -> rec# x, rec# rec x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> rec# x) (top# sent up x -> rec# x, rec# up x -> rec# x) (top# sent up x -> rec# x, rec# bot() -> sent# bot()) (rec# up x -> rec# x, rec# sent x -> sent# rec x) (rec# up x -> rec# x, rec# sent x -> rec# x) (rec# up x -> rec# x, rec# rec x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> rec# x) (rec# up x -> rec# x, rec# up x -> rec# x) (rec# up x -> rec# x, rec# bot() -> sent# bot()) (rec# sent x -> rec# x, rec# sent x -> sent# rec x) (rec# sent x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# rec x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> rec# x) (rec# sent x -> rec# x, rec# up x -> rec# x) (rec# sent x -> rec# x, rec# bot() -> sent# bot()) (rec# bot() -> sent# bot(), sent# up x -> sent# x)} STATUS: arrows: 0.787200 SCCS (5): Scc: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x, top# no up x -> top# check rec x} Scc: {check# sent x -> check# x, check# rec x -> check# x, check# no x -> check# x, check# up x -> check# x} Scc: {no# up x -> no# x} Scc: {rec# sent x -> rec# x, rec# no x -> rec# x, rec# up x -> rec# x} Scc: {sent# up x -> sent# x} SCC (3): Strict: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x, top# no up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Open SCC (4): Strict: {check# sent x -> check# x, check# rec x -> check# x, check# no x -> check# x, check# up x -> check# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Open SCC (1): Strict: {no# up x -> no# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Open SCC (3): Strict: {rec# sent x -> rec# x, rec# no x -> rec# x, rec# up x -> rec# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Open SCC (1): Strict: {sent# up x -> sent# x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Open