/** Alternating bit protocol (ABP)
 *  
 *  Gregor v. Bochmann, October 2015 */

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

// good design of PE1:
PE1 = (s -> PE1_20),
PE1_20 = (sM0 -> PE1_30),
PE1_30 = (rAck0 -> s -> PE1_21 | rAckE -> PE1_20 | rAck1 -> PE1_20),
PE1_21 = (sM1 -> PE1_31),
PE1_31 = (rAck1 -> s -> PE1_20 | rAckE -> PE1_21 | rAck1 -> PE1_21).


// 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 = (rM0 -> r -> PE2_30 | rM1 -> PE2_31 | rME -> PE2_31),
PE2_31 = (sAck1 -> PE2),
PE2_11 = (rM1 -> r -> PE2_31 | rM1 -> PE2_30 | rME -> PE2_30),
PE2_30 = (sAck0 -> PE2_11).

M12 = (sM1 -> M12_M1 | sM0 -> M12_M0),
M12_M1 = (rM1 -> M12 | rME -> M12),
M12_M0 = (rM0 -> M12 | rME -> M12).

M21 = (sAck1 -> M21_M1 | sAck0 -> M21_M0),
M21_M1 = (rAck1 -> M21 | rAckE -> M21),
M21_M0 = (rAck0 -> M21 | rAckE -> M21).

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

||SAFETYCHECK = (SYSTEM || SERVICE).