DTRAM では，Web サービスと同様に階層化されたリソースを扱うことができます．リソースは状態を持ち，その状態を変更することができます．アドレス帳の仕様は次のような階層化されたリソースで表すこととします．
book: アドレス帳全体book.owner: アドレス帳の所有者book.addr: アドレス帳に記載された連絡先の名前と住所の対応表book.addr.{name}: 連絡先の名前 name に対応した住所book：アドレス帳全体book.owner：アドレス帳の所有者book.addr：アドレス帳に記載された連絡先の名前と住所の対応表book.addr.{name}：連絡先の名前 name に対応した住所Init を流れるメッセージを受け取るリソースは book.owner です．同様に，チャンネル Add 内のメッセージを受け取るリソースは book.addr，チャンネル Del 内のメッセージを受け取るリソースも book.addr になります．sig
Alloy では，商品id の集合を ItemId，商品名の集合を Name，
- 商品全体を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
+ 全商品を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
以下のモデルでは ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．
+
Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
ここで，ItemId の右側の Item に対応する ItemId がたかだか１つしかないことを示しています．
+
Item の宣言では，商品名を表す name が Name のインスタンスとして，
在庫数を表す count が Int
最初の述語として記述されている init は，Inventory の
インスタンスである its が初期化されていることを示しています．
+
次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
登録した後のインスタンス its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．
- また，述語定義中の its のデータベースに登録されていない Item のインスタンス it が存在していることを示しており，
- 直観的には Item のインスタンスの生成を示しています．
+ また，述語定義中の its のデータベースに登録されていない Item のインスタンス (it) が存在していることを示しており，
+ 直観的には Item のインスタンスが生成されたことを示しています．
+
receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
- また，述語定義中の its のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており，
- 直観的には，Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
- 最後の execute では，init ，itemRegistraction ，receivingOrShipping を
+ また，述語定義中の its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており，
+ 直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+
+ 最後の execute では，init，itemRegistraction，receivingOrShipping を
この順で呼び出す操作を定義しています．
runexecute を呼び出して仮想実行を行います．
この実行の際に，
左下にある 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個に減少していることに注意して下さい．
diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html
index b5c9284..d334aec 100644
--- a/courseA/IM_DTRAM.html
+++ b/courseA/IM_DTRAM.html
@@ -27,17 +27,21 @@
DTRAMでは，InventoryManagement の仕様を以下のような階層化されたリソースで表します．
inventory: 商品全体を保管する倉庫inventory.{itemId}: itemId で登録されている商品inventory.{itemId}.count: itemId で示された商品の在庫数inventory.{itemId}.name: itemId で示された商品の商品名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: チャンネルでは inventory.{itemId}.count リソースがメッセージ receiveOrShip(quantity) を受け取ると，
遷移前の状態 prev_quantity が prev_quantity + quantity に変わることを示しています．
- は，ある酒屋の在庫管理を行うシステムです．酒類の商品毎に在庫数を管理することができます． + InventoryManagement は，ある酒屋の在庫管理を行うシステムです．酒類の商品毎に在庫数を管理することができます． InventoryManagement の仕様は次の通りです．
AccountId，アカウント名の集合を Name，
ツイートの集合を Tweet，アカウントデータベースの集合を Accounts，アカウントの集合を Account，ツイートリストの集合を List で表します．sig AccountId，Name，Tweet，Accounts，Account，List の順番にこれらの集合を宣言しています．
Accounts には，AccountId から Account への対応関係が accountDB フィールドとして定義されています．
ここで，AccountId の右側の Account に対応する AccountId がたかだか１つしかないことを示しています．
+
Account の宣言では，アカウント名を表す name が Name のインスタンスとして，
ツイートリストを表す tweets が List のインスタンスとして定義されています．