Newer
Older
SpecificationSimulatorExperiments / models / Alloy / InventoryManagement.als
sig ItemId, Name{}
sig Inventory {
    itemDB: ItemId lone -> lone Item
}
sig Item {
    name : Name,
    count: Int  
}

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

pred ItemRegistraction[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
			plus[its.itemDB[itemId].count, quantity] >= 0 implies it'.count = plus[its.itemDB[itemId].count, quantity] 
				else it'.count = its.itemDB [itemId].count
		}
}

pred execute[] {
    some disj its, its', its'': Inventory, itemId: ItemId, quantity, quantity': Int, n: Name | 
		{
			init[its]
			quantity >= 0
			ItemRegistraction[its, its', itemId, quantity, n]
			ReceivingOrShipping[its', its'', itemId, quantity']
		}
}

run execute for 2 but 3 Inventory