In the past we modeled the state machines for what we call a “plain old telephone system (POTS)”. In the early days when telephones were still connected through cables and did not have touch screens,...

In the past we modeled the state machines for what we call a “plain old telephone system (POTS)”. In the early days when telephones were still connected through cables and did not have touch screens, or any screen for that matter, in order to make a call the caller had to go through the following steps. ? The caller off-hooks the handset of the phone. ? If the line is not busy a dial tone is audible, if the line is busy a busy tone is audible. ? If the dial tone is audible the caller can enter digits to select the callee. ? If the line of the callee is not busy, the caller will hear a ring tone while the phone of the callee is ringing. ? If the callee off-hooks the handset while his phone is ringing, he is connected to the caller and the ringing as well as the ring tone for the caller stops. ? Once a call is connected, both parties (caller or callee) can terminate the call by on-hooking their handsets. ? If the caller on-hooks the handset while he hears the ring tone, the call is terminated and the ringing of the callee’s phone stops. a) Model the above described behavior of the POTS system in PROMELA language. You need to model two proctypes (caller and callee) that communicate via synchronous message passing. b) Verify with the SPIN model checker that there are no deadlocks in the system. Submit a copy of the SPIN output to get credit.