- ここでは，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 の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルと，仮想実行を可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
- ここでは，InventoryManagementのDTRAMによる仕様記述に関する課題に取り組んでいただきます．
- 以下にDTRAMで記述されたInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
+ ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
+ 以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
DTRAMでは，InventoryManagement の仕様を以下のような階層化されたリソースで表します．
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引数の対応を追加した結果得られる写像を返す関数です．
ここでは，InventoryManagementモデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
- ここでは，SimpleTwitterのAlloyによる仕様記述に関する課題に取り組んでいただきます．
- 以下にAlloyで記述されたSimpleTwitterのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
+ ここでは，SimpleTwitter の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
sig
- Alloyでは，アカウントidの集合を AccountId ，アカウント名の集合を Name ，
+ Alloy では，アカウントidの集合を AccountId ，アカウント名の集合を Name ，
ツイートの集合を Tweet ，アカウント全体の集合を Accounts ，アカウントの集合を Account，リストの集合を List で表します．
以下のモデルでは AccountId ，Name ，Tweet ，Accounts，Account，List の順番にこれらの集合を宣言しています．
Accounts には，AccountId から Account への対応関係がaccountDB フィールドとして定義されています．
@@ -108,7 +108,7 @@
- 先ほどのSimpleTwitterのモデルの構造を，Alloyの可視化ツールを使用して可視化したものを以下の図に示します．
+ 先ほどの SimpleTwitter のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
- ここでは，SimpleTwitterモデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+ ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
- 左下にあるAccounts2($execute_acs)は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため，
+ 左下にある Accounts2($execute_acs) は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため，
まだ何のアカウント(Account)も登録されていない状態になっています．
- 次に，1番上の段の左にあるAccounts1($execute_acs')は変数 acs' で参照されるインスタンスで，
+ 次に，1番上の段の左にある Accounts1($execute_acs') は変数 acs' で参照されるインスタンスで，
acs で参照されるインスタンスに対して，AccountId で参照される Account のインスタンスをツイートリストの要素数が0の状態で登録したインスタンスになっています．
- Accounts1の右にあるAccounts0($execute_acs'')は少し複雑です．
- まず，Accounts1において，AccountId で参照されるAccountのインスタンスはAccount1です．このインスタンスに対してツイートを行った後のAccountのインスタンスはAccount0になります．
- ここでAccount0のツイートリストの要素数が1に増加していることに注意して下さい．
- AccountId で参照される Account のインスタンスがAccount1からAccount0に変わるので，Account のインスタンスもAccount1からAccount0に変わります．
+ Accounts1 の右にある Accounts0($execute_acs'') は少し複雑です．
+ まず，Accounts1 において，AccountId で参照される Account のインスタンスは Account1 です．このインスタンスに対してツイートを行った後の Account のインスタンスは Account0 になります．
+ ここで Account0 のツイートリストの要素数が1に増加していることに注意して下さい．
+ AccountId で参照される Account のインスタンスが Account1 から Account0 に変わるので，Account のインスタンスも Account1 から Account0 に変わります．
- 本課題ではまず，上記にて説明を行ったSimpleTwitterの仕様に，ある機能を追加した仕様を考えます．
+ 本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルと，仮想実行を可視化した以下の図を見ていただいた上で，２つの設問にお答えいただきます．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．