/*
 * Project:  Petruchio
 * Filename: gsm.pi
 * Created:  16.05.2007
 * Author:   Tim Strazny
 * Remarks:  This translation of the GSM handover protocol into the pi calculus
 *           is taken from Fredrik Orava and Joachim Parrow: "An Algebraic
 *           Verification of a Mobile Network", p. 11, Fig 2. A formal
 *           specification of the handover procedure. (1 Mobile Station, 2 Base
 *           Stations, 1 Mobile Switching Center, 1 channel per Base Station)
 */

CC(fa, fp, l) :=
    ( in(v).fa<data>.fa<v>.CC(fa, fp, l)
    + l(m_new).fa<ho_cmd>.fa<m_new>.
        ( fp(x).[x=ho_com].fa<ch_rel>.fa(m_old).l<m_old>.CC(fp, fa, l)
        + fa(y).[y=ho_fail].l<m_new>.CC(fa, fp, l)
        )
    );

HC(l, m) :=
    l<m>.l(m_new).HC(l, m_new);

BSa(f, m) :=
    f(x).
    ( [x=data].f(v).m<data>.m<v>.BSa(f, m)
    + [x=ho_cmd].f(v).m<ho_cmd>.m<v>.
        ( f(y).[y=ch_rel].f<m>.BSp(f, m)
        + m(z).[z=ho_fail].f<ho_fail>.BSa(f, m)
        )
    );

BSp(f, m) :=
    m(x).[x=ho_acc].f<ho_com>.BSa(f, m);

MS(m) :=
    m(x).
    ( [x=data].m(v).out<v>.MS(m)
    + [x=ho_cmd].m(m_new).
        ( m_new<ho_acc>.MS(m_new)
        + m<ho_fail>.MS(m)
        )
    );

SENDER :=
    new d.in<d>.SENDER;

RECEIVER :=
    out(d).RECEIVER;

new fa, fp, m1, m2, l.
    ( HC(l, m1) | CC(fa, fp, l) | BSp(fp, m1)
    | BSa(fa, m2) | MS(m2)
    | SENDER
    | RECEIVER
    )