HOLD_PREVIOUS

TYPE

message_state: ENUM {election , elected , no_message};

CONST

NumProcess: 5;

VAR

processes: ARRAY[NumProcess] OF integer; -- i is the i'th process
messages: ARRAY[NumProcess] OF integer; -- i is the i'th process channel
message_exist: ARRAY[NumProcess] OF message_state INITVAL no_message;


MODULE INIT_ELECTION(){

VAR

init: boolean INITVAL true;

	TRANS INIT: -- process 0 sends message to process 1
		enable: init = true;
		assign: message_exist[4]' := election;
			init' := false;		
		relation: (messages[4]' = processes[0]);	
}


MODULE PROCESS(i: integer){

VAR

leader: integer INITVAL -1; -- -1 means that nobody is leader

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER_1:
		enable: ((message_exist[1]=election)/\(messages[1]>processes[1]));
		assign: message_exist[1]' := no_message;
			message_exist[0]' := election;
		relation: (messages[0]' = messages[1]);

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER_2:
		enable: ((message_exist[2]=election)/\(messages[2]>processes[2]));
		assign: message_exist[2]' := no_message;
			message_exist[1]' := election;
		relation: (messages[1]' = messages[2]);

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER_3:
		enable: ((message_exist[3]=election)/\(messages[3]>processes[3]));
		assign: message_exist[3]' := no_message;
			message_exist[2]' := election;
		relation: (messages[2]' = messages[3]);

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER_4:
		enable: ((message_exist[4]=election)/\(messages[4]>processes[4]));
		assign: message_exist[4]' := no_message;
			message_exist[3]' := election;
		relation: (messages[3]' = messages[4]);

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER_0:
		enable: ((message_exist[0]=election)/\(messages[0]>processes[0]));
		assign: message_exist[0]' := no_message;
			message_exist[4]' := election;
		relation: (messages[4]' = messages[0]);


	TRANS RECEIVED_ELECTION_AND_I_AM_LESS_1:
		enable: ((message_exist[1]=election)/\(processes[1]>messages[1]));
		assign: message_exist[1]' := no_message;
			message_exist[0]' := election;
		relation: (messages[0]' = processes[1]);

	TRANS RECEIVED_ELECTION_AND_I_AM_LESS_2:
		enable: ((message_exist[2]=election)/\(processes[2]>messages[2]));
		assign: message_exist[2]' := no_message;
			message_exist[1]' := election;
		relation: (messages[1]' = processes[2]);

	TRANS RECEIVED_ELECTION_AND_I_AM_LESS_3:
		enable: ((message_exist[3]=election)/\(processes[3]>messages[3]));
		assign: message_exist[3]' := no_message;
			message_exist[2]' := election;
		relation: (messages[2]' = processes[3]);

	TRANS RECEIVED_ELECTION_AND_I_AM_LESS_4:
		enable: ((message_exist[4]=election)/\(processes[4]>messages[4]));
		assign: message_exist[4]' := no_message;
			message_exist[3]' := election;
		relation: (messages[3]' = processes[4]);

	TRANS RECEIVED_ELECTION_AND_I_AM_LESS_0:
		enable: ((message_exist[0]=election)/\(processes[0]>messages[0]));
		assign: message_exist[0]' := no_message;
			message_exist[4]' := election;
		relation: (messages[4]' = processes[0]);

	TRANS I_AM_THE_LEADER_1:
		enable: ((message_exist[1]=election)/\(processes[1]=messages[1]));
		assign: message_exist[1]' := no_message;
			message_exist[0]' := elected;
		relation: ((leader' = processes[1]) /\
		           (messages[0]' = processes[1]));

	TRANS I_AM_THE_LEADER_2:
		enable: ((message_exist[2]=election)/\(processes[2]=messages[2]));
		assign: message_exist[2]' := no_message;
			message_exist[1]' := elected;
		relation: ((leader' = processes[2]) /\
		           (messages[1]' = processes[2]));

	TRANS I_AM_THE_LEADER_3:
		enable: ((message_exist[3]=election)/\(processes[3]=messages[3]));
		assign: message_exist[3]' := no_message;
			message_exist[2]' := elected;
		relation: ((leader' = processes[3]) /\
		           (messages[2]' = processes[3]));

	TRANS I_AM_THE_LEADER_4:
		enable: ((message_exist[4]=election)/\(processes[4]=messages[4]));
		assign: message_exist[4]' := no_message;
			message_exist[3]' := elected;
		relation: ((leader' = processes[4]) /\
		           (messages[3]' = processes[4]));

	TRANS I_AM_THE_LEADER_0:
		enable: ((message_exist[0]=election)/\(processes[0]=messages[0]));
		assign: message_exist[0]' := no_message;
			message_exist[4]' := elected;
		relation: ((leader' = processes[0]) /\
		           (messages[4]' = processes[0]));
			

	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER_1:
		enable: ((message_exist[1]=elected)/\(processes[1]=messages[1]));
		assign: message_exist[1]' := no_message;
			message_exist[0]' := elected;
			messages[0]' := leader;

	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER_2:
		enable: ((message_exist[2]=elected)/\(processes[2]=messages[2]));
		assign: message_exist[2]' := no_message;
			message_exist[1]' := elected;
			messages[1]' := leader;


	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER_3:
		enable: ((message_exist[3]=elected)/\(processes[3]=messages[3]));
		assign: message_exist[3]' := no_message;
			message_exist[2]' := elected;
			messages[2]' := leader;

	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER_4:
		enable: ((message_exist[4]=elected)/\(processes[4]=messages[4]));
		assign: message_exist[4]' := no_message;
			message_exist[3]' := elected;
			messages[3]' := leader;

	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER_0:
		enable: ((message_exist[0]=elected)/\(processes[0]=messages[0]));
		assign: message_exist[0]' := no_message;
			message_exist[4]' := elected;
			messages[4]' := leader;


	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_1:
		enable: ((message_exist[1]=elected)/\(processes[1]!=messages[1]));
		assign: message_exist[1]' := no_message;
			message_exist[0]' := elected;
		relation: ((messages[0]' = messages[1]) /\
			   (leader' = messages[1]));

	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_2:
		enable: ((message_exist[2]=elected)/\(processes[2]!=messages[2]));
		assign: message_exist[2]' := no_message;
			message_exist[1]' := elected;
		relation: ((messages[1]' = messages[2]) /\
			   (leader' = messages[2]));

	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_3:
		enable: ((message_exist[3]=elected)/\(processes[3]!=messages[3]));
		assign: message_exist[3]' := no_message;
			message_exist[2]' := elected;
		relation: ((messages[2]' = messages[3]) /\
			   (leader' = messages[3]));


	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_4:
		enable: ((message_exist[4]=elected)/\(processes[4]!=messages[4]));
		assign: message_exist[4]' := no_message;
			message_exist[3]' := elected;
		relation: ((messages[3]' = messages[4]) /\
			   (leader' = messages[4]));

	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER_0:
		enable: ((message_exist[0]=elected)/\(processes[0]!=messages[0]));
		assign: message_exist[0]' := no_message;
			message_exist[4]' := elected;
		relation: ((messages[4]' = messages[0]) /\
			   (leader' = messages[0]));

}

MODULE SYSTEM(){

VAR

proc1: integer INITVAL 0;
proc2: integer INITVAL 1;
proc3: integer INITVAL 2;
proc4: integer INITVAL 3;
proc5: integer INITVAL 4;

	

	
(((((INIT_ELECTION()|||PROCESS(proc1))|||PROCESS(proc2))|||PROCESS(proc3))|||PROCESS(proc4))|||PROCESS(proc5))

}