module MiniSIP {

	type record SIP_resquestType {
		charstring method,
		charstring version,
		charstring fromField,
		charstring toField
	}
					
	type record SIP_Status_responseType {
		charstring sipVersion,
		integer statusCode,
		charstring reasonPhrase,
		charstring fromField,
		charstring toField
	}
	
	type port CoordinationPortType message {
		inout charstring;
	}
	
	type port SipPortType message {
		inout SIP_resquestType, SIP_Status_responseType;
	}
	
	type component MTCType {
		port CoordinationPortType coord_port_server;
		port CoordinationPortType coord_port_caller;
		port CoordinationPortType coord_port_callee;
	}
	
	type component ServerType {
		port CoordinationPortType coord_port;
		port SipPortType sipPort_1;
		port SipPortType sipPort_2;	
	}
	
	type component PTCType {
		port CoordinationPortType coord_port;
		port SipPortType sipPort;
	}
	
	type component SystemType {
		
	}
	
	///////////////////////////////////////
	
	template SIP_resquestType caller_SIP_Invite_Request := {
		method := "INVITE",
		version := "SIP/2.0",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}

	template SIP_resquestType SIP_Invite_Request := {
		method := "INVITE",
		version := "SIP/2.0",
		fromField := ?,
		toField := ?
	}
	
	template SIP_resquestType caller_SIP_Bye_Request := {
		method := "BYE",
		version := "SIP/2.0",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}

	template SIP_resquestType callee_SIP_Bye_Request := {
		method := "BYE",
		version := "SIP/2.0",
		fromField := "callee@abcd.com",
		toField := "caller@efgh.com"
	}
	
	template SIP_resquestType SIP_Bye_Request := {
		method := "BYE",
		version := "SIP/2.0",
		fromField := ?,
		toField := ?
	}
	
	template SIP_resquestType caller_SIP_Ack_Request := {
		method := "ACK",
		version := "SIP/2.0",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}
	
	template SIP_resquestType SIP_Ack_Request := {
		method := "ACK",
		version := "SIP/2.0",
		fromField := ?,
		toField := ?
	}
		
	template SIP_Status_responseType SIP_200_OK_Response := {
		sipVersion := "SIP/2.0",
		statusCode := 200,
		reasonPhrase := "OK",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}
	
	template SIP_Status_responseType SIP_100_Trying_Response := {
		sipVersion := "SIP/2.0",
		statusCode := 100,
		reasonPhrase := "Trying",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}
	
	template SIP_Status_responseType SIP_180_Ringing_Response := {
		sipVersion := "SIP/2.0",
		statusCode := 180,
		reasonPhrase := "Ringing",
		fromField := "caller@abcd.com",
		toField := "callee@efgh.com"
	}
	
	//////////////////////////////////////////
	
	/*
	function serverBehavior() runs on ServerType {
		var SIP_resquestType inviteRequest;
		var SIP_resquestType byeRequest;
		var SIP_resquestType ackRequest;
		var SIP_Status_responseType ringingResponse;
		var SIP_Status_responseType OKResponse;
		log("running server");
		
		alt {
			[] sipPort_1.receive(SIP_Invite_Request) -> value inviteRequest	{
				log("server received a INVITE from " & inviteRequest.fromField);
				sipPort_1.send(SIP_100_Trying_Response);
				if(inviteRequest.toField == "callee@efgh.com") {
					sipPort_2.send(inviteRequest);
					
					alt {
						[] sipPort_2.receive(SIP_200_OK_Response) -> value OKResponse {
							sipPort_1.send(OKResponse)
							//setverdict(pass) 
						}
						[] sipPort_2.receive(SIP_180_Ringing_Response) -> value ringingResponse {
							sipPort_1.send(ringingResponse);
							repeat 
						}
						[] sipPort_2.receive {
							setverdict(fail)
						}
					}	
				}
				repeat
			}
			[] sipPort_1.receive(SIP_Bye_Request) -> value byeRequest	{
				log("server received a BYE from " & byeRequest.fromField);
				if(byeRequest.toField == "callee@efgh.com") {
					sipPort_2.send(byeRequest);
					
					alt {
						[] sipPort_2.receive(SIP_200_OK_Response) -> value OKResponse {
							sipPort_1.send(OKResponse);
							setverdict(pass)
						} 
						[] sipPort_2.receive {
							setverdict(fail)
						}
					}	
				}
				repeat
			}
			[] sipPort_1.receive(SIP_Ack_Request) -> value ackRequest	{
				log("server received a BYE from " & ackRequest.fromField);
				if(ackRequest.toField == "callee@efgh.com") {
					sipPort_2.send(ackRequest);
				}
			}
			[] sipPort_2.receive(SIP_Invite_Request) -> value inviteRequest	{
				log("receive a INVITE from " & inviteRequest.fromField)
				
			}
		}
	}
	*/
	

	function serverBehavior() runs on ServerType {
		var SIP_resquestType inviteRequest;
		var SIP_resquestType byeRequest;
		var SIP_resquestType ackRequest;
		var SIP_Status_responseType ringingResponse;
		var SIP_Status_responseType OKResponse;
		log("running server");
		
		alt {
			[] sipPort_1.receive(SIP_Invite_Request) -> value inviteRequest	{
				sipPort_1.send(SIP_100_Trying_Response);
				if(inviteRequest.toField == "callee@efgh.com") {
					sipPort_2.send(inviteRequest);
				}
				repeat
			}
			[] sipPort_1.receive(SIP_200_OK_Response) -> value OKResponse {
				if(OKResponse.fromField == "callee@efgh.com") {
					sipPort_2.send(OKResponse);
				}
				repeat
			}
			[] sipPort_1.receive(SIP_180_Ringing_Response) -> value ringingResponse {
				if(ringingResponse.fromField == "callee@efgh.com") {
					sipPort_2.send(ringingResponse);
				}
				repeat 
			}
			[] sipPort_1.receive(SIP_Bye_Request) -> value byeRequest	{
				if(byeRequest.toField == "callee@efgh.com") {
					sipPort_2.send(byeRequest);
				}
				repeat
			}
			[] sipPort_1.receive(SIP_Ack_Request) -> value ackRequest	{
				if(ackRequest.toField == "callee@efgh.com") {
					sipPort_2.send(ackRequest);
				}
				repeat
			}

			[] sipPort_2.receive(SIP_Invite_Request) -> value inviteRequest	{
				sipPort_2.send(SIP_100_Trying_Response);
				if(inviteRequest.toField == "caller@abcd.com") {
					sipPort_1.send(inviteRequest);
				}
				repeat
			}
			[] sipPort_2.receive(SIP_200_OK_Response) -> value OKResponse {
				if(OKResponse.fromField == "caller@abcd.com") {
					sipPort_1.send(OKResponse);
				}
				repeat
			}
			[] sipPort_2.receive(SIP_180_Ringing_Response) -> value ringingResponse {
				if(ringingResponse.fromField == "caller@abcd.com") {
					sipPort_1.send(ringingResponse);
				}
				repeat 
			}
			[] sipPort_2.receive(SIP_Bye_Request) -> value byeRequest	{
				if(byeRequest.toField == "caller@abcd.com") {
					sipPort_1.send(byeRequest);
				}
				repeat
			}
			[] sipPort_2.receive(SIP_Ack_Request) -> value ackRequest	{
				if(ackRequest.toField == "caller@abcd.com") {
					sipPort_1.send(ackRequest);
				}
				repeat
			}
			[] coord_port.receive("shutdown") {
				stop
			}
			[] sipPort_1.receive {
				setverdict(fail)
			}
			[] sipPort_2.receive {
				setverdict(fail)
			}
		}
	}
	
	
	
	function callerBehavior() runs on PTCType {
		log("running caller");
		
		sipPort.send(caller_SIP_Invite_Request);
		
		alt {
			[] sipPort.receive(SIP_100_Trying_Response) {
				alt {
					[] sipPort.receive(SIP_180_Ringing_Response) {
						alt {
							[] sipPort.receive(SIP_200_OK_Response) {
								sipPort.send(caller_SIP_Bye_Request);
								alt {
									[] sipPort.receive(SIP_200_OK_Response) {
										sipPort.send(caller_SIP_Ack_Request);
										setverdict(pass)
									}
									[] failures() {
										setverdict(fail)
									}
								}		
							}
							[] failures() {
								setverdict(fail)
							}
						}
					}
					[] failures(){
						setverdict(fail)
					}
				}
			}
			[] failures() {
				setverdict(fail)
			}
		}					
	}
	
	function cooperativeCalleeBehavior() runs on PTCType {
		log("running callee");
		
		sipPort.receive(caller_SIP_Invite_Request);
		sipPort.send(SIP_180_Ringing_Response);
		sipPort.send(SIP_200_OK_Response);
		
		sipPort.receive(caller_SIP_Bye_Request);
		sipPort.send(SIP_200_OK_Response);
		sipPort.receive(caller_SIP_Ack_Request);
		setverdict(pass)
	}
	
	function uncooperativeCalleeBehavior() runs on PTCType {
		log("running callee");
		
		sipPort.receive(caller_SIP_Invite_Request);
		sipPort.send(SIP_180_Ringing_Response);
		sipPort.send(callee_SIP_Bye_Request);
		
		setverdict(pass)	
	}
				
	testcase inviteSIP_test() runs on MTCType system SystemType {
		var PTCType callerPTC;
		var PTCType calleePTC;
		var ServerType serverTC;
		
		serverTC := ServerType.create("SIPServer");
		callerPTC := PTCType.create("caller");
		calleePTC := PTCType.create("callee");

		connect(callerPTC:sipPort, serverTC:sipPort_1);
		connect(calleePTC:sipPort, serverTC:sipPort_2);
		
		connect(mtc:coord_port_callee, calleePTC.coord_port);
		connect(mtc:coord_port_caller, callerPTC.coord_port);
		connect(mtc:coord_port_server, serverTC.coord_port);
		
		serverTC.start(serverBehavior());
		callerPTC.start(callerBehavior());
		calleePTC.start(cooperativeCalleeBehavior());
		
		callerPTC.done;
		calleePTC.done;
		log("caller and callee processes done");
		coord_port_server.send("shutdown");
		serverTC.done;
		
	}

	altstep failures() runs on PTCType {
		
		[] any timer.timeout {
			setverdict (fail);
		}
		
		[] any port.receive {
			setverdict (fail);
		}
	}

	control {
		execute(inviteSIP_test())	
	}
}