------------------ MODULE GenericGame -----------------
EXTENDS Game 
-------------------------------------------------------
GenericGameInit == winner = "?"

GenericGamePlay == /\ winner = "?"
                   /\ UNCHANGED winner

GenericGameWinner == /\ winner = "?"
                     /\ winner' \in {"me", "you"}
                
GenericGameNext == GenericGamePlay \/ GenericGameWinner 
-------------------------------------------------------
GenericGameSpec == GenericGameInit /\ [][GenericGameNext]_<<winner>>

THEOREM GameSpec => GenericGameSpec

=======================================================