前回は、MBTツール「MISTA」でブロックゲームのシンプルなモデルを描いてみて、シミュレーションで一手進めたところまでを見ました。
トークンとイベントの関係とは
上の状態から、もう一度pickup(x)を選んで遷移させてみましょう。
2つのトークンが、プレースholdingにあります。つまり、「2つのブロックがともに、アームにつかまれているという状態です。
これは、「一度につかめるブロックは一つだけ」というルールに反していますね。つまりモデルに不備があるということです。
実はこのファンクションネットが表しているのは、
プレース
ontableにあるトークンに対し、イベントpickupを行うと、プレースholdingに遷移する
というよりは、
プレース
ontableにトークンがあるという条件を満たせば、イベントpickupが実行可能になり、プレースholdingに遷移させることができる
だと理解した方が正しいと思います。
一般的な表現にすると、
- あるイベントを起こすためには、そのイベントに流入するすべてのプレースにトークンが存在していないといけない
- そのすべてのトークンは、イベント発生後に、次のプレースに移動する
ということになります。
条件を追加していく
pickup(x)を実行可能にするために必要な条件を、プレースと矢印で表現する必要があります。その条件は、以下の3つです。
- ブロックxがテーブルにあること。 →トークン
xが、プレースontableにあること。 - ブロックxの上に他のブロックがないこと。 →トークン
xが、プレースclearにあること。 - アームがブロックをつかんでいないこと。 →任意のトークン
anyが、プレースholdingにないこと。
元のモデルはこれです。先ほどまでといきなり形が変わりましたが、内容は同じです。完成形から逆に図を作っているため、いびつな形になっています。。
1つ目の条件は表現されています。2つ目の条件のために、プレースclearを追加しましょう。
イベントpickup(x)を起こすには、トークンxがプレースontableだけでなくプレースclearにもなくてはならないので、その矢印を引きます。
また、プレースholdingにあるトークンは、イベントputdown(x)を通じてプレースontableだけでなくclearにも遷移するので、その矢印を引きます。
3つ目の条件に行きます。
「プレースholdingにトークンがあると、イベントpickup(x)が行えない」ということを表現するために、Inhibitor Arc（禁止矢印）を引きます。
最後に、ブロックB1とB2の初期状態は、他のブロックの下にないので、アノテーションにも以下を追加します。
INIT ontable(B1), ontable(B2), clear(B1), clear(B2)
これで、「テーブルからブロックを上げ下げするモデル」はできました。
残りのプレースとイベントも追加する
あと足りないのは、イベントstack(x, y)とunstack(x, y)、プレースonです。
まずイベントstack(x, y)（ブロックyの上にブロックxを置く）から。
これを実行するための条件は以下の通りです。
- ブロックxがアームにつかまれていること。 →トークン
xが、プレースholdingにあること。 - ブロックyの上に他のブロックがないこと。 →トークン
yが、プレースclearにあること。
また、乗せたブロックはclearになることも表現する必要があります。
これらに対応する3つの矢印を引きます。
実はもう1つ条件があります。ブロックxとブロックyが別のブロックであるということです。holdingとclearは両立するプレースなので、この制約を入れないと、ブロック1の上にブロック2を乗せるというアリエナイ遷移を許してしまいます。変数の関係は、プレースstack(x, y)のガード条件としてx<>yと記載してあります。
もう1つ、「xがyの上にある」という状態を表現するために、プレースonを追加して、stack(x, y)から遷移する矢印を引きます。
乗せた後は、トークンが以下のプレースに移動します。
- トークン
xは、プレースclearとon（第1変数）に移る - トークン
yは、プレースon（第2変数）に移る （すでに矢印を追加済み）
同じように、イベントunstack(x ,y)（ブロックyの上からブロックxを持ち上げる）も追加しましょう。
unstack(x, y)に入るための条件は、以下の4つです。
- xがyの上に乗っている。 →トークン
xとyが、プレースon(x, y)にあること。 - xの上に何も乗っていない。 →トークン
xが、プレースclear(x)にあること。 - xとyは別ものであること。 →
x<>y*1 - アームが何もつかんでいない。 →任意のトークン
anyが、プレースholdingにないこと。
また、unstackが完了すると、トークンxはプレースholdingに、yはclearに遷移することも表現します。
これでモデルはいったん完成です。
次回はこのモデルでのシミュレーションと、いよいよテストケース導出をやってみましょう。
*1:1.が満たされればこの条件も自動的に満たされそう。
