This github repo contains the source code to AlloyFL as well as the model used as an example in the paper (under example) and the set of real world faulty models used to evaluate AlloyFL (under experiments).

AlloyFL is an extension to the Alloy Analyzer with support for fault localization. Given a faulty Alloy model (potentially with multiple faults) and a set of AUnit tests that capture the desired model properties, AlloyFL returns a ranked list of suspicious locations within the model that are likely to be faulty.

• Operating Systems

  • Linux (64 bit)
  • Mac OS (64 bit)

• Dependencies

  • Java 8: Must be installed and accessible from PATH.

If you elect to build and compile AlloyFL yourself, it is recommended you follow the installation instructions outlined here and reproduced below for convenience. Since AlloyFL builds on the Analyzer, it requires the user to set up and install the Analyzer's code base.

The Alloy build is using a bnd workspace setup using a maven layout. This means it can be build with Gradle and the Eclipse IDE for interactive development. Projects are setup to continuously deliver the executable.

The workspace is divided into a number of projects:

• cnf – Setup directory. Dependencies are specified in [cnf/central.xml] using the maven POM layout
• org.alloytools.alloy.application – Main application code includes the parser, ast, visualiser, and application code
• org.alloytools.alloy.dist – Project to create the distribution executable JAR
• org.alloytools.alloy.extra – Models and examples
• org.alloytools.pardinus – A Kodkod extension without native code
• org.alloytools.kodkod.nativesat – The native code libraries for Kodkod

This workspace uses bnd. This means that the following have special meaning:

• cnf/build.xml – Settings shared between projects
• ./bnd.bnd – Settings for a project. This file will drag in code in a JAR.
• cnf/central.xml – Dependencies from maven central

The workspace is setup for interactive development in Eclipse with the Bndtools plugin. Download Eclipse and install it. You can then Import existing projects from the Git workspace. You should be asked to install Bndtools from the market place. You can also install Bndtools directly from the Eclipse Market place (see Help/Marketplace and search for Bndtools).

Bndtools will continuously create the final executable. The projects are setup to automatically update when a downstream project changes.

Ensure you have the [Osmorc] plugin is enabled, as this plugin is needed for Bndtools support. It should be enabled by default.

1. Choose "Import Project"
2. Select the org.alloytools.alloy directory.
3. Choose "Import project from external model: Bnd/Bndtools" and click "Next"
4. For "Select Bnd/Bndtools project to import", all projects should be checked by default, click "Next"
5. For project SDK, Choose "1.8", Click Finish

Note: do not link the Gradle project, as this will prevent you from running Alloy within IDEA.

To run the Alloy GUI within IDEA, navigate to org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI and run the SimpleGUI class.