[24 March 2010]

Consider the following Alloy model:

sig Node {}
one sig gl { r, s : Node -> Node }{ s = *r }
run {}

It has no instances, and the Alloy Analyzer comments laconically “Predicate may be inconsistent.” But the similar model below does have instances. Why?

sig Node {}
one sig gl { r, s : univ -> univ }{ s = *r }
run {}

I ran into this phenomenon today, when I was trying to do some work relating to the definition of document order in the XPath data model. It’s convenient to have both a relation like the successor relation of arithmetic on the natural numbers, which gives you the next item in document order, and a relation like the less-than-or-equals relation of arithmetic, which is the reflexive transitive closure of the successor relation. And if you want to have both, you will want to specify, as is done above, that the one is the reflexive transitive closure of the other. And when you do, it’s a bit alarming to be told (and mostly very quickly) that nothing in your model has any instances at all.

It took me a couple hours to reduce the problem to the terms shown above (there were several complications which looked more likely to be the cause of the trouble, and which took time to eliminate), and then a little more time to realize that declaring the relations in question as Node -> Node or as univ -> univ made a difference.

I invite the interested reader, if a user of Alloy, to consider the two models and explain why one has instances and the other doesn’t. No peeking at what follows until you have a theory.

Found it? If you found it without spending a couple hours on it, my hat’s off to you.

The * operator produces the reflexive transitive closure of a binary relation r by essentially taking the union of the positive transitive closure of r and the identity relation iden. That is, for all relations r, *r is defined as ^r + iden.

The problem is that iden covers everything in the model, including the gl (globals) object and the automatically included integers. And the upshot is that s cannot satisfy the constraint s = *r while also satisfying its declaration (Node -> Node).

In his book Software Abstractions, Daniel Jackson remarks on the oddity of * including ‘irrelevant’ tuples in the relation, but (as he points out) it almost never matters, because in many context the irrelevant tuples are dropped out during evaluation of the containing expression. The consequence is that it’s possible to work with Alloy (as I have obviously been doing) with a mental model in which * is somehow smart enough to add only those tuples which are ‘relevant’ to the relation whose closure is being taken. That mental model proves to be an over-complexification.

One reason I like Alloy a lot is that it allows the user to operate at a fairly high level of abstraction, if you can just find the right level. Working in Alloy presents fewer of the small issues of syntax and data typing and so on that can bedevil attempts to explore problems even in high-level programming languages, and so you mostly get to your results a lot faster. But I guess no formal system is ever completely free of cases where the user stares blankly at the screen for some indefinite period of time, trying to figure out why the system is producing such a counter-intuitive and obviously wrong result.

In the words of the old MVS error message: Probable user error. Solution: correct and re-submit.