True and False in Alloy

Question

Alloy has plenty of logical connectives like and and or and implies. But I can't find true and false. Are they missing? At the moment I've been making do with 1=1 and 1=0, but this is rather hacky (and gives a compiler warning).

_{My reason, by the way, for wanting true and false is that I'm writing something that produces an .als file. My top-level .als file expects that my auto-generated .als file defines a wellformed predicate and a faulty predicate. Sometimes these predicates are complicated, but sometimes I just want wellformed[...] to return true, and faulty[...] to return false. This is why I want true and false in the Alloy language.}

score 4 · Accepted Answer · answered Jan 27 '16 at 11:42

4

They're not built in for a good reason: see the FAQ on p137 of Software Abstractions (Daniel Jackson, MIT Press, 2012). The issue in short is that if they were built in, you'd have to be able to declare a relation over the booleans, and then because boolean expressions could evaluate to {} and {T,F}, the connectives would need to be defined over these values, and that seemed like a really bad idea.

answered Jan 27 '16 at 11:42

Daniel Jackson

2,738
12
5

1

I bought your book to follow up on this comment! (Well, I wanted it for other reasons too.) It's an interesting issue. I still can't quite believe that it's ok to have 2-ary conjunction and disjunction operators, but *not* ok to have 0-ary conjunction and disjunction operators (for that is basically what `true` and `false` are). I suppose the problem comes when you start wanting boolean-valued variables. – John Wickerson Mar 24 '16 at 20:18

score 3 · Answer 2 · answered Jan 26 '16 at 14:55

3

Since an empty predicate is true, my favorite implementation of true and false is:

pred true {}
pred false { not true }

answered Jan 26 '16 at 14:55

Alcino Cunha

186
2

score 1 · Answer 3 · answered Jan 26 '16 at 11:44

1

pred true {no none}
pred false {some none}

seems to work; but it would be nice to have these inbuilt.

answered Jan 26 '16 at 11:44

user1513683

419
2
4

True and False in Alloy

3 Answers3