diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html
index 94f270a..8106f23 100644
--- a/courseA/IM_Alloy.html
+++ b/courseA/IM_Alloy.html
@@ -191,30 +191,30 @@
}
}
-pred shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: Int] {
- plus[its.itemDB[itemId].count, quantity] < 0 implies {
+pred receivingOrShipping[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 {
+ 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 | {
+ 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]
+ receivingOrShipping[its', its'', itemId, -50]
+ receivingOrShipping[its'', its''', itemId, -75]
}
}
-run execute for 2 but 4 Inventory, 8 Int
+ run execute for 2 but 4 Inventory, 8 Int
diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html
index d334aec..3062ea4 100644
--- a/courseA/IM_DTRAM.html
+++ b/courseA/IM_DTRAM.html
@@ -168,13 +168,13 @@
out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}
-channel Receiving(itemId:Str) {
+channel Receiving(itemId:Str) {
out inventory.{itemId}.count(prev_quantity:Int, receive(quantity:Int)) = prev_quantity + quantity
}
channel Shipping(itemId:Str) {
out inventory.{itemId}.count(prev_quantity:Int, ship(quantity:Int)) = prev_quantity - quantity
-}
+}
diff --git a/courseA/ST_Alloy.html b/courseA/ST_Alloy.html
index 7c38222..749febe 100644
--- a/courseA/ST_Alloy.html
+++ b/courseA/ST_Alloy.html
@@ -199,10 +199,10 @@
}
pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
- some ac': Account | acs.accountDB[id] = ac' implies {
+ some ac': Account | acs.accountDB[id] = ac' implies {
all id': AccountId | acs'.accountDB[id'] = acs.accountDB[id']
}
- else {
+ else {
some ac: Account | {
no id2: AccountId | acs.accountDB[id2] = ac
acs'.accountDB = acs.accountDB + id -> ac
@@ -210,7 +210,7 @@
ac.tweets.size = 0
no ac.tweets.element
}
- }
+ }
}
pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
@@ -226,15 +226,15 @@
}
pred execute[] {
- some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
+ 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']
+ signUp[acs', acs'', id, n']
tweet[acs'', acs''', id, contents]
}
}
-run execute for 2 but 4 Accounts
+run execute for 2 but 4 Accounts
diff --git a/courseA/ST_DTRAM.html b/courseA/ST_DTRAM.html
index 896ae46..2db4f18 100644
--- a/courseA/ST_DTRAM.html
+++ b/courseA/ST_DTRAM.html
@@ -172,9 +172,9 @@
out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
}
-channel ChangeName(accountId:Str) {
+channel ChangeName(accountId:Str) {
out accounts.{accountId}.name(prevNamr:Str, changeName(name:Str)) = name
-}
+}
diff --git a/courseB/IM_Alloy_B.html b/courseB/IM_Alloy_B.html
index ccd2bea..b86fc1b 100644
--- a/courseB/IM_Alloy_B.html
+++ b/courseB/IM_Alloy_B.html
@@ -190,7 +190,7 @@
}
}
-pred shipping[its, its': Inventory, itemId: ItemId, quantity: Int] {
+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'
@@ -206,18 +206,18 @@
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 | {
+ 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]
+ shipping[its', its'', itemId, 50]
+ receiving[its'', its''', itemId, 25]
}
}
-run execute for 2 but 4 Inventory, 3 Item, 8 Int
+ run execute for 2 but 4 Inventory, 3 Item, 8 Int
diff --git a/courseB/IM_DTRAM_B.html b/courseB/IM_DTRAM_B.html
index d6e62d3..9b8ca75 100644
--- a/courseB/IM_DTRAM_B.html
+++ b/courseB/IM_DTRAM_B.html
@@ -169,7 +169,7 @@
}
channel ReceivingOrShipping(itemId:Str) {
- out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)
+ out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)
}
diff --git a/courseB/ST_Alloy_B.html b/courseB/ST_Alloy_B.html
index 8758be3..e9a1872 100644
--- a/courseB/ST_Alloy_B.html
+++ b/courseB/ST_Alloy_B.html
@@ -219,25 +219,25 @@
}
}
-pred changeName[acs, acs': Accounts, id: AccountId, n: Name] {
+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 | {
+ 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']
+ changeName[acs'', acs''', id, n']
}
}
-run execute for 2 but 4 Accounts, 3 Account
+run execute for 2 but 4 Accounts, 3 Account
diff --git a/courseB/ST_DTRAM_B.html b/courseB/ST_DTRAM_B.html
index 37ab117..3533126 100644
--- a/courseB/ST_DTRAM_B.html
+++ b/courseB/ST_DTRAM_B.html
@@ -165,7 +165,7 @@
channel Signup {
- out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = if(contains(accountDB, accountId), accountDB, insert(accountDB, accountId, {"name": name, "tweets": nil}))
+ out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = if(contains(accountDB, accountId), accountDB, insert(accountDB, accountId, {"name": name, "tweets": nil}))
}
channel Tweet(accountId:Str) {
diff --git a/courseC/IM_Alloy_C.html b/courseC/IM_Alloy_C.html
index d9b8a3f..ffb1ce7 100644
--- a/courseC/IM_Alloy_C.html
+++ b/courseC/IM_Alloy_C.html
@@ -190,7 +190,7 @@
}
}
-pred shipping[its, its': Inventory, itemId: ItemId, quantity: Int] {
+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'
@@ -206,18 +206,18 @@
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 | {
+ 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]
+ shipping[its', its'', itemId, 50]
+ receiving[its'', its''', itemId, 25]
}
}
-run execute for 2 but 4 Inventory, 3 Item, 8 Int
+ run execute for 2 but 4 Inventory, 3 Item, 8 Int
diff --git a/courseC/IM_DTRAM_C.html b/courseC/IM_DTRAM_C.html
index e2049f8..e9e8566 100644
--- a/courseC/IM_DTRAM_C.html
+++ b/courseC/IM_DTRAM_C.html
@@ -169,7 +169,7 @@
}
channel ReceivingOrShipping(itemId:Str) {
- out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)
+ out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = if(prev_quantity + quantity >= 0, prev_quantity + quantity, prev_quantity)
}
diff --git a/courseC/ST_Alloy_C.html b/courseC/ST_Alloy_C.html
index ebe5159..a6a55e0 100644
--- a/courseC/ST_Alloy_C.html
+++ b/courseC/ST_Alloy_C.html
@@ -219,25 +219,25 @@
}
}
-pred changeName[acs, acs': Accounts, id: AccountId, n: Name] {
+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 | {
+ 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']
+ changeName[acs'', acs''', id, n']
}
}
-run execute for 2 but 4 Accounts, 3 Account
+run execute for 2 but 4 Accounts, 3 Account
diff --git a/courseC/ST_DTRAM_C.html b/courseC/ST_DTRAM_C.html
index 0be8edd..2057678 100644
--- a/courseC/ST_DTRAM_C.html
+++ b/courseC/ST_DTRAM_C.html
@@ -165,7 +165,7 @@
channel Signup {
- out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = if(contains(accountDB, accountId), accountDB, insert(accountDB, accountId, {"name": name, "tweets": nil}))
+ out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = if(contains(accountDB, accountId), accountDB, insert(accountDB, accountId, {"name": name, "tweets": nil}))
}
channel Tweet(accountId:Str) {
diff --git a/courseD/IM_Alloy_D.html b/courseD/IM_Alloy_D.html
index 2d6117a..b53fc56 100644
--- a/courseD/IM_Alloy_D.html
+++ b/courseD/IM_Alloy_D.html
@@ -191,30 +191,30 @@
}
}
-pred shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: Int] {
- plus[its.itemDB[itemId].count, quantity] < 0 implies {
+pred receivingOrShipping[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 {
+ 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 | {
+ 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]
+ receivingOrShipping[its', its'', itemId, -50]
+ receivingOrShipping[its'', its''', itemId, -75]
}
}
-run execute for 2 but 4 Inventory, 8 Int
+ run execute for 2 but 4 Inventory, 8 Int
diff --git a/courseD/IM_DTRAM_D.html b/courseD/IM_DTRAM_D.html
index 35872d1..4f1e11f 100644
--- a/courseD/IM_DTRAM_D.html
+++ b/courseD/IM_DTRAM_D.html
@@ -168,13 +168,13 @@
out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
}
-channel Receiving(itemId:Str) {
+channel Receiving(itemId:Str) {
out inventory.{itemId}.count(prev_quantity:Int, receive(quantity:Int)) = prev_quantity + quantity
}
channel Shipping(itemId:Str) {
out inventory.{itemId}.count(prev_quantity:Int, ship(quantity:Int)) = prev_quantity - quantity
-}
+}
diff --git a/courseD/ST_Alloy_D.html b/courseD/ST_Alloy_D.html
index d1cc8b0..c4146f6 100644
--- a/courseD/ST_Alloy_D.html
+++ b/courseD/ST_Alloy_D.html
@@ -199,10 +199,10 @@
}
pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
- some ac': Account | acs.accountDB[id] = ac' implies {
+ some ac': Account | acs.accountDB[id] = ac' implies {
all id': AccountId | acs'.accountDB[id'] = acs.accountDB[id']
}
- else {
+ else {
some ac: Account | {
no id2: AccountId | acs.accountDB[id2] = ac
acs'.accountDB = acs.accountDB + id -> ac
@@ -210,7 +210,7 @@
ac.tweets.size = 0
no ac.tweets.element
}
- }
+ }
}
pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
@@ -226,15 +226,15 @@
}
pred execute[] {
- some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
+ 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']
+ signUp[acs', acs'', id, n']
tweet[acs'', acs''', id, contents]
}
}
-run execute for 2 but 4 Accounts
+run execute for 2 but 4 Accounts
diff --git a/courseD/ST_DTRAM_D.html b/courseD/ST_DTRAM_D.html
index e91ed85..025fd09 100644
--- a/courseD/ST_DTRAM_D.html
+++ b/courseD/ST_DTRAM_D.html
@@ -172,9 +172,9 @@
out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
}
-channel ChangeName(accountId:Str) {
+channel ChangeName(accountId:Str) {
out accounts.{accountId}.name(prevNamr:Str, changeName(name:Str)) = name
-}
+}