| Item | Description |
|---|---|
| Tool | Latest stable release of AlloyFL which is a self-executable JAR file. |
| Source Code | Open source code base for the latest release. Includes a collection of faulty models which can be used to explore AlloyFL. |
| Requirements |
AlloyFL has the following requirements for execution:
|
| Screen Cast | Youtube walkthrough of AlloyFL can be found here. | Paper | AlloyFL is an open source implementation of the ISSRE 2020 Paper "Fault Localization for Declarative Models in Alloy" by K. Wang, A.Sullivan, D. Marinov, and S. Khurshid. |
| Tool | Description |
|---|---|
| Alloy Analyzer v.5.1.0 | Alloy 5 is a self-contained executable, which includes the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples. The same jar file can be incorporated into other applications to use Alloy as an API and includes the source code. See the release notes for details of new features. The Analyzer is Alloy's IDE and the base for AlloyFL. |
| AUnit Analyzer | AUnit Analyzer is an extension to the Alloy Analyzer which provides support for AUnit. AUnit is a testing framework designed for the Alloy language. AUnit establishes the definition of a test case, test execution, and coverage requirements in the context of Alloy and its declarative execution environment. AlloyFL is an extension to the AUnit Analyzer which is built off of Alloy 5's open source toolset. |
| MuAlloy | MuAlloy is a command line tool built on top of Alloy4.2. The tool provides basic features to mutate an Alloy model at its AST level and generate non-equivalent mutant models. For each non-equivalent mutant model, MuAlloy is able to generate an Alloy instance that kills it. All mutant killing instances can be encoded as AUnit tests and saved on the disk. MuAlloy can also run mutation testing on any model given some tests. AlloyFL utilizes MuAlloy as part of its fault localization process. |