# There is always at least one ball in play.
AG((player_A.state=BALL) + (player_B.state=BALL));

# If player_A is not hitting the ball right now, then he will sometime
# in the future.
#AG((ping_pong.player_A.me=NO_HIT) => AF(ping_pong.player_A.me=HIT));
# this formula is not consistant with a Kripke structure.

# Eventually, only one ball is in play.
AF((player_A.state=BALL) ^ (player_B.state=BALL));