| Tool |
Description |
|
Alloy Analyzer
|
Alloy 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. To execute, simply double-click on the jar file, or type java -jar alloy4.jar in a console.
|
|
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.
|
|
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
|
AlloyFL is a fault localization framework for Alloy models built as an extension to the Analyzer version 5.0.1. AlloyFL returns a ranked list of suspicious locations in an Alloy model using a combination of spectrum-based and mutation-based fault localization techniques.
|
|
ARepair
|
ARepair is a command line tool built on top of Alloy4.2. Given a faulty Alloy model (potentially with multiple faults) and a set of AUnit tests that capture the desired model properties, ARepair is able to repair the model so that all AUnit tests. Internally, ARepair has three main components: a fault locator that is able to locate faults, a code generator that generate Alloy code fragments and a synthesizer that implements different search strategies to search for patches that make all tests pass.
|