仮想実行の可視化:
このテストケースはモデル中の execute 述語で実装されています．
- execute の仮想実行を可視化したものを以下に示します．
+ execute の実行を可視化したものを以下に示します．
@@ -131,10 +131,10 @@
左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため，
まだ何の商品(Item)も登録されていない状態になっています．
- 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照されるインスタンスで，
- its で参照されるインスタンスに対して，itemId で参照される Item のインスタンスを初期数量100個で登録したインスタンスになっています．
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで，
+ its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
Inventory1 の右にあるInventory0($execute_its'')は少し複雑です．
- まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスは Item0 になります．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
ここで Item0 の在庫数が50個に減少していることに注意して下さい．
ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．
+ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
- その仕様のモデルと，仮想実行を可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
- 以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
+ 以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
@@ -34,8 +34,8 @@ DTRAMでは，InventoryManagement のモデルを以下のようなチャンネル単位で記述していきます．
- ここでは，商品登録用のイベントチャンネルを
ItemRegistration ，itemId で登録されている商品に対して入荷か出荷を行うためのイベントチャンネルを ReceivingOrShipping(itemId:Str ) として宣言しています．-
ItemRegistration チャンネルでは inventory リソースが，メッセージ registerItem(itemId, itemName, quantity) を受け取ると， リソースの状態 itemDB が insert(itemDB, itemId, {"count": quantity, "name": itemName}) に変わることを示しています．+ 商品登録用のイベントチャンネルを
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 に変わることを示しています．@@ -62,10 +62,10 @@
- この図がモデルの実行に依らない，リソースを表していることに注意して下さい．
+ この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
図の中央にある inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．
inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．
- リソース名に含まれる itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．
+ このリソース名に含まれる itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．
inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースはinventory.{itemId} の在庫数を表しており，
ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．
+ ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
- その仕様のモデルと，仮想実行の流れを可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
1:
+
2:
+
3:
+
+
4:
+
+
5:
+
+
6:
+
+
7:
+