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.
1. 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].
Alloy 3 | int SomeIntegerSet | Int 2 |
---|---|---|
Alloy 4 | int[SomeIntegerSet] | Int[2] |
Change: To say an expression has a particular multiplicity, you must now use the "in" operator rather than the ":" operator.
Rationale:
The ":" symbol in Alloy 3 has two meanings.
The first meaning is to introduce a new name.
For example: "some a:A | a!=b".
The second meaning is to say that an expression
has a particular multiplicity.
For example: "bank.accounts : Person -> one Account".
The second usage intuitively fits better with the existing meaning of
the "in" keyword.
Impact: Inside a formula, the ":" operator must be changed to the "in" operator.
Alloy 3: bank.accounts : Person -> one Account
Alloy 4: bank.accounts in Person -> one Account
In Alloy 4, both forms are now replaced by "condition=>x else y".
Alloy 3 | condition => formula |
condition => formula1, formula2 |
if condition then expression1 else expression2 |
---|---|---|---|
Alloy 4 | condition => formula |
condition => formula1 else formula2 |
condition => expression1 else expression2 |
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]
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 ] {...}
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 ++ & -> <: :> [] . ~ * ^
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.
8. We don't allow "part" and "exh" in declarations any more.
For example, if the following model is /Desktop/MyProject/main.als,
then we will infer that the "helper" module is
located at /Desktop/MyProject/additonal/helper.als
module MyProject/main open MyProject/additional/helper ...
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 presense or absense will affect where Alloy 4 searches for imported modules.
module MyProject/mainIf the module line is specified, then Alloy 4 will infer that the helper module is located in a subdirectory called library.
open MyProject/library/helper
...
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.
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 explcit label if you wish.
For example:
somelabel: check { A != B } for 3
somelabel: run { some a:A, b:B | a=b } for 3
(a) First of all, its value must be relevant to the overall expression.
(b) 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.
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,
addition | a.add[b] | (If unambiguous, you can shorten this to be a+b) | |
subtraction | a.sub[b] | (If unambiguous, you can shorten this to be a-b) | |
multiplication | a.mul[b] | ||
division | a.div[b] | ||
remainder | a.rem[b] | ||
negation | - a | ||
equal | a = b | ||
not equal | a != b | ||
less than | a < b | ||
greater than | a > b | ||
less than or equal to | a <= b | ||
greater than or equal to | a >= b | ||
left-shift | a << b | ||
sign-extended right-shift | a >> b | ||
zero-extended right-shift | a >>> b | ||