Function modelator::traces

pub fn traces<P: AsRef<Path>>(
    tla_tests_file: P, 
    tla_config_file: P, 
    options: &Options
) -> Result<Vec<JsonTrace>, Error>

Generate TLA+ traces (encoded as JSON) given a crate::artifact::TlaFile containing TLA+ assertions and a crate::artifact::TlaConfigFile.

Examples

let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla";
let tla_config_file = "tests/integration/tla/Numbers.cfg";
let options = modelator::Options::default();
let traces = modelator::traces(tla_tests_file, tla_config_file, &options).unwrap();
println!("{:?}", traces);