Software abstraction plays an important role in both requirements engineering and software design. It facilitates the principle of separate of concerns while opening the door for software automation. This paper revisits the notion of software abstraction made for casual games where a single player accumulates her points by performing game activities under a set of rules. We propose to make software abstraction in Alloy - a lightweight, declarative language that is semantically based on first-order logic and syntactically being object-oriented. We show that casual games can be conceptually abstracted and semantically represented in Alloy. More specifically, game concepts (e.g., the main player, gold mine) are represented under Alloy signatures while game rules (e.g., game over, score upped/downed) as Alloy fact. To precisely specify game rules and make them simulatable, we need a mechanism for querying and updating the states of game concepts at different moments during the course of the game. To this end, we employ temporal modeling in making software abstraction for casual games.