diff --git a/Masons.qnt b/Masons.qnt index ed9abeb..7e27a66 100644 --- a/Masons.qnt +++ b/Masons.qnt @@ -20,7 +20,9 @@ module mafia { var votes_by_player: str -> int var game_phase: Phase var game_status: Status - var last_saved: str + var last_saved: Option[str] + var last_moved1: Option[str] + var last_moved2: Option[str] pure def all_voted(players: str -> PlayerFeatures): bool = players.values().filter(p => p.status == Alive).forall(p => p.voted == true) @@ -37,6 +39,9 @@ module mafia { pure def doc_alive(players: str -> PlayerFeatures): int = size(players.values().filter((p) => p.status == Alive and p.role == Doctor)) + pure def mover_alive(players: str -> PlayerFeatures): int = + size(players.values().filter((p) => p.status == Alive and p.role == Mover)) + pure def vig0_alive(players: str -> PlayerFeatures): int = size(players.values().filter((p) => p.status == Alive and p.role == Vigilante(0))) @@ -96,25 +101,64 @@ module mafia { playersNew.transformValues(p => {... p, voted: false}) } + action init = all { + pure val list_of_roles = gen_list_of_roles(size(players)) + pure val set_of_roles = list_of_roles.listToSet() + pure val role_by_player_powerset:Set[str -> Role] = players.setOfMaps(set_of_roles) + pure val role_by_player_subset:Set[str -> Role] = + role_by_player_powerset.filter(m => [] == (m.keys().fold(list_of_roles, (acc, n) => dropFirst(acc,x => x == m.get(n))))) + nondet role_by_player:str -> Role = role_by_player_subset.oneOf() + pure val mascot_potential:Set[str] = role_by_player.mapToSet().filter(x => x._2 != Mafia).map(x => x._1) + nondet mascot_choice:str = mascot_potential.oneOf() + players_to_features' = players.mapBy(p => + { name: p, + alignment: if (role_by_player.get(p) == Mafia) Scum else Town, + role: role_by_player.get(p), + status: Alive, + voted: false, + nominated: false, + mascot: p == mascot_choice + }), + last_saved' = None, + last_moved1' = None, + last_moved2' = None, + game_phase' = Day, // Start with the Day phase + game_status' = Pending, // Game is in Pending status + votes_by_player' = players.mapBy(p => 0) // Initialize vote counts to 0 + } + + action nightPhase = all { nondet victimScum = players_to_features.values().filter(p => p.status == Alive and p.alignment == Town).oneOf() - nondet doctorSave = players_to_features.values().filter(p => p.status == Alive and p.role != Doctor and p.name != last_saved).oneOf() + nondet doctorSave = players_to_features.values().filter(p => p.status == Alive and p.role != Doctor and Some(p.name) != last_saved).oneOf() nondet victimVig0 = players_to_features.values().filter(p => p.status == Alive and p.role != Vigilante(0)).oneOf() nondet victimVig1 = players_to_features.values().filter(p => p.status == Alive and p.role != Vigilante(1)).oneOf() - val victim = if (victimScum == doctorSave and doc_alive(players_to_features) > 0) [] else [victimScum] + nondet move1 = players_to_features.values().filter(p => p.status == Alive and Some(p.name) != last_moved1 and Some(p.name) != last_moved2 ).oneOf() + nondet move2 = players_to_features.values().filter(p => p.status == Alive and Some(p.name) != last_moved1 and Some(p.name) != last_moved2 and p.name != move1.name).oneOf() + val mover = mover_alive(players_to_features) > 0 + val doc = doc_alive(players_to_features) > 0 + val vig0 = vig0_alive(players_to_features) > 0 + val vig1 = vig1_alive(players_to_features) > 0 + val moved = players.mapBy(x => if (not(mover)) x else + if (x == move1.name) move2.name else if (x == move2.name) move1.name else x) + val victim = if (victimScum == doctorSave and doc) [] else [{...victimScum, name: moved.get(victimScum.name)}] val victims: List[PlayerFeatures] = { - val temp = if (vig0_alive(players_to_features) > 0) victim.append(victimVig0) else victim - if (vig1_alive(players_to_features) > 0) temp.append(victimVig1) else temp + val temp = if (vig0) victim.append({...victimVig0, name: moved.get(victimVig0.name)}) else victim + if (vig1) temp.append({...victimVig1, name: moved.get(victimVig1.name)}) else temp } val updated_features = update_after_kill(victims.listMap(p => p.name),players_to_features) val new_game_status = update_status(updated_features) + // TODO: Handle gunsmith 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 + votes_by_player' = votes_by_player, + last_saved' = if (doc and victimScum == doctorSave) None else if (doc) Some(doctorSave.name) else None, + last_moved1' = if (mover and (move1 == victimScum or move2 == victimScum)) None else if (mover) Some(move1.name) else None, + last_moved2' = if (mover and (move1 == victimScum or move2 == victimScum)) None else if (mover) Some(move2.name) else None, } } diff --git a/basicspells.qnt b/basicspells.qnt index d068b5b..41834a1 100644 --- a/basicspells.qnt +++ b/basicspells.qnt @@ -385,4 +385,42 @@ module basicSpells { assert(repeat(5,1) == [1,1,1,1,1]), assert(repeat(2,true) == [true,true]) } + + + /// `listToSet(l)` is set of elements, generated from a list l. + /// + /// - @param n: list of elements + /// - @returns a set of elements. + pure def listToSet(l:List[a]): Set[a] = l.foldl(Set(), (acc,e) => acc.union(Set(e))) + + run listToSetTest = all { + assert(listToSet([1,2,3]) == Set(1,2,3)), + assert(listToSet([1,1,1]) == Set(1)), + } + + pure def dropFirst(l: List[a], cond: (a) => bool): List[a] = { + pure val result = l.foldl(([], true), (acc, e) => { + if (acc._2 and not(cond(e))) { + (acc._1.append(e), true) + } else if (not(acc._2)) { + (acc._1.append(e), acc._2) + } else { + (acc._1, false) + } + }) + + result._1 + } + + run dropFirstTest = all { + assert(dropFirst([1, 5, 4, 3], (x) => x % 2 != 1) == [1, 5, 3]), + assert(dropFirst([1,2,3,4,5], (x) => x == 12) == [1,2,3,4,5]) + } + + pure def mapToSet(m: a -> b):Set[(a,b)] = m.keys().fold(Set(),(acc, k) => acc.union(Set((k,m.get(k))))) + + run mapToSetTest = { + assert(mapToSet(Map(1 -> 2, 3 -> 6)) == Set((1,2),(3,6))) + } + }