ここでは,InventoryManagementのDTRAMによる仕様記述に関する課題に取り組んでいただきます.
以下にDTRAMで記述されたInventoryManagementのモデルを示します.こちらを適宜参照しながらモデルの理解を行ってください.
DTRAMでは,InventoryManagement の仕様を以下のような階層化されたリソースで表します.
inventory
: 商品全体を保管する倉庫inventory.{itemId}
: itemId
で登録されている商品inventory.{itemId}.count
: itemId
で示された商品の在庫数inventory.{itemId}.name
: itemId
で示された商品の商品名ItemRegistration
,itemId
で登録されている商品に対して入荷か出荷を行うためのイベントチャンネルを ReceivingOrShipping(itemId:Str )
として宣言しています.ItemRegistration
チャンネルでは inventory
リソースが,メッセージ registerItem(itemId, itemName, quantity)
を受け取ると, リソースの状態 itemDB
が insert(itemDB, itemId, {"count": quantity, "name": itemName})
に変わることを示しています.insert()
関数は,第1引数に渡された写像に対し,第2引数と第3引数の対応を追加した結果得られる写像を返す関数です.
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モデルの仮想実行について説明します.この仮想実行で用いるテストケースは次の通りです.
シミュレーションツールを使用すると与えられたモデルに対して,任意の仮想実行を行うことができます.
ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます.まず,システムの初期状態を可視化したものが以下の図です.
初期状態では,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
の仕様に,ある機能を追加した仕様を考えます.
その仕様のモデルと,仮想実行の流れを可視化した以下の図を見ていただいた上で,2つの設問にお答えいただきます.
設問にお答えいただく際は,必ず設問1,設問2の順番でご解答下さい.以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません.
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 }
課題アンケート (別タブが開きます)
課題終了後の評価アンケート (別タブが開きます)