Merge pull request #1479 from informalsystems/new-example

Add rock-paper-scissors game example

examples/README.md

@@ -74,6 +74,7 @@ listed without any additional command line arguments.
 | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cryptography/hashes.qnt](./cryptography/hashes.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cryptography/hashesTest.qnt](./cryptography/hashesTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [games/rock_paper_scissors/play_rock_paper_scissors.qnt](./games/rock_paper_scissors/play_rock_paper_scissors.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [games/secret-santa/secret_santa.qnt](./games/secret-santa/secret_santa.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [games/tictactoe/tictactoe.qnt](./games/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/games/rock_paper_scissors/README.md

@@ -0,0 +1,75 @@
+# Rock-Paper-Scissors Game Module
+
+This project implements a simple Rock-Paper-Scissors game, allowing two players to randomly select moves and determine the winner based on the traditional rules of the game.
+
+## Overview
+
+The `rock_paper_scissors` module provides the core functionality for the game, including:
+
+- **Player Setup:** Constants for player names.
+- **Game Logic:** Actions to decide player moves, determine the winner, and reset the game.
+- **Invariant Checking:** Ensures the game status reflects the expected winner based on the rules.
+
+The `play_rock_paper_scissors` module demonstrates how to import and use the `rock_paper_scissors` module with specific player names.
+
+## Components
+
+### Module: `rock_paper_scissors`
+
+This is the main module where the game logic resides.
+
+- **Constants:**
+  - `PLAYER1`: Name of the first player.
+  - `PLAYER2`: Name of the second player.
+
+- **Types:**
+  - `Move`: Enum representing possible moves: `Init`, `Rock`, `Paper`, `Scissors`.
+  - `GameStatus`: Enum representing the status of the game: `Started`, `Pending`, `Draw`, `Winner(str)`.
+
+- **Variables:**
+  - `p1State`: Current move of Player 1.
+  - `p2State`: Current move of Player 2.
+  - `status`: Current status of the game.
+
+- **Functions:**
+  - `beats(m1: Move, m2: Move): bool`: Determines if `m1` beats `m2` based on Rock-Paper-Scissors rules.
+
+- **Actions:**
+  - `init`: Initializes the game with both players in `Init` state and the game status as `Started`.
+  - `decide_moves`: Randomly selects moves for both players from the set of possible moves (`Rock`, `Paper`, `Scissors`) and updates the game status to `Pending`.
+  - `find_winner`: Determines the winner based on the players' moves and updates the game status to `Winner(PLAYER1)`, `Winner(PLAYER2)`, or `Draw`.
+  - `step`: The main game loop that progresses the game through different states (`Started`, `Pending`, etc.) and resets the game for a new round.
+
+- **Invariants:**
+  - `winInv`: Ensures the game status matches the expected winner based on the rules of Rock-Paper-Scissors.
+
+### Module: `play_rock_paper_scissors`
+
+This module imports the `rock_paper_scissors` module and assigns the player names:
+
+```bluespec
+import rock_paper_scissor(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*
+```
+
+## How It Works
+
+1.  **Initialization:**
+    - The game starts with both players in the Init state, and the game status is set to Started.
+
+2.  **Move Decision:**
+    - The `decide_moves` action randomly selects a move for each player and updates the game status to Pending.
+
+3.  **Determine Winner:**
+    - The `find_winner` action evaluates the moves and determines the winner or declares a draw.
+
+4.  **Game Progression:**
+    - The step action orchestrates the progression of the game from initialization to move decision, winner determination, and resetting for a new round.
+
+5.  **Invariant Checking:**
+    - The winInv invariant ensures that the game status correctly reflects the outcome of the moves.
+
+## Usage
+-  To run the spec, import the `rock_paper_scissors` module and specify the player names as shown in the `play_rock_paper_scissors` module.
+
+-  Run using the command:
+    - `quint run play_rock_paper_scissors.qnt --invariant=winInv`

examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt

@@ -0,0 +1,66 @@
+// -*- mode: Bluespec; -*-
+
+module rock_paper_scissors {
+    // Constants for player names
+    const PLAYER1 : str
+    const PLAYER2 : str
+    // Sum types for the possible moves and game status
+    type Move = Init | Rock | Paper | Scissors
+    type GameStatus = Started | Pending | Draw | Winner(str)
+    // Variables to hold the current state of each player's move and the game status
+    var p1State: Move
+    var p2State: Move
+    var status: GameStatus
+
+    def beats(m1: Move, m2: Move): bool = or {
+        (m1 == Rock and m2 == Scissors),
+        (m1 == Paper and m2 == Rock),
+        (m1 == Scissors and m2 == Paper),
+    }
+    /// Initialize the game with both players in 'Init' state and game status as 'Started'
+    action init = all {
+        p1State' = Init,
+        p2State' = Init,
+        status' = Started
+    }
+
+    /// Randomly decide moves for both players from the set of possible moves
+    action decide_moves = {
+        nondet move1 = Set(Rock, Paper, Scissors).oneOf() // Non-deterministically pick a move for player 1
+        nondet move2 = Set(Rock, Paper, Scissors).oneOf() // Non-deterministically pick a move for player 2
+        all {
+            p1State' = move1,
+            p2State' = move2,
+            status' = Pending,
+        }
+    }
+
+    /// Determine the winner based on the current moves of both players
+    action find_winner = any {
+        if (beats(p1State, p2State)) status' = Winner(PLAYER1) // Player 1 wins if their move beats player 2's move
+        else if (beats(p2State, p1State)) status' = Winner(PLAYER2) // Player 2 wins if their move beats player 1's move
+        else status' = Draw // It's a draw if both players chose the same move
+    }
+
+    action step = if (status == Started) {
+        decide_moves
+    } else if (status == Pending) all {
+        p1State' = p1State,
+        p2State' = p2State,
+        find_winner,
+    }  else all {
+        p1State' = Init,
+        p2State' = Init,
+        status' = Started
+    }
+
+    /// Invariant to check if the game status matches the expected winner
+    val winInv = and {
+        status == Winner(PLAYER1) implies beats(p1State, p2State),
+        status == Winner(PLAYER2) implies beats(p2State, p1State),
+    }
+}
+
+module play_rock_paper_scissors {
+    import rock_paper_scissors(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*
+}