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.
The Alloy specifications used in our FSE 2017 paper can be found here.
The INDEX.TXT file says what each spec is.
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.)
Amalgam adds several new commands to the evaluator:
- @ln+ : lists the locally-necessary positive literals;
- @ln- : lists the locally-necessary negative literals;
- @why : generates provenance(s) for a positive literal;
- @whynot : generates provenance(s) for a negative literal;
- @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.
Amalgam supports most of the Alloy language. It does not currently support
higher-order quantification (that cannot be Skolemized) or arithmetic.
If Amalgam reports that a literal is locally necessary but produces no provenances,
then the necessity is likely a result of the analysis bounds.
Amalgam adds an important new setting to Alloy's options menu: Provenance
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.