/** Telephone system (SEG-2x06 - Lab-1)
 *  Gregor v. Bochmann, January 2009, revised Jan. 2015 */

// the side initiating the call
PHONE1 = (pick_up1 -> dial -> WAIT),
   WAIT = (ring_back -> hello -> TALKING1 | busy_tone -> hang_up -> PHONE1),
   TALKING1 = (talk -> TALKING1  |  hang_up -> PHONE1).

// the side receiving the call
PHONE2 = (ring -> pick_up2 -> hello -> TALKING2  | pick_up2 -> BUSY),
   BUSY = (hang_up -> PHONE2  |  busy_tone -> BUSY),
   TALKING2 = (talk -> TALKING2  |  hang_up -> PHONE2).

// the switch is only involved in dialing and ringing; 
// the interactions hello, talk and hang_up go directly between the two phones.
SWITCH = (dial -> Choice),
   Choice = (ring -> ring_back -> SWITCH  |  busy_tone -> SWITCH).

||PHONE_SYSTEM = (PHONE1 || PHONE2 || SWITCH).

// the following are definition of test sequences
set All_interactions = {pick_up1, pick_up2, dial, ring, ring_back, hello, busy_tone, talk, hang_up}

// a normal execution sequence
Sequence_1 = (pick_up1 -> dial -> ring -> ring_back -> pick_up2 -> hello -> talk -> talk -> hang_up -> END) + All_interactions.
||TEST_1 = (PHONE_SYSTEM || Sequence_1).

// an execution sequence where the user of PHONE2 does the pick-up a bit earlier
Sequence_2 = (pick_up1 -> dial -> ring -> pick_up2 -> ring_back -> hello -> talk -> talk -> hang_up -> END) + All_interactions.
||TEST_2 = (PHONE_SYSTEM || Sequence_2).

// an execution sequence where the user of PHONE2 does the pick-up before the SWITCH does the ringing
Sequence_3 = (pick_up1 -> dial -> pick_up2 -> ring -> ring_back -> hello -> talk -> talk -> hang_up -> END) + All_interactions.
||TEST_3 = (PHONE_SYSTEM || Sequence_3).

// Questions: 
// What will happen when the users of both phones first do the pick-up and then the user of PHONE1 dials 
//     while the user of PHONE2 hangs up ?
// By what sequences could you model the case that the users of both phones do the pick-up simultaneously ? 
//     Similarly, what about the simultaneous hang-up done by both users ?

property Abstract = (dial -> Next),
   Next = (hello -> Abstract | busy_tone -> Abstract).
||Check_Abstract = (PHONE_SYSTEM || Abstract).