Module System

type message_state = {election,elected,no_message}
macro NumProcess = 5
local processes : array [0..-1] of int 
local messages : array [0..-1] of int 
local message_exist : array [0..-1] of message_state where Forall i:[0..-1] . (message_exist[i] = no_message)


Module INIT_ELECTION :
local init : bool where init = true


Transition INIT NoFairness:
enable init=true
assign message_exist[NumProcess-1] := election,init := false
modrel (messages[NumProcess-1]'=processes[0])
EndModule


Module PROCESS :
external out i : int 
local leader : int where leader = -1


Transition RECEIVED_ELECTION_AND_I_AM_GREATER NoFairness:
enable ((message_exist[i]=election)/\(messages[i]>processes[i]))
assign message_exist[i] := no_message,message_exist[(i-1) mod NumProcess] := election
modrel (messages[(i-1) mod NumProcess]'=messages[i])

Transition RECEIVED_ELECTION_AND_I_AM_LESS NoFairness:
enable ((message_exist[i]=election)/\(processes[i]>messages[i]))
assign message_exist[i] := no_message,message_exist[(i-1) mod NumProcess] := election
modrel (messages[(i-1) mod NumProcess]'=processes[i])

Transition I_AM_THE_LEADER NoFairness:
enable ((message_exist[i]=election)/\(processes[i]=messages[i]))
assign message_exist[i] := no_message,message_exist[(i-1) mod NumProcess] := elected
modrel ((leader'=processes[i])/\(messages[(i-1) mod NumProcess]'=processes[i]))

Transition RECEIVED_ELECTED_AND_I_AM_THE_LEADER NoFairness:
enable ((message_exist[i]=elected)/\(processes[i]=messages[i]))
assign message_exist[i] := no_message,message_exist[(i-1) mod NumProcess] := elected,messages[(i-1) mod NumProcess] := leader

Transition RECEIVED_ELECTED_I_AM_NOT_THE_LEADER NoFairness:
enable ((message_exist[i]=elected)/\(processes[i]!=messages[i]))
assign message_exist[i] := no_message,message_exist[(i-1) mod NumProcesses] := elected
modrel ((messages[(i-1) mod NumProcess]'=messages[i])/\(leader'=messages[i]))
EndModule


Module SYSTEM :
local proc1 : int where proc1 = 0
local proc2 : int where proc2 = 1
local proc3 : int where proc3 = 2
local proc4 : int where proc4 = 3
local proc5 : int where proc5 = 4

include INIT_ELECTION : ( INIT_ELECTION )
 || PROCESS : ( PROCESS where out i = proc1)
 || PROCESS : ( PROCESS where out i = proc2)
 || PROCESS : ( PROCESS where out i = proc3)
 || PROCESS : ( PROCESS where out i = proc4)
 || PROCESS : ( PROCESS where out i = proc5)
EndModule