mtype = {advertise, register, replyOk};

chan move = [0] of {chan};  		/*Interaction on "move" channel represents movement between networks"*/


proctype MobileNode(chan myHomeAgent)   
{

	chan currentLink;		/*Current network link*/

	chan parCareOfAgent;		/*Care-of-agent parameter in latest message*/

	
       	Movement:
               	move?currentLink;
  
     	WaitForAdvertisement:
		if
       		:: 	currentLink?advertise, parCareOfAgent;
       			goto SendRegistrationRequest;
               	
		:: 	goto Movement;
               
		:: 	goto TimeRunsOut;
               	fi;

       
	TimeRunsOut:
               	goto WaitForAdvertisement;

      
	SendRegistrationRequest:
               	if
       		:: 	parCareOfAgent!register, parCareOfAgent, myHomeAgent;
       			goto WaitForReply;
                  
	 	:: 	goto Movement;
                    
		:: 	goto TimeRunsOut;
               	fi;


       	WaitForReply:
               	if
    		:: 	currentLink?replyOk, parCareOfAgent;
      	   	 	goto Talk;
	        
       		:: 	goto Movement;

       		:: 	goto TimeRunsOut;
            	fi;

         Talk:
	    	/*Keep talking until moving*/
             	if
		:: 	goto Talk;
                  
	  	:: 	goto Movement;
	     	fi;
}



proctype Agent(chan link; chan myAddress)
{

	chan parHomeAgent; 		/*Home-agent parameter in latest message*/

	chan parCareOfAgent;		/*Care-of-agent parameter in latest message*/


       	Start:
               	if 
       		:: 	link!advertise, myAddress;
       			goto Start;
                     
 		:: 	myAddress?register, parCareOfAgent, parHomeAgent;
       			goto HandleRequest;
               	fi;

       	HandleRequest:
               	if
       		:: 	parHomeAgent != myAddress;
       			goto ForwardRequest;

       		:: 	else;                	
			if
       	 		:: 	parCareOfAgent != myAddress;
     	        		goto SendReplyOkToAgent;

                  	:: 	else;
       	               		goto SendReplyOkToLink;
               	 	fi;
	        fi;


        ForwardRequest:
		if 
		:: 	parHomeAgent!register, parCareOfAgent, parHomeAgent;
               		goto WaitForReplyOk;
          	
		:: 	goto TimeRunsOut;
               	fi;
        
	TimeRunsOut:
		goto Start;             

       	WaitForReplyOk:
		if 
		:: 	myAddress?replyOk, parCareOfAgent, parHomeAgent;
               		goto SendReplyOkToLink;

          	:: 	goto TimeRunsOut;
               	fi;
                      

       	SendReplyOkToLink:
		if 
		:: 	link!replyOk, parCareOfAgent;
               		goto Start;
          
		:: 	goto TimeRunsOut;
               	fi;

       	SendReplyOkToAgent:
		if 
		:: 	parCareOfAgent!replyOk, parCareOfAgent, parHomeAgent;
               		goto Start;
          			
		:: 	goto TimeRunsOut;
               	fi;

}


         
init
{
	chan net1Link          	= [0] of {mtype, chan}; 		/*Create a network link on "network 1"*/
        chan net2Link          	= [0] of {mtype, chan};			/*Create a network link on "network 2"*/

        chan agent1Address     	= [0] of {mtype, chan, chan};		/*Create an agent address on "network 1"*/
        chan agent2Address     	= [0] of {mtype, chan, chan};  		/*Create an agent address on "network 2"*/


      
        run Agent(net1Link, agent1Address); 		/*Create an agent on "network 1"*/
        run Agent(net2Link, agent2Address);		/*Create an agent on "network 2"*/

        run MobileNode(agent1Address);			/*Create a mobile node with "Agent 1" as home agent*/

	
        do

	::	move!net1Link ;                       /*Move a mobile node to "network 1"*/

        ::      move!net2Link ;			      /*Move a mobile node to "network 2"*/

        od;

}