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.
Installation
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".
Contact: tbn@cs.brown.edu