From c6497a68b23a2c11e8fd360a7166ca5f4a96d724 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Thu, 8 Aug 2024 15:35:08 -0400
Subject: [PATCH 01/14] Add new example to classic/distributed

---
 examples/README.md                            |  37 +++---
 .../RockPaperScissor/rock_paper_scissor.qnt   | 109 ++++++++++++++++++
 2 files changed, 128 insertions(+), 18 deletions(-)
 create mode 100644 examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt

diff --git a/examples/README.md b/examples/README.md
index 5b525cbc8..37e92bb29 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -48,34 +48,35 @@ listed without any additional command line arguments.
 
 | Example | Syntax (`parse`) | Types (`typecheck`) | Unit tests (`test`) | Apalache (`verify`) |
 |---------|:----------------:|:-------------------:|:-------------------:|:-------------------:|
-| [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/RockPaperScissor/rock_paper_scissor.qnt](./classic/distributed/RockPaperScissor/rock_paper_scissor.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
-| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/bank/bank.qnt](./cosmos/bank/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
-| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/tendermint/TendermintTest.qnt](./cosmos/tendermint/TendermintTest.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [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/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: |
+| [games/tictactoe/tictactoe.qnt](./games/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -83,20 +84,20 @@ listed without any additional command line arguments.
 | [language-features/instances.qnt](./language-features/instances.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/instancesFrom.qnt](./language-features/instancesFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/integers.qnt](./language-features/integers.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1393</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1285</sup> |
 | [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
-| [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [spells/BoundedUInt.qnt](./spells/BoundedUInt.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [spells/commonSpells.qnt](./spells/commonSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
diff --git a/examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt b/examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt
new file mode 100644
index 000000000..b90326672
--- /dev/null
+++ b/examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt
@@ -0,0 +1,109 @@
+
+module rock_paper_scissor {
+
+    // Constants for player names
+    const PLAYER1 : str
+    const PLAYER2 : str
+
+    // Enum types for the possible moves and game status
+    type Move = Init | Rock | Paper | Scissor
+    type GameStatus = Started | Pending | Draw | Winner(str)
+
+    // Variables to hold the current state of each player's move and the game status
+    var p1State : Move
+    var p2State : Move
+    var game : GameStatus
+
+    // Initialize the game with both players in 'Init' state and game status as 'Started'
+    action init = all {
+        p1State' = Init,
+        p2State' = Init,
+        game' = Started
+    }
+
+
+    // Randomly decide moves for both players from the set of possible moves
+    action decideMoves() = {
+        nondet move1 = Set(Rock, Paper, Scissor).oneOf() // Non-deterministically pick a move for player 1
+        nondet move2 = Set(Rock, Paper, Scissor).oneOf() // Non-deterministically pick a move for player 1
+        all {
+            p1State' = move1,
+            p2State' = move2
+        }
+    }
+
+
+    // Determine the winner based on the current moves of both players
+    action updateWinner () = any {
+        if (
+            (p1State == Rock and p2State == Scissor) or
+            (p1State == Paper and p2State == Rock) or
+            (p1State == Scissor and p2State == Paper)
+        ){
+            game' = Winner(PLAYER1) // Player 1 wins if their move beats player 2's move
+            
+        } else {
+            if (
+            (p1State == Rock and p2State == Paper) or
+            (p1State == Paper and p2State == Scissor) or
+            (p1State == Scissor and p2State == Rock)
+            ){
+
+                game' = Winner(PLAYER2) // Player 2 wins if their move beats player 1's move
+            } else {
+                
+                game' = Draw // It's a draw if both players chose the same move
+            }
+        }
+
+    }
+
+
+    action step = if ((p1State == Init) or (p2State == Init)) all {
+        // Decide the moves if the game is in the initial state
+        decideMoves,
+        // Put the game in the Pending status when players have made their moves
+        game' = Pending,
+        
+    } else {
+        if (game == Pending) all{
+            // Put the game on hold with each player's move for one round to decide the winner
+            p1State' = p1State,
+            p2State' = p2State,
+            // Update the winner based on the current moves
+            updateWinner,
+
+        }  else all {
+            // Reset the game if it's not pending
+            p1State' = Init,
+            p2State' = Init,
+            game' = Started
+        }
+    }
+
+
+    // Conditions to determine the winner based on players' moves
+    val winCondition1 = (
+        (p1State == Paper and p2State == Rock)
+        or
+        (p1State == Rock and p2State == Scissor)
+        or
+        (p1State == Scissor and p2State == Paper)
+    )
+
+    val winCondition2 = (
+        (p2State == Paper and p1State == Rock)
+        or
+        (p2State == Rock and p1State == Scissor)
+        or
+        (p2State == Scissor and p1State == Paper)
+    )
+
+    // Invariant to check if the game status matches the expected winner
+    val winInv = (winCondition1 implies (game == Winner(PLAYER1)) or (winCondition2 implies (game == Winner(PLAYER2))))
+
+}
+
+module play_rock_paper_scissor {
+    import rock_paper_scissor(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*    
+}
\ No newline at end of file

From 2115080f5fa6ecaddb995caaf113baba6b311508 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Thu, 8 Aug 2024 15:56:49 -0400
Subject: [PATCH 02/14] fixed README

---
 examples/README.md                                 | 14 +++++++-------
 ...per_scissor.qnt => play_rock_paper_scissor.qnt} |  0
 2 files changed, 7 insertions(+), 7 deletions(-)
 rename examples/classic/distributed/RockPaperScissor/{rock_paper_scissor.qnt => play_rock_paper_scissor.qnt} (100%)

diff --git a/examples/README.md b/examples/README.md
index 37e92bb29..b2d7f15c3 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -54,17 +54,17 @@ listed without any additional command line arguments.
 | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [classic/distributed/RockPaperScissor/rock_paper_scissor.qnt](./classic/distributed/RockPaperScissor/rock_paper_scissor.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt](./classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
-| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/bank/bank.qnt](./cosmos/bank/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
@@ -93,11 +93,11 @@ listed without any additional command line arguments.
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1285</sup> |
 | [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
-| [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [spells/BoundedUInt.qnt](./spells/BoundedUInt.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [spells/commonSpells.qnt](./spells/commonSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
diff --git a/examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt b/examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt
similarity index 100%
rename from examples/classic/distributed/RockPaperScissor/rock_paper_scissor.qnt
rename to examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt

From 94d09e141aa5eff3290d39bc62c14969a1f1b6cb Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Thu, 8 Aug 2024 16:14:51 -0400
Subject: [PATCH 03/14] fixed README

---
 examples/README.md | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/examples/README.md b/examples/README.md
index b2d7f15c3..9a90c051a 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -48,35 +48,35 @@ listed without any additional command line arguments.
 
 | Example | Syntax (`parse`) | Types (`typecheck`) | Unit tests (`test`) | Apalache (`verify`) |
 |---------|:----------------:|:-------------------:|:-------------------:|:-------------------:|
-| [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt](./classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/bank/bank.qnt](./cosmos/bank/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
-| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/bank/bankTest.qnt](./cosmos/bank/bankTest.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/tendermint/Tendermint.qnt](./cosmos/tendermint/Tendermint.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [cosmos/tendermint/TendermintModels.qnt](./cosmos/tendermint/TendermintModels.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/tendermint/TendermintTest.qnt](./cosmos/tendermint/TendermintTest.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
-| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [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/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: | :x: |
+| [games/tictactoe/tictactoe.qnt](./games/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
@@ -84,16 +84,16 @@ listed without any additional command line arguments.
 | [language-features/instances.qnt](./language-features/instances.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/instancesFrom.qnt](./language-features/instancesFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/integers.qnt](./language-features/integers.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1393</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1285</sup> |
 | [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
@@ -111,4 +111,4 @@ listed without any additional command line arguments.
 | [verification/defaultOpNames.qnt](./verification/defaultOpNames.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 
 [^nostatemachine]: This specification does not define a state machine.
-[^parameterized]: This specification is parameterized, and instantiated in another module.
+[^parameterized]: This specification is parameterized, and instantiated in another module.
\ No newline at end of file

From c83bb230403c68d732efbaf2ed2f8a3c941c7187 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Thu, 8 Aug 2024 16:54:06 -0400
Subject: [PATCH 04/14] fixed README

---
 examples/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/README.md b/examples/README.md
index 9a90c051a..108545e36 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -111,4 +111,4 @@ listed without any additional command line arguments.
 | [verification/defaultOpNames.qnt](./verification/defaultOpNames.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 
 [^nostatemachine]: This specification does not define a state machine.
-[^parameterized]: This specification is parameterized, and instantiated in another module.
\ No newline at end of file
+[^parameterized]: This specification is parameterized, and instantiated in another module.

From 834e155fa8b13c3ba64ea861667737a1efab667f Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Wed, 14 Aug 2024 14:32:54 -0400
Subject: [PATCH 05/14] optimized the code and moved it to /games

---
 .../play_rock_paper_scissors.qnt              | 57 +++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt

diff --git a/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
new file mode 100644
index 000000000..a8192f37b
--- /dev/null
+++ b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
@@ -0,0 +1,57 @@
+// -*- mode: Bluespec; -*-
+module rock_paper_scissors {
+    // Constants for player names
+    const PLAYER1 : str
+    const PLAYER2 : str
+    // Enum types for the possible moves and game status
+    type Move = Init | Rock | Paper | scissors
+    type GameStatus = Started | Pending | Draw | Winner(str)
+    // Variables to hold the current state of each player's move and the game status
+    var p1State: Move
+    var p2State: Move
+    var status: GameStatus
+    def beats(m1: Move, m2: Move): bool = or {
+        (m1 == Rock and m2 == scissors),
+        (m1 == Paper and m2 == Rock),
+        (m1 == scissors and m2 == Paper),
+    }
+    // Initialize the game with both players in 'Init' state and game status as 'Started'
+    action init = all {
+        p1State' = Init,
+        p2State' = Init,
+        status' = Started
+    }
+    // Randomly decide moves for both players from the set of possible moves
+    action decide_moves() = {
+        nondet move1 = Set(Rock, Paper, scissors).oneOf() // Non-deterministically pick a move for player 1
+        nondet move2 = Set(Rock, Paper, scissors).oneOf() // Non-deterministically pick a move for player 1
+        all {
+            p1State' = move1,
+            p2State' = move2,
+            status' = Pending,
+        }
+    }
+    // Determine the winner based on the current moves of both players
+    action find_winner() = any {
+        if (beats(p1State, p2State)) status' = Winner(PLAYER1) // Player 1 wins if their move beats player 2's move
+        else if (beats(p2State, p1State)) status' = Winner(PLAYER2) // Player 2 wins if their move beats player 1's move
+        else status' = Draw // It's a draw if both players chose the same move
+    }
+    action step = if (status == Started) {
+        decide_moves
+    } else if (status == Pending) all {
+        p1State' = p1State,
+        p2State' = p2State,
+        find_winner,
+    }  else all {
+        p1State' = Init,
+        p2State' = Init,
+        status' = Started
+    }
+    // Invariant to check if the game status matches the expected winner
+    val winInv = ((status == Winner(PLAYER1) implies beats(p1State, p2State)) and ((status == Winner(PLAYER2)) implies beats(p2State, p1State)))
+}
+
+module play_rock_paper_scissors {
+    import rock_paper_scissors(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*    
+}
\ No newline at end of file

From 3552e7085a6c198e7b7aa464e374651a3776fba0 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Wed, 14 Aug 2024 15:25:51 -0400
Subject: [PATCH 06/14] fixed README

---
 examples/README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/examples/README.md b/examples/README.md
index 108545e36..8bc6ec079 100644
--- a/examples/README.md
+++ b/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/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: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

From 90619fda983deb5dcfe274cfb030fa4d0808e2ed Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Wed, 14 Aug 2024 15:54:25 -0400
Subject: [PATCH 07/14] deleted example from /classic

---
 .../play_rock_paper_scissor.qnt               | 109 ------------------
 1 file changed, 109 deletions(-)
 delete mode 100644 examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt

diff --git a/examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt b/examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt
deleted file mode 100644
index b90326672..000000000
--- a/examples/classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt
+++ /dev/null
@@ -1,109 +0,0 @@
-
-module rock_paper_scissor {
-
-    // Constants for player names
-    const PLAYER1 : str
-    const PLAYER2 : str
-
-    // Enum types for the possible moves and game status
-    type Move = Init | Rock | Paper | Scissor
-    type GameStatus = Started | Pending | Draw | Winner(str)
-
-    // Variables to hold the current state of each player's move and the game status
-    var p1State : Move
-    var p2State : Move
-    var game : GameStatus
-
-    // Initialize the game with both players in 'Init' state and game status as 'Started'
-    action init = all {
-        p1State' = Init,
-        p2State' = Init,
-        game' = Started
-    }
-
-
-    // Randomly decide moves for both players from the set of possible moves
-    action decideMoves() = {
-        nondet move1 = Set(Rock, Paper, Scissor).oneOf() // Non-deterministically pick a move for player 1
-        nondet move2 = Set(Rock, Paper, Scissor).oneOf() // Non-deterministically pick a move for player 1
-        all {
-            p1State' = move1,
-            p2State' = move2
-        }
-    }
-
-
-    // Determine the winner based on the current moves of both players
-    action updateWinner () = any {
-        if (
-            (p1State == Rock and p2State == Scissor) or
-            (p1State == Paper and p2State == Rock) or
-            (p1State == Scissor and p2State == Paper)
-        ){
-            game' = Winner(PLAYER1) // Player 1 wins if their move beats player 2's move
-            
-        } else {
-            if (
-            (p1State == Rock and p2State == Paper) or
-            (p1State == Paper and p2State == Scissor) or
-            (p1State == Scissor and p2State == Rock)
-            ){
-
-                game' = Winner(PLAYER2) // Player 2 wins if their move beats player 1's move
-            } else {
-                
-                game' = Draw // It's a draw if both players chose the same move
-            }
-        }
-
-    }
-
-
-    action step = if ((p1State == Init) or (p2State == Init)) all {
-        // Decide the moves if the game is in the initial state
-        decideMoves,
-        // Put the game in the Pending status when players have made their moves
-        game' = Pending,
-        
-    } else {
-        if (game == Pending) all{
-            // Put the game on hold with each player's move for one round to decide the winner
-            p1State' = p1State,
-            p2State' = p2State,
-            // Update the winner based on the current moves
-            updateWinner,
-
-        }  else all {
-            // Reset the game if it's not pending
-            p1State' = Init,
-            p2State' = Init,
-            game' = Started
-        }
-    }
-
-
-    // Conditions to determine the winner based on players' moves
-    val winCondition1 = (
-        (p1State == Paper and p2State == Rock)
-        or
-        (p1State == Rock and p2State == Scissor)
-        or
-        (p1State == Scissor and p2State == Paper)
-    )
-
-    val winCondition2 = (
-        (p2State == Paper and p1State == Rock)
-        or
-        (p2State == Rock and p1State == Scissor)
-        or
-        (p2State == Scissor and p1State == Paper)
-    )
-
-    // Invariant to check if the game status matches the expected winner
-    val winInv = (winCondition1 implies (game == Winner(PLAYER1)) or (winCondition2 implies (game == Winner(PLAYER2))))
-
-}
-
-module play_rock_paper_scissor {
-    import rock_paper_scissor(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*    
-}
\ No newline at end of file

From 30523c5a001321d7dd092fe8e68835d30ca68286 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Wed, 14 Aug 2024 15:59:04 -0400
Subject: [PATCH 08/14] fixed README

---
 examples/README.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/examples/README.md b/examples/README.md
index 8bc6ec079..183b6df69 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -54,7 +54,6 @@ listed without any additional command line arguments.
 | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt](./classic/distributed/RockPaperScissor/play_rock_paper_scissor.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

From 302ca6e321025360cb9d1bacfaca6229b66fd4ba Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Wed, 14 Aug 2024 16:34:56 -0400
Subject: [PATCH 09/14] added README for the example

---
 examples/games/rock_paper_scissors/README.md | 75 ++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 examples/games/rock_paper_scissors/README.md

diff --git a/examples/games/rock_paper_scissors/README.md b/examples/games/rock_paper_scissors/README.md
new file mode 100644
index 000000000..5a7181d14
--- /dev/null
+++ b/examples/games/rock_paper_scissors/README.md
@@ -0,0 +1,75 @@
+# Rock-Paper-Scissors Game Module
+
+This project implements a simple Rock-Paper-Scissors game, allowing two players to randomly select moves and determine the winner based on the traditional rules of the game.
+
+## Overview
+
+The `rock_paper_scissors` module provides the core functionality for the game, including:
+
+- **Player Setup:** Constants for player names.
+- **Game Logic:** Actions to decide player moves, determine the winner, and reset the game.
+- **Invariant Checking:** Ensures the game status reflects the expected winner based on the rules.
+
+The `play_rock_paper_scissors` module demonstrates how to import and use the `rock_paper_scissors` module with specific player names.
+
+## Components
+
+### Module: `rock_paper_scissors`
+
+This is the main module where the game logic resides.
+
+- **Constants:**
+  - `PLAYER1`: Name of the first player.
+  - `PLAYER2`: Name of the second player.
+
+- **Types:**
+  - `Move`: Enum representing possible moves: `Init`, `Rock`, `Paper`, `Scissors`.
+  - `GameStatus`: Enum representing the status of the game: `Started`, `Pending`, `Draw`, `Winner(str)`.
+
+- **Variables:**
+  - `p1State`: Current move of Player 1.
+  - `p2State`: Current move of Player 2.
+  - `status`: Current status of the game.
+
+- **Functions:**
+  - `beats(m1: Move, m2: Move): bool`: Determines if `m1` beats `m2` based on Rock-Paper-Scissors rules.
+
+- **Actions:**
+  - `init`: Initializes the game with both players in `Init` state and the game status as `Started`.
+  - `decide_moves`: Randomly selects moves for both players from the set of possible moves (`Rock`, `Paper`, `Scissors`) and updates the game status to `Pending`.
+  - `find_winner`: Determines the winner based on the players' moves and updates the game status to `Winner(PLAYER1)`, `Winner(PLAYER2)`, or `Draw`.
+  - `step`: The main game loop that progresses the game through different states (`Started`, `Pending`, etc.) and resets the game for a new round.
+
+- **Invariants:**
+  - `winInv`: Ensures the game status matches the expected winner based on the rules of Rock-Paper-Scissors.
+
+### Module: `play_rock_paper_scissors`
+
+This module imports the `rock_paper_scissors` module and assigns the player names:
+
+```bluespec
+import rock_paper_scissor(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*
+```
+
+## How It Works
+
+1.  **Initialization:**
+    - The game starts with both players in the Init state, and the game status is set to Started.
+
+2.  **Move Decision:**
+    - The `decide_moves` action randomly selects a move for each player and updates the game status to Pending.
+
+3.  **Determine Winner:**
+    - The `find_winner` action evaluates the moves and determines the winner or declares a draw.
+
+4.  **Game Progression:**
+    - The step action orchestrates the progression of the game from initialization to move decision, winner determination, and resetting for a new round.
+
+5.  **Invariant Checking:**
+    - The winInv invariant ensures that the game status correctly reflects the outcome of the moves.
+
+## Usage
+-  To run the spec, import the `rock_paper_scissors` module and specify the player names as shown in the `play_rock_paper_scissors` module.
+
+-  Run using the command:
+    - `quint run play_rock_paper_scissors.qnt --invariant=winInv`
\ No newline at end of file

From b15eafa591858d9a39170e05bc12fa2ddeb0cfc3 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Tue, 27 Aug 2024 01:30:21 -0400
Subject: [PATCH 10/14] changes made

---
 .../play_rock_paper_scissors.qnt              | 39 +++++++++++--------
 1 file changed, 23 insertions(+), 16 deletions(-)

diff --git a/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
index a8192f37b..e3c1b6bf7 100644
--- a/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
+++ b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
@@ -1,42 +1,45 @@
-// -*- mode: Bluespec; -*-
 module rock_paper_scissors {
     // Constants for player names
     const PLAYER1 : str
     const PLAYER2 : str
-    // Enum types for the possible moves and game status
-    type Move = Init | Rock | Paper | scissors
+    // Sum types for the possible moves and game status
+    type Move = Init | Rock | Paper | Scissors
     type GameStatus = Started | Pending | Draw | Winner(str)
     // Variables to hold the current state of each player's move and the game status
     var p1State: Move
     var p2State: Move
     var status: GameStatus
+
     def beats(m1: Move, m2: Move): bool = or {
-        (m1 == Rock and m2 == scissors),
+        (m1 == Rock and m2 == Scissors),
         (m1 == Paper and m2 == Rock),
-        (m1 == scissors and m2 == Paper),
+        (m1 == Scissors and m2 == Paper),
     }
-    // Initialize the game with both players in 'Init' state and game status as 'Started'
+    /// Initialize the game with both players in 'Init' state and game status as 'Started'
     action init = all {
         p1State' = Init,
         p2State' = Init,
         status' = Started
     }
-    // Randomly decide moves for both players from the set of possible moves
-    action decide_moves() = {
-        nondet move1 = Set(Rock, Paper, scissors).oneOf() // Non-deterministically pick a move for player 1
-        nondet move2 = Set(Rock, Paper, scissors).oneOf() // Non-deterministically pick a move for player 1
+
+    /// Randomly decide moves for both players from the set of possible moves
+    action decide_moves = {
+        nondet move1 = Set(Rock, Paper, Scissors).oneOf() // Non-deterministically pick a move for player 1
+        nondet move2 = Set(Rock, Paper, Scissors).oneOf() // Non-deterministically pick a move for player 2
         all {
             p1State' = move1,
             p2State' = move2,
             status' = Pending,
         }
     }
-    // Determine the winner based on the current moves of both players
-    action find_winner() = any {
+    
+    /// Determine the winner based on the current moves of both players
+    action find_winner = any {
         if (beats(p1State, p2State)) status' = Winner(PLAYER1) // Player 1 wins if their move beats player 2's move
         else if (beats(p2State, p1State)) status' = Winner(PLAYER2) // Player 2 wins if their move beats player 1's move
         else status' = Draw // It's a draw if both players chose the same move
     }
+
     action step = if (status == Started) {
         decide_moves
     } else if (status == Pending) all {
@@ -48,10 +51,14 @@ module rock_paper_scissors {
         p2State' = Init,
         status' = Started
     }
-    // Invariant to check if the game status matches the expected winner
-    val winInv = ((status == Winner(PLAYER1) implies beats(p1State, p2State)) and ((status == Winner(PLAYER2)) implies beats(p2State, p1State)))
+
+    /// Invariant to check if the game status matches the expected winner
+    val winInv = and {
+        status == Winner(PLAYER1) implies beats(p1State, p2State),
+        status == Winner(PLAYER2) implies beats(p2State, p1State),
+    }
 }
 
 module play_rock_paper_scissors {
-    import rock_paper_scissors(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*    
-}
\ No newline at end of file
+    import rock_paper_scissors(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").*
+}

From c333288b93160b1fbbc3623dfff58f8404753d77 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Tue, 27 Aug 2024 09:09:44 -0400
Subject: [PATCH 11/14] add bluespec

---
 examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
index e3c1b6bf7..06bee89a6 100644
--- a/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
+++ b/examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+
 module rock_paper_scissors {
     // Constants for player names
     const PLAYER1 : str

From 36c08a56d0b3f2187de062ec8d592110f879df16 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Tue, 27 Aug 2024 16:17:38 -0400
Subject: [PATCH 12/14] Add mafia game exmaple

---
 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..49874a0a2 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 13eb4c2d287ccf5fb8975f09dfc18dd98f8a3e9e Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Tue, 27 Aug 2024 16:50:42 -0400
Subject: [PATCH 13/14] remove wrong example

---
 examples/games/mafia-werewolf/play_mafia.qnt | 185 -------------------
 1 file changed, 185 deletions(-)
 delete mode 100644 examples/games/mafia-werewolf/play_mafia.qnt

diff --git a/examples/games/mafia-werewolf/play_mafia.qnt b/examples/games/mafia-werewolf/play_mafia.qnt
deleted file mode 100644
index a165a4c18..000000000
--- a/examples/games/mafia-werewolf/play_mafia.qnt
+++ /dev/null
@@ -1,185 +0,0 @@
-// -*- 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 7dc73d7e6d07b538183f0453b79340ecde1ef821 Mon Sep 17 00:00:00 2001
From: mahtab75 <norouzimahtab75@gmail.com>
Date: Tue, 27 Aug 2024 16:56:01 -0400
Subject: [PATCH 14/14] fix README

---
 examples/README.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/examples/README.md b/examples/README.md
index 49874a0a2..183b6df69 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -74,7 +74,6 @@ 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: |