# Alloy 6

# Alloy 6

Alloy 6 is a new *major* version. It features new keywords and symbols that allow to specify and assess *behavioral* models natively (rather than by modeling traces explicitly as in previous versions). It also features new solving techniques as well as an upgraded Visualizer. A full reference for the language is available here. **Notice there are a few syntactic changes with respect to older versions of Alloy (see the bottom of this page).**

## Mutable signatures and fields

Alloy 6 extends previous versions of Alloy with a `var`

keyword to specify that a signature or field is *mutable*. A signature or field *not* preceded by `var`

is said to be *static* and assumed to be constant over time.

## Value of an expression in the next state

The value of an expression `e`

in the next state is denoted by `e'`

(`e`

followed by a quote). In addition to constructs from relational logic, constraints are also extended with *linear-time temporal logic with past* connectives, which allow to reason about future and past states along a trace (the meaning of connectives is given below).

## Instances are traces

Instances are now *traces*, that is *infinite* sequences of states, where a state is a valuation for signatures and fields. The considered traces are represented as *lasso* traces: that is, finite sequences featuring a loop from the last state back to a former state. Because the last state can be looped back to itself, this is completely general. The Visualizer shows a depiction of the currently-displayed lasso trace, between the toolbar and the visualization pane (see below).

An instance for a model that does not feature variable signatures or fields can be thought of as a trace made of a single state with a loop to itself. In such a case, notice the Visualizer works exactly as in older versions of Alloy.

The valuation of a mutable signature or field is likely to vary from state to state in a given trace, while *static* (that is, immutable) ones remain unchanged in a given trace. Due to the possible presence of toplevel mutable signatures, the keywords `univ`

and `iden`

no longer represent constants and should themselves be considered mutable values. On the other hand, the interpretation of a plain old Alloy model (provided it does not use any Alloy 6 syntactic construct) collapses to the usual Alloy semantics.

## Time horizon

Analyses proceed as in Alloy by bounding signatures. In addition to placing bounds on sets assigned to type signatures, the scope specification may constrain the *time horizon*, that is the possible number of transitions of *lasso* traces to explore (recall that traces *are* infinite but periodic, which allows to *represent* them as *finite* lasso traces). To do so, Alloy features a reserved `steps`

keyword to be used like type signature names in plain scopes (`steps`

cannot be used anywhere else):

- If the time horizon takes the form
`for M .. N steps`

, only lasso traces with at least`M`

transitions and at most`N`

ones (*including the looping transition*starting in the last state) will be explored (this is called*bounded model checking*). - If the time horizon takes the form
`for N steps`

, this is equivalent to`for 1 .. N steps`

- If no time horizon is given, this is implicitly equivalent to
`for 10 steps`

. - If the time horizon takes the form
`for 1.. steps`

then the time horizon will be unbounded (in that case, the selected solver must support*complete*model checking). Remark that, from the theoretical point of view, the analysis is guaranteed to terminate; but in practice, it may be very long or fail due to unavailable memory. Such an option should therefore preferably be executed to check assertions on small models and only when checking with a bounded time horizon does not find counterexamples anymore.

## Complete model-checking

As discussed just above, Alloy 6 now offers the possibility to perform *complete* model-checking, that is model-checking over all possible traces, without bounding them upfront (as explained above, the time scope must be set to `1.. steps`

). This is possible because the state space is finite thanks to scopes on signatures. Complete model-checking is theoretically guaranteed to terminate, but may fail due to lack of memory or may run for too long. Currently, NuSMV and nuXmv are supported (notice that they can also be used for bounded model checking): they must be installed by the user.

## Decomposed analysis

The `Options`

menu also features an entry labelled `Decompose strategy`

which allows the user to customize the way followed by the solver to explore traces by leveraging multiple CPU cores:

- The
`batch`

strategy analyses a problem to be solved by feeding it to a solver. - The
`parallel`

strategy leverages (signature and field) dependencies in the model to split the problem to be solved into several smaller problems. These sub-problems are then fed*in parallel*to the solver. This approach can be very effective when a problem is expected to be satisfiable as an instance may be found faster than on the original problem. On the other hand, a problem that is expected to be unsatisfiable (e.g. a`check`

expected to find no counterexample) may be solved in more time than with the`batch`

strategy. - The
`hybrid`

strategy is like the`parallel`

, except that a non-decomposed problem is also analyzed in parallel.

## Meaning of temporal connectives

A future-time temporal formula takes this form:

```
expr ::= unOp expr | expr binOp expr
unOp ::= always | eventually | after
binOp ::= until | releases | ;
```

Every such operator is interpreted in a given state of an instance (trace). To give a precise semantics, we consider the trace to be indexed by non-negative integers, starting at state 0. Then, the meaning of these operators is as follows:

- The expression
`after F`

is true in state*i*iff`F`

is true in state*i + 1*. - The expression
`always F`

is true in state*i*iff`F`

is true in every state ≥*i*. - The expression
`eventually F`

is true in state*i*iff`F`

is true in some state ≥*i*. - The expression
`F until G`

is true in state*i*iff`G`

is true in some state*j*>=*i*and`F`

is true in every state*k*such that*i*≤*k*<*j*. - The expression
`F releases G`

is true in state*i*iff`G`

is true in every state ≥*i*up to and including a state*k*in which`F`

is true, or there is no such*k*in which case`G`

holds in any state >=*i*. - The expression
`F ; G`

is true in state*i*iff`F`

is true in state*i*and`G`

is true in state*i + 1*.

The (right-associative) `;`

operator is useful to describe sequences of operations, to describe a scenario passed to a run command for instance. Indeed, supposing `p`

, `q`

, `r`

and `s`

are predicates representing operations, a run command specifying that they are played in sequence could be written:

```
run { p and after (q and after (r and after s)) }
```

or

```
run {
p
after q
after after r
after after after s
}
```

With `;`

, one can simply write:

```
run { p; q; r; s }
```

A past-time temporal formula takes this form:

```
expr ::= unOp expr | expr binOp expr
unOp ::= before | historically | once
binOp ::= since | triggered
```

The meaning of these operators is as follows:

- The expression
`before F`

is true in state*i > 0*iff`F`

is true in state*i - 1*. By convention,`before F`

is false in state 0. - The expression
`historically F`

is true in state*i*iff`F`

is true in every state ≤*i*. - The expression
`once F`

is true in state*i*iff`F`

is true in some state ≤*i*. - The expression
`F since G`

is true in state*i*iff`G`

is true in some state*j*≤*i*and`F`

is true in every state*k*such that*j*<*k*≤*i*. - The expression
`F triggered G`

is true in state*i*iff`F`

is true in some state*j*≤*i*and`G`

is true in every state*j*<*k*≤*i*, or`F`

if false in every state ≤*i*in which case`G`

is true in every state ≤*i*.

## Extended Visualizer

Alloy 6 also features a Visualizer enhanced to display traces in a user-friendly way. The visualization pane shows variable fields and signatures with dashed lines. It is split into two contiguous panes which show two consecutive states. The lasso trace depicted above the two states shows where you are in the trace by coloring the states in white. Finally, the Visualizer features a sophisticated way to explore alternative instances of a specification:

`New config`

yields a trace where the configuration (that is, the valuation of*static*parts) changed`New trace`

yields a new trace under the same configuration`New init`

yields a trace with a different initial state, under the same configuration`New fork`

yields a new trace which is similar to the current one until the currently-displayed state but differs afterwards.

## Compatibility with pre-6 models

Alloy 6 uses new symbols (exactly two: the single quote `'`

and the semicolon `;`

) and several new keywords (as well as ones reserved for possible future extensions) listed below in alphabetical order:

```
after always before enabled event eventually historically invariant modifies once releases since steps triggered until var
```

Alloy 6 is compatible with old models as long as they don’t use these symbols or keywords.

On the other hand, if an old model of yours uses single quotes or some of these keywords (as identifiers), then you will have to replace them to ensure that Alloy 6 interprets your model as before (for instance changing `var`

into `var_`

or `variable`

or `foo`

). Notice the single quote can for instance be replaced with the double quote symbol `"`

(which is legal Alloy).