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

use crate::value::{ValueDisplay, ValueOption};
use anyhow::{Result, bail};
use itf::value::{Record, Value};
use std::fmt;

/// Wraps nondeterministic choices made during trace generation.
#[doc(hidden)] // public for macro use
pub struct NondetPicks(Record);

impl From<Record> for NondetPicks {
    fn from(record: Record) -> Self {
        let mut nondets = Record::new();
        for (key, value) in record {
            if let Some(value) = value.into_option() {
                nondets.insert(key, value);
            }
        }
        Self(nondets)
    }
}

impl NondetPicks {
    pub(crate) fn new(value: Value) -> Result<Self> {
        let Value::Record(record) = value else {
            bail!("Expected nondet picks to be a `Value::Record`")
        };
        Ok(record.into())
    }

    pub(crate) fn empty() -> Self {
        Self(Record::new())
    }

    pub(crate) fn is_empty(&self) -> bool {
        self.0.is_empty()
    }

    #[doc(hidden)] // public for macro use
    pub fn get<'a>(&'a self, var: &str) -> Option<&'a Value> {
        self.0.get(var)
    }
}

impl fmt::Display for NondetPicks {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let mut iter = self.0.iter();
        if let Some((key, value)) = iter.next() {
            write!(f, "+ {}: {}", key, value.display())?;
            for (key, value) in iter {
                write!(f, "\n+ {}: {}", key, value.display())?;
            }
        }
        Ok(())
    }
}

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

    #[test]
    #[should_panic(expected = "Expected nondet picks to be a `Value::Record`")]
    fn test_fail_to_build_nondet_picks() {
        let value = Value::Number(42);
        NondetPicks::new(value).unwrap();
    }

    #[test]
    fn test_get_nondet_pick() {
        let mut option = Record::new();
        option.insert("tag".to_string(), Value::String("Some".to_string()));
        option.insert("value".to_string(), Value::Number(42));

        let mut record = Record::new();
        record.insert("foo".to_string(), Value::Record(option));

        let nondets = NondetPicks::new(Value::Record(record)).unwrap();
        let nondet = nondets.get("foo");

        assert!(nondet.is_some(), "failed to find nondet value")
    }
}