(************************************************************
 *                      IMITATOR MODEL                      
 *
 * BRP (Bounded Retransmission Protocol)
 *
 * Description     : Bounded Retransmission Protocol [version slightly modified]
 * Correctness     : V[] ((S.error ^ x = SYNC) => R.new_file)
                     V [] (R.firstsafe_frame => rb1 = 1)
 * Source          : "The Bounded Retransmission Protocol Must Be on Time!"
 * Author          : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans
 * Modeling        : ?? and Laurent Fribourg
 * Input by        : ?? and Étienne André
 *
 * Created         : ? (< 09/2007)
 * Last modified   : 2018/09/06
 *
 * IMITATOR version: 2.10.4
 ************************************************************)
 

var     x,ys, yr,z,u,v
	(* removed 'w' as only used in R's automaton to mark urgent locations *)
           : clock;

	i,	-- subscript of the chunk currently beeing processed (1<=i<=N)
	ab,	-- alternating bit accompanying the next chunk to be sent
	rc, 	-- nb of attempt undertaken by S to retransmit d_i (0<=rc<=MAX)

	b1,bN, rb1,rbN, 


	retry,	-- specifique ici (borne le nombre de retentatives du sender
		-- lors d'une erreur a Maxr)
	Maxr,

	rab, exp_ab 
           : discrete;
	

        MAX = 2, 	-- maximal number of retransmissions
	N = 2, 	-- number of chunks of a file
	SYNC = 17, 	-- delay added after a failure in order to assure 
		-- that S does not start transmitting a new file before 
		-- the receiver has properly reacted to the failure
	T1 = 3,	-- time-out of the sender for initiating a retransmission
		-- when S has not received an ack from S
	TR,	-- time-out of the receiver for indicating failure
		-- when R has not received the last chunk of a file
	TD  	-- maximum delay in channel K (and L)
           : parameter;
-- -----------------------------------------------



--****************************************************--
--****************************************************--
-- AUTOMATA
--****************************************************--
--****************************************************--


--****************************************************--
  automaton sender
--****************************************************--
synclabs: Sin, B, F, Sout_DK, Sout_NOK, Sout_OK;


loc idleS: invariant x>=0
	when True sync Sin do {b1 := 1,i := 1,x := 0} goto next_frame; 
				

urgent loc next_frame: invariant True

	when i=N sync F do {bN := 1, rc := 0,x := 0}
			goto wait_ack;
	when i<N sync F do {bN := 0, rc := 0,x := 0}
			goto wait_ack;


loc wait_ack: invariant x<=T1
	when x=T1 & rc=MAX & i=N sync Sout_DK do {x := 0} goto error;
	when x=T1 & rc=MAX & i<N sync Sout_NOK do {x := 0} goto error;

	when x<T1 & ab=1 sync B do {ab := 0,x := 0} goto success;
	when x<T1 & ab=0 sync B do {ab := 1,x := 0} goto success;

	when x=T1 & rc<MAX sync F do {rc := rc+1,x := 0} goto wait_ack;


urgent loc success: invariant True
	when i<N do {i := i+1,b1 := 0,x := 0} goto next_frame;
	when i=N sync Sout_OK do {x := 0} goto EndS; -- idleS;


urgent loc error: invariant True
--	when x=0 & retry<Maxr do {ab := 0, retry := retry+1} goto idleS;
	when x=0  do {ab := 0} goto idleS;
--	invariant x<=SYNC
--	when x=SYNC do {ab := 0} goto idleS;


loc EndS: invariant x>=0

end --sender


--****************************************************--
  automaton receiver	
--****************************************************--
synclabs: G, A, Rout_NOK, Rout_OK, Rout_FST, Rout_INC;


loc new_file: invariant z>=0

	when True sync G do {z := 0(*,w := 0*)} goto fst_safe;


urgent loc fst_safe: invariant True (* originally w=0, but turned into urgent *)

	when rab=0 & rb1=1 do {exp_ab := 0} goto frame_received;
	when rab=1 & rb1=1 do {exp_ab := 1} goto frame_received;
	when rb1=0 goto FailureR;

loc frame_received: invariant True (* originally w=0, but turned into urgent *)

	when rab=0 & exp_ab=0 & rb1=1 & rbN=0 sync Rout_FST
			do {} goto frame_reported;

	when rab=0 & exp_ab=0 & rb1=0 & rbN=0 sync Rout_INC
			do {} goto frame_reported;

	when rab=0 & exp_ab=0 & rbN=1 sync Rout_OK
			do {} goto frame_reported;

	when rab=1 & exp_ab=1 & rb1=1 & rbN=0 sync Rout_FST
			do {} goto frame_reported;

	when rab=1 & exp_ab=1 & rb1=0 & rbN=0 sync Rout_INC
			do {} goto frame_reported;

	when rab=1 & exp_ab=1 & rbN=1 sync Rout_OK
			do {} goto frame_reported;


	when rab=1 & exp_ab=0 sync A do {} goto idleR;	-- do {z := 0} ???
	when rab=0 & exp_ab=1 sync A do {} goto idleR;	-- do {z := 0} ???



loc frame_reported: invariant True (* originally w=0, but turned into urgent *)

	when exp_ab=0 sync A do {exp_ab := 1,z := 0} goto idleR;
	when exp_ab=1 sync A do {exp_ab := 0,z := 0} goto idleR;


loc idleR: invariant z<=TR

	when z<TR sync G do {(*w := 0*)} goto frame_received;
	when z=TR & rbN=0 sync Rout_NOK do {} goto new_file;
	when z=TR & rbN=1 goto new_file;


loc FailureR: invariant z>=0

end --receiver




--****************************************************--
automaton channelK
--****************************************************--
synclabs: F,G;

loc startK: invariant u>=0

	when True sync F do {u := 0} goto in_transitK;   


loc in_transitK: invariant u<=TD

	when u<=TD & u>0 goto startK;  -- lost ??? (proba 0.02)

	when u<=TD & u>0 & b1=0 & bN=0 & ab=0
		do {rb1 := 0, rbN := 0, rab := 0}
		sync G  goto startK;
	when u<=TD & u>0 & b1=0 & bN=0 & ab=1
		do {rb1 := 0, rbN := 0, rab := 1}
		sync G  goto startK;
	when u<=TD & u>0 & b1=0 & bN=1 & ab=0
		do {rb1 := 0, rbN := 1, rab := 0}
		sync G  goto startK;
	when u<=TD & u>0 & b1=0 & bN=1 & ab=1
		do {rb1 := 0, rbN := 1, rab := 1}
		sync G  goto startK;
	when u<=TD & u>0 & b1=1 & bN=0 & ab=0
		do {rb1 := 1, rbN := 0, rab := 0}
		sync G  goto startK;
	when u<=TD & u>0 & b1=1 & bN=0 & ab=1
		do {rb1 := 1, rbN := 0, rab := 1}
		sync G  goto startK;
	when u<=TD & u>0 & b1=1 & bN=1 & ab=0
		do {rb1 := 1, rbN := 1, rab := 0}
		sync G  goto startK;
	when u<=TD & u>0 & b1=1 & bN=1 & ab=1
		do {rb1 := 1, rbN := 1, rab := 1}
		sync G  goto startK;

	when True sync F  goto BadK;

loc BadK: invariant u>=0

end -- channelK



--****************************************************--
automaton channelL
--****************************************************--
synclabs: A,B;

loc startL: invariant v>=0

	when True sync A do {v := 0} goto in_transitL;   



loc in_transitL: invariant v<=TD

	when v<=TD & v>0 sync B  goto startL;
	when v<=TD & v>0  goto startL;   -- lost ??? (proba 0.01)

	when True sync A  goto BadL;

loc BadL: invariant v>=0

end -- channelL


--****************************************************--
automaton Sclient	
--****************************************************--
synclabs: Sin, Sout_OK, Sout_DK, Sout_NOK;

loc startSC: invariant ys<=SYNC 		 -- invariant ys>=0

	when ys=SYNC & retry<=Maxr sync Sin do {ys := 0, retry := retry+1} 
				goto transSC; 
	-- when True sync Sin do {ys := 0}

loc transSC: invariant ys>=0

	when True sync Sout_OK do {ys := 0} goto startSC;  -- do{}
	when True sync Sout_DK do {ys := 0} goto startSC;  -- do{}
	when True sync Sout_NOK do {ys := 0} goto startSC; -- do{}

end --Sclient

--****************************************************--
automaton Rclient	
--****************************************************--
synclabs: Rout_FST, Rout_OK, Rout_INC, Rout_NOK;

loc startRC: invariant yr>=0

	when True sync Rout_FST do {yr := 0} goto transRC;
	when True sync Rout_OK  goto startRC;

loc transRC: invariant yr>=0

	when True sync Rout_OK  goto startRC; 
	when True sync Rout_INC  goto transRC; 
	when True sync Rout_NOK  goto startRC; 

end --Rclient



(************************************************************)
(* Initial state *)
(************************************************************)
init := loc[sender]=idleS
	& loc[receiver]=new_file
	& loc[channelK]=startK
	& loc[channelL]=startL
	& loc[Sclient]=startSC
	& loc[Rclient]=startRC
	& x=0 & ys=0 & yr=0 & z=0
(* 	& w=0 *)
	& u=0 & v=0
	& rc=0 & i=0 & ab=0 
	& b1=0 & bN=0 & rb1=0 & rbN=0
	& rab=0 & exp_ab=0
	& retry=0 & Maxr=0 	--Maxr=1

	-- & TR>=4T1+3TD	--TR=SYNC>4T1+3TD
	-- & T1>2TD & TR<=SYNC & TD>0 

(*	& MAX > 0
	& N > 0*)
	& TD > 0
	& T1 > 0
	& TR > 0
	& SYNC > 0
	
(* 	Constraint for EF to be fair with EFIM or IM *)
	& TD   >= 1 & TD <= 50
	& TR   >= 1 & TR <= 50

	
	
	----------------------
	-- Constraint output by IMITATOR 1
	----------------------
-- 	& 5T1 < TD + TR
--       & N = 2
--       & MAX = 2
--       & 0 < TD
--       & TR <= TD + SYNC
--       & 2TD < T1
--       & 3TD + 4T1 <= TR
--       & TR < 2TD + 5T1

;


(************************************************************)
(* Property specification *)
(************************************************************)
property := unreachable loc[receiver] = FailureR;


(************************************************************)
(* The end *)
(************************************************************)
end