電気ポットの「企画要求仕様」（リスト1）を題材にします。以下の5項目の要求が書かれています。
リスト1 企画要求仕様
PR01: 電気ポットの容量は2リットルとし、10度Cから沸騰するまでの時間は、15分以内とする。
PR02: 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90度Cに保温する。
PR03: 再沸騰ボタンが押されたら、再沸騰を始める。
PR04: 水が加えられ、温度が低下したら、再沸騰を始める。
PR05: 保温中であれば、お湯を注ぐことができる。
分析者は、5条項ポットの「企画要求仕様」を読んで、直接、Event-Bのモデルを書きました。まず、初期モデルのコンテキスト（リスト2）を書きました。「コンテキスト」とは、簡単に言うと、Event-Bのモデルで使用する定数を定義するところです。リスト2では「no_power_supply」「heat_until_boil」「keep_temperature」という3個の定数を定義しています。これらは、それぞれ、「電源が供給されていない」「沸騰するまで加熱する」「保温する」という、ポットの状態を表します。
リスト2 初期モデルのコンテキスト
CONTEXT
context_0
CONSTANTS
no_power_supply // 電源が供給されていない
heat_until_boil // 沸騰するまで加熱する
keep_temperature // 保温する
set_of_modes // ポットのモードの集合
AXIOMS
axm1 : no_power_supply = 0
axm2 : heat_until_boil = 1
axm3 : keep_temperature = 2
axm4 : set_of_modes =
{no_power_supply, heat_until_boil, keep_temperature}
END
続いて、初期モデルのマシン（リスト3）を書きました。「マシン」とは、モデルの「動き」を定義するところです。具体的には、変数とイベントを定義します。
リスト3 初期モデルのマシン
MACHINE
machine_0
SEES
context_0
VARIABLES
mode // ポットのモード
INVARIANTS
inv1 : mode ∈ set_of_modes
EVENTS
INITIALISATION ≙ // 初期状態を定義する。
STATUS
ordinary
BEGIN
act1 : mode ≔ no_power_supply // 初期状態では電源が供給されていない。
END
user_connects_power_plug ≙ // ユーザーが電源コンセントをつないだ。[PR02]
STATUS
ordinary
WHEN
grd1 : mode = no_power_supply // 電源が供給されていないとき。
THEN
act1 : mode ≔ heat_until_boil // 沸騰するまで加熱する。[PR02]
END
water_becomes_boil ≙ // 沸騰した。[PR02]
STATUS
ordinary
WHEN
grd1 : mode = heat_until_boil // ヒーターが加熱しているとき。
THEN
act1 : mode ≔ keep_temperature // 90°Cに保温せよ。[PR02]
END
user_pushes_boil_button ≙ // ユーザーが再沸騰ボタンを押した。[PR03]
STATUS
ordinary
WHEN
grd1 : mode = keep_temperature // 保温しているとき。もとの要求にはないが、このように推測できる。
THEN
act1 : mode ≔ heat_until_boil // 再沸騰せよ。[PR03]
END
user_pours_cold_water_into_pot ≙ // ユーザーがポットに水を注いだ。[PR04]
STATUS
ordinary
WHEN
grd1 : mode = keep_temperature // 保温しているとき。もとの要求にはないが、このように推測できる。
THEN
act1 : mode ≔ heat_until_boil // 再沸騰せよ。[PR04]
END
user_requires_discharging_hot_water ≙ // ユーザーがポットにお湯を注ぐことを要求した。[PR05]
STATUS
ordinary
WHEN
grd1 : mode = keep_temperature // 保温中であれば [PR05]
THEN
skip
END
END
さらに、第1次精義化モデルのコンテキスト（リスト4）を書きました。精義化とは、refinementの（当社での）訳語です。
リスト4 第1次精義化モデルのコンテキスト
CONTEXT context_1 EXTENDS context_0 CONSTANTS capacity_of_pot // ポットの容量 [ml] start_volume // 水量の初期値 [ml] start_temperature // 水温の初期値 [°C] AXIOMS axm1 : capacity_of_pot = 2000 // ポットの容量は2000 mlである。[PR01] axm2 : 0 < start_volume // 初期の数量は0ではない。 axm3 : start_volume ≤ capacity_of_pot // 初期の水量はポットの容量以下である。 axm4 : 0 ≤ start_temperature // 初期の水温は0°C以上である。 axm5 : start_temperature < 100 // 初期の水温は沸騰していない。 END
最後に、第1次精義化モデルのマシン（リスト5）を書きました。
リスト5 第1次精義化モデルのマシン
MACHINE
machine_1
REFINES
machine_0
SEES
context_1
VARIABLES
mode
volume // 水量 [ml]
temperature // 水温 [°C]
INVARIANTS
inv1 : 0 ≤ volume // 水量は0以上である。
inv2 : volume ≤ capacity_of_pot // 水量はポットの容量以下である。
inv3 : 0 ≤ temperature // 水温は0°C以上である。
inv4 : temperature ≤ 100 // 水温は0°C以下である。
EVENTS
INITIALISATION ≙
STATUS
ordinary
BEGIN
act1 : volume ≙ start_volume // 水量の初期状態を設定する。
act2 : temperature ≙ start_temperature // 水温の初期状態を設定する。
END
user_connects_power_plug ≙
STATUS
ordinary
REFINES
user_connects_power_plug
WHEN
grd1 : mode = no_power_supply
THEN
act1 : mode ≙ heat_until_boil
END
water_becomes_boil ≙
STATUS
ordinary
REFINES
water_becomes_boil
WHEN
grd1 : temperature = 100 // 水温が100°Cになった。（ただし、もとの要求からは読み取れない）
grd2 : mode = heat_until_boil
THEN
act1 : mode ≙ keep_temperature
END
user_pours_cold_water_into_pot ≙
STATUS
ordinary
REFINES
user_pours_cold_water_into_pot
WHEN
grd1 : mode = keep_temperature
grd2 : volume < capacity_of_pot
grd3 : 0 < temperature
THEN
act1 : volume :≙ volume < volume' ∧ volume' ≤ capacity_of_pot
act2 : temperature :≙ 0 ≤ temperature' ∧ temperature' < temperature
act3 : mode ≙ heat_until_boil
END
user_pushes_boil_button ≙
STATUS
ordinary
REFINES
user_pushes_boil_button
WHEN
grd1 : mode = keep_temperature
THEN
act1 : mode ≙ heat_until_boil
END
user_requires_discharging_hot_water ≙
STATUS
ordinary
REFINES
user_requires_discharging_hot_water
WHEN
grd1 : mode = keep_temperature
grd2 : 0 < volume
THEN
act1 : volume :≙ 0 ≤ volume' ∧ volume' < volume
END
water_becomes_hotter ≙
STATUS
ordinary
WHEN
grd1 : mode = heat_until_boil
grd2 : temperature < 100
THEN
act1 : temperature :≙ temperature < temperature' ∧ temperature' ≤ 100
END
water_becomes_cooler ≙
STATUS
ordinary
WHEN
grd1 : mode = keep_temperature
grd2 : 90 < temperature
THEN
act1 : temperature :≙ 90 ≤ temperature' ∧ temperature' < temperature
END
END
以上のEvent-Bのモデルは、5pot-eventb.zip [ZIP] を Rodin でインポートすると、モデルの正しさを証明することができます。
