What is Alloy?

Alloy is a relational logic-based language used to create models. A key strength of Alloy is its toolset, the Alloy Analyzer. The Analyzer is a scenario finder that enables users to explore the impact of their specifications through concrete instances produced by a reduction to SAT.

To learn more about Alloy, visit the website! (here)

What is 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.

The AUnit Analyzer: An extension to the Alloy Analyzer which provides support for AUnit.

• Jar: (Download)
• Sample Models: (Download)

How to run the AUnit Analyzer? Built on top of the stable release of the Alloy Analyzer (v.4.2.0), the AUnit Analyzer is a self-contained executable .

How to test a model? To see how AUnit is supported check out:

1. The tutorial in the jar (AUnit Menu -> AUnit Tutorial).
2. "Sample Models " contents.
   • "AGenCov Output" contains Alloy models with test suites which were automatically produced by AGenCov.
   • "Basic Example Models" contains two simple models highlighting different ways of formulating test cases.
   • "General Alloy Models" contains the original Alloy models that were the input for `AGenCov Output.' These models do not have any test cases but serve as a pool of models to explore the tool with.