Function modelator::run_tla_steps

pub fn run_tla_steps<P, System, Step>(
    tla_tests_file: P, 
    tla_config_file: P, 
    options: &Options, 
    system: &mut System
) -> Result<(), TestError> 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 crate::traces and execute them against the SUT that implements StepRunner.

For more information, please consult the documentation of traces and StepRunner.

Example

use modelator::{run_tla_steps, 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 = "tests/integration/tla/NumbersAMaxBMinTest.tla";
    let tla_config_file = "tests/integration/tla/Numbers.cfg";
    let options = modelator::Options::default();
    let mut system = NumberSystem::default();
    assert!(run_tla_steps(tla_tests_file, tla_config_file, &options, &mut system).is_ok());
}