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, n: Name |
		{
			init[its]
			ItemRegistraction[its, its', itemId, 100, n]
			ReceivingOrShipping[its', its'', itemId, -50]
		}
}

run execute for 2 but 3 Inventory, 8 Int