I have a model with a sig similar to this one:
sig State {
ps: set P,
cs: set C,
o: set C -> set P,
m: set M
}
And predicates like this, dealing with two State
s:
pred my_pred [s, s': State] {
...
}
I'm trying to create a parameterized version of my model, where I don't have a State
sig, and instead I pass those fields around explicitly in functions and predicates. That would mean having predicates that look something like
pred my_pred [(M -> P -> C -> (C -> P)) ->
(M -> P -> C -> (C -> P))] {
...
}
My question is, how can one easily deal with relations of relatively large arity, such as the one in my_pred
? For instance, I was trying to use dom
from util/relation
, but dom
is defined over a binary relation, and unfortunately it seems that alloy sees this
(M -> P -> C -> (C -> P))
->
(M -> P -> C -> (C -> P))
as a relation of arity 10 rather than 2; meaning that the parenthesizing is ignored. So using dom
would return something of type M
, rather than of the desired type of (M -> P -> C -> (C -> P))
.
Also on a related note, I was wondering if/how one could use the transitive closure operators on relations like this.
It's generally bad practice to have relations of arity greater than 3.
Why don't you simply declare your predicate as follows :