Getting Alloy to find the largest answer for particular sets
-
29-06-2021 - |
Question
I'm trying to see if I can get Alloy to return the largest possible answer for a particular set. So, in this example, I would like the answers x={}
, x=A
, and x=B
to not be generated by the model finder.
abstract sig X{}
one sig A extends X{}
one sig B extends X{}
pred(x: set X) {
x in A + B
}
I have tried something along the lines of:
pred(x: set X) {
x in A + B and
no y : set X |
y in A + B and #(y) > #(x)
}
but I get an error that analysis is not possible since it requires higher-order quantification.
I was wondering if there is a possible (or simpler) way to do this?
Solution
Alloy does not currently have any built-in functionality to produce maximal or minimal solutions. And yes, you're right that specifying that a solution is maximal generally requires higher order quantification. However, you can ensure that the solution is at least locally maximal with a first order quantification:
pred p (x: set X) {...}
pred locally_maximal_p (x: set X) {
p(x)
no e: X - x | p(x + e)
}