mtype = { alert, answer, cutoff, ack };

chan link12 = [0] of { mtype };
chan link21 = [0] of { mtype };

bool idle_st[3] = true;
bool dial_st[3];
bool calling_st[3];
bool ringing_st[3];
bool talking_st[3];
bool finish_st[3];

proctype user(chan in, out) {

   mtype response;
   bit is_caller;

idle:
   assert(idle_st[_pid] && !dial_st[_pid] && !calling_st[_pid] && 
          !ringing_st[_pid] && !talking_st[_pid]);
   is_caller = 0;
   do :: atomic { 
            idle_st[_pid] = 0; 
            dial_st[_pid] = 1
         }; 
         goto dial
      :: in?alert -> 
         out!ack; 
         atomic { 
            idle_st[_pid] = 0; 
            ringing_st[_pid] = 1
         };
         goto ringing
   od;

dial:
   assert(!idle_st[_pid] && dial_st[_pid] && !calling_st[_pid] && 
          !ringing_st[_pid] && !talking_st[_pid]);
   do :: out!alert; 
         in?response; 
         if :: response == ack -> 
               atomic {
                  dial_st[_pid] = 0; 
                  calling_st[_pid] = 1
               }; 
               is_caller = 1; 
               goto calling
            :: response == alert -> 
               atomic {
                  dial_st[_pid] = 0; 
                  talking_st[_pid] = 1
               }; 
               goto talk
         fi
      :: atomic { 
            dial_st[_pid] = 0;
            finish_st[_pid] = 1
         }; 
         goto finish;
   od;

   ... etc.

}

init {
   atomic {
      run user(link21,link12);
      run user(link12,link21);
   }
}