今回は、「集合」を使って仕様を記述します。
1. 集合
集合は高校の数学でやっていると思いますし、分かりやすい説明ページがいくつもあるので、検索して確認しておいてください。
2. 今回記述する仕様
簡単な「座席予約システム」の仕様を記述してみます。
2.1. 日本語の仕様
- 座席予約システムは、ある劇場の座席を管理するシステムです。
- ユーザは座席の予約、キャンセルができます。
- システムは、座席の一覧と、予約済みの座席の一覧を管理しています。
- 座席には A 席と S 席の 2 種類があります。
- A 席と S 席の座席は、それぞれ 1 席以上あります。
- 座席の予約
- ユーザは A 席か S 席のどちらかを指定します。
- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
- 予約は、座席が余っているときのみ可能です。
- 座席のキャンセル
- ユーザは予約済みの座席を 1 つ指定します。
- システムは、指定された座席の予約をキャンセルします。
3. 状態空間の記述
それでは早速 Alloy で仕様を記述してみましょう。
流れは前回のボタンと同じです。
まずはシステムの状態空間を記述します。
3.1. システムのパラメータ
システムの状態空間は、前回やったように
sig System{
パラメータ
}
という形で記述します。
まずは座席予約システムのパラメータを決めます。
日本語の仕様を読むと、「システムは、座席の一覧と、予約済みの座席の一覧を管理しています。」とあるので、
の 2 種類が必要そうです。
座席は S 席と A 席の 2 種類があるので、
- S 席の座席の一覧
- A 席の座席の一覧
- 予約済みの座席の一覧
の 3 種類のパラメータを用意することにします。
3.2. パラメータの型
前回説明したように、パラメータは
名前 : 型
というフォーマットで記述します。
ということで、次はパラメータの型を決めます。
今回のパラメータはどれも「座席の一覧」です。
「座席の一覧」は座席の集まりなので、集合で表すことにします。
3.3. 集合
パラメータの値が集合になる場合、Alloy では以下のように記述します。
名前 : set 型
こう記述すると、パラメータの値は、指定した型の要素を 0 個以上集めた集合になります。
3.3.1. set の例
例えば、
xs : set Int
と書くと、xs の値は要素の数が 0 個以上の整数の集合になります。
xs は、{0, 1, 2}, {-1}, {} といった値になります。
3.3.2. 他のバリエーション
Alloy には set 以外にも some, one, lone といったバリエーションがあります。
3.3.2.1. some
要素の数が 1 個以上の集合になります。
set とは異なり空にはなりません。
3.3.2.2. one
要素の数が１個の集合になります。
なお、何も書かずに
名前 : 型
と書いたものは、
名前 : one 型
の省略型です。
前回ボタンの幅を
width : Int
と書きました。
width の値は 1, 2, 3 といった Int のどれか１個の要素になりそうですが、
実は Alloy では、{1}, {2}, {3} というように、要素ではなく、要素が１個の集合で表されます。
これは Alloy を使う上で非常に重要な概念なので、覚えておいてください。
3.3.2.3. lone
要素の数が 0 個か 1 個の集合になります。
3.4. 型定義
では次に、set や some の後ろに書く型を定義します。
今回は「座席の集合」なので、「座席」という型を定義します。
前回やったように、型は sig や enum を使って定義します。
「座席」の型の要素は具体的にまだ決まっていないので、enum ではなく、sig で定義します。
今回の座席はパラメータを持っていないので、単に
sig Seat{}
となります。
3.5. 具体的に記述
以上のことを踏まえると、今回のシステムの状態空間は以下のように記述することができます。
sig Seat{}
sig System{
A_seats : some Seat, //A 席の一覧
S_seats : some Seat, //S 席の一覧
reserved : set Seat //予約済みの座席の一覧
}
A 席と S 席は、日本語の仕様に「A 席と S 席の座席は、それぞれ 1 席以上あります。」とあるので、some にしました。
予約済みの座席の一覧は、誰も予約していない状態があり得るので、set にしました。
4. 状態空間の検査
前回同様
pred show{}
run show
でおかしな状態がないか確認してみます。
こんなインスタンスが見つかりました。
これは、Seatの要素が1個で、Systemの要素が0個のインスタンスです。
今はSystemの要素にどんなものが入っているかを確認したいので、うれしくないです。
Nextを押すと、今度はこんなインスタンスが見つかりました。
今度はSystemの要素が3個あるようです。
今はSystemの要素におかしなものが無いか、1個ずつ見て確認したいので、一度に3個表示されても見づらいだけです。
4.1. インスタンスの要素の数を指定する
こういう場合は、見つけてほしい要素の数を指定します。
具体的には run コマンドを以下のように書きます。
run show for 3 but exactly 1 System
これは、
sig の各要素は 3 個以下で探してください。
ただし、System の要素だけは 1 個で探してください。
ということを指定しています。
なお、今まで書いていた
run show
は、
run show for 3
と同じです。
4.2. 再度検査
今度は
run show for 3 but exactly 1 System
で検査してみます。
こんなインスタンスが見つかりました。
A 席と S 席に同じ Seat が含まれています。
これは期待していない状態です。
4.3. 不変条件の追加
期待しない状態は、不変条件で除きます。
同じ座席が A と S の両方に含まれることはない
という不変条件を追加します。
この条件は、集合の演算子を使って次のように記述することができます。
no (A_seat & S_seat)
これは、
A_seat と S_seat の共通部分は空である
という意味の論理式です。
4.4. 集合の演算子
Alloy の集合の演算子には以下のものがあります。
