Struct ModelatorRuntime

pub struct ModelatorRuntime {
    pub model_checker_runtime: ModelCheckerRuntime,
    pub dir: PathBuf,
}

Set of options to configure modelator runtime.

Fields

model_checker_runtime: ModelCheckerRuntime

Model checker runtime.

dir: PathBuf

Modelator directory.

Implementations

impl ModelatorRuntime

pub fn model_checker_runtime( self, model_checker_runtime: ModelCheckerRuntime, ) -> Self

Set TLC runtime.

pub fn dir(self, dir: impl AsRef<Path>) -> Self

Set modelator directory.

pub fn traces<P: AsRef<Path>>( &self, tla_tests_file_path: P, tla_config_file_path: P, ) -> Result<BTreeMap<String, Result<Vec<JsonTrace>, Error>>, Error>

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/resource/NumbersAMaxBMinTest.tla";
let tla_config_file_path = "tests/integration/resource/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,

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;
        self.recalculate();
        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/resource/NumbersAMaxBMinTest.tla";
    let tla_config_file_path = "tests/integration/resource/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,

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/resource/NumbersAMaxBMaxTest.tla";
    let tla_config_file_path = "tests/integration/resource/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

impl Clone for ModelatorRuntime

fn clone(&self) -> ModelatorRuntime

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ModelatorRuntime

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ModelatorRuntime

fn default() -> Self

Returns the “default value” for a type.