{
Estelle specification of the DeamonGame in a 'static' 
form, i.e., one GameMachine serves all N Players;
the body of the Players is included in the specification
}
specification DaemonGame;

default individual queue;

const NPlayers = 2;

channel PlayerMachine (Player, Machine);
by Player: Probe; Result; EndGame; NewGame;
by Machine: Win; Lose; Score(nwon: integer); Login;

module Player systemprocess;
ip G: PlayerMachine (Player);
end;

body PlayerBody for Player;

state INI, PLAY, WAITSCORE, WINLOSE;

initialize to INI
begin
end;

trans
from INI to PLAY
when G.Login
name send_NewGame:
begin
output G.NewGame
end;

from PLAY to INI
name send_EndGame:
begin
output G.EndGame
end;

from PLAY to WINLOSE
name send_Probe:
begin
output G.Probe
end;

from WINLOSE to PLAY
when G.Win
begin 
end;

when G.Lose
begin 
end;

from PLAY to WAITSCORE
name send_Result:
begin
output G.Result
end;

from WAITSCORE to PLAY
when G.Score
begin 
end;

end; {PlayerBody}

module GameMachine systemprocess;
ip M: array [1..NPlayers ] of PlayerMachine (Machine);
end;

body MachineBody for GameMachine;

state ODD, EVEN, LOG;
stateset EITHER = [ODD,EVEN];
var x: boolean;
scores: array [1..NPlayers ] of integer;

initialize
to LOG
var i: integer;
begin
for i:=1 to NPlayers do
scores[i] := 0;
x := true
end;

trans
from LOG to ODD
var i:integer;
name distr_Login:
begin
for i:=1 to NPlayers do output M[i].Login;
end;

from EITHER
to same
any j: 1..NPlayers do
when M[j].NewGame
begin
end;

when M[j].EndGame
name send_EndLogin:
begin
output M[j].Login;
scores[j] := 0
end;

when M[j].Probe
name send_Win_Lose:
begin
if x then
begin
output M[j].Win;
scores[j] := scores[j]+1
end
else
begin
output M[j].Lose;
scores[j] := scores[j]-1
end
end;

when M[j].Result
name send_Score:
begin
output M[j].Score(scores[j]);
end;

from ODD to EVEN
name odd_even:
begin 
x := not x
end;

from EVEN to ODD 
name even_odd:
begin 
x := not x
end;

end; {MachineBody}

modvar 
Pinst: array[1..NPlayers] of Player;
Ginst: GameMachine;
initialize
var i: integer;
begin
init Ginst with MachineBody;
for i:=1 to NPlayers do
begin 
init Pinst[i] with PlayerBody;
connect Pinst[i].G to Ginst.M[i]
end
end;
end. {specification DaemonGame}