% TODO: We probably need to unify these (at least for the thesis) predicate random_allocation(array[int] of int: sol) = forall(i in courses) ( (uniform(0,99) < 80) -> (period_of[i] == sol[i]) ); predicate free_period() = let { int: period = uniform(periods) } in forall(i in courses where sol(period_of[i]) != period) (period_of[i] = sol(period_of[i]));