Really Basic Question

Questions
1

So I’m looking at the online tutorial again–when you’re teaching yourself it’s wise to review materials four or five times till you’re sure you’ve mastered them.

I’m trying to understand the

sig FSObject
{
parent: lone Dir
}

signature in terms of what I’ve seen illustrated about sets before. Hence my question–is this the correct understanding of the set mappings associated with that signature?

AlloyTutorial1
AlloyTutorial11373×2092 90.1 KB

2

It is indeed: every FSObject is mapped to at most one Dir, which means some FSObjects may not be mapped to anything (e.g. C in your sketch). Computer scientists usually call this a partial function (while mathematicians would only call it a function). In UML, this corresponds to a 0..1 multiplicity from FSObject to Dir.

If every FSObject is mapped to exactly one Dir, then computer scientists usually call this a total function while mathematicians will often call this a map. In UML, this corresponds to a 1 multiplicity from FSObject to Dir.

3

Thanks for taking the time to reply and to confirm my understanding! Also thanks for taking a moment to help my vocabulary!

4

Looking a bit further on in the tutorial there’s a slightly more complicated relation that I want to insure I’m mapping correctly:

sig FileSystem{
.
.
.
contents: Dir lone → FSObject
}

FileModel2
FileModel21686×2572 177 KB

Should “contents” label the mapping from Dir to FSObject? After I drew it I thought – I bet I labelled the wrong arrow but I left it in there in order to ask.

I’m wondering if my primitive set representation is a good mental model of what the alloy model is saying.

Regardless thanks for helping to confirm my understanding of the first set of notation.

5

First, the Alloy code you wrote means that contents is a ternary relation, that is a set of triples whose first coordinate is in FileSystem, the second in Dir and the third in FSObject. Labelling arrows works well for binary relations, not really for ternary (or more) ones.

OK. So, this was the formalist view, without taking into account the designer’s intent when using this name. The relation could as well be called foo or bar without changing its mathematical meaning (that is, being a set of triples).

But:

  1. The word contents wasn’t chosen without a reason. Designers and programmers name things (sets, relations, types, variables, constants, functions, methods…) to convey a mental model, trying to use names as evocative of the modeled situation as possible.
  2. A ternary relation on sets A, B and C can also be viewed as (in mathematical terms: is isomorphic to) a function from A to P(A x B) or a function from A x B to P(C) (where, given a set X, P(X) is the powerset of X).

Here, it’s likely that the ternary relation was named contents because it is the same to see it as a ternary relation or as a function from FileSystem x Dir to P(FSObject) (if you sit in a given filesystem and a given directory, then you can retrieve _the set of _ objects they contain).

I hope it’s clearer.

Notice also that your sketch doesn’t show some interesting situations. For instance, you could also have a triple (F2, D, O1), or (F2, D, O2), or both (remark that, in the first two cases, you can’t easily go on with drawing arrows as you did).

Finally we haven’t spoken of this lone multiplicty yet: it adds a further constraint that says that, for all other columns of the relation (FileSystem and FSObject), there is at most one (lone) directory. In plain English, we rule out situations where, in a given filesystem, a given FSObject may belong to two (or more) different directories. For instance, you cannot have (F2, D, O3).

In Unix terms, this amounts to ruling out so-called “hard links”.

6

Thanks again for another excellent reply!