Alloy model of the play flow of the card game For The Queen

queen.als

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