※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

今回は「集合」を使って仕様を記述します。

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, lone, one といったバリエーションがあります。

3.3.2.1. some
要素の数が 1 個以上 の集合になります。
set とは異なり空にはなりません。

3.3.2.2. lone
要素の数が 0 個か 1 個 の集合になります。

3.3.2.3. one
要素の数が 1個 の集合になります。

なお、何も書かずに
名前 : 型
と書いたものは、
名前 : one 型
の省略型です。

前回ボタンの幅を
width : Int
と書きました。
width の値は 1, 2, 3 といった Int のどれか1個の要素になりそうですが、
実は Alloy では、{1}, {2}, {3} というように、要素ではなく、要素が1個の集合で表されます。
これは Alloy を使う上で 非常に重要な 概念なので、覚えておいてください。

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 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_seats & S_seats)
これは、
A_seat と S_seat の共通部分は空である
という意味の論理式です。

4.4. 集合の演算子

Alloy の集合の演算子には以下のものがあります。
演算子 構文 意味 結果の型
+ A + B A と B の和集合 集合
- A - B A から B を引いた差集合 集合
& A & B A と B の共通部分 集合
# #A A の濃度 (要素数) Int
= A = B A と B の要素はすべて等しい Bool
!= A != B A と B の要素は異なる Bool
in A in B A は B の部分集合である Bool
some some A A の要素は 1 個以上である Bool
one one A A の要素は 1 個である Bool
lone lone A A の要素は 1 個以下である Bool
no no A A の要素は 0 個である Bool
※ A と B の型は集合です。

4.5. 再度検査

先ほどの条件を不変条件に追加して、再度検査してみます。

何度かNextでインスタンスを確認していると、次のようなインスタンスが見つかりました。
A 席でも S 席でもない Seat0 が予約されています。
これは期待していない状態です。
予約されている座席は、A 席か S 席のどちらかの座席のはずです。

4.6. 不変条件の追加

不変条件に、
予約されている座席は、A 席か S 席のどちらかの座席である
という条件を追加します。

この条件は、集合の演算子を使って次のように書くことができます。
reserved in (A_seats + S_seats)

4.5. 再度検査

先ほどの条件を不変条件に追加して、再度検査してみます。
何度か Next を押してインスタンスを確認してみてもおかしな状態がでてこないので、OKとします。

4.6. 状態空間+不変条件完成

sig Seat{}

sig System{
	A_seats : some Seat,	//A 席の一覧
	S_seats : some Seat,	//S 席の一覧
	reserved : set Seat		//予約済みの座席の一覧
}
{
	no (A_seats & S_seats)	//同じ座席が A と S の両方に含まれることはない 
	reserved in (A_seats + S_seats)	//予約されている座席は、A 席か S 席のどちらかの座席である
}

pred show{}
run show for 3 but exactly 1 System


5. 振る舞いの記述/検査


5.1. 座席の予約

座席の予約の仕様を確認します。
  • ユーザは A 席か S 席のどちらかを指定します。
  • システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
  • 予約は、座席が余っているときのみ可能です。

5.1.1. 引数を決める

まずは pred の引数を決めます。

5.1.1.1. 入力パラメータ
入力として、A 席か S 席を指定しますが、指定するときの "A 席", "S 席"という名前を定義していないので定義します。
enum SeatType {A, S}

pred の引数で SeatType を受け取ります
pred reserve_seat(t : SeatType, 

5.1.1.2. 出力パラメータ
予約した座席をユーザに通知します
とあるので、引数で予約した座席を返すことにします。
pred reserve_seat(t : SeatType, rs : Seat

5.1.1.3. 事前と事後の状態
事前と事後の状態も、忘れず引数で定義しておきます。
pred reserve_seat(t : SeatType, rs : Seat, s, s' : System)
これで引数は完成しました。

5.1.2. 事後条件の記述

事後条件に関係する日本語の仕様は、次の2つです。
  • システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
  • 予約は、座席が余っているときのみ可能です。

まず1つ目について見ていきます。
  • システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
予約した座席 rs は、t で指定された方の座席なので、その条件を追加します。
t = A => rs in s.A_seats
t = S => rs in s.S_seats
それから、rs は事後の reserved に追加されているので、その条件を追加します。
s.reserved + rs = s'.reserved

次に2つ目について見ていきます。
  • 予約は、座席が余っているときのみ可能です。
つまり、事前の状態では、t で指定された方の座席のうち、 reserved に入っていない座席が 1 つ以上ある必要があります。
この条件は次のように書けます。
t = A => some (s.A_seats - s.reserved)
t = S => some (s.S_seats - s.reserved)

最後に、A席とS席自体は振る舞いの前後で変わらないという条件も忘れずに追加しておきます。
s'.A_seats = s.A_seats
s'.S_seats = s.S_seats

これで座席の予約の振る舞いが書けました。
pred reserve_seat(t : SeatType, rs : Seat, s, s' : System){	//t 予約する座席の種類, rs 予約された座席
	t = A => some (s.A_seats - s.reserved)
	t = S => some (s.S_seats - s.reserved)
	t = A => rs in s.A_seats
	t = S => rs in s.S_seats
	s.reserved + rs = s'.reserved
	s'.A_seats = s.A_seats
	s'.S_seats = s.S_seats
}

5.1.3. 振る舞いの検査

振る舞いが書けたので、前回と同じように目視で確認してみます。
run reserve_seat for 3 but exactly 2 System
振る舞いを確認するときは、System の要素は事前と事後の2個で十分なので、2個に制限しました。

検査すると、次のようなインスタンスが見つかりました。
ごちゃごちゃして見づらいですが、まずは System の要素について確認します。
System の要素は System0 と System1 の2つがあります。
事前と事後の状態はどちらも System1 で、System0 はゴミです。

座席を予約したはずなのに、なぜ事前と事後の状態が同じなのでしょうか?
予約した座席が reserved に追加されるので、状態は変わるはずです。
System1 をよく確認してみます。
  • Seat1, Seat2 が A 席で、Seat0 が S 席です。
  • Seat2 が予約されています。
  • 入力パラメータ t は A 席が指定されています。
  • 出力パラメータ rs は Seat2 が返ってきています。
つまり、事前の状態ですでに予約されている Seat2 が新しく予約された座席として返ってきています。

これは期待していないパターンなので、起こらないように次の条件を追加します。
! (rs in s.reserved)  //rs は事前の予約済みの座席に含まれていない

5.1.4. 再度検査

先ほどの条件を追加して検査すると、今度は次のようなインスタンスが見つかりました。
今度は事前と事後の状態が変わっています。
事前の状態が System1 で、事後の状態が System0 です。
ですが相変わらずごちゃごちゃして見づらいです。

5.1.4.1. Projection
要素が複数あってごちゃごちゃして見づらいときは、要素の1つ1つにフォーカスしてインスタンスを見ることができます。
右上の [Projection] ボタンを押して、[System] にチェックを入れてください。
そうすると、次のような画面に変わり、System の要素1つ1つにフォーカスしてインスタンスを確認することができます。
これは、System0 (事後の状態) のインスタンスが表示されています。
  • 入力パラメータ (t) では、S 席が指定されている
  • Seat1 が A 席
  • Seat0 が S 席で、予約済みの座席 (reserved) で、今回予約された座席 (rs)
こっちの表示の方が見やすいと思います。

System1 (事前の状態) も確認してみましょう。
表示を System1 に切り替えるには、画面下のドロップダウンリストで System1 を選択します。
System1 (事前の状態) は次のようになっています。
  • 入力パラメータ (t) では、S 席が指定されている
  • Seat1 が A 席
  • Seat0 が S 席で、今回予約されようとしている座席 (rs)

事前の状態と事後の状態を見比べると、このインスタンスは期待どおりの振る舞いになっているようです。
同様にして Next で他のインスタンスも確認してみましたが、おかしなパターンがでてこないので、OKとします。

5.1.5. 座席の予約の振る舞い完成

pred reserve_seat(t : SeatType, rs : Seat, s, s' : System){	//t 予約する座席の種類, rs 予約された座席
	! (rs in s.reserved)  //rs は事前の予約済みの座席に含まれていない

	t = A => some (s.A_seats - s.reserved)
	t = S => some (s.S_seats - s.reserved)
	t = A => rs in s.A_seats
	t = S => rs in s.S_seats
	s.reserved + rs = s'.reserved
	s'.A_seats = s.A_seats
	s'.S_seats = s.S_seats
}
run reserve_seat for 3 but exactly 2 System

5.2. 座席のキャンセルの振る舞い

座席のキャンセルの仕様を確認します。
  • ユーザは予約済みの座席を 1 つ指定します。
  • システムは、指定された座席の予約をキャンセルします。

5.2.1. 引数を決める

入力パラメータは座席で、出力パラメータは無いので、次のようになります。
pred cancel_seat(st : Seat, s, s' : System)

5.2.2. 事後条件の記述

指定された座席を予約済みの座席から外して、他は変わらないとします。
指定される座席は予約済みとします。
pred cancel_seat(st : Seat, s, s' : System){	//st キャンセルしたい座席
	st in s.reserved

	s'.reserved = s.reserved - st
	s'.A_seats = s.A_seats
	s'.S_seats = s.S_seats
}
run cancel_seat for 3 but exactly 2 System

5.2.3. 振る舞いの検査

何度か Next でインスタンスを確認してみましたが、おかしなパターンが出てこないので OK とします。


6. まとめ


6.1. 最終的な仕様

今回の仕様は、最終的に次のようになりました。
sig Seat{}

enum SeatType{A, S}

sig System{
	A_seats : some Seat,	//A 席の一覧
	S_seats : some Seat,	//S 席の一覧
	reserved : set Seat		//予約済みの座席の一覧
}
{
	no (A_seats & S_seats)	//同じ座席が A と S の両方に含まれることはない 
	reserved in (A_seats + S_seats)	//予約されている座席は、A 席か S 席のどちらかの座席である
}

pred show{}
run show for 3 but exactly 1 System

// 座席の予約の振る舞い
pred reserve_seat(t : SeatType, rs : Seat, s, s' : System){	//t 予約する座席の種類, rs 予約された座席
	! (rs in s.reserved)  //rs は事前の予約済みの座席に含まれていない

	t = A => some (s.A_seats - s.reserved)
	t = S => some (s.S_seats - s.reserved)
	t = A => rs in s.A_seats
	t = S => rs in s.S_seats
	s.reserved + rs = s'.reserved
	s'.A_seats = s.A_seats
	s'.S_seats = s.S_seats
}
run reserve_seat for 3 but exactly 2 System

// 座席のキャンセルの振る舞い
pred cancel_seat(st : Seat, s, s' : System){	//st キャンセルしたい座席
	st in s.reserved	

	s'.reserved = s.reserved - st
	s'.A_seats = s.A_seats
	s'.S_seats = s.S_seats
}
run cancel_seat for 3 but exactly 2 System

6.2. 元の仕様の問題点

今回は元の仕様に次のような問題がありました。
  • 同じ座席が A 席と S 席の両方に含まれることはないということが書かれていなかった
  • 予約されている座席は、A 席か S 席のどちらかの座席であることが書かれていなかった
  • 予約済みの座席は予約できないことが書かれていなかった

6.3. 今回新しく説明した内容

  • 集合
  • 検査コマンドでインスタンスの要素数を指定する方法
  • Projection してインスタンスを見る方法

6.4. 次回予告

次回は「関係」をやります。