Alloy Analyzer 4

Version 4 of the Alloy Analyzer is a complete rewrite, offering improvements in robustness, performance and usability. The new codebase is approximately a quarter of the size of the codebase of Alloy 3. Compilation is now instantaneous for all but the largest models, and analysis is often a factor of 2-10 faster. We recommend that all users switch to this new version. There are a small number of syntactic improvements over Alloy 3, and models written in Alloy 3 will therefore require some very small alterations to run in Alloy 4.

The Alloy Analyzer 4 is based on the new SAT-based model finder Kodkod. Kodkod applies new techniques and optimizations to the translation from relational to boolean logic, such as user-provided partial instances and a more general symmetry-breaking technique that works in the presence of arbitrary partial instances.

System Requirements:

Java 5 or above

Download Alloy Analyzer 4.1.7

Mac OS X: download and open this dmg file.

All Others: download and double-click this jar file. Or download the file then type  java -jar alloy4.jar   into a command prompt.

Note: Ancient versions of Alloy 4.0 BETA uses the Java Webstart deployment technology and is incompatible with the newer Alloy4. Please type javaws into a command prompt, select Alloy4, then click Remove.

Documentation

A step-by-step walkthrough and tutorial of Alloy4 is here and here.

A list of frequently asked questions is here.

The grammar is here.

For existing Alloy 3 users, please refer to the Alloy 4 quick guide for the list of changes, as well as an overview of the new analyzer.

For new users, we are in the process of updating the existing user manual and tutorials for Alloy 4. In the mean time, please refer to the old Alloy 3 documentation in conjunction with the Alloy 4 quick guide.

The book "Software Abstractions: Logic, Language, and Analysis":

Daniel Jackson's book Software Abstractions: Logic, Language, and Analysis was based on Alloy 3.
The complete list of how to update the book for Alloy 4 is listed here.

Furthermore, the examples in the book have been updated to the Alloy 4 syntax.
They are now included in Alloy 4's sample directory, and can also be downloaded as a single zip file, or be browsed online.

What's New

• [2008 Alloy 4.1.7] Bug fixes.
  
  
• [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 Alloy 4.1.2] Fixed a bug on Windows Vista where attemping to load a File Open or File Save dialog could crash the application.
  
  
• [2008 Alloy 4.1.1] Fixed a rare corner case where scope computation sometimes would miss assigning a scope to a signature.
  
  
• [2008 Alloy 4.1] Enhanced solution enumeration to further eliminate some equivalent solutions.
  
  
• [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 RC14] Fixed a few typos in the included models. Also, Alloy4 will now emit a warning when it sees (a = b), (a != b), (a in b), or (a !in b) where a and b are syntactically identical.
  
  
• [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] Alloy4 now has builtin support for sequence of atoms. An introduction on the new seq keyword is here.
  
  
• [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 typechecker now generates warning messages when it detects irrelevant subexpressions. An irrelevant subexpression is an expression whose value does not contribute to the validity of the overall formula, and is thus likely erroneous.
  
  
• [2006] The compiler now inserts automatic int->Int casts and Int->int casts when necessary.
  
  

Using Alloy4 with your own Text Editor

Daniel Le Berre and his group have developed an Eclipse plugin for Alloy Analyzer 4. It is still under development, but it has already proven useful to many users.

Allison Waingold wrote an Emacs major mode for Alloy 3. We have not had the opportunity to update it for Alloy 4, but hopefully its syntax highlighting and other features can still be useful for Alloy 4 users.

There is a VIM syntax for Alloy4.

There is an a2ps stylesheet for Alloy4.

Troubleshooting

1. If you see the error message "java.lang.UnsupportedClassVersionError", that means your Java version is too old. Alloy4 requires Java 5 or newer.
   
   
2. If you've downloaded a new version of Alloy4, but an old version (Alloy4 BETA7) keeps appearing, then you may have a stale entry in your Java Webstart registry.
   Please type javaws into a command prompt, select Alloy4, then click Remove.
   
   
3. If you get the error message "java is not in your current program search path", please add it to your path. For Windows users, please refer to the "update the PATH variable" section in Sun's installation guide. For other OS, please refer to the appropriate documentation.
   
   

Feedback

We'd like to hear from you! Email us at:

To discuss Alloy with other users, post a message in the alloy discussion forum.

Source Download

The source code for the Alloy Analyzer is included in alloy4.jar (in the /edu/mit/csail/sdg directory),
and is placed under the MIT license.

The Alloy Analyzer utilizes several third-party packages whose code may be distributed under a different license (see the various LICENSE files in the distribution for details). We are extremely grateful to the authors of these packages for making their source code freely available.

• Kodkod
• CUP Parser Generator for Java
• JFlex scanner generator
• The SAT4J solver
• The MiniSat solver
• The zChaff solver