Struct modelator::model::language::Tla

pub struct Tla;

modelator’s TLA module.

Implementations

impl Tla

pub fn tla_trace_to_json_trace(tla_trace: TlaTrace) -> Result<JsonTrace, Error>

Convert a TlaTrace into a JsonTrace.

Examples

use modelator::artifact::TlaFileSuite;
use modelator::model::{language::Tla, checker::Tlc};
use modelator::ModelatorRuntime;
use std::convert::TryFrom;

let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla";
let tla_config_file = "tests/integration/resource/Numbers.cfg";
let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap();

let mut tests = Tla::generate_tests(&tla_suite).unwrap();
let test_tla_suite = tests.pop().unwrap();
let runtime = ModelatorRuntime::default();
let (tla_trace, _) = Tlc::test(&test_tla_suite, &runtime).unwrap();
let json_trace = Tla::tla_trace_to_json_trace(tla_trace).unwrap();
println!("{:?}", json_trace);

pub fn generate_tests(
    tla_file_suite: &TlaFileSuite
) -> Result<Vec<TlaTest>, Error>

Generate TLA+ test and config files given a TlaFile containing TLA+ test assertions and a TlaConfigFile.

Examples

use modelator::artifact::TlaFileSuite;
use modelator::model::language::Tla;
use std::convert::TryFrom;

let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla";
let tla_config_file = "tests/integration/resource/Numbers.cfg";
let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap();
let mut tests = Tla::generate_tests(&tla_suite).unwrap();
println!("{:?}", tests);

pub fn extract_test_names(content: &str) -> Result<Vec<String>, Error>

Generate test names from a tla file

pub fn generate_test(
    test_name: &str,
    tla_file_suite: &TlaFileSuite
) -> Result<TlaFileSuite, Error>

Generate test tla file and config for a testname

Trait Implementations

impl Clone for Tla

fn clone(&self) -> Tla

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Tla

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

Formats the value using the given formatter.

impl Copy for Tla