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
diff --git a/models/Alloy/SimpleTwitter.als b/models/Alloy/SimpleTwitter.als
new file mode 100644
index 0000000..011d375
--- /dev/null
+++ b/models/Alloy/SimpleTwitter.als
@@ -0,0 +1,52 @@
+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 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]
+        }
+}
+
+run execute for 2 but 3 Accounts
\ No newline at end of file
diff --git a/models/DTRAM/InventoryManagement.dtram b/models/DTRAM/InventoryManagement.dtram
new file mode 100644
index 0000000..6b453b3
--- /dev/null
+++ b/models/DTRAM/InventoryManagement.dtram
@@ -0,0 +1,10 @@
+channel ItemRegistration {
+	out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity,
+																											"name": itemName})
+}
+
+channel ReceivingOrShipping(itemId:Str) {
+	out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0,
+																						prev_quantity + quantity,
+																						prev_quantity)
+}
diff --git a/models/DTRAM/SimpleTwitter.dtram b/models/DTRAM/SimpleTwitter.dtram
new file mode 100644
index 0000000..0ad6a0d
--- /dev/null
+++ b/models/DTRAM/SimpleTwitter.dtram
@@ -0,0 +1,8 @@
+channel Signup{
+	out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = insert(accountDB, accountId, {"name": name, 
+																									"tweets": nil})
+}
+
+channel Tweet(accountId:Str) {
+	out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
+}
\ No newline at end of file