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

use camino::Utf8PathBuf;
use clap::Args;
use log::info;
use machine_check_common::ExecResult;
use serde::{Deserialize, Serialize};

use crate::CheckError;

mod build;
mod execute;
mod translate;
mod work;

#[derive(Debug, Clone, Args)]
pub struct Cli {
    /// Computation Tree Logic property to verify. Defaults to specification within the system.
    #[arg(long)]
    pub property: Option<String>,

    /// Where the machine crate should be created. Defaults to temporary directory.
    #[arg(long)]
    pub machine_path: Option<Utf8PathBuf>,

    /// Location of preparation directory. Defaults to "machine-check-preparation" next to the executable.
    #[arg(long)]
    pub preparation_path: Option<Utf8PathBuf>,

    /// Location of the system to verify.
    pub system_path: Utf8PathBuf,

    /// Whether state decay should be used. This can speed up or slow down verification depending on the system.
    #[arg(long)]
    pub use_decay: bool,
}

#[derive(Debug, Serialize, Deserialize)]
pub struct VerifyResult {
    pub exec: Option<ExecResult>,
    pub stats: VerifyStats,
}

#[derive(Debug, Serialize, Deserialize)]
pub struct VerifyStats {
    pub transcription_time: Option<f64>,
    pub build_time: Option<f64>,
    pub execution_time: Option<f64>,
    pub prepared: Option<bool>,
}

pub(crate) fn run(args: super::Cli, verify_args: Cli) -> Result<(), CheckError> {
    let mut verify = Verify {
        args,
        verify_args,
        stats: VerifyStats {
            transcription_time: None,
            build_time: None,
            execution_time: None,
            prepared: None,
        },
    };

    let exec_result = verify.work();

    let exec = match &exec_result {
        Ok(ok) => Some(ok.clone()),
        Err(_) => None,
    };

    let verify_result = VerifyResult {
        exec,
        stats: verify.stats,
    };

    if verify.args.batch {
        // serialize the result
        serde_json::to_writer(std::io::stdout(), &verify_result)?;
    }
    // get the actual exec result
    let exec_result = match exec_result {
        Ok(ok) => ok,
        Err(err) => return Err(err),
    };

    // print interesting facts
    info!(
        "Used {} states and {} refinements.",
        exec_result.stats.num_states, exec_result.stats.num_refinements
    );
    // print conclusion or return exec error
    let conclusion = exec_result.result?;
    info!("Reached conclusion: {}", conclusion);
    Ok(())
}

struct Verify {
    args: super::Cli,
    verify_args: Cli,
    stats: VerifyStats,
}