CODEWITHSUNDEEP
alloy
Jakumi
Jakumi

Reputation: 8374

Alloy - reflexive-transitive closure includes foreign elements

So I have this mwe:

abstract sig S { r: set S }
one sig A, B extends S {}
one sig C  { }
run { r = A->B and A->A + B->B + A->B = *r }

Where I would expect the reflexive-transitive closure to be A->A + B->B + A->B, which would be the smallest enclosing relation that is transitive and reflexive, containing all elements from the domain it is defined for (S = A+B). However, it is not.

In the language reference it says

The reflexive-transitive closure of a relation is the smallest enclosing relation that is transitive and reflexive (that is, includes the identity relation).

The addition in parenthesis however seems to be meant quite literally, meaning C->C is in the reflexive-transitive closure of the relation, defined for S->S. I wonder why that is ... since it's technically not in the "real" reflexive-transitive closure as defined in math.

Wouldn't *r = ^r + iden & S->S be better? Especially, since C->C in *r throws a warning. I think this suggests that *r is indeed meant to be limited to S->S, but isn't actually limited to S->S.

Upvotes: 1

Views: 287

Answers (2)

Daniel Jackson
Daniel Jackson

Reputation: 2768

Adding one point to CMS's good answer...

You ask

Wouldn't *r = ^r + iden & S->S be better?

But this is not an option -- at least not obviously. The reason is that we don't what S is, so it would either need to be inferred (and that could create some strange cases), or it would need to be given explicitly.

Upvotes: 0

C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25054

Yes, this is one thing about Alloy's * operator that is occasionally surprising. Jackson discusses it in the questions after section 3.4.3.5 of Software Abstractions (pp. 65-66 in the revised edition). The explanation offered there is:

Although this seems odd, it follows naturally from the definition of reflexive-transitive closure and the identity relation. The alternative would be to have sets implicitly associated with each relation that represent the possible members of its domain and range, which would complicate the logic.

He goes on to point out that this is rarely an issue in practice, since when transitive closures are used in navigation expressions, the irrelevant tuples will disappear in the join, and when not, writing S <: *r will also filter out the non-S tuples. My experience, such as it is, confirms Jackson's claim: I remember this point, because it very much surprised me, the one time I encountered the issue in practice. Once in eight years (admittedly, I don't spend all my time writing Alloy models) seems a pretty modest incidence. (Translation: yes, it's surprising. But you can learn to live with it. I promise.)

I infer that the warning on C->C in *r is not a sign that * is intended to exclude irrelevant triples; it may be an acknowledgement (like the discussion in 3.4.3.5) of the fact that many users are a little taken aback at finding unexpected pairs in the transitive closure of a relation.

I hope this helps.

Upvotes: 3

Related Questions