CompoSAT is a version of Alloy that produces sets of instances called ensembles. These ensembles maximize provenance coverage for the command being run. For the definition of provenance coverage, see the paper.


To download the CompoSAT jarfile, click here. If you are running Linux and have Java 8 or later installed, you should be able to run the JAR archive directly. We've tested CompoSAT on both MacOS and Linux (64-bit). (At the moment, Windows is not supported.) You can run the JAR file by typing: "java -jar composat.jar" at your terminal.

Example Specification

The running example used in our FM18 paper can be found here.

Using CompoSAT

CompoSAT is built atop Amalgam. To enumerate instances in the ensemble, use "CompoSAT Next" in the visualizer dialog. Note that the first output model is not a part of CompoSAT's output. As such, it is possible that models output by CompoSAT will contain the first output model. CompoSAT currently doesn't support interleaving between regular "Next" and "CompoSAT Next" (or any other options such as Shrink and Grow). That is, make sure that you only use "CompoSAT Next". To see CompoSAT logs, set the Alloy's verbosity level to "debug".