【InventoryManagement(DTRAM)】

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

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

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

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 モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

仮想実行の可視化:

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

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

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

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

次の状態に遷移し，遷移後の状態が表示されます．@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 の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
なお，以下のモデル中にある関数 if(x, y, z) は，x が true のときは y を返し，false のときは z を返します．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

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)
}

【InventoryManagement(DTRAM) の課題】

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

モデルの可視化

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

仮想実行の可視化:

課題概要

1:

2:

3:

4:

5:

6:

7: