diff --git a/models/Alloy/InventoryManagement.als b/models/Alloy/InventoryManagement.als index 19fafcf..c450e08 100644 --- a/models/Alloy/InventoryManagement.als +++ b/models/Alloy/InventoryManagement.als @@ -1,20 +1,20 @@ sig ItemId, Name{} sig Inventory { - itemDB: ItemId lone -> lone Item + itemDB: ItemId lone -> lone Item } sig Item { - name : Name, - count: Int + name : Name, + count: Int } pred init[its: Inventory] { - no its.itemDB + 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 + its'.itemDB = its.itemDB + itemId -> it it.name = n it.count = quantity } @@ -30,7 +30,7 @@ } pred execute[] { - some disj its, its', its'': Inventory, itemId: ItemId, n: Name | { + some disj its, its', its'': Inventory, itemId: ItemId, n: Name | { init[its] itemRegistration[its, its', itemId, 100, n] receivingOrShipping[its', its'', itemId, -50]