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: 
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.
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.