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[NumProcess-1]' := election;
			init' := false;		
		relation: (messages[NumProcess-1]' = processes[0]);	
}


MODULE PROCESS(i: integer){

VAR

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

	TRANS RECEIVED_ELECTION_AND_I_AM_GREATER:
		enable: ((message_exist[i]=election)/\(messages[i]>processes[i]));
		assign: message_exist[i]' := no_message;
			message_exist[(i-1)%NumProcess]' := election;
		relation: (messages[(i-1)%NumProcess]' = messages[i]);

	TRANS RECEIVED_ELECTION_AND_I_AM_LESS:
		enable: ((message_exist[i]=election)/\(processes[i]>messages[i]));
		assign: message_exist[i]' := no_message;
			message_exist[(i-1)%NumProcess]' := election;
		relation: (messages[(i-1)%NumProcess]' = processes[i]);

	TRANS I_AM_THE_LEADER:
		enable: ((message_exist[i]=election)/\(processes[i]=messages[i]));
		assign: message_exist[i]' := no_message;
			message_exist[(i-1)%NumProcess]' := elected;
		relation: ((leader' = processes[i]) /\
		           (messages[(i-1)%NumProcess]' = processes[i]));
			

	TRANS RECEIVED_ELECTED_AND_I_AM_THE_LEADER:
		enable: ((message_exist[i]=elected)/\(processes[i]=messages[i]));
		assign: message_exist[i]' := no_message;
			message_exist[(i-1)%NumProcess]' := elected;
			messages[(i-1)%NumProcess]' := leader;

	TRANS RECEIVED_ELECTED_I_AM_NOT_THE_LEADER:
		enable: ((message_exist[i]=elected)/\(processes[i]!=messages[i]));
		assign: message_exist[i]' := no_message;
			
			message_exist[(i-1)%NumProcesses]' := elected;
		relation: ((messages[(i-1)%NumProcess]' = messages[i]) /\
			   (leader' = messages[i]));
}

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))

}