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)
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 の要素は事前と事後の２個で十分なので、２個に制限しました。
検査すると、次のようなインスタンスが見つかりました。
ごちゃごちゃして見づらいですが、まずは System の要素について確認します。
System の要素は System0 と System1 の２つがあります。
事前と事後の状態はどちらも System1 で、System0 はゴミです。
事前の状態と事後の状態を見比べると、このインスタンスは期待どおりの振る舞いになっているようです。
同様にして 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
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
