Struct modelator::ModelatorRuntime [−][src]
pub struct ModelatorRuntime {
pub model_checker_runtime: ModelCheckerRuntime,
pub dir: PathBuf,
}
Expand description
Set of options to configure modelator
runtime.
Fields
model_checker_runtime: ModelCheckerRuntime
Model checker runtime.
dir: PathBuf
Modelator directory.
Implementations
Set TLC runtime.
Given a crate::artifact::TlaFile
with TLA+ test assertions,
as well as a crate::artifact::TlaConfigFile
with TLA+ configuration,
generate all traces resulting from the test assertions.
The traces are generated by executing a model checker,
which can be selected via ModelatorRuntime
.
Examples
let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla";
let tla_config_file_path = "tests/integration/tla/Numbers.cfg";
let runtime = modelator::ModelatorRuntime::default();
let trace_results = runtime.traces(tla_tests_file_path, tla_config_file_path).unwrap();
println!("{:?}", trace_results);
pub fn run_tla_steps<P, System, Step>(
&self,
tla_tests_file_path: P,
tla_config_file_path: P,
system: &mut System
) -> Result<TestReport, Error> where
P: AsRef<Path>,
System: StepRunner<Step> + Debug + Clone,
Step: DeserializeOwned + Debug + Clone,
pub fn run_tla_steps<P, System, Step>(
&self,
tla_tests_file_path: P,
tla_config_file_path: P,
system: &mut System
) -> Result<TestReport, Error> where
P: AsRef<Path>,
System: StepRunner<Step> + Debug + Clone,
Step: DeserializeOwned + Debug + Clone,
This is the most simple interface to run your system under test (SUT)
against traces obtained from TLA+ tests.
The function generates TLA+ traces using ModelatorRuntime::traces
and execute them against
the SUT that implements StepRunner
.
For more information, please consult the documentation of ModelatorRuntime::traces
and
StepRunner
.
Example
use modelator::StepRunner;
use serde::Deserialize;
// Suppose your system under test (SUT) consists of two integer variables,
// where each number can be increased independently;
// SUT also maintains the sum and product of the numbers.
use modelator::test_util::NumberSystem;
// We define a structure that is capable to serialize the states of a TLA+ trace.
#[derive(Debug, Clone, Deserialize)]
#[serde(rename_all = "camelCase")]
struct NumbersStep {
a: u64,
b: u64,
action: Action,
action_outcome: String
}
// We also define the abstract actions: do nothing / increase a / increase b.
#[derive(Debug, Clone, Deserialize)]
enum Action {
None,
IncreaseA,
IncreaseB
}
// We implement `StepRunner` for our SUT
// This implementation needs to define only a couple of functions:
impl StepRunner<NumbersStep> for NumberSystem {
// how to handle the initial step (initialize your system)
fn initial_step(&mut self, step: NumbersStep) -> Result<(), String> {
self.a = step.a;
self.b = step.b;
Ok(())
}
// how to handle all subsequent steps
fn next_step(&mut self, step: NumbersStep) -> Result<(), String> {
// Execute the action, and check the outcome
let res = match step.action {
Action::None => Ok(()),
Action::IncreaseA => self.increase_a(1),
Action::IncreaseB => self.increase_b(2),
};
let outcome = match res {
Ok(()) => "OK".to_string(),
Err(s) => s,
};
assert_eq!(outcome, step.action_outcome);
// Check that the system state matches the state of the model
assert_eq!(self.a, step.a);
assert_eq!(self.b, step.b);
Ok(())
}
}
// To run your system against a TLA+ test, just point to the corresponding TLA+ files.
fn test() {
let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla";
let tla_config_file_path = "tests/integration/tla/Numbers.cfg";
let runtime = modelator::ModelatorRuntime::default();
let mut system = NumberSystem::default();
assert!(runtime.run_tla_steps(tla_tests_file_path, tla_config_file_path, &mut system).is_ok());
}
pub fn run_tla_events<P, System>(
&self,
tla_tests_file_path: P,
tla_config_file_path: P,
system: &mut System,
runner: &mut EventRunner<System>
) -> Result<TestReport, Error> where
P: AsRef<Path>,
System: Debug + Default,
pub fn run_tla_events<P, System>(
&self,
tla_tests_file_path: P,
tla_config_file_path: P,
system: &mut System,
runner: &mut EventRunner<System>
) -> Result<TestReport, Error> where
P: AsRef<Path>,
System: Debug + Default,
Run the system under test (SUT) using the abstract events obtained
from TLA+ traces. Traces are generated using ModelatorRuntime::traces
,
To interpret abstract events an EventRunner
needs to be created,
as well as StateHandler
and ActionHandler
to be implemented
for abstract states and actions you want to handle.
Example
use modelator::{EventRunner, ActionHandler, StateHandler};
use serde::Deserialize;
// Suppose your system under test (SUT) consists of two integer variables,
// where each number can be increased independently;
// SUT also maintains the sum and product of the numbers.
use modelator::test_util::NumberSystem;
// In order to drive your SUT, we could define two abstract states,
// that contain the state of the variables `a` and `b`.
#[derive(Debug, Clone, Deserialize, PartialEq)]
struct A {
a: u64,
}
#[derive(Debug, Clone, Deserialize, PartialEq)]
struct B {
b: u64,
}
// We also define the abstract actions: do nothing / increase a / increase b.
#[derive(Debug, Clone, Deserialize)]
enum Action {
None,
IncreaseA,
IncreaseB
}
// We define StateHandlers that are able to initialize your SUT from
// these abstract states, as well as to read them at any point in time.
impl StateHandler<A> for NumberSystem {
fn init(&mut self, state: A) {
self.a = state.a
}
fn read(&self) -> A {
A { a: self.a }
}
}
impl StateHandler<B> for NumberSystem {
fn init(&mut self, state: B) {
self.b = state.b
}
fn read(&self) -> B {
B { b: self.b }
}
}
// We define also an action handler that processes abstract actions
impl ActionHandler<Action> for NumberSystem {
type Outcome = String;
fn handle(&mut self, action: Action) -> Self::Outcome {
let result_to_outcome = |res| match res {
Ok(()) => "OK".to_string(),
Err(s) => s
};
match action {
Action::None => "OK".to_string(),
Action::IncreaseA => result_to_outcome(self.increase_a(1)),
Action::IncreaseB => result_to_outcome(self.increase_b(2))
}
}
}
// To run your system against a TLA+ test, just point to the corresponding TLA+ files.
fn main() {
let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMaxTest.tla";
let tla_config_file_path = "tests/integration/tla/Numbers.cfg";
let runtime = modelator::ModelatorRuntime::default();
// We create a system under test
let mut system = NumberSystem::default();
// We construct a runner, and tell which which states and actions it should process.
let mut runner = EventRunner::new()
.with_state::<A>()
.with_state::<B>()
.with_action::<Action>();
// run your system against the events produced from TLA+ tests.
let result = runtime.run_tla_events(tla_tests_file_path, tla_config_file_path, &mut system, &mut runner);
// At each step of a test, the state of your system is being checked
// against the state that the TLA+ model expects
assert!(result.is_ok());
// You can also check the final state of your system, if you want.
assert_eq!(system.a, 6);
assert_eq!(system.b, 6);
assert_eq!(system.sum, 12);
assert_eq!(system.prod, 36);
}
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for ModelatorRuntime
impl Send for ModelatorRuntime
impl Sync for ModelatorRuntime
impl Unpin for ModelatorRuntime
impl UnwindSafe for ModelatorRuntime
Blanket Implementations
Mutably borrows from an owned value. Read more
Instruments this type with the provided Span
, returning an
Instrumented
wrapper. 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