Struct modelator::model::language::Tla [−][src]
pub struct Tla;
Expand description
modelator
’s TLA module.
Implementations
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);
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);
Generate test names from a tla file
pub fn generate_test(
test_name: &str,
tla_file_suite: &TlaFileSuite
) -> Result<TlaFileSuite, Error>
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
Auto Trait Implementations
impl RefUnwindSafe for Tla
impl UnwindSafe for Tla
Blanket Implementations
Mutably borrows from an owned value. Read more
pub fn vzip(self) -> V
Attaches the provided Subscriber
to this type, returning a
WithDispatch
wrapper. Read more
Attaches the current default Subscriber
to this type, returning a
WithDispatch
wrapper. Read more