【InventoryManagement(Alloy)】

ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください．
Alloy の説明をもう一度ご覧になりたい方はこちらへ(別タブが開きます)．

InventoryManagement の Alloy による仕様記述についての説明

sig:

Alloy では，商品id の集合を ItemId，商品名の集合を Name，全商品を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
以下のモデルでは sig を用いて，ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．

Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
ここで，ItemId の右側の lone は１つの Item に対応する ItemId がたかだか１つしかないことを示しています．

Item の宣言では，商品名を表す name が Name のインスタンスとして，在庫数を表す count が Int のインスタンスとして定義されています．

pred:

最初の述語として記述されている init は，Inventory のインスタンスである its が初期化されていることを示しています．具体的には述語定義中の noで，its.itemDB が空であることを示しています．

次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，登録した後のインスタンス its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．
また，述語定義中の some it: Item は，its のデータベースに登録されていない Item のインスタンス (it) が存在していることを示しており，直観的には Item のインスタンスが生成されたことを示しています．

receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス (it') が存在していることを示しており，直観的には Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
なお x ++ y -> z は，関係 x 中ですでに y に何らかの値が対応していた場合に，それを y から z への対応に置き換えたものを表しています．関数 plus[x, y] は，加算 x + y を表します．

最後の execute では，init，itemRegistration，receivingOrShipping をこの順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います．この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています．

sig ItemId, Name{}
sig Inventory {
	itemDB: ItemId lone -> lone Item
}
sig Item {
	name : Name,
	count: Int
}

pred init[its: Inventory] {
	no its.itemDB
}

pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
	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 | {
		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 | {
		init[its]
		itemRegistration[its, its', itemId, 100, n]
		receivingOrShipping[its', its'', itemId, -50]
	}
}

run execute for 2 but 3 Inventory, 8 Int

モデルの可視化

先ほどの InventoryManagement のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．

この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
Inventory が，ItemId のインスタンスを Item のインスタンスに対応させる itemDB というフィールドを持っており，Item が Name のインスタンスを参照する name フィールドと， Int のインスタンスを参照する count フィールドを持っていることがわかります．

InventoryManagement モデルの仮想実行について

ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

仮想実行の可視化:

このテストケースはモデル中の execute 述語で実装されています．
execute の実行を可視化したものを以下に示します．

左下にある 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個に減少していることに注意して下さい．
ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります．

課題概要

ここからが課題です．
本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
なお，以下のモデル中にある implies はその前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．

sig ItemId, Name{}
sig Inventory {
	itemDB: ItemId lone -> lone Item
}
sig Item {
	name : Name,
	count: Int
}

pred init[its: Inventory] {
	no its.itemDB
}

pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
	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] {
		plus[its.itemDB[itemId].count, quantity] < 0 implies {
		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]
		}
		} 
}

pred execute[] {
		some disj its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {
		init[its]
		itemRegistration[its, its', itemId, 100, n]
				receivingOrShipping[its', its'', itemId, -50]
		receivingOrShipping[its'', its''', itemId, -75]
	}
}

	run execute for 2 but 4 Inventory, 8 Int

【InventoryManagement(Alloy) の課題】

InventoryManagement の Alloy による仕様記述についての説明

`sig`:

`pred`:

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

課題概要

【InventoryManagement(Alloy) の課題】

InventoryManagement の Alloy による仕様記述についての説明

sig:

pred:

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

課題概要

`sig`:

`pred`: