CODEWITHSUNDEEP
alloy
mjl48
mjl48

Reputation: 3

Why does NoRoomConflicts generate a binary relation while NoRoomConflicts_alt "works"

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)

Upvotes: 0

Views: 51

Answers (1)

Daniel Jackson
Daniel Jackson

Reputation: 2768

First, what you're seeing in the solution is that certain quantified variables (d in this case) get skolemized so that you can see their values. If you're solving a constraint of the form (all x | some y | ...), the skolemized value of y will have to be a relation -- giving a y value for each x. This is not the actual type of the Alloy variable, which is why there is no type error. For a full explanation, see Section 5.2.2 of my book (Software Abstractions).

Second, the two formulas are not the same. This is explained on page 293 of my book. In short, it's because "no c, d | P" means you can't find a c and d such that P, and "no c | no d | P" means you can't find a c such that you can't find a d such that P.

Upvotes: 1

Related Questions