diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html
index c70978b..1072f45 100644
--- a/courseA/IM_Alloy.html
+++ b/courseA/IM_Alloy.html
@@ -15,38 +15,39 @@
- 【InventoryManagement(Alloy)の概要説明】
+ 【InventoryManagement(Alloy)の課題】
- ここでは，Alloyを用いて記述したInventoryManagementについて説明します．
- 以下にInventoryManagementのソースコードを示します．こちらを適宜参照しながらソースコードの理解を行ってください．
+ ここでは，Alloyを用いて記述したInventoryManagementの課題について説明します．
+ 以下にInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
InventoryManagementのAlloyによる記述についての説明
sig:
- 以下のソースコードでは始めに，商品を識別するためのIDを表すItemIdと 商品名を表すNameを構造のない集合として宣言しています．
- 次に，商品全体を管理する倉庫を表しているInventoryは，itemDBフィールドを持っています．
- このフィールドを定義している行では，itemDBフィールドがItemIdから，
- 商品の情報を表すItemとの対応関係を参照していることを表しています．
- 最後のItemでは始めに，商品名を表すnameをItemの要素と，Nameの要素の間の関係として定義しています．
- 次にある，在庫数を表すcountでは在庫数をInt型で表すように定義を行っています．
+ 以下のモデルでは始めに，商品を識別するためのIDを表す ItemId と商品名を表す Name を集合として宣言しています．
+ 次に，商品全体を管理する倉庫を表している Inventory は， itemDB フィールドを持っています．
+ このフィールドを定義している行では， itemDB フィールドが ItemId から，
+ 商品の情報を表す Item との対応関係を参照していることを表しています．
+ 最後の Item では始めに，商品名を表す name を Item の要素と， Name の要素の間の関係として定義しています．
+ 次にある，在庫数を表す count では在庫数を Int 型で表すように定義を行っています．
pred:
- 以下のソースコードで最初に記述されているinitは，Inventoryの
- 構造を持ったits初期化するという操作になっています．
- 次の，itemRegistractionでは初めて取り扱う商品を入荷する際に，
- 商品名と入荷数量をInventoryに登録するという操作になっています．
- その次にある，receivingOrShippingでは登録されている商品に対して
+ 以下のモデルで最初に記述されている init は， Inventory の
+ 構造を持った its 初期化するという操作になっています．
+ 次の， itemRegistraction では初めて取り扱う商品を入荷する際に，
+ 商品名と入荷数量を Inventory に登録するという操作になっています．
+ その次にある， receivingOrShipping では登録されている商品に対して
入荷か出荷を行った際に起こる数量の変化の操作を表しています．
- 最後のexecuteでは上記にて説明を行った，
- init，itemRegistraction，receivingOrShippingを
+ 最後の execute では上記にて説明を行った，
+ init ， itemRegistraction ， receivingOrShipping を
上から順番に実行を進めるという操作になっています．
- そして，最後にあるrunでは，executeを呼び出して実行を行っています．
- この実行の際に100や-50の数字を扱うため，末尾に8 Intという
+ そして，最後にある run では， execute を呼び出して実行を行っています．
+ この実行の際に 100 や -50 の数字を扱うため，
+ 末尾に 8 Int という
Alloyで8bitの数字を扱うことができるようにするための記述を行っています．
@@ -54,41 +55,41 @@
sig ItemId, Name{}
sig Inventory {
- itemDB: ItemId lone -> lone Item
+ itemDB: ItemId lone -> lone Item
}
sig Item {
- name : Name,
- count: Int
+ name : Name,
+ count: Int
}
pred init[its: Inventory] {
- no its.itemDB
+ no its.itemDB
}
pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
- some it: Item | {
+ 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 | {
+ 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 | {
+ some disj its, its', its'': Inventory, itemId: ItemId, n: Name | {
init[its]
itemRegistration[its, its', itemId, 100, n]
receivingOrShipping[its', its'', itemId, -50]
- }
+ }
}
run execute for 2 but 3 Inventory, 8 Int
@@ -104,29 +105,29 @@
- Inventoryが，商品名を表すnameと在庫数を表すcountの２つのフィールドを持っている，
- Itemを管理するというモデルになっています．
+ Inventory が，商品名を表す name と在庫数を表す count の２つのフィールドを持っている，
+ Item を管理するというモデルになっています．
-InventoryManagementの例題仕様について
+InventoryManagementの仮想実行について
- ここでは，InventoryManagementの例題仕様について説明します．InventoryManagementの例題仕様は次の通りです．
+ ここでは，InventoryManagementの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．
- Inventoryに新しく取り扱う商品を100個入荷します．
- お客様が商品を50個購入してくれたので，在庫数が50個に減少しました．
-例題仕様の可視化:
+仮想実行の可視化:
- 先ほどの例題仕様で，実行時の状態を可視化したものを以下に示します．
+ 先ほどの仮想実行を可視化したものを以下に示します．
- 左下にあるInventory2($execute_its)は，始めにinitが実行された時の状態になっているため，
+ 左下にあるInventory2($execute_its)は，始めに init が実行された時の状態になっているため，
まだ何の商品(Item)も登録されていない状態になっています．
次に，1番上の段の左にあるInventory1($execute_its')はテストケースの１が行われた時の状態になっているため，
100個のItem1を入荷している状態になっています．
@@ -139,56 +140,56 @@
課題概要
- 本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のソースコードと可視化の図を
+ 本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のモデルと可視化の図を
実験参加者の皆様に見て頂きます．
- 次に，その２つを見てどの様な機能が追加されたのか，またどの様なシナリオになっているのかを
+ 次に，その２つを見てどの様な機能が追加されたのか，またどの様なテストケースになっているのかを
考えて頂き，以下のアンケートにお答えください．
sig ItemId, Name{}
sig Inventory {
- itemDB: ItemId lone -> lone Item
+ itemDB: ItemId lone -> lone Item
}
sig Item {
- name : Name,
- count: Int
+ name : Name,
+ count: Int
}
pred init[its: Inventory] {
- no its.itemDB
+ no its.itemDB
}
pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
- some it: Item | {
+ some it: Item | {
no itemId2: ItemId | its.itemDB[itemId2] = it
its'.itemDB = its.itemDB + itemId -> it
it.name = n
- it.count = quantity
- }
+ it.count = quantity
+ }
}
pred shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: Int] {
plus[its.itemDB[itemId].count, quantity] < 0 implies {
- all itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId']
+ all itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId']
}
else {
- 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]
- }
+ 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]
- shippingOrReceiving[its', its'', itemId, -50]
- shippingOrReceiving[its'', its''', itemId, -75]
- }
+ some disj its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {
+ init[its]
+ itemRegistration[its, its', itemId, 100, n]
+ shippingOrReceiving[its', its'', itemId, -50]
+ shippingOrReceiving[its'', its''', itemId, -75]
+ }
}
run execute for 2 but 4 Inventory, 8 Int
