Download Alloy Analyzer 4.2 software

[Mirror1 download link] - file hosted by alloy.mit.edu

A structural modelling language based on first-order logic, for expressing complex structural constraints and behaviour

Whats new in version 4.2:
int vs Int:
• Small ints are not supported any longer; all integers (including constant literals, the result of the cardinality operator #, etc.) are always treated as sets of integers, i.e. Int.
• Alloy built-in operators plus (+) and minus (-) are always treated as relational union and relational difference respectively.
• For arithmetic operations, the users should always use the functions provided in util/integer.als. For example, what could be written previously as a+b and a-b must now be written a.plus[b] and a.minus[b] respectively.
• Module util/integer.als is automatically included in every user-defined module. Forbid overflow option added to the Options main menu:
• When this option is set to "Yes", the Alloy Analyzer will not report models that involve integer overflows. When this option is set to "Yes", the quantifiers over integer variables have a slightly different semantics:
• all x: Int | body means for all integers "x" such that "body" doesn't overflow, "body" holds.
• some x:...