Consider the Alloy model below, a stripped-to-the-essence version of a student submission. The problem is a course scheduling system, and the student was trying to say there are no conflicts (two distinct courses meeting in the same place at the same time):
abstract sig Room{}
one sig S20, S30, S50 extends Room{}
abstract sig Period{}
one sig Mon, Tue, Wed, Thu, Fri extends Period{}
// Courses and the room and periods when they meet.
some sig Course {
where : Room,
when : some Period
}
// No two Courses with any common meeting Periods can be
// in the same Room - from the student.
pred NoRoomConflicts_student {
no c : Course | no d : Course |
c != d && some c.when & d.when && d.where = c.where
}
run NoRoomConflicts_student
// No two Courses with any common meeting Periods can be
// in the same Room - my recasting.
pred NoRoomConflicts_alt {
no c : Course, d : Course |
c != d && some c.when & d.when && d.where = c.where
}
run NoRoomConflicts_alt
When NoRoomConflicts_alt is run we get solutions that conform to the spec.
But when NoRoomConflicts_student is run, suddenly "d" becomes a binary relation between Courses and the solutions show conflicts.
(a) Why was "d" transformed in this way?
(b) Given (a), shouldn't c != d raise a type error?
Note: I'm not claiming that the two predicates are equivalent (my head aches trying to do the double negation) - I just want to know how "d" suddenly becomes a binary relation when NoRoomConflicts is run.
Version: Alloy Analyzer 4.2_2015-02-22 (build date: 2015-02-22 18:21 EST)
