/** Simple protocol
 *  
 *  Gregor v. Bochmann, September 2014 */

property SERVICE = (s -> r -> SERVICE).

// good design of PE1:
PE1 = (s -> sM -> rAck -> PE1).

// faulty design of PE1 - saftety problem:
// PE1 = (s -> XXX),
// XXX = (sM -> rAck -> PE1  |  s -> PE1).

// faulty design of PE1 - progress problem:
// PE1 = (s -> XXX),
// XXX = (sM -> rAck -> PE1  |  sM -> YYY),
// YYY = (dummy -> YYY).

PE2 = (rM -> sAck -> r -> PE2).

M12 = (sM -> rM -> M12).
M21 = (sAck -> rAck -> M21).

||SYSTEM = (PE1 || PE2 || M12 || M21).

||SAFETYCHECK = (SYSTEM || SERVICE).