Amalgam is an extension to the Alloy Analyzer that provides explanations for the instances it finds. Concretely, if an element of an instance cannot be consistently removed, Amalgam will say so and provide a justification in the form of a proof.


Download the Amalgam JAR archive here. If you are running Linux and have Java 8 or later installed, you should be able to run the JAR archive directly. We have tested this on Ubuntu 16.04, Mac OSX 10.11.6, and Windows 7.

You can run the JAR file by typing: "java -jar amalgam.jar" at your terminal.

Example Specifications

The Alloy specifications used in our FSE 2017 paper can be found here. The INDEX.TXT file says what each spec is.

Using Amalgam

Amalgam extends the Alloy Analyzer with new explanatory features. These features are largely accessed via the evaluator. (To reach the evaluator, run a satisfiable predicate, click on "Instance" to view the instance, and then press the "Evaluator" button in the top bar.)

Provenance Commands

Amalgam adds several new commands to the evaluator:

  1. @ln+ : lists the locally-necessary positive literals;
  2. @ln- : lists the locally-necessary negative literals;
  3. @why : generates provenance(s) for a positive literal;
  4. @whynot : generates provenance(s) for a negative literal;
  5. @prov # : displays the #th provenance for the last @why or @whynot command. The evaluator will print only debugging information; the structured provenance tree and highlighting will appear in the model-editing window.

Provenance Detail

Amalgam adds an important new setting to Alloy's options menu: Provenance Detail.

The default of "1" provides less information than "2"; to see more information about each alpha formula and derivation, change this setting to "2". Different users may prefer different settings.

New Instance-Viewing Options

Buttons in the instance-viewing screen allow users (e.g.) minimize and maximize instances. The "next" button functionality remains unchanged.