Skip to content

Commit

Permalink
Fix comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@MahtabNorouzi
MahtabNorouzi authored Sep 17, 2024
1 parent 08633a6 commit c2fbdd6
Showing 1 changed file with 64 additions and 59 deletions.
123 changes: 64 additions & 59 deletions examples/games/mafia_werewolf/play_mafia.qnt
View file
Original file line number Diff line number Diff line change
@@ -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) {
Expand All @@ -31,86 +44,73 @@ 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
}
}

/// 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,
}
Expand All @@ -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
Expand All @@ -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,
Expand All @@ -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")).*
}

0 comments on commit c2fbdd6

Please sign in to comment.