tla-checker 0.3.9

A TLA+ model checker written in Rust
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

use std::sync::Arc;

use indexmap::IndexSet;

use crate::ast::State;

#[derive(Debug, Clone)]
pub struct Edge {
    pub target: usize,
    pub action: Option<Arc<str>>,
}

pub struct StateGraph {
    pub states: IndexSet<State>,
    pub edges: Vec<Vec<Edge>>,
    pub parents: Vec<Option<usize>>,
}

impl StateGraph {
    pub fn new() -> Self {
        Self {
            states: IndexSet::new(),
            edges: Vec::new(),
            parents: Vec::new(),
        }
    }

    pub fn add_state(&mut self, state: State, parent: Option<usize>) -> (usize, bool) {
        let (idx, is_new) = self.states.insert_full(state);
        if is_new {
            self.parents.push(parent);
            self.edges.push(Vec::new());
        }
        (idx, is_new)
    }

    pub fn add_edge(&mut self, from: usize, to: usize, action: Option<Arc<str>>) {
        if from < self.edges.len() {
            self.edges[from].push(Edge { target: to, action });
        }
    }

    pub fn state_count(&self) -> usize {
        self.states.len()
    }

    pub fn edge_count(&self) -> usize {
        self.edges.iter().map(|e| e.len()).sum()
    }

    pub fn get_state(&self, idx: usize) -> Option<&State> {
        self.states.get_index(idx)
    }

    pub fn reconstruct_trace(&self, state_idx: usize) -> Vec<State> {
        let mut trace = Vec::new();
        let mut idx = Some(state_idx);
        while let Some(i) = idx {
            if let Some(state) = self.states.get_index(i) {
                trace.push(state.clone());
            }
            idx = self.parents.get(i).copied().flatten();
        }
        trace.reverse();
        trace
    }

    pub fn successors(&self, idx: usize) -> &[Edge] {
        self.edges.get(idx).map(|v| v.as_slice()).unwrap_or(&[])
    }

    pub fn outgoing_edges(&self, idx: usize) -> impl Iterator<Item = &Edge> {
        self.edges.get(idx).into_iter().flat_map(|v| v.iter())
    }

    pub fn has_edge_with_action(&self, idx: usize, action_name: &str) -> bool {
        self.outgoing_edges(idx)
            .any(|e| e.action.as_ref().is_some_and(|a| a.as_ref() == action_name))
    }
}

impl Default for StateGraph {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::ast::{State, Value};

    fn state_with_x(n: i64) -> State {
        State {
            values: vec![Value::Int(n)],
        }
    }

    #[test]
    fn graph_basic_operations() {
        let mut graph = StateGraph::new();

        let s0 = state_with_x(0);
        let (idx0, is_new0) = graph.add_state(s0, None);
        assert_eq!(idx0, 0);
        assert!(is_new0);

        let s1 = state_with_x(1);
        let (idx1, is_new1) = graph.add_state(s1, Some(0));
        assert_eq!(idx1, 1);
        assert!(is_new1);

        graph.add_edge(0, 1, Some("Inc".into()));

        assert_eq!(graph.state_count(), 2);
        assert_eq!(graph.edge_count(), 1);
        assert!(graph.has_edge_with_action(0, "Inc"));
        assert!(!graph.has_edge_with_action(0, "Dec"));
    }

    #[test]
    fn trace_reconstruction() {
        let mut graph = StateGraph::new();

        graph.add_state(state_with_x(0), None);
        graph.add_state(state_with_x(1), Some(0));
        graph.add_state(state_with_x(2), Some(1));

        let trace = graph.reconstruct_trace(2);
        assert_eq!(trace.len(), 3);
    }
}