|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
See:
Description
Class Summary | |
---|---|
A4Options | Mutable; this class encapsulates the customizable options of the Alloy-to-Kodkod translator. |
A4Options.SatSolver | This enum defines the set of possible SAT solvers. |
A4Solution | This class stores a SATISFIABLE or UNSATISFIABLE solution. |
A4SolutionReader | This helper class contains helper routines for reading an A4Solution object from an XML file. |
A4SolutionWriter | This helper class contains helper routines for writing an A4Solution object out as an XML file. |
A4Tuple | Immutable; represents a single Alloy tuple; comparison is by identity rather than by value. |
A4TupleSet | Immutable; represents a collection of Alloy tuples; comparison is by identity rather than by value. |
Simplifier | Immutable; this class shrinks the unknowns as much as possible in order to reduce the number of variables in final CNF. |
TranslateAlloyToKodkod | Translate an Alloy AST into Kodkod AST then attempt to solve it using Kodkod. |
TranslateKodkodToJava | Translate a Kodkod formula node to an equivalent Java program that solves the formula. |
This package contains the translator from Alloy4 to CNF (using kodkod).
|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |