For pedagogical reasons, I’m trying to model a well known card game (Tichu) with the model below.
The problem I’m facing is that the SuitedCard signature doesn’t seem to be populated with the full set of cards (a Tichu deck is basically a normal 52 cards deck with 4 special cards added); I’d like the cross product for Suit X Value to be available at all times.
I’ve played with large scope numbers (I understand it might be horribly slow) and thought about using a set comprehension expression but haven’t quite figured out the syntax to do what I want:
{ s: Suit, v: Value | SuitedCard[s, v] } // incorrect syntax
I’m afraid I’m likely both using Alloy for something a little bit outside of its core domain, and probably missing something really obvious. Any pointers?
// Suits
enum Suit { Jade, Swords, Pagodas, Stars }
enum Value { N2, N3, N4, N5, N6, N7, N8, N9, N10, Jack, Queen, King, Ace }
// Cards
abstract sig Card {}
one sig Hound, Phoenix, Dragon, MahJong extends Card {}
sig SuitedCard extends Card {
value: Value,
suit: Suit
}
fact {
all x, y: SuitedCard |
x != y implies
(x.value != y.value or x.suit != y.suit)
}
// Players
abstract sig Player {}
one sig Alice, Bob, Carol, Dave extends Player {
hand: disj SuitedCard
}
// State
sig State {
players: some Player
}
fact { State.players = Alice + Bob + Carol + Dave }
fact { Card + SuitedCard = Alice.hand + Bob.hand + Carol.hand + Dave.hand }
pred show() {}
