-
Notifications
You must be signed in to change notification settings - Fork 1
/
timetabling.essence
71 lines (45 loc) · 2.98 KB
/
timetabling.essence
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
given nb_activities : int
given nb_lecturers : int
given nb_rooms : int
letting ACTIVITY be domain int(1..nb_activities)
letting LECTURER be domain int(1..nb_lecturers)
letting ROOM be domain int(1..nb_rooms)
letting DAY be domain int(1..5)
letting HOUR be domain int(9..16)
letting M be 100000
find assignment : function (total) ACTIVITY --> record {lecturer : LECTURER, day : DAY, hour : HOUR, room : ROOM }
$ two activities that happen at the same time cannot be delivered by the same lecturer
such that
[ (assignment(i)[day] = assignment(j)[day] /\ assignment(i)[hour] = assignment(j)[hour]) -> assignment(i)[lecturer] != assignment(j)[lecturer]
| i : ACTIVITY
, j : int(i+1..nb_activities)
]
$ two activities that happen at the same time cannot be in the same room
such that
[ (assignment(i)[day] = assignment(j)[day] /\ assignment(i)[hour] = assignment(j)[hour]) -> assignment(i)[room] != assignment(j)[room]
| i : ACTIVITY
, j : int(i+1..nb_activities)
]
given activity_allowed_times : function (total) ACTIVITY --> set of (DAY, HOUR)
such that [ (rec[day], rec[hour]) in activity_allowed_times(a) | (a, rec) <- assignment ]
given activity_preferred_times : function (total) ACTIVITY --> set of (DAY, HOUR)
find activity_preferred_times_penalty : int(0..M)
such that activity_preferred_times_penalty = sum([ toInt(!((rec[day], rec[hour]) in activity_preferred_times(a))) | (a, rec) <- assignment ])
given lecturer_allowed_times : function (total) LECTURER --> set of (DAY, HOUR)
such that [ (rec[day], rec[hour]) in lecturer_allowed_times(rec[lecturer]) | (a, rec) <- assignment ]
given lecturer_preferred_times : function (total) LECTURER --> set of (DAY, HOUR)
find lecturer_preferred_times_penalty : int(0..M)
such that lecturer_preferred_times_penalty = sum([ toInt(!((rec[day], rec[hour]) in lecturer_preferred_times(rec[lecturer]))) | (a, rec) <- assignment ])
given room_allowed_times : function (total) ROOM --> set of (DAY, HOUR)
such that [ (rec[day], rec[hour]) in room_allowed_times(rec[room]) | (a, rec) <- assignment ]
given room_preferred_times : function (total) ROOM --> set of (DAY, HOUR)
find room_preferred_times_penalty : int(0..M)
such that room_preferred_times_penalty = sum([ toInt(!((rec[day], rec[hour]) in room_preferred_times(rec[room]))) | (a, rec) <- assignment ])
given activity_allowed_rooms : function (total) ACTIVITY --> set of ROOM
such that [ rec[room] in activity_allowed_rooms(a) | (a, rec) <- assignment ]
given activity_allowed_lecturers : function (total) ACTIVITY --> set of LECTURER
such that [ rec[lecturer] in activity_allowed_lecturers(a) | (a, rec) <- assignment ]
$ make sure the given set of activities are on separate days
given activities_on_seperate_days : set of sequence of ACTIVITY
such that forAll seq in activities_on_seperate_days . forAll i : int(2..|seq|) . assignment(seq(i-1))[day] < assignment(seq(i))[day]
minimising activity_preferred_times_penalty + lecturer_preferred_times_penalty + room_preferred_times_penalty