Struct Spec 

pub struct Spec { /* private fields */ }

A specification: a root module together with every module it reaches.

Implementations

impl Spec

pub fn parse(src: &str) -> Result<Self>

Parse a self-contained specification. EXTENDS of a standard module is honoured; anything else it names is reported as missing.

pub fn from_file(path: impl AsRef<Path>) -> Result<Self>

Read a specification from a .tla file, resolving whatever it extends or instantiates from the directory the file is in — which is where TLA+ tools look, and what makes a path enough to work from.

pub fn load(src: &str, modules: &impl Modules) -> Result<Self>

pub fn name(&self) -> &str

pub fn variables(&self) -> impl Iterator<Item = &str>

The variables of the root module, including any it inherits.

pub fn constants(&self) -> impl Iterator<Item = &str>

pub fn defines(&self, name: &str) -> bool

Trait Implementations

impl Debug for Spec

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

Formats the value using the given formatter.