Alloy syntax for remainder types?

Question

Is there a direct way to represent a remainder type in Alloy, rather than having to subtract the union all subtypes explicitly? For instance, in:

sig Test {}
one sig A, B extends Test {}    

I'd like to be able to refer to the expression Test-(A+B) via shorthand that doesn't need to change every time Test gets extended by a new sig. Although this would only be syntactic sugar, it could help me avoid mistakes when refactoring models.

Answer 1

You could introduce a set that represents the remainder as follows:

abstract sig Test {}
sig Remainder extends Test {}
one sig A, B extends Test {}

This will partition the set of Test atoms into three subsets, with Remainder being equivalent to Test - (A + B). If you later decide to extend Test by adding one sig C, for example, Remainder will still give you the remainder set.

Answer 2

I haven't used Alloy in a while, but I don't think it is possible the way you want it. However, you can refactor the union to just one place in the model. Example:

sig Test {}
one sig A, B extends Test {}

fun Remainder : set Test {
    Test - (A+B)
}

run { some Remainder } for 5

You define a relation, using a function, here called Remainder, that is defined by subtracting the union of all subtypes from the base type.
Everytime you add a new subtype to the model, just remember to add it to the definition of Remainder as well and you're good to go.

Throughout the model, you can just refer to Remainder to get all pure Test atoms, just as I used in the anonymous predicate in the run command.

Answer 3

If you want the definition to hold whatever the new sigs extending Test are introduced, you can use Alloy's little known meta capabilities, that allow you to iterate through sigs through a special set sig$.

E.g., you can do something like:

fun Remainder [] : set Test {
  {t : Test | all sig : sig$ | sig = Test$ || t not in sig.value}
}