+
sig
- Alloy では，商品id の集合を ItemId ，商品名の集合を Name ，
- 商品全体を保管する倉庫の集合を Inventory ，商品の集合を Item で表します．
- 以下のモデルでは ItemId ，Name ，Inventory ，Item の順番にこれらの集合を宣言しています．
+ Alloy では，商品id の集合を ItemId，商品名の集合を Name，
+ 商品全体を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
+ 以下のモデルでは ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．
Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
ここで，ItemId の右側の Item に対応する ItemId がたかだか１つしかないことを示しています．
Item の宣言では，商品名を表す name が Name のインスタンスとして，
@@ -134,7 +134,7 @@
まだ何の商品(Item)も登録されていない状態になっています．
次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで，
its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
- Inventory1 の右にあるInventory0($execute_its'')は少し複雑です．
+ Inventory1 の右にあるInventory0($execute_its'') は少し複雑です．
まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
ここで Item0 の在庫数が50個に減少していることに注意して下さい．
ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．
diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html
index 3eea040..9638fd1 100644
--- a/courseA/IM_DTRAM.html
+++ b/courseA/IM_DTRAM.html
@@ -33,7 +33,7 @@
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引数の対応を追加した結果得られる写像を返す関数です．inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースはinventory.{itemId} の在庫数を表しており，
+ inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースは inventory.{itemId} の在庫数を表しており，
ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．
+ ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
+
sig
+ Alloy では，商品id の集合を ItemId，商品名の集合を Name，
+ 商品全体を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
+ 以下のモデルでは ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．
+ Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
+ ここで，ItemId の右側の Item に対応する ItemId がたかだか１つしかないことを示しています．
+ Item の宣言では，商品名を表す name が Name のインスタンスとして，
+ 在庫数を表す count が Int
+
pred
+ 最初の述語として記述されている init は，Inventory の
+ インスタンスである its が初期化されていることを示しています．
+ 次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
+ 登録した後のインスタンス its' の関係を述語として定義しています．
+ ここで quantity は初期数量，n は商品名を示しています．
+ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
+ 操作後のインスタンス its' の関係を述語として定義しています．
+ ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ 最後の execute では，init ，itemRegistraction ，receivingOrShipping を
+ この順で呼び出す操作を定義しています．
+ runexecute を呼び出して仮想実行を行います．
+ この実行の際に，
++sig ItemId, Name{} +sig Inventory { + itemDB: ItemIdlone ->lone Item +} +sig Item { + name : Name, + count:Int +} + +pred init[its: Inventory] { +no its.itemDB +} + +pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity:Int , n: Name] { +some it: Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it + its'.itemDB = its.itemDB + itemId -> it + it.name = n + it.count = quantity + } +} + +pred receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity:Int ] { +some it': Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it' + its'.itemDB = its.itemDB ++ itemId -> it' + it'.name = its.itemDB[itemId].name + it'.count = plus[its.itemDB[itemId].count, quantity] + } +} + +pred execute[] { +some disj its, its', its'': Inventory, itemId: ItemId, n: Name | { + init[its] + itemRegistration[its, its', itemId,100 , n] + receivingOrShipping[its', its'', itemId, -50 ] + } +} + +run executefor 2 but3 Inventory,8 Int +
+ 先ほどの InventoryManagement のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
+
+ この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
+ Inventory が，ItemId のインスタンスを Item のインスタンスに対応させる itemDB という
+ フィールドを持っており，Item が Name のインスタンスを参照する name フィールドと，
+ count フィールドを持っていることがわかります．
+
+ ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+
+ このテストケースはモデル中の execute 述語で実装されています．
+ execute の実行を可視化したものを以下に示します．
+
+ 左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため，
+ まだ何の商品(Item)も登録されていない状態になっています．
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで，
+ its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
+ Inventory1 の右にあるInventory0($execute_its'') は少し複雑です．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
+ ここで Item0 の在庫数が50個に減少していることに注意して下さい．
+ ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．
+
+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
+
++sig ItemId, Name{} +sig Inventory { + itemDB: ItemIdlone ->lone Item +} +sig Item { + name : Name, + count:Int +} + +pred init[its: Inventory] { +no its.itemDB +} + +pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity:Int , n: Name] { +some it: Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it + its'.itemDB = its.itemDB + itemId -> it + it.name = n + it.count = quantity + } +} + +pred shipping[its, its': Inventory, itemId: ItemId, quantity:Int ] { +some it': Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it' + its'.itemDB = its.itemDB ++ itemId -> it' + it'.name = its.itemDB[itemId].name + it'.count = minus[its.itemDB[itemId].count, quantity] + } +} + +pred receiving[its, its': Inventory, itemId: ItemId, quantity:Int ] { +some it': Item | { +no itemId2: ItemId | its.itemDB[itemId2] = it' + its'.itemDB = its.itemDB ++ itemId -> it' + it'.name = its.itemDB[itemId].name + it'.count = plus[its.itemDB[itemId].count, quantity] + } +} + +pred execute[] { +some disj its, its', its'', its''': Inventory, itemId: ItemId, n: Name | { + init[its] + itemRegistration[its, its', itemId,100 , n] + shipping[its', its'', itemId,50 ] + receiving[its'', its''', itemId,25 ] + } +} + +run executefor 2 but 4 Inventory,3 Item,8 Int + +
+
+
+ 課題アンケート (別タブが開きます)
+
+
+
+
+
+ 課題終了後の評価アンケート (別タブが開きます)
+
+
+
+ ここでは，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引数の対応を追加した結果得られる写像を返す関数です．{"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 モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+
+ シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．
+ ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です．
+
+ 初期状態では，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 ReceivingOrShipping(itemId:Str ) { +out inventory.{itemId}.count(prev_quantity:Int , receiveOrShip(quantity:Int )) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity) +} + +
+
+
+ 課題アンケート (別タブが開きます)
+
+
+
+
+
+ 課題終了後の評価アンケート (別タブが開きます)
+
+
+