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

6126 ワード
AlloyAnalyzer どう書く どう書く テキストリンク

第一回 オフラインリアルタイムどう書くの参考問題 より。
ポーカーの役判定を 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

リスト

// 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
}

結果例

フルハウス
　

役なし
　

追加

ポーカーの残り にも対応した版

// 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*の厳密さに差がある点も少し気になる。

ストレート
　

カードの指定方法

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

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

　

参考