Struct modelator::artifact::TlaFileSuite

pub struct TlaFileSuite {
    pub tla_file: TlaFile,
    pub tla_config_file: TlaConfigFile,
    pub dependency_tla_files: Vec<TlaFile>,
}

TODO: split module and cfg into two parts and contain the main module and extended modules in module struct An in-memory representation of all the resources needed to perform model checking Includes the main .tla and .cfg files as well as depended on (via EXTENDS) .tla files.

Fields

tla_file: TlaFile

The tla file being used as a target for a model checker command

tla_config_file: TlaConfigFile

The config file being used for a model checker command

dependency_tla_files: Vec<TlaFile>

Depended-on TLA files (via transitive closure of EXTENDS)

Implementations

impl TlaFileSuite

pub fn from_tla_and_config_paths<P: AsRef<Path>>(
    tla_file_path: P,
    config_file_path: P
) -> Result<Self, Error>

Gather all model checking resources from a main .tla and .cfg file

pub fn from_tla_path<P: AsRef<Path>>(tla_file_path: P) -> Result<Self, Error>

Gather all resources from a main .tla without .cfg file

Trait Implementations

impl Debug for TlaFileSuite

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

Formats the value using the given formatter.

impl<'a> IntoIterator for &'a TlaFileSuite

type Item = Box<&'a dyn ArtifactSaver>

The type of the elements being iterated over.

type IntoIter = IntoIter<Self::Item>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.