ソフトウェアの品質を学びまくる2.0

ソフトウェアの品質、テストなどについて学んだことを記録するブログです。

モデルベースドテストについて学んでみよう - その3

Mannequins

 前回は、MBTツール「MISTA」でブロックゲームのシンプルなモデルを描いてみて、シミュレーションで一手進めたところまでを見ました。

www.kzsuzuki.com

f:id:kz_suzuki:20200426185300p:plain

トークンとイベントの関係とは

 上の状態から、もう一度pickup(x)を選んで遷移させてみましょう。

f:id:kz_suzuki:20200428045811p:plain

 2つのトークンが、プレースholdingにあります。つまり、「2つのブロックがともに、アームにつかまれているという状態です。
 これは、「一度につかめるブロックは一つだけ」というルールに反していますね。つまりモデルに不備があるということです。

 実はこのファンクションネットが表しているのは、

プレースontableにあるトークンに対し、イベントpickupを行うと、プレースholdingに遷移する

というよりは、

プレースontableにトークンがあるという条件を満たせば、イベントpickupが実行可能になり、プレースholdingに遷移させることができる

だと理解した方が正しいと思います。

 一般的な表現にすると、

  • あるイベントを起こすためには、そのイベントに流入するすべてのプレースにトークンが存在していないといけない
  • そのすべてのトークンは、イベント発生後に、次のプレースに移動する

ということになります。

条件を追加していく

 pickup(x)を実行可能にするために必要な条件を、プレースと矢印で表現する必要があります。その条件は、以下の3つです。

  • ブロックxがテーブルにあること。 →トークンxが、プレースontableにあること。
  • ブロックxの上に他のブロックがないこと。 →トークンxが、プレースclearにあること。
  • アームがブロックをつかんでいないこと。 →任意のトークンanyが、プレースholdingにないこと。

 元のモデルはこれです。先ほどまでといきなり形が変わりましたが、内容は同じです。完成形から逆に図を作っているため、いびつな形になっています。。

f:id:kz_suzuki:20200428051702p:plain

 1つ目の条件は表現されています。2つ目の条件のために、プレースclearを追加しましょう。
 イベントpickup(x)を起こすには、トークンxがプレースontableだけでなくプレースclearにもなくてはならないので、その矢印を引きます。
 また、プレースholdingにあるトークンは、イベントputdown(x)を通じてプレースontableだけでなくclearにも遷移するので、その矢印を引きます。

f:id:kz_suzuki:20200428051740p:plain

 3つ目の条件に行きます。
 「プレースholdingにトークンがあると、イベントpickup(x)が行えない」ということを表現するために、Inhibitor Arc(禁止矢印)を引きます。

f:id:kz_suzuki:20200428051751p:plain

 最後に、ブロックB1とB2の初期状態は、他のブロックの下にないので、アノテーションにも以下を追加します。

INIT ontable(B1), ontable(B2), clear(B1), clear(B2)

 これで、「テーブルからブロックを上げ下げするモデル」はできました。

残りのプレースとイベントも追加する

 あと足りないのは、イベントstack(x, y)unstack(x, y)、プレースonです。

 まずイベントstack(x, y)(ブロックyの上にブロックxを置く)から。
 これを実行するための条件は以下の通りです。

  1. ブロックxがアームにつかまれていること。 →トークンxが、プレースholdingにあること。
  2. ブロックyの上に他のブロックがないこと。 →トークンyが、プレースclearにあること。

 また、乗せたブロックはclearになることも表現する必要があります。
 これらに対応する3つの矢印を引きます。

f:id:kz_suzuki:20200428052716p:plain

 実はもう1つ条件があります。ブロックxとブロックyが別のブロックであるということです。holdingclearは両立するプレースなので、この制約を入れないと、ブロック1の上にブロック2を乗せるというアリエナイ遷移を許してしまいます。変数の関係は、プレースstack(x, y)ガード条件としてx<>yと記載してあります。

 もう1つ、「xがyの上にある」という状態を表現するために、プレースonを追加して、stack(x, y)から遷移する矢印を引きます。

f:id:kz_suzuki:20200428053230p:plain

 乗せた後は、トークンが以下のプレースに移動します。

  • トークンxは、プレースclearon(第1変数)に移る
  • トークンyは、プレースon(第2変数)に移る (すでに矢印を追加済み)

 同じように、イベントunstack(x ,y)(ブロックyの上からブロックxを持ち上げる)も追加しましょう。
 unstack(x, y)に入るための条件は、以下の4つです。

  1. xがyの上に乗っている。 →トークンxyが、プレースon(x, y)にあること。
  2. xの上に何も乗っていない。 →トークンxが、プレースclear(x)にあること。
  3. xとyは別ものであること。 →x<>y *1
  4. アームが何もつかんでいない。 →任意のトークンanyが、プレースholdingにないこと。

 また、unstackが完了すると、トークンxはプレースholdingに、yclearに遷移することも表現します。

f:id:kz_suzuki:20200428053714p:plain

 これでモデルはいったん完成です。
 次回はこのモデルでのシミュレーションと、いよいよテストケース導出をやってみましょう。

www.kzsuzuki.com

*1:1.が満たされればこの条件も自動的に満たされそう。