Commit 553d17ef authored by validator's avatar validator
Browse files

No commit message

No commit message
parent 2f057fc6
Loading
Loading
Loading
Loading
+148 −31
Original line number Diff line number Diff line
@@ -127,13 +127,127 @@ module LibIpv6_Rfc3775Mipv6_Functions {
	group bindingFns {
		
	
		
		/*
		 * @desc  primaryCareOfAddressRegistration
	 	 * @param p_mnCoaTn Mobile Node Care Of Address of test node
		 * @param p_mnHoaTn Mobile Node Home Address of test node
		 * @param p_haGlaNut Home Agent Address of node under test
		*/
		altstep a_receiveBindingUpdateAndReplyAtHome(in template Ipv6NodeParams p_paramsTn, in template Ipv6Address p_haGlaTn)
		runs on Ipv6Node {
			//Variables
			var GeneralIpv6 v_generalIpv6 ;
			var UInt16 v_seqNr := 0;
			var Ipv6Address v_mnCareOfAddr1 := c_16ZeroBytes;
			var Ipv6Address v_mnCareOfAddr2 := c_16ZeroBytes;
			var Ipv6Address v_mnHomeAddr := c_16ZeroBytes;
			var FncRetCode v_ret := e_error;
			var Ipv6Address v_receivedTargetAddr := c_16ZeroBytes;
			var NeighborSolicitation v_nbrSol ;
			
			//tc_wait.start;
			//alt {
			[]	ipPort.receive(mw_nbrSol_addressDetermination(PX_SOL_NODE_MCA_IUT_A, ?)) -> value v_nbrSol{
					v_receivedTargetAddr := v_nbrSol.targetAddr ;
					
					f_sendNbrAdv (m_nbrAdv_noExtHdr( 	p_paramsTn.lla,
														c_allNodesMca,
														c_rFlag0,
														c_sFlag0,
														c_oFlag0,
														v_receivedTargetAddr,
														m_nbrAdvOpt_tllaOpt(p_paramsTn.macUca)  )) ;	
					repeat;
				}
		
				//1st alternative : m_optPad2 + Coa
				[]	ipPort.receive(mw_generalIpv6_dst(	c_dstHdr,
															//p_mnCoaTn,
															p_haGlaTn,
															m_extHdrList_1Elem(
																mw_extHdr_mipHeader (c_noNextHdr,
																					c_bindingUpdate,
																					mw_bindingUpdate(c_aFlag1,
																									c_hFlag1,
																									c_lFlag0,
																									c_kFlag0,
																									m_mipOptList_2Elem(
																										m_mipOpt_padN(m_optPad2),
																										m_mipOpt_altCoa(mw_mipOptAltCoA))))))) -> value v_generalIpv6 {
						//Get SeqNr
						v_seqNr := v_generalIpv6.extHdrList[1].mipHeader.mipMessage.bindingUpdate.sequenceNumber;
						//Get CareOfAddress
						v_mnCareOfAddr1 := v_generalIpv6.ipv6Hdr.sourceAddress;
						//TODO read v_mnCareOfAddr2 from MipOptions
						//GetHomeAddress
						v_mnHomeAddr := v_generalIpv6.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress;
						//tc_wait.stop;	
						v_ret := e_success ;
						v_ret := f_sendGeneralIpv6(m_generalIpv6_srcDst(	c_routeHdr,
																			p_haGlaTn,
																			v_mnCareOfAddr1,
																			m_extHdrList_1Elem(
																				m_extHdr_mipHeader (
																					c_noNextHdr,
																					c_bindingAck,
																					m_bindingAck(
																						v_seqNr,
																						m_mipOptList_1Elem(
																						m_mipOpt_padN(m_optPad4)))))));
					repeat;
					}
				//2nd alternative : m_optPad4
				[]	ipPort.receive(mw_generalIpv6_dst(	c_dstHdr,
															//p_mnCoaTn,
															p_haGlaTn,
															m_extHdrList_1Elem(
																mw_extHdr_mipHeader (c_noNextHdr,
																					c_bindingUpdate,
																					mw_bindingUpdate(c_aFlag1,
																									c_hFlag1,
																									c_lFlag0,
																									c_kFlag0,
																									m_mipOptList_1Elem(
																										m_mipOpt_padN(m_optPad4))))))) -> value v_generalIpv6 {
						//Get SeqNr
						v_seqNr := v_generalIpv6.extHdrList[1].mipHeader.mipMessage.bindingUpdate.sequenceNumber;
						//Get CareOfAddress
						v_mnCareOfAddr1 := v_generalIpv6.ipv6Hdr.sourceAddress;
						//GetHomeAddress
						v_mnHomeAddr := v_generalIpv6.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress;
						//tc_wait.stop;	
						v_ret := e_success ;
						v_ret := f_sendGeneralIpv6(m_generalIpv6_srcDst(	c_routeHdr,
																							p_haGlaTn,
																							v_mnCareOfAddr1,
																							m_extHdrList_1Elem(
																								m_extHdr_mipHeader (
																									c_noNextHdr,
																									c_bindingAck,
																									m_bindingAck(
																										v_seqNr,
																										m_mipOptList_1Elem(
																										m_mipOpt_padN(m_optPad4)))))));
					repeat;
					}
//				[]	tc_wait.timeout{
//						v_ret :=  e_timeout;
//						log("**** f_receiveBindingUpdateAndReply: ERROR: tc_ac.timeout **** ");
//					}		
			//} // end alt

			//return v_ret;

		}//end a_receiveBindingUpdateAndReplyAtHome
		
		/*
				 * @desc  primaryCareOfAddressRegistration
				 * @param p_mnCoaTn Mobile Node Care Of Address of test node
				 * @param p_mnHoaTn Mobile Node Home Address of test node
				 * @param p_haGlaNut Home Agent Address of node under test
				*/
		altstep a_receiveBindingUpdateAndReply(in template Ipv6NodeParams p_paramsTn, in template Ipv6Address p_haGlaTn)
				altstep a_receiveBindingUpdateAndReplyOffHome(in template Ipv6NodeParams p_paramsTn, in template Ipv6Address p_haGlaTn)
				runs on Ipv6Node {
					//Variables
					var GeneralIpv6 v_generalIpv6 ;
@@ -153,8 +267,8 @@ module LibIpv6_Rfc3775Mipv6_Functions {
							f_sendNbrAdv (m_nbrAdv_noExtHdr( 	p_paramsTn.lla,
																c_allNodesMca,
																c_rFlag0,
														c_sFlag1,
														c_oFlag1,
																c_sFlag0,
																c_oFlag0,
																v_receivedTargetAddr,
																m_nbrAdvOpt_tllaOpt(p_paramsTn.macUca)  )) ;	
							repeat;
@@ -260,7 +374,10 @@ module LibIpv6_Rfc3775Mipv6_Functions {

					//return v_ret;

		}//end f_receiveBindingUpdateAndReply
				}//end a_receiveBindingUpdateAndReplyOffHome

		

		
		/*
		 * @desc  primaryCareOfAddressRegistration
@@ -268,7 +385,7 @@ module LibIpv6_Rfc3775Mipv6_Functions {
		 * @param p_mnHoaTn Mobile Node Home Address of test node
		 * @param p_haGlaNut Home Agent Address of node under test
		*/
		function f_receiveBindingUpdateAndReply_lifeTime(in template Ipv6Address p_haGlaTn, in UInt16 p_lifeTime)
		function f_receiveBindingUpdateAndReplyOffHome(in template Ipv6Address p_haGlaTn, in UInt16 p_lifeTime)
		runs on Ipv6Node
		return FncRetCode {
			//Variables