Macros¶
The Alloy Analyzer comes with a textual macro system that can be handy to define reusable expressions or constraints with less technical restrictions than functions or predicates, but less safeguards too.
Macro definition¶
A predicate or function provides the ability to define a reusable expression or constraint, possibly with formal parameters. A predicate or function definition must comply with certain technical requirements, which are checked by the Alloy Analyzer:
The possible formal arguments can only stand for expressions (not predicates);
The actual arguments must comply with the arity of formal parameters as well as with related type constraints.
Macros are also reusable expressions or constraints. Syntactically, a macro is defined at the top level of a file, using the let keyword, like a pred or fun:
let m [x, y, ...] { ... }
But the definition, on the other hand, is less constrained:
The type and arity of formal arguments is not checked;
The arguments can not only stand for expressions or constraints, but even for partially-applied functions, predicates or macros.
Then, calling a macro and passing it an actual parameter corresponds to substituting textually the bound variable with the said parameter. This process is classically called macro expansion in programming languages. This is very powerful but the consequence is that most typing or arity errors, made when calling a macro, may be cryptic, and the originating error may be difficult to spot.
For this reason, the use of macros is rather discouraged. Nevertheless, their flexibility can be useful to write shorter and clearer specifications, so we illustrate them on two examples:
The first one shows how the absence of arity checking can be leveraged to simplify the writing of frame conditions;
The second one shows how one can define constraint schemas thanks to formal parameters standing for constraints.
Like predicates and functions, macros are lexically scoped, which means that if a macro refers to a name that is not part of the list of parameters, then the name will be looked for in the file where the macro was defined (rather than the file where the macro is used).
Furthermore, macros can be partially applied. This means that if a macro with say, n arguments, is called with only k < n arguments, then it yields a new macro where the said k arguments have been applied.
A macro for frame conditions¶
The effects of an event can be specified with many different styles, for example action share can be specified using two different styles. For instance, in a relational style it could look as follows.
// relational style
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
shared' = shared + f->t // effect on shared
uploaded' = uploaded // no effect on uploaded
trashed' = trashed // no effect on trashed
}
Alternatively, in a pointwise style it could take the following shape.
// pointwise style
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
f.shared' = f.shared + t // effect on f.shared
all g : File - f | g.shared' = g.shared // no effect on other shared files
uploaded' = uploaded // no effect on uploaded
trashed' = trashed // no effect on trashed
}
In both approaches, specifying frame conditions (constraints stating that some mutable signature or field doesn’t change under the action) is tedious and error-prone. Now suppose we had an unchanged predicate ensuring some argument doesn’t change in the next instant. With such a predicate, our specification of frame conditions would be shorter and safer. The version in the relational style would be adapted as follows.
// relational style
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
shared' = shared + f->t // effect on shared
unchanged[uploaded] // no effect on uploaded
unchanged[trashed] // no effect on trashed
}
The version in the pointwise style would instead be adapted as follows, where the macro is applied to particular projections of relation shared.
// pointwise style
pred share [f : File, t : Token] {
f in uploaded - trashed // guard
historically t not in File.shared // guard
f.shared' = f.shared + t // effect on f.shared
all g : File - f | unchanged[g.shared] // no effect on other shared files
unchanged[uploaded] // no effect on uploaded
unchanged[trashed] // no effect on trashed
}
In the example above, unchanged is applied to sets but, for full generality, it should also be possible to apply it to a relation, such as the binary relation shared in action upload:
// relational style
pred upload [f : File] {
f not in uploaded // guard
uploaded' = uploaded + f // effect on uploaded
unchanged[trashed] // no effect on trashed
unchanged[shared] // no effect on shared
}
Defining such a generic predicate is however impossible in Alloy. Indeed, in an Alloy predicate (or function) arguments must have a single, fixed arity, while this hypothetical unchanged predicate should accept arguments with any positive arity.
However, it is possible to define unchanged as a macro, since macros do not check the type nor arity of arguments, which is precisely the feature we need. This could be declared as follows.
let unchanged[x] { x = (x)' }
Note that the parentheses in (x)' are absolutely required: when calling unchanged, the actual argument coming in place of x may be an arbitrary complex expression, like in unchanged[g.shared] in action predicate share in the pointwise style. Suppose the expression has the shape r.s.t, with r and t both mutable fields, while s is static. Then our definition of unchanged will ensure that the prime operator is properly applied to every mutable sub-term. Indeed, according to the semantics of the prime operator, (r.s.t)' is equal to r'.s'.t', which is equal to r'.s.t' as s is static. This is different from expression r.s.t' that would results without parenthesis, with is equal to r.s.(t').
Defining constraint schemas¶
In Behavioral modeling, checking the non_restored_files_will_disappear assertion (a liveness property) relied on a fairness assumption specified as follows.
fact fairness_on_empty {
always eventually empty
}
While it was not the case here, often, several events must share a similar fairness assumption in order to ensure a liveness property. The only difference between all these assumptions is the fired event (here empty). We could just repeat them several times but it’s admittedly cumbersome and even error-prone.
A better solution would be to create a parameterized constraint. This is precisely the second usage of the macro system mentioned in the beginning of this chapter. We can thus define a fair macro as follows:
let fair [ev] { always (eventually (ev)) }
fact fairness_on_empty { fair[empty] }
Notice, again, that we write ev between parentheses in case the actual parameter contains logical connectives of lower precedence than always (such as or, if we wanted to impose the constraint on a disjunction of events). Without parentheses, fair[a or b] would expand to always (eventually a or b), which is not equivalent to always (eventually (a or b)), which is what we wanted to enforce.