Information Technology Reference
In-Depth Information
Fig. 1.
The GUI of the modified version of Infinite Mario Bros
threw (event
name
EnemyFireballDeath), the next event should indicate the
disappearance of the fireball so that it does not hit anything else.
G
(name = EnemyFireballDeath
→
X
name = FireballDisappear)
The presence of first-order quantifiers is necessary for two reasons: the same
parameter may occur multiple times in the same event (such as when multiple
enemy IDs are killed by Mario at the same time), and some gameplay properties
may affect a single element across multiple events, as in the following expression.
G
((name = Stomp
∧
isWinged = true)
→
∀
x
∈
id :
X
(id =
x
→
name
=EnemyDead))
In a normal playthrough, if Mario jumps on a flying enemy, it should lose
its wings. In this formula, we make sure that a winged enemy cannot die after
Mario stomps on it, as it should only stop flying. Since we are keeping the
corresponding
id
in a variable named
, we can check the next event related
to the
same
enemy to make sure it's respecting the normal flow of the game.
However, one can see that, for this correlation between object IDs to be possible,
first-order quantification on event parameters is necessary. As a matter of fact,
we discovered early on that
propositional
Linear Temporal Logic is not expressive
enough to represent but the simplest gameplay properties.
x
