Struct AlloyModel 

pub struct AlloyModel {
    pub module_name: String,
    pub signatures: Vec<Signature>,
    pub facts: Vec<Fact>,
    pub assertions: Vec<Assertion>,
    pub comment: Option<String>,
}

A complete Alloy model comprising sigs, facts, assertions, and commands.

This is the top-level structure that gets serialised into an .als file. The model can be loaded into Alloy Analyzer for verification.

Fields

module_name: String

The module name (first line of the .als file).

signatures: Vec<Signature>

All signatures in the model.

facts: Vec<Fact>

All facts (constraints) in the model.

assertions: Vec<Assertion>

All assertions to check.

comment: Option<String>

Optional opening comment describing the model’s purpose.

Implementations

impl AlloyModel

pub fn new(module_name: impl Into<String>) -> Self

Create a new empty model with the given module name.

pub fn add_signature(&mut self, sig: Signature)

Add a signature to the model.

pub fn add_fact(&mut self, fact: Fact)

Add a fact to the model.

pub fn add_assertion(&mut self, assertion: Assertion)

Add an assertion to the model.

pub fn render(&self) -> String

Render the complete model as an Alloy 6 .als file.

Trait Implementations

impl Clone for AlloyModel

fn clone(&self) -> AlloyModel

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AlloyModel

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.