release notes

• [2012 Alloy 4.2] Includes the following semantic changes:
  • 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.

• [2008 Alloy 4.1.10] Includes a new atom numbering heuristic which should make util/ordering numbering more intuitive; also upgraded to the latest Kodkod, and upgraded to SAT4J 2.0.5.
• [2008 Alloy 4.1.10] PDF export uses compression techniques and results in up to 20x smaller file size.
• [2008 Alloy 4.1.3] Added syntax highlighting to the builtin text editor (which can be enabled or disabled in the Options menu).
  Also, the full Kodkod source code is now included in alloy4.jar as well.
• [2008 Alloy 4.1.3] You can now use the new enum keyword to declare singleton subsigs.
  For example, "enum X { A, B, C }" means "abstract sig X { } one sig A, B, C extends X { }"
• [2008 Alloy 4.1.3] You can now use the existing disj keyword on the right hand side of a field declaration to mean that every distinct atom of that sig will have disjoint values for that field.
  For example, "sig X { f: disj Y }" means "all disj a, b: X | no (a.f & b.f)"
• [2008 RC18] Other than bug fixes, we've also modifed the XML instance file format to include richer semantic information (If your research depends on the previous version, you can still download Alloy4 RC17 here.
• [2008 RC17] Other than bug fixes, we've also added left-shift (<<), sign-extended right shift (>>), and zero-extended right shift (>>>) operators for the primitive integers. The Alloy4 quick guide and the builtin help files have been updated to reflect these new features and changes.
• [2008 RC16] In the visualizer, you can now click THEME and then choose whether private sigs and fields should be shown or hidden (by default, Alloy4 will now hide all private sigs and fields in the visualizer unless you UNCHECK this option). Also, starting with this version, the source code is now available under the MIT license instead of GPL.
• [2008 RC15] private is a new reserved keyword that you can use to declare a given sig/fun/pred is private to this module, and does not show up in the name space of other modules that import this module. For more information, please see this.
• [2008 RC15] util/integer now provides add/sub/mul/div/rem functions for performing integer addition, subtraction, multiplication, division, and remainder.
  Just import util/integer and then you can write 2.mul[3] to multiply 2 by 3, for example.
• [2008 RC15] You no longer have to provide an alias for complicated import statements. (Though if you imported two modules that both have a function named X, and if there is an ambiguity over which X you mean, then you need to add the alias for the two import statements in order to disambiguate it)
• [2007 RC12] Alloy Analyzer now uses a pure Java graph layout engine. We no longer need to distribute a platform-dependent GraphViz binary for doing graph layout. Furthermore, the new layout algorithm allows the user to click on a node and move it around on the screen. (You can right-click on the graph to export it as PDF or PNG, or you can click on the DOT button to get the equivalent DOT description and then use GraphViz DOT to render it if you want).
• [2007 RC12] To enable unsat core, go to the options menu and choose "MiniSat with Unsat Core" as the solver. If an assertion or command is unsatisfiable, you can click it to highlight the relevant portions of the original model that contributed to the unsatisfiability. The unsat core algorithm is now much more precise, and you can change the speed/precision setting (between "fast and imprecise" and "slower and more precise")
• [2007 RC12] Added a RELOAD button to reload the model from disk if you were editing the file using a separate text editor outside of Alloy4's user interface.
• [2007 RC12] The evaluator now supports command history, where you can use the UP and DOWN arrow keys to bring back previously typed expressions.
• [2007 RC11] You can click "Magic Layout" in the visualizer to automatically infer visualizer settings for you. The heuristics are described in our upcoming paper Automatic Visualization of Relational Logic Models
• [2007 RC11] You can now type the atoms and skolem values in the evaluator.
• [2007 RC11] You can now use <= (as well as the original =<) to say "less than or equal".
• [2007 RC7] Builtin support for sequences of atoms added.
• [2007] When executing a "run" or "check" command that is taking too long, you can now click the Stop button to reliably abort the command.
• [2007] You can set the amount of memory allocated for SAT solving by going to the Options menu. The default amount of allocated memory is 768M.
• [2006] When viewing an instance in the visualizer, you can click Evaluate to evaluate Alloy expressions on that instance, or click Next to see the next satisfying instance if one exists.
• [2006] The compiler now inserts automatic int->Int casts and Int->int casts when necessary.
© 2012 Daniel Jackson. Built on the Not Just a Grid framework and a design by Emina Torlak.