diff --git a/img/Alloy/Alloy MetaModel Ver InventoryManagement.png b/img/Alloy/Alloy MetaModel Ver InventoryManagement.png new file mode 100644 index 0000000..e60f1ab --- /dev/null +++ b/img/Alloy/Alloy MetaModel Ver InventoryManagement.png Binary files differ diff --git a/img/Alloy/Alloy MetaModel Ver SimpleTwitter.png b/img/Alloy/Alloy MetaModel Ver SimpleTwitter.png new file mode 100644 index 0000000..31f3c7b --- /dev/null +++ b/img/Alloy/Alloy MetaModel Ver SimpleTwitter.png Binary files differ diff --git a/img/Alloy/Alloy Ver InventoryManagement.png b/img/Alloy/Alloy Ver InventoryManagement.png new file mode 100644 index 0000000..87a7658 --- /dev/null +++ b/img/Alloy/Alloy Ver InventoryManagement.png Binary files differ diff --git a/img/Alloy/Alloy Ver SimpleTwitter.png b/img/Alloy/Alloy Ver SimpleTwitter.png new file mode 100644 index 0000000..9d214fa --- /dev/null +++ b/img/Alloy/Alloy Ver SimpleTwitter.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png b/img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png new file mode 100644 index 0000000..9f4af68 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 1 Ver InventoryManagement.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png b/img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png new file mode 100644 index 0000000..8fb7922 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 2 Ver InventoryManagement.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png b/img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png new file mode 100644 index 0000000..aca4298 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 3 Ver InventoryManagement.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png new file mode 100644 index 0000000..eb9b7c2 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 4 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png new file mode 100644 index 0000000..5330622 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 5 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png new file mode 100644 index 0000000..51b8c99 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 6 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png new file mode 100644 index 0000000..ce6d295 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 7 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 8 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 8 Ver Inventory Management.png new file mode 100644 index 0000000..2f1d4fe --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 8 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png b/img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png new file mode 100644 index 0000000..e5bef5e --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM 9 Ver Inventory Management.png Binary files differ diff --git a/img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png b/img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png new file mode 100644 index 0000000..3e15298 --- /dev/null +++ b/img/DTRAM/InventoryManagement/DTRAM Ver InventoryManagement architecture Visualize.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 1 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 1 VerSimpleTwitter.png new file mode 100644 index 0000000..812fc63 --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 1 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 2 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 2 VerSimpleTwitter.png new file mode 100644 index 0000000..16d909a --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 2 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 3 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 3 VerSimpleTwitter.png new file mode 100644 index 0000000..4a83d76 --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 3 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 4 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 4 VerSimpleTwitter.png new file mode 100644 index 0000000..69f8c1a --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 4 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 5 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 5 VerSimpleTwitter.png new file mode 100644 index 0000000..8f5e4fd --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 5 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 6 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 6 VerSimpleTwitter.png new file mode 100644 index 0000000..e7d28ed --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 6 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 7 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 7 VerSimpleTwitter.png new file mode 100644 index 0000000..43b7d42 --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 7 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 8 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 8 VerSimpleTwitter.png new file mode 100644 index 0000000..f7c9c87 --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 8 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM 9 VerSimpleTwitter.png b/img/DTRAM/SimpleTwitter/DTRAM 9 VerSimpleTwitter.png new file mode 100644 index 0000000..d8dfc84 --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM 9 VerSimpleTwitter.png Binary files differ diff --git a/img/DTRAM/SimpleTwitter/DTRAM Ver SimpleTwitter architecture Visualize.png b/img/DTRAM/SimpleTwitter/DTRAM Ver SimpleTwitter architecture Visualize.png new file mode 100644 index 0000000..3367dff --- /dev/null +++ b/img/DTRAM/SimpleTwitter/DTRAM Ver SimpleTwitter architecture Visualize.png Binary files differ diff --git a/models/Alloy/InventoryManagement.als b/models/Alloy/InventoryManagement.als index b36a34f..dc9271e 100644 --- a/models/Alloy/InventoryManagement.als +++ b/models/Alloy/InventoryManagement.als @@ -15,31 +15,30 @@ some it: Item | { no itemId2: ItemId | its.itemDB[itemId2] = it - its'.itemDB = its.itemDB + itemId -> it - it.name = n - it.count = quantity + its'.itemDB = its.itemDB + itemId -> it + it.name = n + it.count = quantity } } -pred ReceivingOrShipping[its, its': Inventory, itemId: ItemId, quantity: Int ] { // 出荷と入荷 - some it': Item | +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] + 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 | + some disj its, its', its'': Inventory, itemId: ItemId, n: Name | { init[its] - quantity >= 0 - ItemRegistraction[its, its', itemId, quantity, n] - ReceivingOrShipping[its', its'', itemId, quantity'] + ItemRegistraction[its, its', itemId, 100, n] + ReceivingOrShipping[its', its'', itemId, -50] } } -run execute for 2 but 3 Inventory \ No newline at end of file +run execute for 2 but 3 Inventory, 8 Int \ No newline at end of file