【InventoryManagement(DTRAM) の課題】

ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
DTRAM の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

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

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

DTRAM では，InventoryManagement のモデルを以下のようなチャンネル単位で記述していきます．
商品登録用のイベントチャンネルを ItemRegistration ，itemId で登録されている商品に対して入荷か出荷を行うためのイベントチャンネルを ReceivingOrShipping(itemId:Str) として宣言しています．

ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態が itemDB から insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．
ここで，関数 insert(x, y, z) は，写像 x に対し，キー y と値 z の対応を追加した結果得られる写像を返す関数です．
また {"count": quantity, "name": itemName} は，"count" と "name" をキーに持つ JSON オブジェクトを表しています．

ReceivingOrShipping(itemId:Str) チャンネルでは inventory.{itemId}.count リソースがメッセージ receiveOrShip(quantity) を受け取ると， 遷移前の状態 prev_quantity が prev_quantity + quantity に変わることを示しています．

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 Receiving(itemId:Str) {
	out inventory.{itemId}.count(prev_quantity:Int, receive(quantity:Int)) = prev_quantity + quantity
}

channel Shipping(itemId:Str) {
	out inventory.{itemId}.count(prev_quantity:Int, ship(quantity:Int)) = prev_quantity - quantity
}

1:


2:


3:


4:


5:


6:


7:


設問１ (別タブが開きます)
設問２ (別タブが開きます)
課題評価アンケート (別タブが開きます)


【InventoryManagement(Alloy)】へ