/*
 * Project:  Petruchio
 * Filename: phones.pi
 * Created:  22.02.2007
 * Author:   Tim Strazny
 * Remarks:  This example is taken from Robin Milner: Communicating and Mobile
 *           Systems: the Pi-Calculus, 1999, Cambridge University Press,
 *           pages 80 and following
 */

TRANS_1(gain, lose, talk, switch) :=
    (  talk().TRANS_1(gain, lose, talk, switch)
     + lose(t, s).switch<t, s>.IDTRANS_1(gain, lose) )
    ;

IDTRANS_1(gain, lose) :=
    gain(t, s).TRANS_1(gain, lose, t, s)
    ;

//
TRANS_2(gain, lose, talk, switch) :=
    (  talk().TRANS_2(gain, lose, talk, switch)
     + lose(t, s).switch<t, s>.IDTRANS_2(gain, lose) )
    ;

IDTRANS_2(gain, lose) :=
    gain(t, s).TRANS_2(gain, lose, t, s)
    ;


CONTROL_1(talk_1, switch_1, gain_1, lose_1, talk_2, switch_2, gain_2, lose_2) :=
    lose_1<talk_2, switch_2>.gain_2<talk_2, switch_2>.CONTROL_2(talk_1, switch_1, gain_1, lose_1, talk_2, switch_2, gain_2, lose_2)
    ;
    
CONTROL_2(talk_1, switch_1, gain_1, lose_1, talk_2, switch_2, gain_2, lose_2) :=
    lose_2<talk_1, switch_1>.gain_1<talk_1, switch_1>.CONTROL_1(talk_1, switch_1, gain_1, lose_1, talk_2, switch_2, gain_2, lose_2)
    ;

CAR(talk, switch) :=
    (  talk<>.CAR(talk, switch)
     + switch(t, s).CAR(t, s) )
    ;

new gain_1, lose_1, gain_2, lose_2, talk_1, talk_2, switch_1,  switch_2.
    ( CAR(talk_1, switch_1)
    | TRANS_1(gain_1, lose_1, talk_1, switch_1)
    | IDTRANS_2(gain_2, lose_2)
    | CONTROL_1(talk_1, switch_1, gain_1, lose_1, talk_2, switch_2, gain_2, lose_2)
    )