smc_scan_core 0.2.0

Core module for the Scan model checker.
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

use bumpalo::Bump;

use crate::program_graph::{Action, Transition};

pub(super) struct TransitionsIterator<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> {
    iters: &'a mut [I],
    bump: &'a Bump,
    action: Action,
}

impl<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> TransitionsIterator<'a, I> {
    pub(super) fn new(iters: &'a mut [I], bump: &'a Bump) -> Self {
        Self {
            iters,
            bump,
            action: Action(0),
        }
    }
}

impl<'a, I: Iterator<Item = &'a (Action, Vec<Transition>)>> Iterator
    for TransitionsIterator<'a, I>
{
    type Item = (Action, &'a [&'a [Transition]]);

    fn next(&mut self) -> Option<Self::Item> {
        let len = self.iters.len();
        let mut total = 0;
        let mut i = 0;
        let mut vals = bumpalo::vec![in self.bump; [].as_slice(); len];
        while total < len {
            let &(next_a, ref next_t) = self.iters[i].find(|&&(a, _)| a.0 >= self.action.0)?;
            vals[i] = next_t.as_slice();
            i = (i + 1) % len;
            total = total * (next_a.0 == self.action.0) as usize + 1;
            self.action = next_a;
        }
        Some((self.action, vals.into_bump_slice()))
    }
}