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

#![doc = include_str!("../README.md")]

mod model_check;
mod precision;
mod proposition;
mod refinery;
mod space;

use log::{error, info, log_enabled, trace};
use machine_check_common::{ExecError, ExecResult};
use mck::refin::{Input, Machine, State};

use clap::Parser;
use proposition::{Literal, PropTemp, PropU, PropUni, Proposition};
use refinery::Refinery;

#[derive(Parser, Debug)]
struct Args {
    #[arg(short, long)]
    batch: bool,

    #[arg(short, long, action = clap::ArgAction::Count)]
    verbose: u8,

    #[arg(long)]
    property: Option<String>,

    #[arg(long)]
    use_decay: bool,
}

pub fn run<I: Input, S: State, M: Machine<I, S>>() {
    if let Err(err) = run_inner::<I, S, M>() {
        // log root error
        error!("{:#?}", err);
        // terminate with non-success code
        std::process::exit(-1);
    }
    // terminate successfully, the information is in stdout
}

fn run_inner<I: Input, S: State, M: Machine<I, S>>() -> Result<ExecResult, anyhow::Error> {
    let args = Args::parse();
    // logging to stderr, stdout will contain the result in batch mode
    let filter_level = match args.verbose {
        0 => log::LevelFilter::Info,
        1 => log::LevelFilter::Debug,
        _ => log::LevelFilter::Trace,
    };
    env_logger::builder().filter_level(filter_level).init();

    info!("Starting verification.");

    let verification_result = verify::<I, S, M>(args.property.as_ref(), args.use_decay);

    if log_enabled!(log::Level::Trace) {
        trace!("Verification result: {:?}", verification_result);
    }

    if log_enabled!(log::Level::Info) {
        // the result will be propagated, just inform that we ended somehow
        match verification_result.result {
            Ok(_) => info!("Verification ended."),
            Err(_) => error!("Verification failed."),
        }
    }

    // serialize the verification result to stdout
    serde_json::to_writer(std::io::stdout(), &verification_result)?;
    Ok(verification_result)
}

fn verify<I: Input, S: State, M: Machine<I, S>>(
    property: Option<&String>,
    use_decay: bool,
) -> ExecResult {
    let mut refinery = Refinery::<I, S, M>::new(use_decay);
    let proposition = select_proposition(property);
    let result = match proposition {
        Ok(proposition) => refinery.verify(&proposition),
        Err(err) => Err(err),
    };

    ExecResult {
        result,
        stats: refinery.info(),
    }
}

fn select_proposition(property: Option<&String>) -> Result<Proposition, ExecError> {
    if let Some(property_str) = property {
        Proposition::parse(property_str)
    } else {
        // check AG[safe]
        Ok(Proposition::Negation(PropUni::new(Proposition::E(
            PropTemp::U(PropU {
                hold: Box::new(Proposition::Const(true)),
                until: Box::new(Proposition::Negation(PropUni::new(Proposition::Literal(
                    Literal::new(String::from("safe")),
                )))),
            }),
        ))))
    }
}