So the event reification pattern [aside, is anyone writing up Alloy/Electrum expertise in one of the defined Pattern forms?] defines a function in a way that I’d not seen before, what in this example I’m calling “product style”.
fun mul_product_style: Int -> Int -> Int {
multiplication_table
}
fun mul_dereference_style[x, y: Int]: Int{
y::(x::(multiplication_table))
}
behave identically, as shown by
run {
all x, y: {i: Int | 0 <= i && i < 3} | {
let p = x fun/mul y | {
mul_product_style[x,y] = p
mul_product_style[x][y] = p
x::mul_product_style[y] = p
y::(x::mul_product_style) = p
y.(x.mul_product_style) = p
mul_dereference_style[x,y] = p
mul_dereference_style[x][y] = p
x::mul_dereference_style[y] = p
y::(x::mul_dereference_style) = p
y.(x.mul_dereference_style) = p
}
}
}
which along the way illustrates all the ways I know of to apply a function.
The crucial difference is that the mul_product_style form creates a relation in the instance, which we can see in the evaluator
Indeed. The name I’ve most seen used is derived relation (or set depending in the arity). You could also call it a view as in databases. Can’t remember if it’s discussed in Daniel’s book?
Derived relations work this way too, but that’s not the intent I see in the use of this fact about functions in the event reification pattern. These:
fun _send : Event -> Node {
Send -> { n : Node | send[n] }
}
fun _compute : Event -> Node {
Compute -> { n : Node | compute[n] }
}
fun _skip : Event {
{ e : Skip | skip }
}
from your event reification example aren’t meant to be invoked, or even mentioned other than in this
fun events : set Event {
(_send + _compute).Node + _skip
}
so far as I can tell.
So not the usual sense of “a function”. They also don’t seem to me like views onto any prior thing, or a derived anything, they look to me like a way to force a structural relation into the instance de novo.
they don’t force anything, why is why I call them derived or views, as:
the possible traces would be exactly the same without these event funs
at the same time, their value is computed out of the meaningful parts of the model (tuples for which the respecting preds are true in a given state)
BUT: they can be used (and are actually used) to reason over the model: for instance, if you want to say that compute happens in a state, you can write some _compute instead of some n : Node | compute[n]. For events with larger arity, this is quite neat!
Witness my model above, in which the instance still contains a representation of 2 -> 2-> 4 even if the set of Ints in the run is restricted to {i: Int | 0 <= i && i < 2}.
The definition of a function like mul_product_style or fun _send doesn’t force anything to happen, or not happen, in the execution of a model, but it plainly does force a relation to exist in the instances even if it is not used by a run or check. In fact, if I comment out the body of the run in my model completely, the relation is still present in the instance, but if comment out the definition of mul_product_style as well then the instance is empty. It is in this sense that I say that such functions force relations into existence in an instance.
Hmm in run { all x, y: {i: Int | 0 <= i && i < 3} | { ... }} you’re limiting the scope of x and y but not of their product, which remains Int, so 2->2->4 is an acceptable tuple. Unless you add for 2 Int to your run.
Sure, I agree that these relations appear in the instances. This is the reason why we used them for the event reification idiom. It’s a very nice aspect of Alloy to have this feature, including styling capabilities.
But what I meant is that these relations are defined out of others and do not add constraints (they do not reduce the set of instances).
Which I don’t understand. In the complete model below, out of what other relations is mul_product_style built, if as previously claimed a fun is just a name for an expression?
fun mul_product_style: Int -> Int -> Int {
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
}
run {
all x, y: {i: Int | 0 <= i && i < 2} | {
let p = x fun/mul y | {
mul_product_style[x,y] = p
mul_product_style[x][y] = p
x::mul_product_style[y] = p
y::(x::mul_product_style) = p
y.(x.mul_product_style) = p
}
}
}
Your point about not limiting the scope of the product is interesting. Doing so has a very surprising effect, I find. The below model has an instance containing this value for mul_product_style
In the Alloy language and type system, you can only manipulate relations. An atom is only manipulable as a a singleton set containing one 1-tuple. So 1 is in fact {(1)}. And, for a scope of 2 Int, you have these implicit declarations:
abstract sig Int {}
one sig -2 extends Int {}
one sig -1 extends Int {}
one sig 0 extends Int {}
one sig 1 extends Int {}
or
enum Int { -2, -1, 0, 1 }
As a convenience, Alloy has a special treatment for integers to ensure that they follow the laws of two-complement integers (e.g. plus[1,1] = -2 for a scope of 2 Int) and that these laws rely on machine integers (for efficiency).
I don’t use the tabular notation… The “real” instance is the one you can see when you click the “Txt” button in the Viz.
It’s a very nice aspect of Alloy to have this feature, including styling capabilities.