14: Relations and Reachability

tags: Tag(sp22)

Today we'll work with a fairly simple model, and use it to demonstrate how reachability works in Forge. That is, You'll see how the reachable predicate is defined (via transitive closure), and get some more practice with sets in Forge.

Logistics

• Hopefully everyone has been making good progress with Curiosity Modeling! I'm seeing a lot of awesome questions on Ed and at hours.
• Some of you are curious about how far you need to go to earn a check. This is hard to give a precise answer to, because everyone's models will be different. However, I can say that we're looking for:
  • evidence that you explored your topic of choice;
  • evidence that you validated your model;
  • something you got from the model (generating or solving puzzles, checking a property, or even understanding a domain better).
• There's a lab this week that focuses on sets and other relational concepts. You'll be exploring automated memory management in Forge. This lab leads directly into the next homework, and is meant to give you useful insight into how these systems work.

Reachability

Consider this small Forge model:

#lang forge
sig Person {
    friends: set Person,
    followers: set Person
}
one sig Nim, Tim extends Person {}

pred wellformed {
    -- friends is symmetric
    all disj p1, p2: Person | p1 in p2.friends implies p2 in p1.friends 
    -- cannot follow or friend yourself
    all p: Person | p not in p.friends and p not in p.followers
}
run {wellformed} for exactly 8 Person

Let's run it, get a reasonably large instance, and try to figure out how to express some goals in the evaluator.

Nim's followers

This is just Nim.followers.

Nim's followers' followers

Another application of the field! Nim.followers.followers.

Nim is reachable from Tim via "followers"

We can use the reachable built-in: reachable[Nim, Tim, followers.

This all seems pretty doable…

Nim is reachable from Tim via the inverse of "followers" (what we might call "following")?

Hmm. This seems harder. We don't have a field called following, and the reachable built-in takes fields!

Right?

Let's try something else.

Nim is reachable from Tim via followers, but not including Tim's friends?

We might try reachable[Nim, Tim, (followers-Tim.friends)] but this will produce an error. Why? Well, because followers is a field but Tim.friends is a set.

But is that the real answer? The error complains about "arity": 2 vs 1. Let's type those two expressions into the evaluator and see what we get. For followers, we get a set of pairs of people. But Tim.friends is a set of singletons.

Important: The evaluator prints these as parenthesized lists of lists. But don't be fooled! It's really printing a set of lists. The order in which the inner lists print shouldn't matter.

Arity, Relations, and Tuples

Arity is another word for how wide the elements of a set are. Here, we'd say that followers has arity 2 and Tim.friends has arity 1. So Forge is pointing out that taking the set difference of these two makes no sense: you'll never find a singleton in a set of pairs.

When we're talking about sets in this way, we sometimes call them relations. E.g., the followers field is a binary relation because it has arity 2. We'll call elements of relations tuples. E.g., if Nim follows Tim, the tuple (Tim, Nim) would be present in followers.

(Almost) Everything Is A Set

The truth is that reachable doesn't take "fields"; it takes relations. Specifically, binary relations, which define the steps it can use to connect the two objects.

That's the fact we'll use to solve the 2 problems above.

Nim is reachable from Tim via the inverse of "followers" (what we might call "following")?

Now that we know followers is a binary relation, we can imagine flipping it to get its inverse. How can we do that? Well, there are multiple ways! We could write a set-comprehension:

{p1, p2: Person | p1 in p2.followers}

The order matters here! If p1 is in p2.followers, then there is an entry in the relation that looks like (p2, p1). We could make this more explicit by writing:

{p1, p2: Person | p2->p1 in followers}

Now that we know followers is a set, this makes sense! The product (->) operator combines p2 and p1 into a binary tuple, which may (or may not) be in followers.

Forge provides an operator that does this directly: transpose (~). So we could write instead:

~followers

Which should you use? It's up to you! Regardless, we could now answer this question with:

reachable[Nim, Tim, ~followers]

Nim is reachable from Tim via followers, but not including Tim's friends?

Everything is a set, so let's build the subset of followers that doesn't involve anyone in Tim.friends. We can't write followers-(Tim.friends), since that's an arity mismatch. Somehow, we need to remove entries in followers involving one of Tim's friends and anybody else.

One way is to use the product operator to build cooresponding binary relations. E.g.:

followers-(Tim.friends->Person)

Important: You may notice that we've now used -> in what seems like 2 different ways. We used it to combine specific people, p1 and p2 above into a single tuple. But now we're using it to combine two sets into a set of tuples. This flexibility is a side effect of sets being the fundamental concept in full Forge:

• the product of (Tim) and (Nim) is (Tim, Nim);
• the product of ((Person1), (Person2)) and ((Person3), (Person4)) is ((Person1, Person3), (Person1, Person4), (Person2, Person3), (Person2, Person4)).

Formally, -> is the cross-product operation on sets.

You'll see this apparently double-meaning when using in and =, too: singletons are single-element sets.

How Reachability Works

If we wanted to encode reachability, we could start by writing a helper predicate:

pred reachable2[to: Person, from: Person, via: Person -> Person]: set Person {
    to in 
    from.via +
    from.via.via +
    from.via.via.via 
    -- ...and so on...
}

But we always have to stop writing somewhere. We could write the union out to 20 steps, and still we wouldn't catch some very long (length 21 or higher) paths. So we need some way to talk about unbounded reachability.

Forge's reachable built-in does this, but it's just a facade over a new relational operator: transitive closure (^R).

The transitive closure ^R of a binary relation R is the smallest binary relation such that:

• if (x, y) is in R, then (x, y) is in ^R; and
• if (x, z) is in R and (z, y) is in ^R then (x, y) is in R.

That is, ^R encodes exactly what we were trying to encode above. The reachable[to, from, f1, ...] built-in is just syntactic sugar for:

    to in from.^(f1 + ...)

You'll get more practice with this in this week's lab.