New Syntactic Features in Alloy 4

The syntax of Alloy 4 differs very slightly from the syntax of Alloy 3. Changes were made for three reasons: to make the syntax more uniform; to add some new features for greater convenience; to simplify the grammar to allow faster parsing and to make it easier for others to implement tools for Alloy. The grammar is now LALR(1), and compilation is instantaneous for all but the largest models.

The changes are explained in detail below. For each change, the rationale is explained, and short comments highlight the small changes that users are likely to need to make to Alloy 3 models. We expect that, for most users, the only changes needed will be replacing round by square brackets in invocations, and adding aliases for imported modules.

To cast between integers and Int atoms, use Int[ ] and int[ ]

Change: To cast from integer to an Int atom, you must use the new “Int[ ]” function. Likewise, to cast from Int to integer, you should use the new “int[ ]” function.

Rationale: This simplifies the grammar by using the function invocation syntax to do type casts.

Impact: To update an Alloy3 model, you need to replace sum X and int X with int[X], and replace Int X with Int[X].

The “:” symbol can only be used to declare a variable or field.

Change: To say an expression has a particular multiplicity, you must now use the “in” operator rather than the “:” operator.

Impact: Inside a formula, the “:” operator must be changed to the “in” operator.

if-then-else is now written as “condition=>x else y”

In Alloy 3, if-then-else formulas are written as “condition=>formula1,formula2” where as if-then-else expressions are written as “if condition then x else y”.

In Alloy 4, both forms are now replaced by “condition=>x else y”.

Function/predicate calls must use the same operators [ ] and . as relational joins.

To invoke f(a,b), you must write it as f[a,b], f[a][b], a.f[b], or b.(a.f)

To invoke f(a), you must write it as f[a] or a.f

To invoke f(), you must write it as f[ ] or simply f

In particular, note that a.add[b].sub[c] is equivalent to sub[add[a,b],c]

Likewise, a function or predicate can be declared using [ ]:

    pred contains [ m:Map, k:Key, v:Value ] {…}

Furthermore, if the list of arguments is empty, the [ ] can be omitted:

    pred acyclic {…}

Finally, the first argument can be declared using the receiver syntax:

    pred List.contains [ e:Element ] {…}

is internally converted into

    pred contains [ this:List, e:Element ] {…}

Grammar for int expressions, set/relation expressions, and formulas are unified.

This means some expressions legal in Alloy 3 may require additional parentheses for it to parse.

Operator Precedence (from low to high)

let    all a:X|F   no a:X|F   some a:X|F   lone a:X|F
one a:x|F   sum a:x|F
||
<=>
=>     => else
&&
!
in    =    <    >   <=   >=
!in   !=   !<   !>  !<=  !>=
no X   some X   lone X   one X   set X   seq X
<<     >>       >>>
+      -
#X
++
&
->
<:
:>
[]
.
~    *     ^

You can no longer set a separate scope on the number of Int atoms.

Its scope is always exactly equal to the number of possible integers corresponding to the current bitwidth (default is 4).

To set the bitwidth, use the “int” keyword in a run or check command.

For example, if you write “check MyAssertion for 4 int”, the assertion will be checked with integer bitwidth of 4. That means there are exactly 16 Int atoms ranging from -8 to 7.

You can no longer declare a signature that extends Int, or declare a signature to be a subset of Int

We don’t allow “part” and “exh” in declarations any more.

Module Search Path:**

When importing a module, Alloy 4 first searches in the installation directory. If not found, it will attempt to derive a relative path based on the current module’s name and the name of the module being imported.

For example, if the following model is /Desktop/MyProject/main.als, then we will infer that the “helper” module is located at /Desktop/MyProject/additional/helper.als

module MyProject/main
open MyProject/additional/helper
...

module” declaration is now optional.

If a model is not parametric, you can omit the “module” declaration.

Example 1

In this example, the first line is require, since it lists the parameters:

module MyProject/main[T]
...

Example 2

In this example, the first line is optional. But its presence or absence will affect where Alloy 4 searches for imported modules.

module MyProject/main
open MyProject/library/helper
...

If the module line is specified, then Alloy 4 will infer that the helper module is located in a subdirectory called library.

If the module line is omitted, then Alloy 4 assumes the main file has no path. Thus, the helper module is assumed to be in the subdirectory MyProject/library.

You can now write “check {…}” and “run {…}”

Instead of declaring an assertion X and then write check X, you can now combine them by just writing check {some formula}.

Likewise, instead of declaring a predicate X and then write run X, you can now combine them by just writing run {some formula}.

For example:

check { A!=B } for 3

is equivalent to

assert NOTEQUAL { A!=B }
check NOTEQUAL for 3

These are called “anonymous” assertions and predicates. Alternatively, you can prepend an explicit label if you wish. For example:

somelabel: check { A != B } for 3
somelabel: run { some a:A, b:B | a=b } for 3

predicates, functions, and fields can now overload each other.

That is, you can declare functions, predicates, and fields with the same name. When there’s an ambiguity, we’ll use the following rule to determine whether each candidate is compatible:

1 First of all, its value must be relevant to the overall expression. 2 Furthermore, if it’s a predicate or function, then the type of each parameter must have nonempty intersection with the type of each argument.

If exactly one function, predicate, or field is compatible, Alloy 4 will choose it automatically. Otherwise, an ambiguity error will be reported.

When necessary, Alloy4 will add int->Int and Int->int casts automatically.

For example, given an atom X, then the relational product X->3 is illegal, since both operands of -> must be set or relation values. Alloy4 knows the only way for this to be legal is to add an int-to-Int cast, so Alloy4 will parse it as if the user wrote X->Int[3]

Likewise, given an Int atom X, then the left shift expression X«2 is illegal, since both operands of « must be int values. Alloy4 knows the only way for this to be legal is to add an Int-to-int cast, so Alloy4 will parse it as if the user wrote int[X]«2.

Note: When there are two ways to make an expression legal, by adding either Int-to-int cast or int-to-Int cast, then Alloy4 prefers the Int-to-int cast since it is cheaper.

For example, given an Int atom X, then the expression X+3 is illegal, since both operands of + must be of the same type. Alloy4 knows there are two ways for this to be legal:

convert X to int[X], and you get the int value representing the sum of X and 3.
convert 3 to Int[3], and you get the union containing two atoms ("X" and "3").

Since Alloy4 prefers the Int-to-int cast since it is cheaper, so Alloy4 will parse it as if the user wrote int[X]+3</div>

Alloy4 now has syntax support for “sequence of atoms”.

For more information, please click this.</div>

Alloy4 now has syntax support for “private namespace”

Alloy4 allows you to declare a sig, a field, a function, or a predicate as “private” to the module, and not visible from other modules. For more information, please click this.</div>

Alloy4 now supports all the standard operations on int values

Note: The first five operators (add, sub, mul, div, and rem) requires that you add “open util/integer” to your model.