Struct modelator::model::checker::Tlc [−][src]
pub struct Tlc;
Expand description
modelator
’s TLC module.
Implementations
pub fn test(
tla_file_suite: &TlaFileSuite,
runtime: &ModelatorRuntime
) -> Result<(Vec<TlaTrace>, ModelCheckerStdout), Error>
pub fn test(
tla_file_suite: &TlaFileSuite,
runtime: &ModelatorRuntime
) -> Result<(Vec<TlaTrace>, ModelCheckerStdout), Error>
Generate a TLA+ trace given a TlaFile
and a TlaConfigFile
produced
by crate::model::language::Tla::generate_tests
.
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();
println!("{:?}", tla_trace);
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Tlc
impl UnwindSafe for Tlc
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