SPECIFICATION GameSpec
INVARIANT GameInvariant