# Exercise: card game

**URL:** <https://alloytools.discourse.group/t/exercise-card-game/172>\
**Category:** Questions\
**Created:** [August 2, 2021, 12:26pm UTC](https://alloytools.discourse.group/t/exercise-card-game/172 "2021-08-02T12:26:05Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![christian.lavoie](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/christian.lavoie/32/9_2.png) [@christian.lavoie](https://alloytools.discourse.group/u/christian.lavoie)\
**Post date:** [August 2, 2021, 12:26pm UTC](https://alloytools.discourse.group/t/exercise-card-game/172/1 "2021-08-02T12:26:05Z")

</div>

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?

```auto
// 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() {}

```

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [August 2, 2021, 2:25pm UTC](https://alloytools.discourse.group/t/exercise-card-game/172/2 "2021-08-02T14:25:54Z")

</div>

I think the following fact enforces your complete `SuitedCard`

```auto
  fact {
	{ s:Suit,v:Value | (one c : SuitedCard | c.suit=s and c.value=v) } = Suit->Value
  }

```

You might want to run it with `run {} for 4 but 52 SuitedCard, 7 int`

```auto
┌───────────────┬────────┬──────┐
│this/SuitedCard│suit │value │
├───────────────┼────────┼──────┤
│SuitedCard⁰ │Stars⁰ │Ace⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹ │Stars⁰ │King⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁰ │Pagodas⁰│N9⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹¹ │Pagodas⁰│N8⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹² │Stars⁰ │Queen⁰│
├───────────────┼────────┼──────┤
│SuitedCard¹³ │Pagodas⁰│N7⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁴ │Pagodas⁰│N6⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁵ │Pagodas⁰│N5⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁶ │Pagodas⁰│N4⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁷ │Pagodas⁰│N3⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁸ │Pagodas⁰│N2⁰ │
├───────────────┼────────┼──────┤
│SuitedCard¹⁹ │Swords⁰ │Ace⁰ │
├───────────────┼────────┼──────┤
│SuitedCard² │Stars⁰ │N4⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁰ │Swords⁰ │King⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²¹ │Swords⁰ │Queen⁰│
├───────────────┼────────┼──────┤
│SuitedCard²² │Swords⁰ │Jack⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²³ │Stars⁰ │Jack⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁴ │Swords⁰ │N10⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁵ │Swords⁰ │N9⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁶ │Swords⁰ │N8⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁷ │Swords⁰ │N7⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁸ │Swords⁰ │N6⁰ │
├───────────────┼────────┼──────┤
│SuitedCard²⁹ │Swords⁰ │N5⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³ │Stars⁰ │N3⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁰ │Swords⁰ │N4⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³¹ │Swords⁰ │N3⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³² │Swords⁰ │N2⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³³ │Jade⁰ │Ace⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁴ │Stars⁰ │N10⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁵ │Jade⁰ │King⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁶ │Jade⁰ │Queen⁰│
├───────────────┼────────┼──────┤
│SuitedCard³⁷ │Jade⁰ │Jack⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁸ │Jade⁰ │N10⁰ │
├───────────────┼────────┼──────┤
│SuitedCard³⁹ │Jade⁰ │N9⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴ │Stars⁰ │N2⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁰ │Jade⁰ │N8⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴¹ │Jade⁰ │N7⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴² │Jade⁰ │N6⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴³ │Jade⁰ │N5⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁴ │Jade⁰ │N4⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁵ │Stars⁰ │N9⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁶ │Jade⁰ │N3⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁷ │Jade⁰ │N2⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁸ │Stars⁰ │N8⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁴⁹ │Stars⁰ │N7⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁵ │Pagodas⁰│Ace⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁵⁰ │Stars⁰ │N6⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁵¹ │Stars⁰ │N5⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁶ │Pagodas⁰│King⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁷ │Pagodas⁰│Queen⁰│
├───────────────┼────────┼──────┤
│SuitedCard⁸ │Pagodas⁰│Jack⁰ │
├───────────────┼────────┼──────┤
│SuitedCard⁹ │Pagodas⁰│N10⁰ │
└───────────────┴────────┴──────┘

```

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [August 4, 2021, 7:47pm UTC](https://alloytools.discourse.group/t/exercise-card-game/172/3 "2021-08-04T19:47:52Z")

</div>

I give examples in my [book](http://softwareabstractions.org) of this kind of “canonicalization” constraint. I think you could simplify Peter’s constraint to something like

`all s:Suit,v:Value | some c : SuitedCard | c.suit=s and c.value=v`

since there’s probably no need to insist on at most one.

The bigger question is why you need to canonicalize at all. One of the insights of Alloy is that it’s almost never needed, and you can get a lot of fast analysis and compelling examples without it. So I’d suggest that you try to put aside any preconceptions about what the space of instances should look like, and instead ask yourself: what’s an interesting scenario I might simulate, or property I might check?

---

<div class="post-metadata">

**Author:** ![christian.lavoie](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/christian.lavoie/32/9_2.png) [@christian.lavoie](https://alloytools.discourse.group/u/christian.lavoie)\
**Post date:** [August 5, 2021, 3:25pm UTC](https://alloytools.discourse.group/t/exercise-card-game/172/4 "2021-08-05T15:25:31Z")

</div>

Yeah, that’s a fair point – right now I’m more interested in figuring out the language’s basics’ exact semantics than anything else, even sometimes doing something “wrong” on purpose 😉

Thanks all, very helpful.
