%% $Id: model.utf8,v 1.1 2007/08/02 10:30:07 alimanfoo Exp $
@begin@

= Formal Specification: conception.games.swat =

The Simple Word Association Test (SWAT) is a game played individually, where a word or phrase is presented to the player as a ''stimulus'', and the player responds with one or more words or phrases.

This document is a formal specification of this game.

== Types ==

Given the set of character strings.

─ [ STRING ] 


A SWAT game is divided into a number of rounds. Each round begins with a single stimulus and captures a sequence of responses to that stimulus. The same response cannot be repeated. A response cannot be the same as a stimulus.

┌ SwatGameRound
  stimulus : STRING
  responses : iseq STRING
|
  stimulus ∉ ran responses


A SWAT game can be at one of three stages, either pending, playing or over. 

─
  GameStage ::= pending | playing | over


During play, there is a current round in progress, and a sequence of completed rounds. All stimuli are strings drawn from a common, non-empty source.

There may be more than one source of stimuli available for use in any one game. The stimulus source must be chosen prior to the start of the game, and is fixed once the game has started.

┌ SwatGame
  stage : GameStage
  stimuli : â„™ STRING
  currentRound : SwatGameRound
  completedRounds : seq SwatGameRound
|
  stimuli ≠ ∅


== Safe Operations ==

These operations do not change the state of the game.

Return the current game stage.

┌ getGameStage
  ΞSwatGame
  stage! : GameStage
|
  stage! = stage


Return the current game round.

┌ getCurrentRound
  ΞSwatGame
  round! : SwatGameRound
|
  round! = currentRound


Return all completed rounds.

┌ getCompletedRounds
  ΞSwatGame
  rounds! : seq SwatGameRound
|
  rounds! = completedRounds


== Operations with Side-Effects ==

These operations may change the state of the game.

Start the game.

┌ startGame
  ΔSwatGame
|
  stage = pending
  stage′ = playing


End the game.

┌ gameOver
  ΔSwatGame
|
  stage = playing
  stage′ = over
  completedRounds′ = completedRounds ⁀ ⟨ currentRound ⟩


Request a new stimulus (start a new round of the game).

┌ stimulate
  ΔSwatGame
  stimulus! : STRING
|
  stimulus! ∈ stimuli
  completedRounds′ = completedRounds ⁀ ⟨ currentRound ⟩
  currentRound′.stimulus = stimulus!
  currentRound′.responses = ⟨ ⟩


Respond to a stimulus.

┌ respond
  ΔSwatGame
  response? : STRING
|
  currentRound′.responses = currentRound.responses ⁀ ⟨ response? ⟩


----
$Revision: 1.1 $
  
@end@
%% $Log: model.utf8,v $
%% Revision 1.1  2007/08/02 10:30:07  alimanfoo
%% Moved from components, simplified (removed set of all sources, assume handle elsewhere).
%%
%% Revision 1.1  2007/07/23 09:47:57  alimanfoo
%% Initial, moved content from separate project.
%%