Relational Operators and Quantified Expressions

I understand the arguments for preferring relational expressions over quanitfications in general.

What I’m finding in my first exploration of a big, messy model is that it’s valuable to me in managing my thoughts and actions to write predicates which are in my intent primarily part of the model in relational style and predicates which are in my intent primarily about the model in quantifier style. It helps me to use these two different (but formally equivalent) idioms to refelect a difference in my intent.

One of the things I really like about Alloy (by contrast with, say, Z) is the way it affords a behaviour similar to TDD: going back and forth between what I want to be true of the model next and making it so. I find that writing in quantifier style the predicates that I explicitly check, which by analogy are my tests, I can build them up, often capturing ideas that I’ve explored in the evaluator. This, rather than having to figure them out in one go, as it feels I need to do with relational expressions.

Which is not to say that it isn’t valuable to know the idiomatic use of relational operators, it clearly is. But it is to say that I don’t at this time feel that that they are alwasy preferred when writin any pred.

How do others mark that about vs of distinction? If you draw it at all.


To me conciseness is why I like Alloy. I love the fact that a single page of Alloy can describe a complex problem. So I take the least complex expression. I.e. Doors.state = Locked is imho significantly simpler than all d : Doors | d.state = Locked. After all, the quantifier is more text to parse and it introduces a new name to understand.

Another problem is that you sometimes are forced to use quantifiers (or get really complex relational expressions), I think you will confuse people that assumed the use that read then more (or less) in the quantifier than there really is.