Merge branch 'main' into gabriela/bump-apalache

examples/README.md

@@ -75,6 +75,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/mafia_werewolf/play_mafia.qnt](./games/mafia_werewolf/play_mafia.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [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: |

examples/games/mafia_werewolf/README.md

@@ -0,0 +1,71 @@
+# Overview
+
+This is an implementation of the Mafia party game, where players are secretly assigned roles (Mafia or Citizen) and must either work together or against each other to win. The game alternates between two phases: Day and Night. During the day, players vote to eliminate suspected Mafia members, and at night, the Mafia secretly kills a Citizen. The game continues until either all Citizens or all Mafia members are eliminated
+
+# Objective
+
+- **Mafia:** Eliminate all Citizens.
+- **Citizen:** Identify and eliminate all Mafia.
+
+# Components
+
+## Types:
+
+-   **Role:** Each player is either a `Mafia` or a `Citizen`.
+-   **LifeState:** Represents whether a player is `Alive` or `Dead`.
+-   **Phase:** The game alternates between `Day` and `Night` phases.
+-   **PlayerFeatures:** The structure stores key data about a player, including their role, life status, and whether they have voted.
+
+## Variables:
+
+-   **players_to_features:** A map from player names to their respective `PlayerFeatures`.
+-   **votes_by_player:** Tracks the votes each player has received.
+-   **game_phase:** Indicates whether it's currently `Day` or `Night`.
+-   **game_status:** Indicates whether the game is `Pending` or if a specific role has won.
+
+## Game Status:
+
+-   The game continues until all players from one of the roles (Mafia or Citizen) are dead.
+
+-   The game can be in one of three states:
+    -   **Pending:** The game is still ongoing.
+    -   **Done(Role):** The game is finished, and the `Role` represents the winning team (either Mafia or Citizens).
+
+
+# How It Works:
+
+## Initial Setup:
+
+The game starts in the `Night` phase. Players are randomly assigned as either `Mafia` or `Citizen`, and their status is set to `Alive`. Votes are also initialized to zero. 
+Note: A game should consist of both `Mafia` and `Citizen` to be valid.
+
+
+## Game Phases:
+
+1.  **Night Phase:** During this phase, a Mafia selects a Citizen to kill.
+2.  **Day Phase:** During this phase, all players(Citizens and Mafia) vote to hang one player based on suspicion. The player with maximum votes will be eliminated from the game. In case of a tie in votes for two or more players, nothing happens and the game moves on.
+
+## Actions:
+
+-   **Mafia Kills:** The Mafia can kill one Citizen during the night.
+-   **Vote:** During the day, all living players vote to hang a player.
+-   **Hang:** The player with the most votes is hung.
+-   **Tie:** If there is a tie in the vote, no one is hung, and the game proceeds to the next night phase.
+
+## Winning Conditions:
+
+-   **Mafia Wins:** If all Citizens are dead.
+-   **Citizen Wins:** If all Mafia are dead.
+
+## Special Features:
+
+-   **Voting System:** Each player can vote once per day to hang a player. If all votes are tied, no player is eliminated.
+-   **Status Check:** The game constantly checks if all Mafia or Citizen players are dead to determine if the game should end.
+
+## Usage:
+
+-   **Initializing the Game:** Import the `mafia` module and specify the desired amount of players participating in the game. Roles will be randomly assigned.
+
+-   **Running the Game:**
+    - `quint run play_mafia.qnt`
+

examples/games/mafia_werewolf/play_mafia.qnt

@@ -0,0 +1,195 @@
+// -*- mode: Bluespec; -*-
+/**
+ * Mafia, also called Werewolf, is a party game to enjoy your gathering!
+ *
+ * To get more familiar with the game and rules check this link:
+ * https://en.wikipedia.org/wiki/Mafia_(party_game)
+ *
+ * For more information on the implementation and details of the code check this:
+ * https://github.com/informalsystems/quint/blob/main/examples/games/mafia_werewolf/README.md
+
+ * Mahtab Norouzi, Informal Systems, 2024
+ */
+
+module mafia {
+    import basicSpells.* from "../../spells/basicSpells"
+
+    const PLAYERS : Set[str]
+    // Types for roles and life states of players
+    type Role = Mafia | Citizen
+    type LifeState = Alive | Dead
+    type Phase = Day | Night
+    type PlayerFeatures = {
+        name: str,
+        role: Role,
+        status: LifeState,
+        voted: bool  // Indicates whether the player has voted
+    }
+
+    var players_to_features: str -> PlayerFeatures
+    var votes_by_player: str -> int
+    var game_phase: Phase
+
+    type Status = Pending | Done(Role)
+    var game_status: Status
+
+    /// Check if all live players have voted
+    val all_voted = players_to_features.values().filter(p => p.status == Alive).forall(p => p.voted == true)
+
+    /// Check if there are any Mafia players
+    val has_alive_mafia = players_to_features.values().exists(p => p.role == Mafia and p.status == Alive)
+
+    /// Check if there are any Citizen players
+    val has_alive_citizen = players_to_features.values().exists(p => p.role == Citizen and p.status == Alive)
+
+    /// Find players with the most votes if all players have voted
+    val get_most_voted_players = {
+        if (all_voted) {
+            val max_votes = PLAYERS.fold(-1, (acc, p) => {
+                val votes = votes_by_player.get(p)
+                if (votes > acc) votes else acc
+            })
+            PLAYERS.filter(p => votes_by_player.get(p) == max_votes)
+        } else Set()  // Return an empty set if not all players have voted
+    }
+
+    /// Check if all Mafia players are dead
+    pure def all_mafias_dead(players: str -> PlayerFeatures): bool = {
+        players.values().forall(p => p.role == Mafia implies p.status == Dead)
+    }
+
+    /// Check if all Citizen players are dead
+    pure def all_citizens_dead(players: str -> PlayerFeatures): bool = {
+        players.values().forall(p => p.role == Citizen implies p.status == Dead)
+    }
+
+    /// Update the game status based on the current state
+    pure def update_status(players: str -> PlayerFeatures): Status = {
+        if (all_mafias_dead(players)) Done(Citizen)  // Citizens win if all Mafias are dead
+        else if (all_citizens_dead(players)) Done(Mafia)  // Mafia wins if all Citizens are dead
+        else Pending  // The game is still ongoing
+    }
+
+    /// Function to update player features after being killed
+    def update_features_after_kill(victim: str): str -> PlayerFeatures = {
+        players_to_features.setBy(victim, p => { ...p, status: Dead })
+    }
+
+    /// Function to update player features after hanging
+    def update_features_after_hang(player_to_hang: str): str -> PlayerFeatures = {
+        players_to_features
+          .setBy(player_to_hang, p => { ...p, status: Dead })
+          .transformValues(p => { ...p, voted: false })
+    }
+
+    action init = all {
+        pure val roles = Set(Mafia, Citizen)
+        nondet role_by_player = PLAYERS.setOfMaps(roles).oneOf()
+        players_to_features' = PLAYERS.mapBy(p => { name: p, role: role_by_player.get(p), status: Alive, voted: false }),
+        game_phase' = Night,  // Start with the Night phase
+        game_status' = Pending,  // Game is in Pending status
+        votes_by_player' = PLAYERS.mapBy(p => 0)  // Initialize vote counts to 0
+    }
+
+    /// Action for Mafia killing a player
+    action mafia_kills = {
+        nondet victim = players_to_features.values().filter(p => p.status == Alive and p.role == Citizen).oneOf()
+        val updated_features = update_features_after_kill(victim.name)
+        val new_game_status = update_status(updated_features)
+        all {
+            players_to_features.values().exists(p => p.status == Alive and p.role == Mafia),
+            game_phase == Night,
+            players_to_features' = updated_features,
+            game_status' = new_game_status,         
+            game_phase' = Day,
+            votes_by_player' = votes_by_player
+        }
+    }
+
+    /// Voting action during the Day phase
+    action vote = { 
+        nondet current_voter = players_to_features.values().filter(p => p.status == Alive).oneOf()
+        nondet selected_target = players_to_features.values().filter(p => p.status == Alive and p.name != current_voter.name).oneOf()
+        all {
+            game_phase == Day,
+            game_status == Pending,
+            current_voter.voted == false,
+            players_to_features' = players_to_features.set(current_voter.name, { ...current_voter, voted: true }),
+            votes_by_player' = votes_by_player.set(selected_target.name, votes_by_player.get(selected_target.name) + 1),
+            game_phase' = Day,
+            game_status' = Pending,
+        }
+    }
+
+    /// Action to hang a player based on voting results
+    action hang_someone = {
+        val players_with_max_votes = get_most_voted_players
+        all {
+            game_phase == Day,
+            game_status == Pending,
+            all_voted,
+            if (players_with_max_votes.size() == 1) execute_hanging
+            else votes_tied
+        }
+    }
+
+    /// If exactly one player has the maximum votes, hang that player
+    action execute_hanging = {
+        nondet player_to_hang = get_most_voted_players.oneOf()
+        val updated_features = update_features_after_hang(player_to_hang)
+        val new_game_status = update_status(updated_features) 
+        all {
+            players_to_features.get(player_to_hang).status == Alive,
+            players_to_features' = updated_features,
+            game_phase' = Night,
+            votes_by_player' = PLAYERS.mapBy(p => 0),
+            game_status' = new_game_status
+        }
+    }
+
+    /// If there's a tie, reset the votes and move to the Night phase without hanging anyone
+    action votes_tied = all {
+        players_to_features' = players_to_features.transformValues( p => {
+            ...p,
+            voted: false
+        }),
+        game_phase' = Night,
+        votes_by_player' = PLAYERS.mapBy(p => 0),
+        game_status' = Pending
+    }
+
+    action step = if (has_alive_mafia and has_alive_citizen) any {
+            mafia_kills,
+            vote,
+            hang_someone,
+    } else init
+
+    // Invariants
+    /// Check if all Mafia players are dead
+    val mafias_dead: bool = {
+        players_to_features.values().filter(p => p.role == Mafia).forall(p => p.status == Dead)
+    }
+
+    /// Check if all Citizen players are dead
+    val citizens_dead: bool = {
+        players_to_features.values().filter(p => p.role == Citizen).forall(p => p.status == Dead)
+    }
+
+    /// Invariant to ensure the game status correctly reflects the state of the game
+    val correct_game_status = and {
+        game_status == Done(Citizen) implies mafias_dead,
+        game_status == Done(Mafia) implies citizens_dead,
+        game_status == Pending implies not((mafias_dead) or (citizens_dead))
+    }
+
+    /// Invariant to check with a specific ratio, mafias outnumber the citizens and will always win the game.
+    // Here because there are three players, having two mafias guarantee they win.
+    val win_ratio = {
+        (PLAYERS.filter(p => players_to_features.get(p).role == Mafia).size() >= 2) implies not (game_status == Done(Citizen))
+    }
+}
+
+// Module to play the Mafia game with a specific set of players
+module play_mafia {
+    import mafia(PLAYERS = Set("mahtab", "gabriela", "max")).*
+}