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.