/* HANDOVER PROTOCOL (from Robin Milner's CUP 1999 book) */

defproc
    Mobile(talk,switchto)=
        select {
            talk?().Mobile(talk, switchto);
            switchto?(talkn, switchn).Mobile(talkn,switchn)
        };

defproc
    BaseStation(talk, switchto, give, alert) =
        select {
            talk!().BaseStation(talk, switchto, give, alert); 
            give?(talkn, switchn).switchto!(talkn,switchn).
                BaseStationIdle(talk,switchto, give, alert)
        }
and
    BaseStationIdle(talk, switchto, give, alert) = 
        alert?().BaseStation(talk, switchto, give, alert);

defproc
    Central(talk, talkNxt,
            switchto, switchNxt,
            give, giveNxt,
            alert, alertNxt) = 
        give!(talkNxt, switchNxt).alertNxt!().Central(talkNxt, talk,
                                                      switchNxt, switchto,
                                                      giveNxt, give,
                                                      alertNxt, alert);

/* --- */

defproc
    System = (new talk1, talk2,
                  switch1, switch2,
                  give1, give2,
                  alert1, alert2
                    in ( 
                        Mobile(talk1, switch1) |
                        BaseStation(talk1,switch1,give1,alert1) |
                        BaseStationIdle(talk2,switch2,give2,alert2) |
                        Central(talk1, talk2,
                                switch1, switch2,
                                give1, give2,
                                alert1, alert2)
                    ));

/* PROPERTIES */

defprop deadLockFree = maxfix X. (<>true and []X);

check System |= deadLockFree;

/* ---------- */

defprop write(x) = (1 and < x! >true);

defprop read(x) = (1 and < x? >true);

defprop hasRace = 
    inside (exists x.( write(x) | write(x) | read(x) | true));

defprop raceFree = maxfix X.((not hasRace) and []X);

check System |= raceFree;