traceforge 0.2.1

TraceForge is a model checker for concurrent and distributed programs 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

use traceforge::*;
use channel::{Builder, Channel};
use msg::Message;

fn unique_channel<T: Message + Clone + 'static>() -> Channel<T> {
    Builder::new().build()
}

#[test]
fn dropped() {
    let stats = traceforge::verify(
        Config::builder()
            .with_lossy(1)
            .with_cons_type(ConsType::FIFO)
            .build(),
        move || {
            let ch = unique_channel();
            ch.0.send_lossy_msg(1);
        },
    );
    assert_eq!(stats.execs, 2);
}

#[test]
fn lossy_channel() {
    let stats = traceforge::verify(
        Config::builder()
            .with_lossy(1)
            .with_cons_type(ConsType::FIFO)
            .build(),
        move || {
            let (sender, receiver) = unique_channel();
            sender.send_lossy_msg(1);
            sender.send_msg(2);
            let _ = thread::spawn(move || {
                assume!(receiver.recv_msg_block() == 2);
            });
        },
    );
    assert_eq!(stats.execs, 1);
}

#[test]
fn lossy_channel_rev_max() {
    for b in 1..3 {
        let stats = traceforge::verify(
            Config::builder()
                .with_lossy(b)
                .with_cons_type(ConsType::FIFO)
                .build(),
            move || {
                let (sender, receiver) = unique_channel();
                let _ = thread::spawn(move || {
                    let v = receiver.recv_msg();
                    assume!(v == Some(2));
                });
                let senderp = sender.clone();
                let _ = thread::spawn(move || {
                    sender.send_lossy_msg(1);
                });
                let _ = thread::spawn(move || {
                    senderp.send_msg(2);
                });
            },
        );
        assert_eq!(stats.execs, 2);
    }
}