Below is an Alloy model representing this set of integers: {0, 2, 4, 6}
As you know, the plus symbol (+) denotes set union. How can 0 be unioned to 2? 0 and 2 are not sets. I thought the union operator applies only to sets? Isn't this violating a basic notion of set union?
Second question: Is there a better way to model this, one that is less cognitively jarring?
one sig List {
numbers: set Int
} {
numbers = 0 + 2 + 4 + 6
}
In Alloy, everything you work with is a set of tuples. none is the empty set, and many sets are sets of relations (tuples with arity > 1). So also each integer, when you use it, is a set with a relation of arity 1 and cardinality 1. I.e. in Alloy when you use 1 it is really {(1)}, a set of a type containing the atom 1. I.e. the definition is in reality like:
enum Int {-8,-7,-6,-5,-4,-3,-2,-1,0,1,2,3,4,5,6,7}
Ints in Alloy are just not very good integers :-( The finite set of atoms is normally not a problem but with Ints there are just too few of them to be really useful. Worse, they quickly overflow and Alloy is not good in handling this at all.
But I do agree it looks ugly. I have an even worse problem with seq.
0-A + 1->B + 2->C + 3->C
I already experimented with adding literal seq to Alloy and got an experimental version running. Maybe sets could also be implemented this way:
// does not work in Alloy 4
seq [ A, B, C, C ] = 0->A + 1->B + 2->C + 3->C
set [ 1, 2, 3, 3 ] = 1+2+3
Today you could do this:
let x[a , b ] = { a + b }
run {
x[1,x[2,x[3,4]]] = 1+2+3+4
} for 4 int
But not sure I like this any better. If macros would have meta fields or would make the arguments available as a sequence (like most interpreters have) then we could do this
// does not work in Alloy 4
let list[ args ... ] = Int.args // args = seq univ
run {
range[ list[1,2,3,4,4] ] = 1+2+3+4
}
If you like the seq [ A, B, C, C ] syntax or the varargs then start a thread on the AlloyTools list. As said, I got the seq [ A, B, C, C ] working in a prototype.
