PV3 ⊧ Alloy Analyzerchecks user-specified assertions in Alloy models

Application domain/field

State machines with complex structured state

Type of tool

Constraint solver

Expected input

Model (with assertions/properties)

Format:

Alloy language

Expected output

Counterexample or "assertion may be valid"

Internals

The Alloy Analyzer translates the given problem into a boolean formula which is then handed to a SAT solver. When the SAT solver is done, the solution is translated back into the language of the original model. The user needs to specify a scope that bounds the size of the domains thereby making the problem finite and thus reducible to a boolean formula. Uses SAT solvers to refute a formula. It uses Sat4j, MiniSat, plingeling and Glucose for SAT solving.

Comments

Domains (in the model) are bound by the user, resulting in a finite problem.