(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : BRPAAPP21_GSinFSdk
 * Description      : Bounded Retransmission Protocol [version slightly modified]
 * Correctness      : 
 * Scalable         : no
 * Generated        : no
 * Categories       : Protocol
 * Source           : "Iterative bounded synthesis for efficient cycle detection in parametric timed automata", TACAS 2021
 * bibkey           : AAPP21
 * Author           : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans; then Laurent Fribourg, Étienne André, Laure Petrucci, Jaco van de Pol
 * Modeling         : Laurent Fribourg
 * Input by         : Étienne André, Laure Petrucci, Jaco van de Pol
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : ? (< 09/2007)
 * Last modified    : 2021/10/05
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)

var
	x,z,u,v
		: clock;

	i,	(* subscript of the chunk currently beeing processed (1<=i<=N) *)
	rc, 	(* nb of attempt undertaken by S to retransmit d_i (0<=rc<=MAX) *)
	MAX = 2, 	(* maximal number of retransmissions *)
	N = 2, 		(* number of chunks of a file *)
		: int;
	b1,bN, rb1,rbN, (* these Boolean variables are used for communication between S-K-L-R *)
	ab, rab, exp_ab	(* to be sent/received/expected alternating bit *)
		: bool;

	SYNC,		(* 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 *)
	TS,	(* 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 monitor
(************************************************************)

actions: S_in, S_OK, S_NOK, S_DK, sndD;

loc s0: invariant True
    	when True sync sndD goto s0;
    	when True sync S_OK goto s0;
		when True sync S_DK goto s0;
    	when True sync S_NOK goto s0;
    	when True sync S_in goto s0;
    	when True sync S_in goto s1;

accepting loc s1: invariant True
    	when True sync sndD goto s1;
    	when True sync S_in goto s1;

end (* monitor *)

(****************************************************)
automaton sender
(****************************************************)
actions: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;

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

urgent loc next_frame: invariant True
	when i=N sync sndD do {bN:=True} goto wait_ack;
	when i<N sync sndD do {bN:=False} goto wait_ack;

loc wait_ack: invariant x<=TS
	when x=TS & rc=MAX & i=N sync S_DK do {x:=0,rc:=0,i:=1} goto error;
	when x=TS & rc=MAX & i<N sync S_NOK do {x:=0,rc:=0,i:=1} goto error;
	when x<TS sync rcvA do {ab:=not(ab),x:=0,rc:=0} goto success;
	when x=TS & rc<MAX sync sndD do {rc:=rc+1,x:=0} goto wait_ack;

urgent loc success: invariant True
	when i<N do {i:=i+1,b1:=False} goto next_frame;
	when i=N sync S_OK do {i:=1} goto idleS;

loc error: invariant x <= SYNC
	when x=SYNC do {ab:=False} goto idleS;

end (* sender *)


(****************************************************)
automaton receiver
(****************************************************)
actions: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;

loc new_file: invariant True
	when True sync rcvD do {z:=0} goto fst_safe;

urgent loc fst_safe: invariant True
	when rb1 do {exp_ab:=rab} goto frame_received;

urgent loc frame_received: invariant True
	when rab=exp_ab & rb1 & not(rbN) sync R_FST
			do {rb1:=False,rab:=False} goto frame_reported;
	when rab=exp_ab & not(rb1) & not(rbN) sync R_INC
			do {rb1:=False,rab:=False} goto frame_reported;
	when rab=exp_ab & rbN sync R_OK
			do {rb1:=False,rab:=False} goto frame_reported;
	when rab=not(exp_ab) sync sndA do {rb1:=False,rab:=False} goto idleR;


urgent loc frame_reported: invariant True
	when True sync sndA do {exp_ab:=not(exp_ab),z:=0} goto idleR;

loc idleR: invariant z<=TR
	when z<TR sync rcvD do {} goto frame_received;
	when z=TR & not(rbN) sync R_NOK do {rbN:=False,exp_ab:=False} goto new_file;
	when z=TR & rbN do {rbN:=False,exp_ab:=False} goto new_file;

end (* receiver *)


(****************************************************)
automaton channelK
(****************************************************)
actions: sndD, rcvD, lostK;

loc startK: invariant u>=0
	when True sync sndD do {u:=0} goto in_transitK;


loc in_transitK: invariant u<=TD
	when True sync lostK goto startK;
	when True do {rb1:=b1, rbN:=bN, rab:=ab} sync rcvD goto startK;

end (* channelK *)



(****************************************************)
automaton channelL
(****************************************************)
actions: sndA, rcvA, lostL;

loc startL: invariant v>=0
	when True sync sndA do {v:=0} goto in_transitL;

loc in_transitL: invariant v<=TD
	when True sync rcvA  goto startL;
	when True sync lostL goto startL;

end (* channelL *)



(************************************************************)
(* Initial state *)
(************************************************************)
init :=   {
	discrete =
		(* Initial state *)
		loc[sender]:=idleS,
		loc[receiver]:=new_file,
		loc[channelK]:=startK,
		loc[channelL]:=startL,
		loc[monitor]:=s0,

		(* Initial discrete variables assignments *)
		rc		:= 0,
		i		:= 1,
		ab		:= False,
		b1		:= False,
		bN		:= False,
		rb1		:= False,
		rbN		:= False,
		rab		:= False,
		exp_ab	:= False,
	;

	continuous =
		(* Initial clock constraints *)
		& x=0 & z=0 & u=0 & v=0

		(* Parameter constraints *)
		& TD > 0
		& TS > 0
		& TR > 0
		& SYNC > 0

		& TS > 2*TD
	;
}

end