%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%	XSB/LMC Code for Leader Election Protocol:
%%		Dolev, Klawe, Rodeh,
%%		Adapted from SPIN test suite by Y.S.R., 19 Dec 96.
%%		Parameterized wrt size of ring and buffer size by C.R., Aug 98.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%=============================================================================
%%	the node process involved in electing a leader

%% one node.  N is the number of nodes in the network
node(N, Id) ::=
	out(right, first(Id)) o 
	nodeActive(N, Id, _Nbr).

nodeActive(N, Maxi, Nbr) ::=
	in(left, first(NId)) o
	if(NId \== Maxi
		, out(right, second(NId)) o
		  nodeActive(N, Maxi, NId)
		, if( Maxi is N-1
			, action(leader) o
			  nodeActive(N, Maxi, NId)
			, action(fail) o end
		  )
	)
    #
	in(left, second(NId)) o
	if((Nbr > NId, Nbr > Maxi)
		, out(right, first(Nbr)) o
		  nodeActive(N, Nbr, Nbr)
		, nodeInactive
	).

nodeInactive ::=
	in(left, Msg) o 
	out(right, Msg) o 
	nodeInactive.

%%=============================================================================
%%	A size-N buffer
:- import length/2 from basics.

chan(N, Buf) ::=
	length(Buf, Len) o
	(
		Len < N o
		in(chan_in, Msg) o
		chan(N, [Msg|Buf])
	#
		Len > 0 o
		strip_from_end(Buf, Msg, NewBuf) o
		out(chan_out, Msg) o 
		chan(N, NewBuf)
	).

strip_from_end([X], X, []).
strip_from_end([X,Y|Ys], Z, [X|Zs]) :- strip_from_end([Y|Ys], Z, Zs).

%%-----------------------------------------------------------------------------
%%	instantiated system specifications

leader3 ::=
	( node(3,2) @ [left/left(0), right/right(0)]
	| node(3,1) @ [left/left(1), right/right(1)]
	| node(3,0) @ [left/left(2), right/right(2)]
	| chan(6,[]) @ [chan_in/right(0), chan_out/left(1)]
	| chan(6,[]) @ [chan_in/right(1), chan_out/left(2)]
	| chan(6,[]) @ [chan_in/right(2), chan_out/left(0)]
	) \ {snd(_), left(_), right(_)}.

leader4 ::=
	( node(4,3) @ [left/left(0), right/right(0)]
	| node(4,2) @ [left/left(1), right/right(1)]
	| node(4,1) @ [left/left(2), right/right(2)]
	| node(4,0) @ [left/left(3), right/right(3)]
	| chan(8,[]) @ [chan_in/right(0), chan_out/left(1)]
	| chan(8,[]) @ [chan_in/right(1), chan_out/left(2)]
	| chan(8,[]) @ [chan_in/right(2), chan_out/left(3)]
	| chan(8,[]) @ [chan_in/right(3), chan_out/left(0)]
	) \ {snd(_), left(_), right(_)}.

leader5 ::=
	( node(5,4) @ [left/left(0), right/right(0)]
	| node(5,3) @ [left/left(1), right/right(1)]
	| node(5,2) @ [left/left(2), right/right(2)]
	| node(5,1) @ [left/left(3), right/right(3)]
	| node(5,0) @ [left/left(4), right/right(4)]
	| chan(10,[]) @ [chan_in/right(0), chan_out/left(1)]
	| chan(10,[]) @ [chan_in/right(1), chan_out/left(2)]
	| chan(10,[]) @ [chan_in/right(2), chan_out/left(3)]
	| chan(10,[]) @ [chan_in/right(3), chan_out/left(4)]
	| chan(10,[]) @ [chan_in/right(4), chan_out/left(0)]
	) \ {snd(_), left(_), right(_)}.

leader6 ::=
	( node(6,5) @ [left/left(0), right/right(0)]
	| node(6,4) @ [left/left(1), right/right(1)]
	| node(6,3) @ [left/left(2), right/right(2)]
	| node(6,2) @ [left/left(3), right/right(3)]
	| node(6,1) @ [left/left(4), right/right(4)]
	| node(6,0) @ [left/left(5), right/right(5)]
	| chan(12,[]) @ [chan_in/right(0), chan_out/left(1)]
	| chan(12,[]) @ [chan_in/right(1), chan_out/left(2)]
	| chan(12,[]) @ [chan_in/right(2), chan_out/left(3)]
	| chan(12,[]) @ [chan_in/right(3), chan_out/left(4)]
	| chan(12,[]) @ [chan_in/right(4), chan_out/left(5)]
	| chan(12,[]) @ [chan_in/right(5), chan_out/left(0)]
	) \ {snd(_), left(_), right(_)}.

leader7 ::=
	( node(7,6) @ [left/left(0), right/right(0)]
	| node(7,5) @ [left/left(1), right/right(1)]
	| node(7,4) @ [left/left(2), right/right(2)]
	| node(7,3) @ [left/left(3), right/right(3)]
	| node(7,2) @ [left/left(4), right/right(4)]
	| node(7,1) @ [left/left(5), right/right(5)]
	| node(7,0) @ [left/left(6), right/right(6)]
	| chan(14,[]) @ [chan_in/right(0), chan_out/left(1)]
	| chan(14,[]) @ [chan_in/right(1), chan_out/left(2)]
	| chan(14,[]) @ [chan_in/right(2), chan_out/left(3)]
	| chan(14,[]) @ [chan_in/right(3), chan_out/left(4)]
	| chan(14,[]) @ [chan_in/right(4), chan_out/left(5)]
	| chan(14,[]) @ [chan_in/right(5), chan_out/left(6)]
	| chan(14,[]) @ [chan_in/right(6), chan_out/left(0)]
	) \ {snd(_), left(_), right(_)}.

%%=============================================================================
%%	Properties

ae_leader += diam(-nil, tt) /\ box(-leader, ae_leader).
ee_fail += diam(fail, tt) \/ diam(-nil, ee_fail).

one_leader += box(-leader, one_leader) /\ box(leader, no_leader).
no_leader -= box(leader, ff) /\ box(-nil, no_leader).

aa_true -= box(fail, ff) /\ box(-nil, aa_true).
aa_leader -= diam(-nil, tt) /\ box(-leader, aa_leader).