Skip to content

Instantly share code, notes, and snippets.

@clarkenciel
Last active December 31, 2020 21:17
Show Gist options
  • Save clarkenciel/1c349fe439b2f0766bffd0087694b493 to your computer and use it in GitHub Desktop.
Save clarkenciel/1c349fe439b2f0766bffd0087694b493 to your computer and use it in GitHub Desktop.
Alloy model of the play flow of the card game For The Queen
module queen
open util/time
open util/ordering[Player]
abstract sig Card{}
sig NormalCard extends Card{}
one sig FinalCard extends Card{}
sig Player{ succ : one Player }
fact playersAreRing { all t : Player | Player in t.^succ }
abstract sig Action{}
one sig Pass extends Action{}
one sig Nix extends Action{}
one sig Play extends Action{}
sig GameState {
deck : set Card,
nixed : set Card,
players : set Player,
speaker : one Player,
card: one Card,
action : one Action,
} { speaker in players }
pred drewCard [now, later : GameState] {
later.card in now.deck
later.card not in now.nixed
later.card != now.card
later.deck in now.deck
}
pred nixedCard [now, later : GameState] {
now.card in later.nixed
now.card not in later.deck
now.card != later.card
now.nixed in later.nixed
later.nixed in (now.nixed + now.card)
}
pred maintainedCard [now, later : GameState] {
now.nixed = later.nixed
now.deck = later.deck
now.card = later.card
}
pred cardInHand [g : GameState] {
g.card not in g.deck + g.nixed
}
pred advancedSpeaker [now, later : GameState] {
later.speaker = now.speaker.succ
}
pred maintainedSpeaker [now, later : GameState] {
later.speaker = now.speaker
}
pred played [now : GameState] {
now.action = Play
}
pred played [now, later : GameState] {
cardInHand [now]
played [now]
advancedSpeaker [now, later]
drewCard [now, later]
nixedCard [now, later]
cardInHand [later]
}
pred nixed [now : GameState] {
now.action = Nix
}
pred nixed [now, later : GameState] {
cardInHand [now]
nixed [now]
maintainedSpeaker [now, later]
nixedCard [now, later]
drewCard [now, later]
cardInHand [later]
}
pred passed [now : GameState] {
now.action = Pass
}
pred passed [now, later : GameState] {
cardInHand [now]
passed [now]
maintainedCard [now, later]
advancedSpeaker [now, later]
cardInHand [later]
}
pred over [now : GameState] {
now.card = FinalCard
}
sig Game { state : dynamic [GameState] }
fact oneGame { one Game }
fact finalCardEnds { all t : Time, g : Game | over[g.state.t] => t = last }
fact statesDontRepeat { all t : Time, g : Game | g.state.t != g.state.(t.next) }
pred init [t : Time] {
no Game.state.t.nixed
some Game.state.t.deck
Game.state.t.card not in Game.state.t.nixed
Game.state.t.card not in Game.state.t.deck
Game.state.t.card != FinalCard
Game.state.t.speaker = first
}
fact trace {
init[first]
all t : Time - first, t' : t.prev, g : Game |
let now = g.state.t', later = g.state.t {
over [now] => t = last else
(played [now, later]) or
(nixed [now, later]) or
(passed [now, later])
}
}
check nixedCardsNeverInDeck {
all t : Time, g : Game |
some g.state.t.nixed => {
g.state.t.nixed not in g.state.t.deck
}
}
check drawnCardNeverNixed {
all t : Time, g : Game |
some g.state.t.nixed => {
g.state.t.card not in g.state.t.nixed
}
}
check drawnCardNeverInDeck {
all t : Time, g : Game |
some g.state.t.deck => {
g.state.t.card not in g.state.t.deck
}
}
check drawnCardComesFromDeckOrPriorTurn {
all t : Time - first, g : Game | let t' = t.next |
g.state.t'.card in g.state.t.deck or
g.state.t'.card = g.state.t.card
}
check nixedCardsWereInDeckOrHand {
all t : Time - first, g : Game |
let history = t.^prev |
all c : g.state.t.nixed |
c in (g.state.history.deck + g.state.history.card)
}
check speakerFromPlayerSet {
all t : Time, g : Game |
g.state.t.speaker in g.state.t.players
}
fun totalCards [g : GameState]: set Card {
g.deck & g.nixed & g.card
}
check neverLoseCards {
all t : Time, g : Game | let t' = t.prev, now = g.state.t', later = g.state.t |
totalCards[now] = totalCards[later]
}
check finalCardEndsGame {
all t : Time, g : Game | let now = g.state.t |
now.card = FinalCard => t = last
}
run{ one card.FinalCard } for 5 but exactly 1 FinalCard
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment