{
Estelle specification of the DeamonGame in a 'dynamic' 
form, i.e., a GameMachine is created (by Server) each time a Player
wants to play a new game (the Player sends NewGame message)
and the GameMachine is removed when the Player ends the game;
the body of the Players is not included in the specification
(it is the same as in the DeamonGame 'static' specification)
}
specification DaemonGame;

default individual queue;

const NPlayers = any integer;

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

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

body PlayerBody for Player;
external; {PlayerBody}

module Server systemprocess;
ip M: array [1..NPlayers ] of PlayerMachine (Machine);
end;
body ServerBody for Server;

module GameMachine activity;
ip M : PlayerMachine (Machine);
export E : boolean;
end;

body MachineBody for GameMachine

state ODD, EVEN;
stateset EITHER = [ODD,EVEN];
var x: boolean;
scor: integer;

initialize
to ODD
begin
scor := 0;
x := true;
E := false;
end;

trans
from EITHER
to same
when M.EndGame
begin
E := true;
scor := 0
end;

when M.Probe
begin
if x then
begin
output M.Win;
scor := scor+1
end
else
begin
output M.Lose;
scor := scor-1
end;

when M.Result
begin
output M.Score(scor);
end;

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

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

end; {MachineBody}

modvar
Ginst: array[1..NPlayers] of GameMachine;

initialize
i: integer;
begin
for i:=1 to NPlayers do
output M[i].Login;
end;

trans
any j: 1..NPlayers;
when M[j].NewGame
begin
init Ginst[j] with GameMachine;
attach M[j] to Ginst[j].M
end;
any j=1..NPlayers
provided Ginst[j].E
begin 
terminate Ginst[j];
output M[j].Login
end;
end; {ServerBody}

modvar 
Pinst: array[1..NPlayers] of Player;
Sinst: Server;

initialize
i: integer;
begin
for i=1 to NPlayers do
begin 
init Pinst[i] with PlayerBody;
init Sinst with ServerBody
connect Pinst[i].G to Sinst.M[i]
end;
end. {specification DaemonGame}