Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
But, in every event, this macro should be called for every unchanged relation (or part of, e.g. with <:), as in:
var sig S { var r1, r2 : set S }
...
pred ev[...] {
...
unchanged[S]
unchanged[r1]
unchanged[x <: r2]
...
}
Can we implement a single call to unchanged? Almost, using meta... The following is possible:
let allUnchanged[X] { all x: X | x.value = (x.value)' }
pred ev[...] {
...
allUnchanged[S$ + S$r1] // won't work with `x <: r2`
unchanged[x <: r2]
...
}
The allUnchanged macro is nice but (1) it must be called with ugly meta-arguments (incl. fully-qualified meta-names like S$r1) and (2) it only works for fully-unchanged stuff (it won't work on x <: r2.
I am here proposing that we add comma-delimited var-args to macros as well as an args$ meta-sig, local to its enclosing macro, so that something like this could be written:
let allUnchanged[X] { all x : args$ | x = (x)' }
pred ev[...] {
...
allUnchanged[S, r1, (x <: r2)]
...
}
Macros allow to implement an
unchanged
macro as:But, in every event, this macro should be called for every unchanged relation (or part of, e.g. with
<:
), as in:Can we implement a single call to unchanged? Almost, using meta... The following is possible:
The
allUnchanged
macro is nice but (1) it must be called with ugly meta-arguments (incl. fully-qualified meta-names likeS$r1
) and (2) it only works for fully-unchanged stuff (it won't work onx <: r2
.I am here proposing that we add comma-delimited var-args to macros as well as an
args$
meta-sig, local to its enclosing macro, so that something like this could be written: