(************************************************************
 *                      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   : 2020/04/30
 *
 * IMITATOR version: 3
 ************************************************************)
 

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;




(************************************************************)
  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;
	when True sync Sout_DK do {ys := 0} goto startSC;
	when True sync Sout_NOK do {ys := 0} goto startSC;

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*)

;


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