+
init は，Inventory の
インスタンスである its が初期化されていることを示しています．itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
- 登録した後のインスタンス its' の関係を述語として定義しています．quantity は初期数量，n は商品名を示しています．its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．some it: Itemits のデータベースに登録されていない Item のインスタンス it が存在していることを示しており，
+ 直観的には Item のインスタンスの生成を示しています．receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
- 操作後のインスタンス its' の関係を述語として定義しています．quantity が正の値のときは入荷，負の値のときは出荷を表しています．its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．some it': Itemits のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており，
+ 直観的には，Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．execute では，init ，itemRegistraction ，receivingOrShipping を
この順で呼び出す操作を定義しています．runexecute を呼び出して仮想実行を行います．
@@ -115,16 +117,16 @@
ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
-
このテストケースはモデル中の execute 述語で実装されています．
- execute の実行を可視化したものを以下に示します．
+ execute の実行を可視化したものを以下に示します．
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引数の対応を追加した結果得られる写像を返す関数です．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 に変わることを示しています．ReceivingOrShipping(itemId:Str ) チャンネルでは inventory.{itemId}.count リソースがメッセージ receiveOrShip(quantity) を受け取ると，
+遷移前の状態 prev_quantity が prev_quantity + quantity に変わることを示しています．inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．itemId は商品idを表すパスパラメータで，一意な商品の特定を可能にしています．inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースは inventory.{itemId} の在庫数を表しており，
ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．
@@ -107,7 +107,7 @@
registerItem メッセージのシグニチャが表示されます．
- itemId は商品ID，itemName は商品名 ，quantity は初期数量を表します．
+ itemId は商品id，itemName は商品名 ，quantity は初期数量を表します．
+ ここでは，SimpleTwitter の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください．
+
sig
+ Alloy では，アカウントidの集合を AccountId，アカウント名の集合を Name，
+ ツイートの集合を Tweet，アカウントデータベースの集合を Accounts，アカウントの集合を Account，ツイートリストの集合を List で表します．
+ 以下のモデルでは AccountId，Name，Tweet，Accounts，Account，List の順番にこれらの集合を宣言しています．
+ Accounts には，AccountId から Account への対応関係が accountDB フィールドとして定義されています．
+ ここで，AccountId の右側の Account に対応する AccountId がたかだか１つしかないことを示しています．
+ Account の宣言では，アカウント名を表す name が Name のインスタンスとして，
+ ツイートリストを表す tweets が List のインスタンスとして定義されています．
+
+
pred
+ 最初の述語として記述されている init は，Accounts の
+ インスタンスである acs が初期化されていることを示しています．
+ 次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と，
+ 登録した後のインスタンス acs' の関係を述語として定義しています．ここで n はアカウント名を示しています．
+ また，述語定義中の acs のデータベースに登録されていない Account のインスタンス ac が存在していることを示しており，
+ 直観的には Account のインスタンスの生成を示しています．
+ tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と，
+ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
+ 述語定義中の acs のデータベースに登録されていない Account のインスタンス ac' が存在していることを示しており，
+ 直観的には，Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ また
+ 最後の execute では，init，signUp，tweet をこの順で呼び出す操作を定義しています．
+ runexecute を呼び出して仮想実行を行います．
+
++sig AccountId, Name, Tweet { } +sig Accounts { + accountDB: AccountIdlone ->lone Account +} +sig Account { + name: Name, + tweets: List +} + +sig List { + size:Int , + element:Int ->lone Tweet +} + +pred init[acs: Accounts] { +no acs.accountDB +} + +pred signUp[acs, acs': Accounts, id: AccountId, n: Name] { +some ac: Account | { +no id2: AccountId | acs.accountDB[id2] = ac + acs'.accountDB = acs.accountDB + id -> ac + ac.name = n + ac.tweets.size =0 +no ac.tweets.element + } +} + +pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] { +some ac': Account | { +no id2: AccountId | acs.accountDB[id2] = ac' + acs'.accountDB = acs.accountDB ++ id -> ac' + ac'.name = acs.accountDB[id].name + ac'.tweets != acs.accountDB[id].tweets + ac'.tweets.size = plus[acs.accountDB[id].tweets.size,1 ] + ac'.tweets.element[minus[ac'.tweets.size,1 ]] = contents +all n:Int | n != minus[ac'.tweets.size,1 ]implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n] + } +} + +pred execute[] { +some disj acs, acs', acs'': Accounts, id: AccountId, n: Name, contents: Tweet | { + init[acs] + signUp[acs, acs', id, n] + tweet[acs', acs'', id, contents] + } +} + +run executefor 2 but 3 Accounts +
+ 先ほどの SimpleTwitter のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
+
+ この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
+ Accounts が，AccountId のインスタンスを Account のインスタンスに対応させる accountDB というフィールドを持っており，
+ Account が Name のインスタンスを参照する name フィールドと，List のインスタンスを参照する tweets フィールドを，
+ List が size フィールドと，
+ Tweet のインスタンスに対応させる element フィールドをもっていることがわかります．
+
+ ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+
+ このテストケースはモデル中の execute 述語で実装されています．
+ execute の仮想実行を可視化したものを以下に示します．
+
+ 左下にある Accounts2($execute_acs) は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため，
+ まだ何のアカウント(Account)も登録されていない状態になっています．
+ 次に，1番上の段の左にある Accounts1($execute_acs') は変数 acs' で参照される Account のインスタンスで，
+ acs で参照される Account のインスタンスに対して，Account のインスタンス Account1($signUp_ac) をツイートリストの要素数が0の状態で登録したインスタンスになっています．
+ Accounts1 の右にある Accounts0($execute_acs'') は少し複雑です．
+ まず，Accounts1 において，AccountId で参照される Account のインスタンスは Account1 です．このインスタンスに対してツイートを行った後の Account のインスタンスは Account0 になります．
+ ここで Account0 のツイートリストの要素数が1に増加していることに注意して下さい．
+ AccountId で参照される Account のインスタンスが Account1 から Account0 に変わるので，Accounts のインスタンスも Accounts1 から Accounts0 に変わります．
+
+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
+
++sig AccountId, Name, Tweet { } +sig Accounts { + accountDB: AccountIdlone ->lone Account +} +sig Account { + name: Name, + tweets: List +} + +sig List { + size:Int , + element:Int ->lone Tweet +} + +pred init[acs: Accounts] { +no acs.accountDB +} + +pred signUp[acs, acs': Accounts, id: AccountId, n: Name] { +some ac: Account | { +no id2: AccountId | acs.accountDB[id2] = ac + acs'.accountDB = acs.accountDB + id -> ac + ac.name = n + ac.tweets.size =0 +no ac.tweets.element + } +} + +pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] { +some ac': Account | { +no id2: AccountId | acs.accountDB[id2] = ac' + acs'.accountDB = acs.accountDB ++ id -> ac' + ac'.name = acs.accountDB[id].name + ac'.tweets != acs.accountDB[id].tweets + ac'.tweets.size = plus[acs.accountDB[id].tweets.size,1 ] + ac'.tweets.element[minus[ac'.tweets.size,1 ]] = contents +all n:Int | n != minus[ac'.tweets.size,1 ]implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n] + } +} + +pred changeName[acs, acs': Accounts, id: AccountId, n: Name] { +some ac': Account | { +no id2: AccountId | acs.accountDB[id2] = ac' + acs'.accountDB = acs.accountDB ++ id -> ac' + ac'.name = n + ac'.tweets = acs.accountDB[id].tweets + } +} + +pred execute[] { +some disj acs, acs', acs'', acs''': Accounts, id: AccountId,disj n, n': Name, contents: Tweet | { + init[acs] + signUp[acs, acs', id, n] + tweet[acs', acs'', id, contents] + changeName[acs'', acs''', id, n'] + } +} + +run executefor 2 but 4 Accounts,3 Account + +
+
+
+ 課題アンケート (別タブが開きます)
+
+
+
+
+
+ 課題終了後の評価アンケート (別タブが開きます)
+
+
+