Ouch

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
+            val temp = if (vig0) victim.append({...victimVig0, name: moved.get(victimVig0.name)}) else victim
-            if (vig1_alive(players_to_features) > 0) temp.append(victimVig1) else temp
+            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,
         }
     }
 

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)))
+  }
+
 }