Alloy Analyzer Changelog

What's new in Alloy Analyzer 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: Int | body means there exists some integer "x" such that "body" doesn't overflow and "body".
• Support for unicode identifiers.
• Cosmetic changes in the visualizer:
• "Dot" and "XML" tabs were moved to "File->Export To" menu.
• A new tab, labeled as "Text" was added to display the textual representation of the solution.