- ここでは，InventoryManagementのAlloyによる仕様記述に関する課題に取り組んでいただきます．
- 以下にAlloyで記述されたInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
+ ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
sig
- Alloyでは，商品idの集合を ItemId ，商品名の集合を Name ，
+ Alloy では，商品id の集合を ItemId ，商品名の集合を Name ，
商品全体を保管する倉庫の集合を Inventory ，商品の集合を Item で表します．
以下のモデルでは ItemId ，Name ，Inventory ，Item の順番にこれらの集合を宣言しています．
Inventory には，ItemId から Item への対応関係がitemDB フィールドとして定義されています．
@@ -38,7 +38,7 @@
最初の述語として記述されている init は，Inventory の
インスタンスである its が初期化されていることを示しています．
- 次のitemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
+ 次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
登録した後のインスタンス its' の関係を述語として定義しています．
ここで quantity は初期数量，n は商品名を示しています．
receivingOrShipping ではitemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
@@ -98,7 +98,7 @@
- 先ほどのInventoryManagementのモデルの構造を，Alloyの可視化ツールを使用して可視化したものを以下の図に示します．
+ 先ほどの InventoryManagement のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
- ここでは，InventoryManagementモデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+ ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
- 左下にあるInventory2($execute_its)は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため，
+ 左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため，
まだ何の商品(Item)も登録されていない状態になっています．
- 次に，1番上の段の左にあるInventory1($execute_its')は変数 its' で参照されるインスタンスで，
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照されるインスタンスで，
its で参照されるインスタンスに対して，itemId で参照される Item のインスタンスを初期数量100個で登録したインスタンスになっています．
- Inventory1の右にあるInventory0($execute_its'')は少し複雑です．
- まず，Inventory1において，ItemId で参照されるItemのインスタンスはItem1です．このインスタンスに対して50個出荷した後のItemのインスタンスはItem0になります．
- ここでItem0の在庫数が50個に減少していることに注意して下さい．
- ItemId で参照される Item のインスタンスがItem1からItem0に変わるので，Inventory のインスタンスもInventory1からInventory0に変わります．
+ Inventory1 の右にあるInventory0($execute_its'')は少し複雑です．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスは Item0 になります．
+ ここで Item0 の在庫数が50個に減少していることに注意して下さい．
+ ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．
- 本課題ではまず，上記にて説明を行ったInventoryManagementの仕様に，ある機能を追加した仕様を考えます．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルと，仮想実行を可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．