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

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

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

proctype user(chan in, out; byte id) {

   mtype response;
   bit is_caller;

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

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

   ... etc.

}

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