%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%	rtf.xl
%%	Rether RTF version
%%	translated to XL by Yifei Dong
%%	October 1998
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%----------------------------------------------------------------------
%	System constants
%	numNodes(NumberOfNodes).
%	maxID(NumberOfNodes-1).
%	TotalSlots(TotalTimeSlots).
%	maxRTSlots(TotalTimeSlots-1).
config(NumNodes, TotalSlots) :-
	retractall(numNodes(_)),
	retractall(maxID(_)),
	retractall(totalSlots(_)),
	retractall(maxRTSlots(_)),
	abolish_all_tables,
	MaxID is NumNodes-1,
	MaxRT is TotalSlots-1,
	assert(numNodes(NumNodes)),
	assert(maxID(MaxID)),
	assert(totalSlots(TotalSlots)),
	assert(maxRTSlots(MaxRT)).

numNodes(4).
maxID(3).
totalSlots(3).
maxRTSlots(2).

%%----------------------------------------------------------------------
%	ID arithmetic
incID(ID, NextID) :-
	numNodes(N),
	NextID is (ID+1) mod N.

%%----------------------------------------------------------------------
%	Format of token
%	token(
%		ServingRealtimeFlag,
%		RealtimeModeBooleanArray,
%		RealtimeSlots,
%		NonRealtimeSlotsRemaining,
%		NextNonRealtimeNodeID
%	)

%%----------------------------------------------------------------------
%	Channel convention
%	input:	in(port(ThisNode), Token)
%	output:	out(port(DestNode), Token)

%%----------------------------------------------------------------------
%	Node
%	States:	ID
%		RealtimeMode (stored in token?)
node(ID) ::=
	in(port(ID), Token) o
	nodeActive(ID, Token).

nodeActive(ID, Token) ::=
	Token = token(ServingRT, _RTMode, _RTSlots, _NRTAvail, _NextNRT) o
	if( ServingRT == 1
	,	nodeRT(ID, Token)
	,	nodeNRT(ID, Token)
	).

%%	RT action
%	1. optionally release realtime slot
%	2. pass token
nodeRT(ID, Token) ::=
	action(rt(ID)) o
	( releaseRT(ID, Token, Token1) 
	# Token1 = Token
	) o
	findNextNodeRT(ID, Token1, Next, NewToken) o
	if( Next == ID
	,	% no token passing within the same node
		nodeActive(ID, NewToken)
	,	(out(port(Next), NewToken) o
		node(ID))
	).


releaseRT(ID, Token, NewToken) :-
	Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT),
	( RTSlots > 1
	->	(NewRTSlots is RTSlots-1,
		 resetbit(RTMode, ID, NewRTMode),
		 NewToken = token(ServingRT, NewRTMode, NewRTSlots,
				  NRTAvail, NextNRT))
	,	NewToken = Token).

findNextNodeRT(ID, Token, Next, NewToken) :-
	Token = token(_ServingRT, RTMode, RTSlots, NRTAvail, NextNRT),
	ID1 is (ID + 1),
	(0 is (RTMode >> ID1)
	->	% no more RT node, then pass token to NRT node
		(Next = NextNRT,
		NewToken = token(0, RTMode, RTSlots, NRTAvail, NextNRT))
	;	(firstTrue(RTMode,ID1,Next),
		NewToken = Token)
	).

%%	NRT action
%	1. optionally reserve realtime slot
%	2. pass token
nodeNRT(ID, Token) ::=
	action(nrt(ID)) o
	( reserveRT(ID, Token, NewToken)
	# NewToken = Token) o
	passTokenNRT(ID, NewToken).

reserveRT(ID, Token, NewToken) ::=
	Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT) o
	maxRTSlots(MaxRT) o
	if( (falsebit(RTMode, ID), RTSlots < MaxRT)
	,	(NewRTSlots is RTSlots+1 o
		 setbit(RTMode, ID, NewRTMode) o
		 NewToken = token(ServingRT, NewRTMode, NewRTSlots,
				  NRTAvail, NextNRT) o
		 action(reserve(ID)))
	,	NewToken = Token).

passTokenNRT(ID, Token) ::=
	Token = token(ServingRT, RTMode, RTSlots, NRTAvail, NextNRT) o
	incID(NextNRT, NewNextNRT) o
	NewNRTAvail is NRTAvail - 1 o
	if( NewNRTAvail > 0
	,	% if NRT slots are available,
		% pass the token to the next NRT ndde
		(NewToken = token(ServingRT, RTMode, RTSlots, 
				NewNRTAvail, NewNextNRT) o
		out(port(NewNextNRT), NewToken) o
		node(ID))
	,	% if NRT slots are used up,
		% end this cycle and start a new cycle
		(action(endcycle) o
		totalSlots(Slots) o
		ResetNRTAvail is Slots - RTSlots o
		NewToken = token(1, RTMode, RTSlots,
				ResetNRTAvail, NewNextNRT) o
		firstTrue(RTMode, 0, FirstRT) o
		action(startcycle) o
		if( FirstRT == ID
		,	% no token passing within the same node
			nodeActive(ID, NewToken)
		,	(out(port(FirstRT), NewToken) o
			node(ID))
		))
	).

%%----------------------------------------------------------------------
%	System specification

starter ::=
	action(startcycle) o
	out(port(0), token(1,1,1,2,0)) o
	end.

rether ::=
	(starter | node(0) | node(1) | node(2) | node(3) | node(4))
	\ %{ port() }.
	{ port(0), port(1), port(2), port(3), port(4) }.

%%----------------------------------------------------------------------
%	Boolean array arithmetics
truebit(Array, Bit) :-
	1 is ((Array >> Bit) mod 2).

falsebit(Array, Bit) :-
	0 is ((Array >> Bit) mod 2).

setbit(Array, Bit, NewArray) :-
	truebit(Array, Bit)
	->	NewArray = Array
	;	NewArray is Array + (1 << Bit).

resetbit(Array, Bit, NewArray) :-
	truebit(Array, Bit)
	->	NewArray is Array - (1 << Bit)
	;	NewArray = Array.

firstTrue(Array, Begin, Result) :-
%	(0 is Array >> Begin
%	 -> (write('Error parameter for firstTrue'),
%		write(Array), writeln(Begin), halt)
%	; true),
	truebit(Array, Begin)
	->	Result = Begin
	;	(Next is Begin+1,
		 firstTrue(Array, Next, Result)).

%%=============================================================================
%%	properties

% deadlock
dl	+= box(-nil, ff) \/ diam(-nil, dl).

% deadlock free
dlf	-= box(-nil, dlf) /\ diam(-nil, tt).

% cycle completion
cc	-= box(-nil, cc) /\ box(startcycle, ccY).
ccY	+= diam(-nil, tt) /\ box(startcycle, ff)
	   /\ box(-endcycle, ccY).

% bandwidth guarantee for realtime nodes
rt(I)	-= box(-nil, rt(I)) /\ box(reserve(I), rtY(I)).
rtY(I)	+= box(-endcycle, rtY(I)) /\ box(rt(I), ff)
	   /\ box(endcycle, rtZ(I)).
rtZ(I)	+= diam(-nil, tt) /\ box(-rt(I), rtZ(I))
	   /\ box(endcycle, ff).

% no starvation for NRT traffic
ns(I)	-= box(-nil, ns(I)) /\ box(startcycle, nsY(I)).
nsY(I)	-= box(-[nrt(I),endcycle], nsY(I))
	   /\ box(endcycle, nsZ(I)).
nsZ(I)	+= box(-nrt(I), nsZ(I)) /\ diam(-nil, tt).

% at least one RT data transmission in each cycle
rtt	-= box(-nil, rtt) /\ box(startcycle, rttY).
rttY	+= box(endcycle, ff) /\ diam(-nil, tt)
	   /\ box(-rt(_), rttY).

% at least one NRT data in each cycle
nrt	-= box(-nil, nrt) /\ box(startcycle, nrtY).
nrtY	+= box(startcycle, ff) /\ diam(-nil, tt)
	   /\ box(-rt(_), nrtY).

% RT-first property
rtf	-= box(-nil, rtf)
	   /\ box([nrt(_)], rtfY).
rtfY	+= diam(-nil, tt) /\ box(-endcycle, rtfY)
	   /\ box([rt(_)], ff).