diff --git a/models/Alloy/InventoryManagement.als b/models/Alloy/InventoryManagement.als
index dc9271e..19fafcf 100644
--- a/models/Alloy/InventoryManagement.als
+++ b/models/Alloy/InventoryManagement.als
@@ -11,34 +11,30 @@
     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 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
-			plus[its.itemDB[itemId].count, quantity] >= 0 implies it'.count = plus[its.itemDB[itemId].count, quantity]
-				else it'.count = its.itemDB [itemId].count
-		}
+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]
-			ItemRegistraction[its, its', itemId, 100, n]
-			ReceivingOrShipping[its', its'', itemId, -50]
-		}
+    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
\ No newline at end of file
+run execute for 2 but 3 Inventory, 8 Int
diff --git a/models/Alloy/InventoryManagementCheckMinus.als b/models/Alloy/InventoryManagementCheckMinus.als
new file mode 100644
index 0000000..1ea8ef3
--- /dev/null
+++ b/models/Alloy/InventoryManagementCheckMinus.als
@@ -0,0 +1,46 @@
+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
diff --git a/models/Alloy/InventoryManagementShippingReceiving.als b/models/Alloy/InventoryManagementShippingReceiving.als
new file mode 100644
index 0000000..619d551
--- /dev/null
+++ b/models/Alloy/InventoryManagementShippingReceiving.als
@@ -0,0 +1,50 @@
+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 shipping[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 = minus[its.itemDB[itemId].count, quantity] 
+	}
+}
+
+pred receiving[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'', its''': Inventory, itemId: ItemId, n: Name | {
+		init[its]
+		itemRegistration[its, its', itemId, 100, n]
+		shipping[its', its'', itemId, 50]
+		receiving[its'', its''', itemId, 25]
+	}
+}
+
+run execute for 2 but 4 Inventory, 3 Item, 8 Int
diff --git a/models/Alloy/SimpleTwitter.als b/models/Alloy/SimpleTwitter.als
index 011d375..8927fab 100644
--- a/models/Alloy/SimpleTwitter.als
+++ b/models/Alloy/SimpleTwitter.als
@@ -1,52 +1,49 @@
 sig AccountId, Name, Tweet { }
 sig Accounts {
-    accountDB: AccountId lone -> lone Account
+	accountDB: AccountId lone -> lone Account
 }
 sig Account {
-    name: Name,
-    tweets: List
+	name: Name,
+	tweets: List
 }
 
 sig List {
-    size: Int,
-    element: Int -> lone Tweet
+	size: Int,
+	element: Int -> lone Tweet
 }
 
 pred init[acs: Accounts] {
-    no acs.accountDB
+	no acs.accountDB
 }
 
 pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
-    some ac: Account | 
-        {
-            no id2: AccountId | acs.accountDB[id2] = ac
-            acs'.accountDB = acs.accountDB + id -> ac
-            ac.name = n
-            ac.tweets.size = 0
-            no ac.tweets.element
-        }
+	some ac: Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac
+		acs'.accountDB = acs.accountDB + id -> ac
+		ac.name = n
+		ac.tweets.size = 0
+		no ac.tweets.element
+	}
 }
 
 pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
-    some ac': Account | 
-        {
-            no id2: AccountId | acs.accountDB[id2] = ac'
-            acs'.accountDB = acs.accountDB ++ id -> ac'
-            ac'.name = acs.accountDB[id].name
-            ac'.tweets != acs.accountDB[id].tweets
-            ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
-            ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
-            all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
-        }
+	some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = acs.accountDB[id].name
+		ac'.tweets != acs.accountDB[id].tweets
+		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
+		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
+		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
+	}
 }
 
 pred execute[] {
-    some disj acs, acs', acs'': Accounts, id: AccountId, n: Name, contents: Tweet | 
-        {
-            init[acs]
-            signUp[acs, acs', id, n]
-            tweet[acs', acs'', id, contents]
-        }
+	some disj acs, acs', acs'': Accounts, id: AccountId, n: Name, contents: Tweet | {
+		init[acs]
+		signUp[acs, acs', id, n]
+		tweet[acs', acs'', id, contents]
+	}
 }
 
-run execute for 2 but 3 Accounts
\ No newline at end of file
+run execute for 2 but 3 Accounts
diff --git a/models/Alloy/SimpleTwitterChangeName.als b/models/Alloy/SimpleTwitterChangeName.als
new file mode 100644
index 0000000..f4b9152
--- /dev/null
+++ b/models/Alloy/SimpleTwitterChangeName.als
@@ -0,0 +1,59 @@
+sig AccountId, Name, Tweet { }
+sig Accounts {
+    accountDB: AccountId lone -> lone Account
+}
+sig Account {
+    name: Name,
+    tweets: List
+}
+
+sig List {
+    size: Int,
+    element: Int -> lone Tweet
+}
+
+pred init[acs: Accounts] {
+    no acs.accountDB
+}
+
+pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
+    some ac: Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac
+		acs'.accountDB = acs.accountDB + id -> ac
+		ac.name = n
+		ac.tweets.size = 0
+		no ac.tweets.element
+	}
+}
+
+pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
+    some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = acs.accountDB[id].name
+		ac'.tweets != acs.accountDB[id].tweets
+		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
+		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
+		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
+	}
+}
+
+pred changeName[acs, acs': Accounts, id: AccountId, n: Name] {
+    some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = n
+		ac'.tweets = acs.accountDB[id].tweets			
+	}
+}
+
+pred execute[] {
+    some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
+		init[acs]
+		signUp[acs, acs', id, n]
+		tweet[acs', acs'', id, contents]
+		changeName[acs'', acs''', id, n']
+	}
+}
+
+run execute for 2 but 4 Accounts, 3 Account
diff --git a/models/Alloy/SimpleTwitterDuplicationCheck.als b/models/Alloy/SimpleTwitterDuplicationCheck.als
new file mode 100644
index 0000000..9176d8e
--- /dev/null
+++ b/models/Alloy/SimpleTwitterDuplicationCheck.als
@@ -0,0 +1,55 @@
+sig AccountId, Name, Tweet { }
+sig Accounts {
+    accountDB: AccountId lone -> lone Account
+}
+sig Account {
+    name: Name,
+    tweets: List
+}
+
+sig List {
+    size: Int,
+    element: Int -> lone Tweet
+}
+
+pred init[acs: Accounts] {
+    no acs.accountDB
+}
+
+pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
+	some ac': Account | acs.accountDB[id] = ac' implies {
+		all id': AccountId | acs'.accountDB[id'] = acs.accountDB[id']
+	}
+	else {
+    	some ac: Account | {
+			no id2: AccountId | acs.accountDB[id2] = ac
+			acs'.accountDB = acs.accountDB + id -> ac
+			ac.name = n
+			ac.tweets.size = 0
+			no ac.tweets.element
+		}
+	}
+}
+
+pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
+    some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = acs.accountDB[id].name
+		ac'.tweets != acs.accountDB[id].tweets
+		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
+		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
+		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
+	}
+}
+
+pred execute[] {
+    some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
+		init[acs]
+		signUp[acs, acs', id, n]
+		signUp[acs', acs'', id, n']
+		tweet[acs'', acs''', id, contents]
+	}
+}
+
+run execute for 2 but 4 Accounts