Create a new Alloy instance. If no text is provided, an empty instance is created.
A string containing the XML output from an Alloy instance
Get an atom by ID.
The atom ID
An atom or null if there is no atom with the specified ID
Get an array of all atoms in the instance.
Get the bitwidth of the instance.
Generate a deep clone of the instance.
Get the command used to generate the instance.
Get a field by ID.
The field ID
A field or null if there is no field with the specified ID
Get an array of all fields in the instance.
Get the full path of the model used to generate the instance.
Project the instance over the specified atoms. There may be a maximum of one atom per signature that is a direct descendant of the univ signature.
The list of atoms over which to project the instance.
A clone of the instance with the projection applied.
Get the currently projected atoms.
A Map object with key-value pairs mapping signatures to projected atoms
Get a signature by ID
The signature ID
A signature or null if there is no signature with the specified ID
Get an array of all signatures in the instance.
Get a skolem by ID
The skolem ID
A skolem or null if there is no skolem with the specified ID
Get an array of all skolems in the instance.
Get all source files that define the model from which this instance was created.
A Map object with key-value pairs mapping full path names to file contents
Get the univ signature.
The univ signature if it exists, null if it does not
In Alloy, when you run a predicate or check an assertion, the analyzer searches for an instance of an analysis constraint: an assignment of values to the variables of the constraint for which the constraint evaluates to true [Jackson 2012].