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
69
70
71
72
73
74
75
76
77
78

//extern crate traceforge;

use traceforge::thread;

#[derive(Clone, Debug, PartialEq)]
enum Msg {
    Work,
    Terminate,
}

fn example() {
    let t1 = thread::spawn_daemon(move || {
        let mut i = 0;
        loop {
            let m = traceforge::recv_msg_block();
            match m {
                Msg::Work => i = i + 1, 
                Msg::Terminate => assert!(i < 10), 
            }
        }
    });
    let t1_id = t1.thread().id();

    let t2 = thread::spawn(move || {
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
        traceforge::send_msg(t1_id, Msg::Work);
    });
    traceforge::send_msg(t1_id.clone(), Msg::Terminate);

    let _ = t1.join();
    let _ = t2.join();
}

fn random() {
    let ntests = 10;
    println!("Running the example in random mode {ntests} times");
    let _ = traceforge::test(
        traceforge::Config::builder().build(),
        example,
        ntests
    );
}

fn forge() {
    println!("Running the example in systematic mode");
    let stats = traceforge::verify(
        traceforge::Config::builder().build(),
        example,
    );
    println!("Stats = {}, {}", stats.execs, stats.block);

}

fn main() {
    // Get command line arguments
    let args: Vec<String> = std::env::args().collect();

    // Check if any argument was provided
    if args.len() < 2 {
        println!("Usage: {} --random|--forge", args[0]);
        return;
    }

    // Match the first argument
    match args[1].as_str() {
        "--random" => random(),
        "--forge" => forge(),
        _ => println!("Invalid argument. Use --random or --forge"),
    }
}