Alloyの seq キーワードの使いどころと注意点

Alloy Analyzer

前回扱った仕様の完全版を記述してみます。


＜仕様＞

  • 何枚かの"くちばし" があります。くちばしには、金、銀、黄色、の三種の色分けがあります。
  • 金のくちばし1つにつき、缶詰め1つと交換できます。
  • 銀のくちばし5つにつき、缶詰め1つと交換できます。

これ、数の指定がありますね。指定した数だけ、集合から要素を切り出すには、どうしたらいいんでしょう。

教科書である『抽象によるソフトウェア設計−Alloyではじめる形式手法−』の、
329ページによると、seq というキーワードをつけると、その対象の集合の各要素に番号が振られ、
そしてその集合に対して、配列操作的ないくつかの関数が使えるようになるようです。これだ！

ただし、これ、教科書のとおりに

sig Book {}
sig Person {
  books: seq Book
}

こう書いただけだと、


こんなことになってしまいます。
番号と、番号が振られるモデルインスタンスが、1対1にならないんですね。

うーん、これは

sig Person {
  books: seq Book
} {
  #(books.inds) = #(books.elems)
}

こうして、個数を制限することで回避することにします。inds() は、indexつまり配列の添え字だけ取り出す関数、
elms() は、seq が指し示すモデルインスタンスだけを取得する関数です。（他にもっといい回避方法あるかな？）

さて、これで seq キーワードを使う準備ができました。

今回の記述では、「缶詰め」をいくつか、フィールドとして保持する状態空間があるとして、
そのフィールドに対して、seq をつけてみます。ひとつのフィールドに対して、シーケンス番号つきの別な
アクセス経路を開いたかたちです。こうすることで、

”その缶詰め群のうち、n番目からm番目まで”

という指定で、要素を取得することでできるようになります。（subseq 関数を使用。）
つまり、手持ちのくちばしが、
GOLD 1枚、SILVER 2枚、YELLOW 5枚、だったら、対象の缶詰め配列の、0番目から0番目までが自分の取り分です。
GOLD 1枚、SILVER 7枚、YELLOW 15枚、だったら、対象の缶詰め配列の、0番目から1番目までが自分の取り分です。

以下がその全文です。

enum Color {GOLD, SILVER, YELLOW}
some sig Beak {
  color: one Color
}
some sig Can {}

-- 取得したCanを保持した状態空間
abstract sig Bag { have : some Can }
one sig MyBefore extends Bag {}
one sig MyAfter extends Bag {}
one sig Stock extends Bag {
  haveAccessor: seq have
} {
  // ※番号とインスタンスの組を1対1にするために
  #(haveAccessor.inds) = #(haveAccessor.elems)
  // ※have と、haveAccessor が指すものは同一。
  have = haveAccessor.elems
}
// ※状態の定義にかかわるfact
fact theirsOrMine {
  // ※取得済み缶詰めと、未取得缶詰めは互いに素
  MyBefore.have & Stock.have = none
}
fact whatIsAfter {
  all stock:Stock, before:MyBefore, after:MyAfter | 
     getCan[stock] + before.have = after.have
}

-- 定数
one sig Number {
  silverRate : one Int,
  goldRate : one Int
} {
  silverRate = 5
  goldRate = 1
}

-- くちばしと缶詰めの交換ロジック
fun getCan(stock:Stock) : some Can {
  stock.haveAccessor.subseq[
    0, 
    plus[
      div[
        #(color & (Beak -> SILVER)), 
        Number.silverRate
      ], 
      div[
        #(color & (Beak -> GOLD)), 
        Number.goldRate
      ]
    ].minus[1]
  ].elems
}


// ※ご都合主義的に、在庫を潤沢に確保
fact 在庫を潤沢に確保 { #(Stock.have) >= #(Beak)}
// ※くちばしもある程度数確保
fact くちばしもある程度数確保 { #(Beak) >= 7}
// 
run {} for 8


このように、
「個数」を指定した配列操作を表現したいときは、seq キーワードをつけると、s.subseq() が使えて便利でした。
seq キーワードを使うときは、番号と、番号が振られるモデルインスタンスが、1対1になるように細工が必要ではありますが。