sig
- 以下のモデルでは始めに，商品IDの集合を表す ItemId と商品名の集合を表す Name を宣言しています．
- 次に，商品全体を保管する倉庫の集合を表す Inventory を宣言しています．Inventory には，ItemId から
- 商品情報を表す Item への対応関係がitemDB フィールドとして定義されています．
+ Alloyでは，商品idの集合を ItemId ，商品名の集合を Name ，
+ 商品全体を保管する倉庫の集合を Inventory ，商品の集合を Item で表します．
+ 以下のモデルでは ItemId ，Name ，Inventory ，Item の順番にこれらの集合を宣言しています．
+ Inventory には，ItemId から Item への対応関係がitemDB フィールドとして定義されています．
Item の宣言では，商品名を表す name が Name のインスタンスとして，
在庫数を表す count が Int
- 以下のモデルでは始めに，新規商品登録用のイベントチャンネル，ItemRegistraction を宣言しています．
- 次の ReceivingOrShipping(itemId: は，itemId で登録されている商品に対して入荷か出荷を行う用のイベントチャンネルとして宣言しています．
+ 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 に変わることを示しています．
この図がモデルの実行に依らない，リソースを表していることに注意して下さい．
- 始めに，図の中央にある inventory リソースは商品全体を保管する倉庫を表しており，
- registerItem )を受け取ります．
- 次に，inventory リソースの子リソースとして，inventory.{itemId} リソースが表示されています．
- このリソースは，商品IDを表す itemId というパスパラメータを持っているため，一意なリソース(商品)の特定を可能にしています．
- 最後に，inventory.{itemId} リソースの子リソースとして，itemId で示された商品の在庫数を表す inventory.{itemId}.count リソースが表示されており，
- receiveOrShip )を受け取ります．
+ 図の中央にある inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．
+ inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．
+ リソース名に含まれる itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．
+ inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースはinventory.{itemId} の在庫数を表しており，
+ ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．
- 仮想実行を，シミュレーションツールを使用して可視化したものを以下に示していきます．
- まず，システムの初期状態を可視化したものが以下の図です．
+ シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．
+ ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．
- 初期状態のため，inventory リソースには何の商品も登録されていない状態になっています．
- 次に，新商品(Asahi)を登録するので，inventory リソースをダブルクリックします．
+ 初期状態では，inventory リソースには何の商品も登録されていない状態になっています．nil は空のマップやリストを表しています．
+ 次に，inventory に商品(Asahi)を登録するため，inventory リソースをダブルクリックします．
- inventory リソースに対して，registerItem という商品を登録するためのメッセージが選択できるので，こちらを選択します．
+ registerItem という商品を登録するためのメッセージを選択します．
- 商品IDを表す itemId と商品名を表す itemName ，初期数量を表す quantity を入力できる画面が表示されます．
+ registerItem メッセージのシグニチャが表示されます．
+ itemId 商品ID，itemName は商品名 ，quantity は初期数量を表します．
- 次の状態に遷移したので，商品IDが@123という状態の inventory.@123 と
- 在庫数量が100という状態の inventory.@123.count ，商品名がAsahiという状態の inventory.@123.name の３つのリソースが表示されました．
- 次に，登録した商品(Asahi)を50個出荷したいので，inventory.@123.count リソースをダブルクリックします．
+ 次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つ商品 inventory.@123 が inventory の子リソースとして生成されていることがわかります．
+ inventory.@123 の在庫数量 inventory.@123.count が100，商品名 inventory.@123.name がAsahiとなっていることを確認できます．
+ 次に，登録した商品 inventory.@123 を50個出荷したいので，inventory.@123.count リソースをダブルクリックします．
- 本課題ではまず，上記にて説明を行ったInventoryManagementの仕様に，ある機能を追加した仕様を考えます．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルと，仮想実行の流れを可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．