%% $Id: model.utf8,v 1.1 2007/08/02 08:49:46 alimanfoo Exp $
@begin@

= Formal Specification: conception.games.host =

A game host provides a virtual space within which players can play games of different types. 

== Types ==

Given as basic types the set of game types.

─ [ GAMETYPE ] 


A game can be in one of three basic stages.

─
  GameStage ::= pending | playing | over


Each game has a unique number, a game type and a stage.

┌ Game
  number : ℤ
  type : GAMETYPE
  stage : GameStage
|
  number > 0


A game host reception has a set of supported game types, a set of existing games and a number to allocate to the next requested new game.

┌ GameHost
  supported : â„™ GAMETYPE
  games : â„™ Game
  nextGameNumber : ℤ
|
  ∀ g : games ⦁ g.type ∈ supported
  ∀ x, y : games ⦁ x.number ≠ y.number
  nextGameNumber = max ( { g : games ⦁ g.number } ) + 1


== Safe Operations ==

Request the list of supported game types.

┌ getSupportedGames
  ΞGameHost
  supported! : â„™ GAMETYPE
|
  supported! = supported


== Operations with Side-Effects ==

Request a new game.

┌ newGame
  ΔGameHost
  gameType? : GAMETYPE
  number! : ℤ
|
  gameType? ∈ supported
  number! = nextGameNumber
  nextGameNumber′ = nextGameNumber + 1
  games′ = games ∪ { ⦉ number == nextGameNumber, type == gameType?, stage == pending ⦊ }


----
$Revision: 1.1 $
  
@end@
%% $Log: model.utf8,v $
%% Revision 1.1  2007/08/02 08:49:46  alimanfoo
%% Refactored, moved from reception in components. Revised definitions.
%%
%% Revision 1.3  2007/07/23 09:38:42  alimanfoo
%% Change main type name to "reception". Minor tag changes.
%%
%% Revision 1.2  2007/07/23 09:02:54  alimanfoo
%% Minor mods, for style, and heading changes.
%%
%% Revision 1.1  2007/07/20 16:39:04  alimanfoo
%% Initial, moved from separate project.
%%