quint-connect 0.1.0

A model-based testing framework that connects Quint specifications with Rust applications
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

mod seed;

pub use crate::trace::generator::{RunConfig, TestConfig};
pub use seed::gen_random_seed;

use crate::{
    Driver, State, Step,
    logger::*,
    trace::{
        generator::{Config as GenConfig, generate_traces},
        iter::Traces,
    },
    value::ValueDisplay,
};
use anyhow::{Result, bail, ensure};
use itf::Value;
use similar::TextDiff;

/// Configuration for running model-based tests, combining test metadata with
/// trace generation settings.
pub struct Config<C: GenConfig> {
    pub test_name: String,
    pub gen_config: C,
}

/// Run the test configuration using the given test driver.
pub fn run_test<C: GenConfig>(driver: impl Driver, config: Config<C>) -> Result<()> {
    title!("Running model based tests for {}", config.test_name);
    info!(
        "Generating {} traces using `{}` as random seed ...",
        config.gen_config.n_traces(),
        config.gen_config.seed()
    );

    let traces = generate_traces(&config.gen_config)?;
    let result = replay_traces(driver, traces);

    if result.is_ok() {
        success!("[OK] {}", config.test_name);
    } else {
        error!("[FAIL] {} ", config.test_name);
        error!(
            "Reproduce this error with `QUINT_SEED={}`\n",
            config.gen_config.seed()
        );
    }

    result
}

fn replay_traces<D: Driver>(mut driver: D, traces: Traces) -> Result<()> {
    info!("Replaying traces ...");

    let ann = D::config();
    let mut iter = traces.peekable();
    ensure!(
        iter.peek().is_some(),
        "Trace generation produced zero traces.\n\
         Please check your specification and/or your test configuration."
    );

    for (trace, t) in iter.zip(1usize..) {
        trace!(1, "[Trace {}]", t);

        for (s, state) in trace?.states.into_iter().enumerate() {
            trace!(2, "Deriving step from:\n{}\n", state.value.display());
            let Value::Record(state) = state.value else {
                bail!("Expected current state to be a Record")
            };

            let step = Step::new(state, &ann)?;
            trace!(1, "[Step {}]\n{}\n", s, step);
            ensure!(
                !step.action_taken.is_empty(),
                "An anonymous action was found!\n\
                 Please make sure all actions in the specification are properly named.\n\
                 Check the crate docs for tips and tricks on nondeterminism."
            );

            driver.step(&step)?;
            check_state(&driver, step)?;
        }
    }

    Ok(())
}

fn check_state<D: Driver>(driver: &D, step: Step) -> Result<()> {
    trace!(2, "Extracting state from:\n{}\n", step.state.display());
    let spec_state = D::State::from_spec(step.state)?;
    let driver_state = D::State::from_driver(driver)?;

    if spec_state != driver_state {
        let left = format!("{:#?}", spec_state);
        let right = format!("{:#?}", driver_state);
        let diff = TextDiff::from_lines(&left, &right);

        error!("Specification and implementation states diverge");
        trace!(
            1,
            "{}",
            diff.unified_diff()
                .context_radius(256) // XXX: large enough?
                .header("specification", "implementation")
                .missing_newline_hint(false)
        );

        bail!("State invariant failed")
    }

    Ok(())
}