diff --git a/models/Alloy/InventoryManagement.als b/models/Alloy/InventoryManagement.als
new file mode 100644
index 0000000..b36a34f
--- /dev/null
+++ b/models/Alloy/InventoryManagement.als
@@ -0,0 +1,45 @@
+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
\ No newline at end of file