From 6f7d44ff83e4505db30bed9f13267e8f5bec1288 Mon Sep 17 00:00:00 2001 From: Jeremy Wall Date: Sun, 28 Jan 2024 16:56:36 -0500 Subject: [PATCH] Alloy models for browser_state --- models/browser_state.als | 51 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 models/browser_state.als diff --git a/models/browser_state.als b/models/browser_state.als new file mode 100644 index 0000000..2adf814 --- /dev/null +++ b/models/browser_state.als @@ -0,0 +1,51 @@ +sig Id {} +sig Text {} + +sig Recipe { + , id: one Id + , text: one Text +} + +fact { + no r1, r2: Recipe | (r1.id = r2.id) and (r1.text != r2.text) + no r1, r2: Recipe | (r1 != r2) and (r1.id = r2.id) +} + +sig Ingredient {} +sig Modifier {} +sig Amt {} + +sig ModifiedInventory { + , ingredient: one Ingredient + , modifier: lone Modifier + , amt: one Amt +} + +fact { + no mi1, mi2: ModifiedInventory | mi1 != mi2 && (mi1.ingredient = mi2.ingredient) and (mi1.modifier = mi2.modifier) +} + +sig DeletedInventory { + , ingredient: one Ingredient + , modifier: lone Modifier +} + +fact { + no mi1, mi2: DeletedInventory | mi1 != mi2 && (mi1.ingredient = mi2.ingredient) and (mi1.modifier = mi2.modifier) +} + +sig ExtraItems { + , ingredient: one Ingredient + , amt: one Amt +} + +sig State { + , recipes: some Recipe + , modified: set ModifiedInventory + , deleted: set DeletedInventory + , extras: set ExtraItems +} { + no rs: Recipe | rs not in recipes +} + +run { } for 3 but exactly 2 State, 2 Modifier, exactly 3 ModifiedInventory, exactly 9 Ingredient