Add rock-paper-scissors game example #1479
Conversation
| @@ -0,0 +1,109 @@ | |||
|
|
|||
There was a problem hiding this comment.
We can add this line to the start of a Quint file to instruct GitHub to highlight it as bluespec, which is better than no highlighting at all (and we don't have highlighting for Quint in GitHub yet)
| // -*- mode: Bluespec; -*- |
| (p1State == Rock and p2State == Scissor) or | ||
| (p1State == Paper and p2State == Rock) or | ||
| (p1State == Scissor and p2State == Paper) |
There was a problem hiding this comment.
We could use winCondition1 here
| // 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 |
There was a problem hiding this comment.
| nondet move2 = 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 2 |
| var p1State : Move | ||
| var p2State : Move | ||
| var game : GameStatus |
There was a problem hiding this comment.
In general, modern languages don't have spaces between name and type, so I prefer not to add those
| var p1State : Move | |
| var p2State : Move | |
| var game : GameStatus | |
| var p1State: Move | |
| var p2State: Move | |
| var game: GameStatus |
There was a problem hiding this comment.
I think this fits much better under examples/games.
| ) | ||
|
|
||
| // Invariant to check if the game status matches the expected winner | ||
| val winInv = (winCondition1 implies (game == Winner(PLAYER1)) or (winCondition2 implies (game == Winner(PLAYER2)))) |
There was a problem hiding this comment.
This should be an and, as both implications need to hold!
| val winInv = (winCondition1 implies (game == Winner(PLAYER1)) or (winCondition2 implies (game == Winner(PLAYER2)))) | |
| val winInv = (winCondition1 implies (game == Winner(PLAYER1)) and (winCondition2 implies (game == Winner(PLAYER2)))) |
| // Constants for player names | ||
| const PLAYER1 : str | ||
| const PLAYER2 : str | ||
| // Enum types for the possible moves and game status |
There was a problem hiding this comment.
These are technically sum types (although there's a pretty blurred line between them, we call it sum types in Quint, so it's good to be consistent in the examples)
| // Enum types for the possible moves and game status | |
| // Sum types for the possible moves and game status |
| const PLAYER1 : str | ||
| const PLAYER2 : str | ||
| // Enum types for the possible moves and game status | ||
| type Move = Init | Rock | Paper | scissors |
There was a problem hiding this comment.
Scissors should be capitalized like the others
| type Move = Init | Rock | Paper | scissors | |
| type Move = Init | Rock | Paper | 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' |
There was a problem hiding this comment.
If you use triple slashes /// instead of double // on comments that immediately precede a definition, that comment is treated as a doc-comment. This means that, in your editor, if you hover over definition names, it will show this comment as the documentation for that name 😄. Not super important, but cool to know.
| // 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' |
| p2State' = Init, | ||
| status' = Started | ||
| } | ||
| // Randomly decide moves for both players from the set of possible moves |
There was a problem hiding this comment.
| // Randomly decide moves for both players from the set of possible moves | |
| /// Randomly decide moves for both players from the set of possible moves |
| // 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 |
There was a problem hiding this comment.
| nondet move2 = 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 |
| p2State' = Init, | ||
| status' = Started | ||
| } | ||
| // Invariant to check if the game status matches the expected winner |
There was a problem hiding this comment.
| // Invariant to check if the game status matches the expected winner | |
| /// Invariant to check if the game status matches the expected winner |
|
|
||
| module play_rock_paper_scissors { | ||
| import rock_paper_scissors(PLAYER1 = "Mahtab", PLAYER2 = "Gabriela").* | ||
| } |
There was a problem hiding this comment.
We should always have a linebreak at the end of the file to make GitHub happy. I have a config on my editors to automate this
| } | |
| } | |
examples/games/rock_paper_scissors/play_rock_paper_scissors.qnt
Outdated
Show resolved
Hide resolved
romac
changed the title
CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality