Alloyで書こう：ポーカーの役判定 

[第一回 オフラインリアルタイムどう書くの参考問題](https://qiita.com/Nabetani/items/cbc3af152ee3f50a822f) より。
ポーカーの役判定を Alloy ではどう書くか、やってみた。

# 問題
> 5枚のカードを示す文字列を入力とし、ポーカーの役を出力せよ。
ただし:
>
> - 一枚のカードは、スートを表す文字＋ランクを表す文字列 で構成される。
- スートを表す文字は、S, H, D, C のいずれか
- ランクを表す文字列は、2, 3, ..., 9, 10, J, Q, K, A のいずれか
- 下表の役に対応すること。下表の役に該当しない場合は '--' を出力すること。
- カードはジョーカーを含まない52枚から5枚が選ばれる。
- 不正な入力への対応は不要。
>
> 対応すべき役と、その役だった場合に出力する文字列は以下のとおり：
>
- フォーカード : 4K
- フルハウス : FH
- スリーカード : 3K
- ツーペア : 2P
- ワンペア : 1P
- 上記のいずれにも該当しない : --
>
例えば、入力が「D3C3C10D10S3」ならフルハウスなので「FH」と出力する。
入力が「S8D10HJS10CJ」ならツーペアなので「2P」と出力する。

入力や出力が Alloy 向きでないので少し読み替える。

- ５枚のカードは自動生成にまかせる  
`run`時に必要なだけ与えても良い
- 数字で始まるランクは`N2`..`N10`に変える
- 役名も`FourCard`,`FullHouse`等に変える
- 役なしは判定`none`

# リスト
```alloy
// Poker judge

enum Suit { S,H,D,C }
enum Rank { A,N2,N3,N4,N5,N6,N7,N8,N9,N10,J,Q,K }
sig Card {
	suit: Suit,
	rank: Rank
}
fact 同じカードを含まない {
	no disj a,b:Card | (a.suit=b.suit) && (a.rank=b.rank)
}

enum Hand { FourCard,FullHouse,ThreeCard,TwoPair,OnePair }
one sig Poker {
	hand: lone Hand
} {
	isFourCard => hand=FourCard
	else isFullHouse => hand=FullHouse
	else isThreeCard => hand=ThreeCard
	else isTwoPair => hand=TwoPair
	else isOnePair => hand=OnePair
	else hand=none
}

run {} for exactly 5 Card

pred isFourCard {
	some disj a,b,c,d:Card | one (a+b+c+d).rank
}

pred isFullHouse {
	some disj a,b,c,d,e:Card | (one (a+b+c).rank) && (one (d+e).rank)
}

pred isThreeCard {
	some disj a,b,c:Card | one (a+b+c).rank
}

pred isTwoPair {
	some disj a,b,c,d:Card | (one (a+b).rank) && (one (c+d).rank)
}

pred isOnePair {
	some disj a,b:Card | a.rank=b.rank
}
```

# 結果例

フルハウス
　![Poker1.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/e2f36e4d-31f0-c7b2-947c-ed8b502dbea9.png)

役なし
　![Poker2.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/c9a02602-460e-fa73-ac25-f4cc9b53f415.png)


# 追加

[ポーカーの残り](http://nabetani.sakura.ne.jp/hena/ord10pokarest/) にも対応した版

```alloy
// Poker judge

enum Suit { S,H,D,C }
enum Rank { A,N2,N3,N4,N5,N6,N7,N8,N9,N10,J,Q,K }
sig Card {
    suit: Suit,
    rank: Rank
}
fact 同じカードを含まない {
    no disj a,b:Card | (a.suit=b.suit) && (a.rank=b.rank)
}

enum Hand { RoyalFlash,StraitFlash,Flash,Strait,FourStraitFlash,FourFlash,FourStrait,
            FourCard,FullHouse,ThreeCard,TwoPair,OnePair }
one sig Poker {
    hand: lone Hand
} {
    isRoyalFlash => hand=RoyalFlash
    else isStraitFlash => hand=StraitFlash
    else isFlash => hand=Flash
    else isStrait => hand=Strait
    else isFourStraitFlash => hand=FourStraitFlash
    else isFourFlash => hand=FourFlash
    else isFourStrait => hand=FourStrait
    else isFourCard => hand=FourCard
    else isFullHouse => hand=FullHouse
    else isThreeCard => hand=ThreeCard
    else isTwoPair => hand=TwoPair
    else isOnePair => hand=OnePair
    else hand=none
}

run {} for exactly 5 Card

pred sameSuit[cards:set Card] { one cards.suit }
pred sameRank[cards:set Card] { one cards.rank }
let nextRank = Rank<:next + K->A    // 次のランク（Kの次はA）
pred strait[cards:set Card] {
    #cards > 1
    #(cards.rank & cards.rank.nextRank) = prev[#cards]
    #rank.(K+N2) < 2
}

pred isRoyalFlash { isFlash && (Card.rank = (N10+J+Q+K+A)) }
pred isStraitFlash { isFlash && isStrait }
pred isFlash { sameSuit[Card] }
pred isStrait { strait[Card] }
pred isFourStraitFlash { one a:Card | sameSuit[Card-a] && strait[Card-a] }
pred isFourFlash { one a:Card | sameSuit[Card-a] }
pred isFourStrait { one a:Card | strait[Card-a] }
pred isFourCard { one a:Card | sameRank[Card-a] }
pred isFullHouse { some disj a,b,c,d,e:Card | sameRank[a+b+c] && sameRank[d+e] }
pred isThreeCard { some disj a,b,c:Card | sameRank[a+b+c] }
pred isTwoPair { some disj a,b,c,d:Card | sameRank[a+b] && sameRank[c+d] }
pred isOnePair { some disj a,b:Card | sameRank[a+b] }
```
`strait`の記述に説明が必要そうなところが、仕様記述としては今ひとつか。
また、`is*`の厳密さに差がある点も少し気になる。

ストレート
　![Poker3.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/07e61f68-c424-7109-ff89-51b7f30bfb7a.png)



# カードの指定方法

`run`時にカードを指定するにはこのように書く。

```alloy
fun card[r:Rank,s:Suit] : Card { {c:Card | c.rank=r && c.suit=s} }

Sample00 : run {   // Qs9s3dJd10h -> 4S
    Card = card[Q,S] + card[N9,S] + card[N3,D] + card[J,D] + card[N10,H]
} for exactly 5 Card
```
　![Poker4.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/20005/c6e9dff7-603f-68e9-dff7-a1179510fa1b.png)

# 参考

- [オフラインどう書く第1回参考問題　第10回参考問題　CodeIQ:カードゲームの役を判定する](https://qiita.com/smallbigcats/items/20578165933c370bb4d0)
- [第一回 オフラインリアルタイムどう書くの参考問題](https://qiita.com/Nabetani/items/cbc3af152ee3f50a822f)
- [ポーカーの残り](http://nabetani.sakura.ne.jp/hena/ord10pokarest/)