【InventoryManagement(Alloy)の概要説明】

ここでは，Alloyを用いて記述したInventoryManagementについて説明します．
以下にInventoryManagementのソースコードを示します．こちらを適宜参照しながらソースコードの理解を行ってください．

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

sig:

以下のソースコードでは始めに，商品を識別するためのIDを表すItemIdと 商品名を表すNameを構造のない集合として宣言しています．
次に，商品全体を管理する倉庫を表しているInventoryは，itemDBフィールドを持っています． このフィールドを定義している行では，itemDBフィールドがItemIdから， 商品の情報を表すItemとの対応関係を参照していることを表しています．
最後のItemでは始めに，商品名を表すnameをItemの要素と，Nameの要素の間の関係として定義しています． 次にある，在庫数を表すcountでは在庫数をInt型で表すように定義を行っています．

pred:

以下のソースコードで最初に記述されているinitは，Inventoryの 構造を持ったits初期化するという操作になっています．
次の，itemRegistractionでは初めて取り扱う商品を入荷する際に， 商品名と入荷数量をInventoryに登録するという操作になっています．
その次にある，receivingOrShippingでは登録されている商品に対して 入荷か出荷を行った際に起こる数量の変化の操作を表しています．
最後のexecuteでは上記にて説明を行った， init，itemRegistraction，receivingOrShippingを 上から順番に実行を進めるという操作になっています．
そして，最後にあるrunでは，executeを呼び出して実行を行っています． この実行の際に100や-50の数字を扱うため，末尾に8 Intという Alloyで8bitの数字を扱うことができるようにするための記述を行っています． 

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が，商品名を表すnameと在庫数を表すcountの２つのフィールドを持っている， Itemを管理するというモデルになっています．

InventoryManagementの例題仕様について

ここでは，InventoryManagementの例題仕様について説明します．InventoryManagementの例題仕様は次の通りです．

  1. Inventoryに新しく取り扱う商品を100個入荷します．
  2. お客様が商品を50個購入してくれたので，在庫数が50個に減少しました．

例題仕様の可視化:

先ほどの例題仕様で，実行時の状態を可視化したものを以下に示します．


左下にあるInventory2($execute_its)は，始めにinitが実行された時の状態になっているため， まだ何の商品(Item)も登録されていない状態になっています．
次に，1番上の段の左にあるInventory1($execute_its')はテストケースの１が行われた時の状態になっているため， 100個のItem1を入荷している状態になっています．
そして，Inventory1の右にあるInventory0($execute_its'')ではテストケース２が行われた時の状態になっているため， 在庫数が50個に減少しています．

課題概要

本課題ではまず，上記にて説明を行ったInventoryManagementに，とある機能を追加した時のソースコードと可視化の図を 実験参加者の皆様に見て頂きます．
次に，その２つを見てどの様な機能が追加されたのか，またどの様なシナリオになっているのかを 考えて頂き，以下のアンケートにお答えください． 

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 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']
	}
	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]
	 shippingOrReceiving[its', its'', itemId, -50]
	 shippingOrReceiving[its'', its''', itemId, -75]
    }
}

run execute for 2 but 4 Inventory, 8 Int

課題アンケート (別タブが開きます)
課題終了後の評価アンケート (別タブが開きます)


【InventoryManagement(DTRAM)】へ