From 12ff407908152c686b29e373a8be5469a1c6a08b Mon Sep 17 00:00:00 2001 From: mahtab75 Date: Tue, 27 Aug 2024 17:17:59 -0400 Subject: [PATCH 1/6] Add mafia game to examples --- examples/README.md | 1 + examples/games/mafia_werewolf/play_mafia.qnt | 185 +++++++++++++++++++ 2 files changed, 186 insertions(+) create mode 100644 examples/games/mafia_werewolf/play_mafia.qnt diff --git a/examples/README.md b/examples/README.md index 183b6df69..f2541eab0 100644 --- a/examples/README.md +++ b/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/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: | diff --git a/examples/games/mafia_werewolf/play_mafia.qnt b/examples/games/mafia_werewolf/play_mafia.qnt new file mode 100644 index 000000000..a165a4c18 --- /dev/null +++ b/examples/games/mafia_werewolf/play_mafia.qnt @@ -0,0 +1,185 @@ +// -*- mode: Bluespec; -*- + +module mafia { + 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 = { + role: Role, + status: LifeState, + voted: bool // Indicates whether the player has voted + } + var player_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 alive players have voted + val all_voted = PLAYERS.filter(p => player_to_features.get(p).status == Alive) + .forall(p => player_to_features.get(p).voted == true) + /// Check if there are any Mafia players left + val has_mafia = PLAYERS.exists(p => player_to_features.get(p).role == Mafia) + /// Check if there are any Citizen players left + val has_citizen = PLAYERS.exists(p => player_to_features.get(p).role == Citizen) + /// 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(player: str -> PlayerFeatures): bool = { + PLAYERS.filter(p => player.get(p).role == Mafia).forall(p => player.get(p).status == Dead) + } + /// Check if all Citizen players are dead + pure def all_citizens_dead(player: str -> PlayerFeatures): bool = { + PLAYERS.filter(p => player.get(p).role == Citizen).forall(p => player.get(p).status == Dead) + } + /// Update the game status based on the current state + pure def update_status(player: str -> PlayerFeatures): Status = { + if (all_mafias_dead(player)) Done(Citizen) // Citizens win if all Mafias are dead + else if (all_citizens_dead(player)) Done(Mafia) // Mafia wins if all Citizens are dead + else Pending // The game is still ongoing + } + /// Function to reset the players votes after voting is done + pure def reset_votes_and_statuses(player_to_features: str -> PlayerFeatures): str -> PlayerFeatures = { + PLAYERS.mapBy(p => { + ...player_to_features.get(p), + voted: false + }) + } + /// Function to update player features after hanging + def update_features_after_hang(player_to_hang: str): str -> PlayerFeatures = { + PLAYERS.mapBy(p => + if (p == player_to_hang) { + ...player_to_features.get(p), + status: Dead, + voted: false + } else { + ...player_to_features.get(p), + voted: false + } + ) + } + /// Function to update player features after being killed by the mafia + def update_features_after_kill(victim: str): str -> PlayerFeatures ={ + player_to_features.set(victim, { + ...player_to_features.get(victim), + status: Dead + }) + } + + action init = all { + pure val roles = Set(Mafia, Citizen) + nondet role_by_player = PLAYERS.setOfMaps(roles).oneOf() + player_to_features' = PLAYERS.mapBy(name => { role: role_by_player.get(name), 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 = any { + nondet killer = PLAYERS.filter(p => player_to_features.get(p).status == Alive and player_to_features.get(p).role == Mafia).oneOf() + nondet victim = PLAYERS.filter(p => player_to_features.get(p).status == Alive and player_to_features.get(p).role == Citizen).oneOf() + + val updated_features = update_features_after_kill(victim) + val new_game_status = update_status(updated_features) + all { + game_phase == Night, + player_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 selected_target = PLAYERS.filter(p => player_to_features.get(p).status == Alive).oneOf() + nondet current_voter = PLAYERS.filter(p => player_to_features.get(p).status == Alive and p != selected_target).oneOf() + all { + game_phase == Day, + game_status == Pending, + player_to_features.get(current_voter).voted == false, + + player_to_features' = player_to_features.set(current_voter, { ...player_to_features.get(current_voter), voted: true}), + votes_by_player' = votes_by_player.set(selected_target, votes_by_player.get(selected_target) + 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 { + player_to_features.get(player_to_hang).status == Alive, + player_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 { + player_to_features' = reset_votes_and_statuses(player_to_features), + game_phase' = Night, + votes_by_player' = PLAYERS.mapBy(p => 0), + game_status' = Pending + } + + action step = if (has_mafia and has_citizen) any { + mafia_kills, + vote, + hang_someone, + } else init + + // Invariants + /// Check if all Mafia players are dead + val mafias_dead: bool = { + PLAYERS.filter(p => player_to_features.get(p).role == Mafia).forall(p => player_to_features.get(p).status == Dead) and has_mafia and has_citizen + } + /// Check if all Citizen players are dead + val citizens_dead: bool = { + PLAYERS.filter(p => player_to_features.get(p).role == Citizen).forall(p => player_to_features.get(p).status == Dead) and has_mafia and has_citizen + } + /// 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 ration, mafias outnumber the citizens will always win the game. + // Here because there are three players, having two mafias guaranty they win. + val win_ratio = { + (PLAYERS.filter(p => player_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")).* +} From 08633a60d1100c329fe4992cc79879a4671d8a23 Mon Sep 17 00:00:00 2001 From: Mahtab <67663333+MahtabNorouzi@users.noreply.github.com> Date: Mon, 16 Sep 2024 18:24:26 -0400 Subject: [PATCH 2/6] Create README.md --- examples/games/mafia_werewolf/README.md | 71 +++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 examples/games/mafia_werewolf/README.md diff --git a/examples/games/mafia_werewolf/README.md b/examples/games/mafia_werewolf/README.md new file mode 100644 index 000000000..e6f947ee4 --- /dev/null +++ b/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:** Eliminates all Citizens. +- **Citizen:** Identify and eliminate all Mafias. + +# 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 that 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 randpmpoly 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 Mafias) 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 Mafias 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 and specify the desired amount of players participating in the game. Roles will be randomly assigned. + +- **Running the Game:** + - `quint run play_mafia.qnt` + From c2fbdd68c87375ed6078ef56c5438b031deb9d98 Mon Sep 17 00:00:00 2001 From: Mahtab <67663333+MahtabNorouzi@users.noreply.github.com> Date: Tue, 17 Sep 2024 15:25:53 -0400 Subject: [PATCH 3/6] Fix comments --- examples/games/mafia_werewolf/play_mafia.qnt | 123 ++++++++++--------- 1 file changed, 64 insertions(+), 59 deletions(-) diff --git a/examples/games/mafia_werewolf/play_mafia.qnt b/examples/games/mafia_werewolf/play_mafia.qnt index a165a4c18..a53c8d313 100644 --- a/examples/games/mafia_werewolf/play_mafia.qnt +++ b/examples/games/mafia_werewolf/play_mafia.qnt @@ -1,28 +1,41 @@ // -*- 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: + * [1]: 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 player_to_features: str -> PlayerFeatures + 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 alive players have voted - val all_voted = PLAYERS.filter(p => player_to_features.get(p).status == Alive) - .forall(p => player_to_features.get(p).voted == true) - /// Check if there are any Mafia players left - val has_mafia = PLAYERS.exists(p => player_to_features.get(p).role == Mafia) - /// Check if there are any Citizen players left - val has_citizen = PLAYERS.exists(p => player_to_features.get(p).role == Citizen) + 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) { @@ -31,69 +44,57 @@ module mafia { 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 + } else Set() // Return an empty set if not all players have votedx + } + pure def transformValues(m: a -> b, f: (b) => c): a -> c = { + m.keys().mapBy(k => f(m.get(k))) } /// Check if all Mafia players are dead - pure def all_mafias_dead(player: str -> PlayerFeatures): bool = { - PLAYERS.filter(p => player.get(p).role == Mafia).forall(p => player.get(p).status == 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(player: str -> PlayerFeatures): bool = { - PLAYERS.filter(p => player.get(p).role == Citizen).forall(p => player.get(p).status == 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(player: str -> PlayerFeatures): Status = { - if (all_mafias_dead(player)) Done(Citizen) // Citizens win if all Mafias are dead - else if (all_citizens_dead(player)) Done(Mafia) // Mafia wins if all Citizens are dead + 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 reset the players votes after voting is done - pure def reset_votes_and_statuses(player_to_features: str -> PlayerFeatures): str -> PlayerFeatures = { - PLAYERS.mapBy(p => { - ...player_to_features.get(p), - voted: false - }) + /// 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.mapBy(p => - if (p == player_to_hang) { - ...player_to_features.get(p), - status: Dead, - voted: false - } else { - ...player_to_features.get(p), + players_to_features.setBy(player_to_hang, p => { ...p, status: Dead }).transformValues( + p => { + ...p, voted: false } ) } - /// Function to update player features after being killed by the mafia - def update_features_after_kill(victim: str): str -> PlayerFeatures ={ - player_to_features.set(victim, { - ...player_to_features.get(victim), - status: Dead - }) - } action init = all { pure val roles = Set(Mafia, Citizen) nondet role_by_player = PLAYERS.setOfMaps(roles).oneOf() - player_to_features' = PLAYERS.mapBy(name => { role: role_by_player.get(name), status: Alive, voted: false }), + 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 = any { - nondet killer = PLAYERS.filter(p => player_to_features.get(p).status == Alive and player_to_features.get(p).role == Mafia).oneOf() - nondet victim = PLAYERS.filter(p => player_to_features.get(p).status == Alive and player_to_features.get(p).role == Citizen).oneOf() - - val updated_features = update_features_after_kill(victim) + 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, - player_to_features' = updated_features, + players_to_features' = updated_features, game_status' = new_game_status, game_phase' = Day, votes_by_player' = votes_by_player @@ -101,16 +102,15 @@ module mafia { } /// Voting action during the Day phase - action vote = { - nondet selected_target = PLAYERS.filter(p => player_to_features.get(p).status == Alive).oneOf() - nondet current_voter = PLAYERS.filter(p => player_to_features.get(p).status == Alive and p != selected_target).oneOf() + 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, - player_to_features.get(current_voter).voted == false, - - player_to_features' = player_to_features.set(current_voter, { ...player_to_features.get(current_voter), voted: true}), - votes_by_player' = votes_by_player.set(selected_target, votes_by_player.get(selected_target) + 1), + 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, } @@ -132,11 +132,10 @@ module mafia { 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) - + val new_game_status = update_status(updated_features) all { - player_to_features.get(player_to_hang).status == Alive, - player_to_features' = updated_features, + 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 @@ -145,13 +144,16 @@ module mafia { /// If there's a tie, reset the votes and move to the Night phase without hanging anyone action votes_tied = all { - player_to_features' = reset_votes_and_statuses(player_to_features), + 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_mafia and has_citizen) any { + action step = if (has_alive_mafia and has_alive_citizen) any { mafia_kills, vote, hang_someone, @@ -160,26 +162,29 @@ module mafia { // Invariants /// Check if all Mafia players are dead val mafias_dead: bool = { - PLAYERS.filter(p => player_to_features.get(p).role == Mafia).forall(p => player_to_features.get(p).status == Dead) and has_mafia and has_citizen + 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.filter(p => player_to_features.get(p).role == Citizen).forall(p => player_to_features.get(p).status == Dead) and has_mafia and has_citizen + 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 ration, mafias outnumber the citizens will always win the game. // Here because there are three players, having two mafias guaranty they win. val win_ratio = { - (PLAYERS.filter(p => player_to_features.get(p).role == Mafia).size() >= 2) implies not (game_status == Done(Citizen)) + (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")).* + import mafia(PLAYERS = Set("mahtab", "gabriela","max","kobra","arman","fat")).* } From 982f701b939f701a1b72cde9b94afa417a449ccb Mon Sep 17 00:00:00 2001 From: Mahtab <67663333+MahtabNorouzi@users.noreply.github.com> Date: Tue, 17 Sep 2024 16:42:48 -0400 Subject: [PATCH 4/6] Update README.md --- examples/games/mafia_werewolf/README.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/examples/games/mafia_werewolf/README.md b/examples/games/mafia_werewolf/README.md index e6f947ee4..b1b11f9fb 100644 --- a/examples/games/mafia_werewolf/README.md +++ b/examples/games/mafia_werewolf/README.md @@ -4,8 +4,8 @@ This is an implementation of the Mafia party game, where players are secretly as # Objective -- **Mafia:** Eliminates all Citizens. -- **Citizen:** Identify and eliminate all Mafias. +- **Mafia:** Eliminate all Citizens. +- **Citizen:** Identify and eliminate all Mafia. # Components @@ -14,7 +14,7 @@ This is an implementation of the Mafia party game, where players are secretly as - **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 that stores key data about a player, including their role, life status, and whether they have voted. +- **PlayerFeatures:** The structure stores key data about a player, including their role, life status, and whether they have voted. ## Variables: @@ -36,14 +36,14 @@ This is an implementation of the Mafia party game, where players are secretly as ## Initial Setup: -The game starts in the `Night` phase. Players are randpmpoly assigned as either `Mafia` or `Citizen`, and their status is set to `Alive`. Votes are also initialized to zero. +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 Mafias) 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. +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: @@ -55,7 +55,7 @@ Note: A game should consist of both `Mafia` and `Citizen` to be valid. ## Winning Conditions: - **Mafia Wins:** If all Citizens are dead. -- **Citizen Wins:** If all Mafias are dead. +- **Citizen Wins:** If all Mafia are dead. ## Special Features: @@ -64,7 +64,7 @@ Note: A game should consist of both `Mafia` and `Citizen` to be valid. ## Usage: -- **Initializing the Game:** Import the `mafia` module and and specify the desired amount of players participating in the game. Roles will be randomly assigned. +- **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` From 7f9911ce18b56868440418dda55796e2d3d8b763 Mon Sep 17 00:00:00 2001 From: Mahtab <67663333+MahtabNorouzi@users.noreply.github.com> Date: Tue, 17 Sep 2024 17:24:48 -0400 Subject: [PATCH 5/6] Update play_mafia.qnt --- examples/games/mafia_werewolf/play_mafia.qnt | 25 +++++++++++++------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/examples/games/mafia_werewolf/play_mafia.qnt b/examples/games/mafia_werewolf/play_mafia.qnt index a53c8d313..fb1c867de 100644 --- a/examples/games/mafia_werewolf/play_mafia.qnt +++ b/examples/games/mafia_werewolf/play_mafia.qnt @@ -24,18 +24,24 @@ module mafia { role: Role, status: LifeState, voted: bool // Indicates whether the player has voted - } + } var players_to_features: str -> PlayerFeatures + 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 alive 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) { @@ -46,35 +52,38 @@ module mafia { PLAYERS.filter(p => votes_by_player.get(p) == max_votes) } else Set() // Return an empty set if not all players have votedx } + pure def transformValues(m: a -> b, f: (b) => c): a -> c = { m.keys().mapBy(k => f(m.get(k))) } + /// 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 - } - ) + players_to_features + .setBy(player_to_hang, p => { ...p, status: Dead }) + .transformValues(p => { ...p, voted: false }) } action init = all { @@ -186,5 +195,5 @@ module mafia { // Module to play the Mafia game with a specific set of players module play_mafia { - import mafia(PLAYERS = Set("mahtab", "gabriela","max","kobra","arman","fat")).* + import mafia(PLAYERS = Set("mahtab", "gabriela", "max").* } From ead41a388919d2982b3e624b6e566676db41a884 Mon Sep 17 00:00:00 2001 From: Mahtab <67663333+MahtabNorouzi@users.noreply.github.com> Date: Thu, 19 Sep 2024 15:23:39 -0400 Subject: [PATCH 6/6] Update play_mafia.qnt --- examples/games/mafia_werewolf/play_mafia.qnt | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/examples/games/mafia_werewolf/play_mafia.qnt b/examples/games/mafia_werewolf/play_mafia.qnt index fb1c867de..f2e4ee671 100644 --- a/examples/games/mafia_werewolf/play_mafia.qnt +++ b/examples/games/mafia_werewolf/play_mafia.qnt @@ -6,7 +6,7 @@ * https://en.wikipedia.org/wiki/Mafia_(party_game) * * For more information on the implementation and details of the code check this: - * [1]: https://github.com/informalsystems/quint/blob/main/examples/games/mafia_werewolf/README.md + * https://github.com/informalsystems/quint/blob/main/examples/games/mafia_werewolf/README.md * Mahtab Norouzi, Informal Systems, 2024 */ @@ -24,7 +24,7 @@ module mafia { role: Role, status: LifeState, voted: bool // Indicates whether the player has voted - } var players_to_features: str -> PlayerFeatures + } var players_to_features: str -> PlayerFeatures var votes_by_player: str -> int @@ -33,7 +33,7 @@ module mafia { type Status = Pending | Done(Role) var game_status: Status - /// Check if all alive players have voted + /// 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 @@ -50,13 +50,9 @@ module mafia { 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 votedx + } else Set() // Return an empty set if not all players have voted } - pure def transformValues(m: a -> b, f: (b) => c): a -> c = { - m.keys().mapBy(k => f(m.get(k))) - } - /// 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) @@ -186,8 +182,8 @@ module mafia { game_status == Pending implies not((mafias_dead) or (citizens_dead)) } - /// Invariant to check with a specific ration, mafias outnumber the citizens will always win the game. - // Here because there are three players, having two mafias guaranty they win. + /// 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)) } @@ -195,5 +191,5 @@ module mafia { // Module to play the Mafia game with a specific set of players module play_mafia { - import mafia(PLAYERS = Set("mahtab", "gabriela", "max").* + import mafia(PLAYERS = Set("mahtab", "gabriela", "max")).* }