%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%	XL code for the i-protocol
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%-----------------------------------------------------------------------------
%%	The data channel
medium ::=
	in(chan_in, X)
	o (
		out(chan_out, recvpak(true, true, X))
	#	action(drop)
	#	action(corrupt)
		o (
			out(chan_out, recvpak(true, false, X)) 
		#	out(chan_out, recvpak(false, false, X))
		#	out(chan_out, recvpak(false, true, X))
		)
	)
	o medium.


%%-----------------------------------------------------------------------------
%%	The sender
%%
%%	SendState == s(SendSeq, Rack) 
%%	Packet = packet(PakType, Seq, Ack)
%%
%%	Sender's active window = open(Rack, SendSeq).
%%	Receiver's active window = upper_closed(RecSeq, Lack).

sender(In) ::=
	(
		s_sendmsg(In, Mid)
	#	s_getpkt(In, Mid)
	#	action(progress) o s_timeout(In, Mid)
	) 
	o sender(Mid).

s_sendmsg(In, Out) ::=
	in(user_send)
	o s_sendmsg_while1(In, Mid)
	o Mid = s(SendSeq, Rack)
	o out(med_out, packet(type_DATA, SendSeq, /* RecSeq */ 0))
	o eval(NextSend := SendSeq+1)
	o Out = s(NextSend, Rack).

s_sendmsg_while1(In, Out) ::=
	In = s(SendSeq, Rack)
	o if( (eval(SendSeq-Rack > window_size); SendSeq == Rack)
		, ( 	( s_getpkt(In, Mid)
			# action(timeout) o s_timeout(In, Mid)
			)
		      o s_sendmsg_while1(Mid, Out))
		, Out = In
	).

s_getpkt(In, Out) ::=
	in(med_in, RecvPak)
	o RecvPak = recvpak(Hck, _Dck, Pak)
	o if( Hck == true
		, ( Pak = packet(PakType, _Seq, Ack)
		  o s_handle_ack(Ack, In, Mid)
		  o if( PakType == type_NAK
			, s_handle_nak(Mid, Out, Pak)
			, Out = Mid
		  ))
		, Out = In
	).

s_handle_ack(Ack, In, Out) :-
	In = s(SendSeq, Rack),
	(in_interval(Ack, open(SendSeq, Rack))
		-> Out = s(SendSeq, /* Rack = */ Ack)
		;  Out = In
	).

s_handle_nak(In, In, Pak) ::=
	Pak = packet(_PakType, Seq, _Ack)
	o In = s(SendSeq, Rack)
	o if(in_interval(Seq, open(SendSeq, Rack))
		, out(med_out, packet(type_DATA, Seq, /* RecSeq */ 0))
	  )
	.

s_timeout(In, Out) ::=
	In = s(SendSeq, Rack)
	o (
		s_getpkt(In, Out)
	    # 
		(
		out(med_out, packet(type_NAK, /* PakSeq */ 1, /* RecSeq */ 0))
		o if( (not(eval(SendSeq == (Rack+1))))
			, 	( eval(PakSeq1 := Rack + 1)
				o out(med_out, packet(type_DATA, 
						PakSeq1, /* RecSeq */ 0))
				)
		  )
		o Out = In
	        )
	  ).

%%-----------------------------------------------------------------------------
%%	The receiver
%%
%%	State == r(SendSeq, RecSeq, Lack, Rack, Nakd, RecBuf) 
%%	Packet = packet(PakType, Seq, Ack)
%%
%%	Receiver's active window = upper_closed(RecSeq, Lack).

receiver(In) ::=
	(
		r_getpkt(In, Mid)
	#	action(progress) o r_timeout(In, Mid)
	) 
	o receiver(Mid).

r_getpkt(In, Out) ::=
	in(med_in, RecvPak)
	o RecvPak = recvpak(Hck, Dck, Pak)
	o if( Hck == true
		, ( Pak = packet(PakType, _Seq, _Ack)
%		  o r_handle_ack(Ack, In, Mid)
		  o if( PakType == type_DATA
			, r_handle_data(In, Out, Pak, Dck)
			, if( PakType == type_NAK
				, r_handle_nak(In, Out, Pak)
				, Out = In
			)
		  ))
		, Out = In
	).

r_handle_data(In, Out, Pak, Dck) ::=
	In = r(_SendSeq, _RecSeq, Lack, _Rack, _Nakd, _RecBuf)
	o Pak = packet(_PakType, Seq, _Ack)
	o if( (not(eval(Seq-Lack > window_size)), Seq =\= Lack)
		, r_handle_data_correct(In, Out, Pak, Dck)
		, Out = In
	).

r_handle_data_correct(In, Out, Pak, Dck) ::= 
	In = r(SendSeq, RecSeq, Lack, Rack, Nakd, RecBuf)
	o Pak = packet(_PakType, Seq, _Ack)
	o if( Dck == true
		, ( remove_from_set(Seq, Nakd, MidNakd)
		  o Mid = r(SendSeq, RecSeq, Lack, Rack, MidNakd, RecBuf)
		  o if( eval(Seq == RecSeq + 1)
			, r_handle_data_expected_seqno(Mid, Out, Pak)
			, r_handle_data_unexpected_seqno(Mid, Out, Pak)
		  ))
		% Dck == false
		, if( (Seq =\= RecSeq;
		       (in_set(Seq, RecBuf));
		       (in_set(Seq, Nakd)))
			, ( out(med_out, packet(type_NAK, Seq, RecSeq))
			  o add_to_set(Seq, Nakd, NewNakd)
			  o Out = r(SendSeq, RecSeq, RecSeq, Rack, NewNakd, RecBuf)
			  )
			, Out = In
		  )
	).

r_handle_data_expected_seqno(In, Out, Pak) ::= 
	In = r(SendSeq, RecSeq, Lack, Rack, Nakd, RecBuf)
	o Pak = packet(_PakType, _Seq, _Ack)
	o eval(MidRecSeq := RecSeq + 1)
	o action(user_recv)
	o eval(Tmp := MidRecSeq + 1)
	o r_supply_to_user(Tmp, MidRecSeq, RecBuf, NewRecSeq, NewRecBuf)
	o if( eval((NewRecSeq-Lack) >= window_size//2)
		, ( out(med_out, packet(type_ACK, NewRecSeq, NewRecSeq))
			o NewLack = NewRecSeq)
		, NewLack = Lack
		)
	o Out = r(SendSeq, NewRecSeq, NewLack, Rack, Nakd, NewRecBuf).


r_supply_to_user(Tmp, RecSeq, RecBuf, NewRecSeq, NewRecBuf)  ::=
	if( in_set(Tmp, RecBuf)
		, ( action(user_recv)
			o remove_from_set(Tmp, RecBuf, MidRecBuf)
			o eval(Next := Tmp + 1)
			o r_supply_to_user(Next, Tmp, MidRecBuf,
							NewRecSeq, NewRecBuf))
		, (NewRecBuf = RecBuf o NewRecSeq = RecSeq)
	).

r_handle_data_unexpected_seqno(In, Out, Pak) ::=
	In = r(SendSeq, RecSeq, Lack, Rack, Nakd, RecBuf)
	o Pak = packet(_PakType, Seq, _Ack)
	o if( (Seq =\= RecSeq,
		not(in_set(Seq, RecBuf)))
		, ( add_to_set(Seq, RecBuf, NewRecBuf)
			o eval(Tmp := RecSeq + 1)
			o r_send_naks(Tmp, Seq, RecSeq, Nakd, NewRecBuf, Lack,
							NewNakd, NewLack)
			o Out = r(SendSeq, RecSeq, NewLack, Rack,
							NewNakd, NewRecBuf))
		, Out = In
	).

r_send_naks(Tmp, Seq, RecSeq, Nakd, RecBuf, Lack, NewNakd, NewLack) ::=
	if((Tmp =\= Seq)
		, ( if( (not(in_set(Tmp, Nakd)), not(in_set(Tmp, RecBuf)))
			, ( out(med_out, packet(type_NAK, Tmp, RecSeq))
				o add_to_set(Tmp, Nakd, MidNakd)
				o MidLack = RecSeq)
			, (MidNakd = Nakd o MidLack = Lack)
		    )
		    o eval(Next := Tmp + 1)
		    o r_send_naks(Next, Seq, RecSeq, MidNakd, RecBuf, MidLack,
				NewNakd, NewLack)
		  )
		, (NewNakd = Nakd o NewLack = Lack)
	).


r_handle_ack(Ack, In, Out) :-
	In = r(SendSeq, RecSeq, Lack, Rack, Nakd, RecBuf),
	(in_interval(Ack, open(SendSeq, Rack))
		-> Out = r(SendSeq, RecSeq, Lack, /* Rack = */ Ack, 
				Nakd, RecBuf)
		;  Out = In
	).

r_handle_nak(In, Out, Pak) ::=
	if( fixed(fix)
	,
		Pak = packet(_PakType, _Seq, _Ack)
		o In = r(SendSeq, RecSeq, _Lack, Rack, Nakd, RecBuf)
		o out(med_out, packet(type_ACK, RecSeq, RecSeq))
		o Out = r(SendSeq, RecSeq, RecSeq, Rack, Nakd, RecBuf)
	,
		Out = In
	).

r_timeout(In, Out) ::=
	  In = r(SendSeq, RecSeq, Lack, Rack, _Nakd, RecBuf)
	o Mid = r(SendSeq, RecSeq, Lack, Rack, 0, RecBuf)
	o (
		r_getpkt(Mid, Out)
	    #
		eval(PakSeq := RecSeq + 1)
		o add_to_set(PakSeq, 0, NewNakd)
		o out(med_out, packet(type_NAK, PakSeq, RecSeq))
		o Out = r(SendSeq, RecSeq, /* Lack = */ RecSeq, Rack,
							NewNakd, RecBuf)
	  ).

%%=============================================================================
%%	The system

i ::= 
	( sender(s(1,0))
		@ [ user_send/lsend, user_recv/lrecv, 
		    med_in/rl_out, med_out/lr_in
		  ]
	| receiver(r(1,0,0,0,0,0))
		@ [ user_send/rsend, user_recv/rrecv,
		    med_in/lr_out, med_out/rl_in
		  ]
	| medium 
		@ [ chan_in/lr_in, chan_out/lr_out]
	| medium 
		@ [ chan_in/rl_in, chan_out/rl_out]
	)
	\ {lr_in, lr_out, rl_in, rl_out}.

%%-----------------------------------------------------------------------------
%%	 system configuration

config(WS,Fix) :-
	abolish_all_tables,
	retractall(window_size(_)),
	retractall(seq(_)),
	retractall(fixed(_)),
	S is 2*WS,
	assert(window_size(WS)),
	assert(seq(S)),
	assert(fixed(Fix)).

%%=============================================================================
%%	The livelock property

try += tx6 \/ diam(-nil, try).
tx6 -= diam([timeout,nop,tau], tx6).

%%=============================================================================
%%	Some arithmetic

:- import ground/1 from basics.

eval(X = Y)  :- !, X = Y.
eval(X == Y) :- !, eval(X, U), eval(Y, V), modulus(U, Ua), modulus(V, Va), Ua == Va.
eval(X := Y) :- !, eval(Y, U), modulus(U, X).
eval(X is Y) :- !, eval(Y, U), modulus(U, X).
eval(X > Y)  :- !, eval(X, U), eval(Y, V), modulus(U, Ua), modulus(V, Va), Ua > Va.
eval(X < Y)  :- !, eval(X, U), eval(Y, V), modulus(U, Ua), modulus(V, Va), Ua < Va.
eval(X >= Y) :- !, eval(X, U), eval(Y, V), modulus(U, Ua), modulus(V, Va), Ua >= Va.
eval(X =< Y) :- !, eval(X, U), eval(Y, V), modulus(U, Ua), modulus(V, Va), Ua =< Va.
eval(not(E)) :- !, not(eval(E)).

eval(A+B, V) :- !, eval(A, Va), eval(B, Vb), V is Va+Vb.
eval(A-B, V) :- !, eval(A, Va), eval(B, Vb), V is Va-Vb.
eval(A*B, V) :- !, eval(A, Va), eval(B, Vb), V is Va*Vb.
eval(A/B, V) :- !, eval(A, Va), eval(B, Vb), V is Va/Vb.
eval(A//B, V) :- !, eval(A, Va), eval(B, Vb), V is Va//Vb.
eval(window_size, V) :- !, window_size(V).
eval(E, V) :- V is E.

modulus(E, V) :- seq(Seq), X is E mod Seq, abs(X, V).
abs(X, V) :- ( X < 0 -> (seq(Seq), V is X+Seq) ; V = X).

%% Now, some interval stuff

in_interval(X, open(L,U)) :- 
	X =\= L,
	eval((L-X) =< window_size),
	eval((X-U) =< window_size).

in_open_interval(X, L,U) :- 
	X =\= L,
	eval((L-X) =< window_size),
	eval((X-U) =< window_size).

in_interval(X, upper_closed(L, U)) :-
	(L > U -> (X > L; X =< U)
		; (X > L, X =< U)).
in_interval(X, closed(L, U)) :-
	(L > U -> (X >= L; X =< U)
		; (X >= L, X =< U)).

%% Finally, some set stuff

in_set(Element, Set) :-
	1 is ((Set >> Element) mod 2).

add_to_set(Element, Set, NewSet) :- 
	in_set(Element, Set)
	->	NewSet = Set
	;	NewSet is Set + (1 << Element).

remove_from_set(Element, Set, NewSet) :-
	in_set(Element, Set)
	->	NewSet is Set - (1 << Element)
	;	NewSet = Set.