【InventoryManagement(DTRAM) の課題】

ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．

InventoryManagement の DTRAM による記述についての説明

DTRAMでは，InventoryManagement の仕様を以下のような階層化されたリソースで表します．

• inventory: 商品全体を保管する倉庫
• inventory.{itemId}: itemId で登録されている商品
• inventory.{itemId}.count: itemId で示された商品の在庫数
• inventory.{itemId}.name: itemId で示された商品の商品名

channel ItemRegistration {
	out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}

channel ReceivingOrShipping(itemId:Str) {
	out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = prev_quantity + quantity
}
	

モデルの可視化

先ほどの InventoryManagement のモデルのリソースとチャンネルを，DTRAM のモデリングツールを使用して可視化したものを以下の図に示します．

この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
図の中央にある inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．
inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．
このリソース名に含まれる itemId は商品idを表すパスパラメータで，一意な商品の特定を可能にしています．
inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースは inventory.{itemId} の在庫数を表しており， ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．

InventoryManagement モデルの仮想実行について

ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

1. inventory に新しく取り扱う商品(Asahi)を初期数量100で登録します．
2. 登録した商品(Asahi)を50個出荷します．

仮想実行の可視化:

シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．
ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．

初期状態では，inventory リソースには何の商品も登録されていない状態になっています．nil は空のマップやリストを表しています．
次に，inventory に商品(Asahi)を登録するため，inventory リソースをダブルクリックします．

registerItem という商品を登録するためのメッセージを選択します．

registerItem メッセージのシグニチャが表示されます．
itemId は商品id，itemName は商品名 ，quantity は初期数量を表します．

ここでは，registerItem("@123", "Asahi", 100) を入力します．

次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つ商品 inventory.@123 が inventory の子リソースとして生成されていることがわかります．
inventory.@123 の在庫数量 inventory.@123.count が100，商品名 inventory.@123.name がAsahiとなっていることを確認できます．
次に，登録した商品 inventory.@123 を50個出荷したいので，inventory.@123.count リソースをダブルクリックします．

メッセージを選択する画面が同様に表示されますので，入荷か出荷を行う receiveOrShip というメッセージを選択します．

入荷数量，または出荷数量の入力が可能な画面が表示されますので，ここでは receiveOrShip(-50) と入力して実行します．
ここで quantity が正の値のときは入荷，負の値のときは出荷が行われます．

次の状態に遷移したため，inventory.@123.count リソースの状態が50に遷移したことが確認できました．

課題概要

ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

channel ItemRegistration {
	out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}

channel ReceivingOrShipping(itemId:Str) {
	out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)
}

1:

2:

3:

4:

5:

6:

7:

課題アンケート (別タブが開きます)
課題終了後の評価アンケート (別タブが開きます)