-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathFoodDB.als
84 lines (75 loc) · 2.03 KB
/
FoodDB.als
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
/**
* A simple model of a food database.
* Foods can be basic (like bread) or recipes (like a sandwich).
* Recipes in the database have ingredients drawn from other foods
* (basic or recipes) in the database.
* There may be foods and recipes that are not in the database (yet).
*/
/**
* Foods are either but not both basic or a recipe.
*/
abstract sig Food {}
sig BasicFood extends Food{}
sig Recipe extends Food {
ingredients : set Food
}
/**
* The database is simply a set of foods.
* Note that there is exactly one database, so
* FDB.foods is all the foods known in the DB.
*/
one sig FDB {
foods : set Food
}
/**
* All recipes not in the database have no ingredients.
*/
fact RecipesNotInFDBDoNotHaveIngredients {
// Fill in
all r: Recipe| r not in FDB.foods => no r.ingredients
}
/**
* All recipes in the database have at least 2 ingredients.
*/
fact RecipesInFDBHaveTwoOrMoreIngredients {
// Fill in
all r:Recipe | r in FDB.foods => #r.ingredients >=2
}
/**
* All ingredients needed for a recipe in the database are also
* in the database.
*/
fact RecipeIngredientsInDatabase {
// Fill in
all r: Recipe | r in FDB.foods => r.ingredients in FDB.foods
//all r:Recipe, i:r.ingredients |
}
/**
* No recipe is directly or indirectly an
* ingredient of itself.
* That is, the foods in the database form a DAG.
*/
fact NoRecipeCycles {
// Fill in
// all p: Person | (p not in p.enemies)
all r: Recipe| r in FDB.foods => r not in r.^ingredients
}
/**
* Assertion: All the ingredients needed for any recipe in the database,
* either directly or indirectly, are also in the database.
*/
assert AllNecessaryIngredientsInDatabase {
all r:Recipe |r in FDB.foods => r.*ingredients in FDB.foods
// Fill in
}
check AllNecessaryIngredientsInDatabase for 10
/**
* If you run this predicate and you model is correct
* you should get solutions.
*/
run {
// some recipes have other recipes as ingredients
some Recipe.ingredients & Recipe
// some recipes have no ingredients
some r : Recipe | no r.ingredients
} for exactly 10 Food