pub struct Apalache;
Expand description
modelator
’s Apalache module.
Implementations
pub fn test(
input_artifacts: &TlaFileSuite,
runtime: &ModelatorRuntime
) -> Result<(Vec<TlaTrace>, ModelCheckerStdout), Error>
pub fn test(
input_artifacts: &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::Apalache};
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, _) = Apalache::test(&test_tla_suite, &runtime).unwrap();
println!("{:?}", tla_trace);
pub fn parse(
tla_file_suite: &TlaFileSuite,
runtime: &ModelatorRuntime
) -> Result<(TlaFile, ModelCheckerStdout), Error>
pub fn parse(
tla_file_suite: &TlaFileSuite,
runtime: &ModelatorRuntime
) -> Result<(TlaFile, ModelCheckerStdout), Error>
Runs Apalache’s parse
command, returning the TlaFile
produced by
Apalache.
Examples
ⓘ
use modelator::artifact::TlaFileSuite;
use modelator::model::checker::Apalache;
use modelator::ModelatorRuntime;
use std::convert::TryFrom;
let tla_file = "tests/integration/resource/NumbersAMaxBMinTest.tla";
let tla_file_suite = TlaFileSuite::from_tla_path(tla_file).unwrap();
let runtime = ModelatorRuntime::default();
let (tla_parsed_file, _) = Apalache::parse(&tla_file_suite, &runtime).unwrap();
println!("{:?}", tla_parsed_file);
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Apalache
impl UnwindSafe for Apalache
Blanket Implementations
Mutably borrows from an owned value. Read more
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