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

use crate::trace::generator::{Config, DEFAULT_TRACES, utils::opt_arg};
use std::{path::Path, process::Command};

/// Configuration for generating traces using `quint test`.
pub struct TestConfig {
    pub spec: String,
    pub main: Option<String>,
    pub test: String,
    pub max_samples: Option<usize>,
    pub seed: String,
}

impl Config for TestConfig {
    fn seed(&self) -> &str {
        self.seed.as_str()
    }

    fn n_traces(&self) -> usize {
        self.max_samples.unwrap_or(DEFAULT_TRACES)
    }

    fn to_command(&self, tmpdir: &Path) -> Command {
        let n_traces = self.n_traces().to_string();
        let mut cmd = Command::new("quint");
        cmd.arg("test")
            .arg(Path::new(&self.spec))
            .arg("--seed")
            .arg(&self.seed)
            .arg("--match")
            .arg(format!("^{}$", self.test))
            .arg("--max-samples")
            .arg(n_traces)
            .arg("--out-itf")
            .arg(tmpdir.join("test_{seq}.itf.json"))
            .arg("--verbosity")
            .arg("0");

        opt_arg(&mut cmd, "--main", self.main.as_ref());
        cmd
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    fn basic_config() -> TestConfig {
        TestConfig {
            spec: "foo.qnt".to_string(),
            test: "happyTest".to_string(),
            seed: "42".to_string(),
            main: None,
            max_samples: None,
        }
    }

    #[test]
    fn test_basic_config() {
        let config = basic_config();

        assert_eq!(
            to_string(config),
            "quint test foo.qnt \
             --seed 42 \
             --match ^happyTest$ \
             --max-samples 100 \
             --out-itf tmpdir/test_{seq}.itf.json \
             --verbosity 0"
        );
    }

    #[test]
    fn test_main_module() {
        let mut config = basic_config();
        config.main = Some("tests".to_string());

        assert_eq!(
            to_string(config),
            "quint test foo.qnt \
             --seed 42 \
             --match ^happyTest$ \
             --max-samples 100 \
             --out-itf tmpdir/test_{seq}.itf.json \
             --verbosity 0 \
             --main tests"
        );
    }

    #[test]
    fn test_max_samples() {
        let mut config = basic_config();
        config.max_samples = Some(42);

        assert_eq!(
            to_string(config),
            "quint test foo.qnt \
             --seed 42 \
             --match ^happyTest$ \
             --max-samples 42 \
             --out-itf tmpdir/test_{seq}.itf.json \
             --verbosity 0"
        );
    }

    fn to_string(config: TestConfig) -> String {
        let dir = Path::new("tmpdir");
        let cmd = config.to_command(dir);
        format!("{:?}", cmd).replace("\"", "")
    }
}