Today, we'll look at more examples of how Alloy uses relationional logic to describe interesting systems.

Workday example

Let's use Alloy to model our favorite part of the Wellesley experience: registering for classes on Workday!

First, we'll define some people. Recall that we use the abstract keyword to indicate that we only want actual atoms of a sub-sig, not the sig itself.

sig TimeSlot {}
abstract sig Person {}
sig Student extends Person {}

sig Admin extends Person {
  office: Room
}

sig CourseID {}
sig Room {}
sig Faculty extends Person {
  // We can use set as the multiplicity
  advisees: set Student,
    
  // Both Admin and Faculty have "office" fields!
  // Is this a problem? No: we can use <: to disambiguate
  // Example: Faculty <: office
  office: Room
}

Now, we can model a course:

sig Course {
  instructor : Faculty,
  when : TimeSlot,
  where : Room,
  tutors: set Student,
  staff: set Person,
  roster : set Student,
}

Sig facts

Alloy has a special syntax to indicate fact along with a sig, like below. In the "sig-fact" syntax, everything in the second block is scoped to be over all c: Course.

sig Course {
	instructor : Faculty,
	tutors: set Student,
	staff: set Person,
	roster : set Student,
	when : TimeSlot,
	where : Room,
} {
    // Staff is set union of prof and tutors
	staff = instructor + tutors 
        
    // No students can be tutors for that class
	no (tutors & roster)
}

Because we are scoped to talking about all courses for the sig, the first line is equivalent to the following, if defined outside of the sig definition:

fact {
	all c: Course | no (c.tutors & c.roster)
}

The above says: "no course can have overlap between its tutors and its students".

Note that this is different from the following, which would say: "no person can be both a tutor for any course and a student for any course":

fact {
	no (c.tutors & c.roster)
}

Workday constraints using relations

Now, let's set up some facts that relate different courses.

// Goal: people can't be in two places at once! At least,
// the professor and students can't. 
// Which field should be on the left of our implication?
// "when", since it's the overlapping times that causes
// problems. 
fact noTimeTraveling {
	all disj c1, c2 : Course | 
		c1.when = c2.when => {
			c1.instructor != c2.instructor 
			c1.where != c2.where
			no c1.roster & c2.roster
		}
}

Relations between sigs and fields

We can use relations on the full sig and a field together in interesting ways.

For example, some instances have a problem where the course is supossed to take place in some faculty member's office. Let's model for that to not be allowed:

fact differentRooms {
  // No courses in faculty or admin offices
  no Course.where & (Admin.office + Faculty.office)
}

Does this prevent faculty and admin from sharing offices?

(Think, then click!)

No since we don't say anything about the intersection of Admin.office and Faculty.office, or do anything to say two admins can't be in the same office. But, we'll leave that as unconstrained for now.


Joins

The join, or ., syntax is very general!

We can conceptualize joins are taking two database tables, finding all the rows were the columns in the middle of the join are the same, and keeping just those rows with the "matched" columns removed.

Said another way, a join a.b on two binary relations, a and b:

Numbers

Alloy can also reason about numbers. For example, we can say that the total number of rooms must be great than 3.

fact roomCount {
  #Room > 3
}

However, using integers to count can often be slower in the solver than expressing constraints on number with relations directly. Only use counting if you actually care about the specific integer relationships.

Note that Alloy can model integers both with and without overflow allowed. This is something you can change in the settings (search Help for Overflow). In general, we'll keep overflow on if we want to model a system where overflow can really happen (like a 4-bit counter chip, as seen in a CS240 lab), and otherwise turn overflow off (for cases like this Workday example, where the number of rooms is a mathematical, counting integer we aren't storing somewhere small).

See the end of these notes for the full Workday file.

More on relations (graph example)

Let's look at a very simple Alloy example to see how powerfun Alloy's use of relations and the join operator is.

sig Node {
    edges : set Node
}
run { #Node = 3}

Does this model a directed or undirected graph?

(Think, then click!)

Directed, since the order of atoms in a relation matters.


We can use the Evaluator to examine the value of different relations in a given instance of this model.

The instance we get first is:

[N1] -> [N0] -> [N3], (N1 also has a self loop)

The following results are all from the Evaluator in the Alloy Analyzer.

If we ask for just the name of the entire sig:

Node

We get:

The set of all nodes ({N0, N1, N2}).


edges

We get:

The set of all edges ({N0->N2, N1->N0, N1->N1}).


N.edges

We get:

The set of all nodes with some incoming edge ({N0, N1, N2}).


edges.N =

We get:

The set of all nodes with some outgoing edge ({N0, N1}).


edges.edges

We get:

The set of two-hop paths ({N1->N0, N1->N1, N1->N2} ).

That is, the set of paths we can take in the graph of length 2, starting at any node.


Next time, we'll see how we (and Alloy) can take this idea of paths and reachability even further.

/* Full new model: Workday + Course Browser! */

abstract sig Person {}

// when with no children is this possible with abstract
sig Room {}


sig Faculty extends Person {
  office: Room,
  advisees: set Student,
}

sig Admin extends Person {
  office: Room
}

sig Student extends Person {

}

sig TimeSlot {}

sig Course {
  instructor : Faculty,
  when: TimeSlot,
  where: Room,
  roster: set Student,
  tutors: set Student,
  staff: set Person,
} {
  // sig fact, true for all instances/atoms of the sig

  // No students can be tutors for this same class 
  no (roster & tutors)

  // Staff: instructor and the tutors
  staff = instructor + tutors
}

// Goal: people can't be in two different places at once
fact noTimeTraveling {
  all disj c1, c2 : Course | {
    c1.when = c2.when => // if the courses are at the same time
      {
        c1.instructor != c2.instructor
        c1.where != c2.where
        // What about c1.roster != c2.roster? Does not work!
        no (c1.roster & c2.roster)

      }
  }
}

fact differentRooms {
  // The set of Rooms used as any course's location
  // Course: set Course, where: Course-> Room, results: set Room
  no (Course.where & (Admin.office + Faculty.office))

  // This now says: classes are not taught where admin or faculty
  // have offices
}

fact numerics {
  // You only want to use numbers if you actually need them 
  #Room > 3
}


run { 
  some Room 
} for 5