machine_check_hw/
verify.rs

1use camino::{Utf8Path, Utf8PathBuf};
2use clap::{ArgGroup, Args};
3use log::{debug, info};
4use machine_check_common::ExecResult;
5use serde::{Deserialize, Serialize};
6
7use crate::CheckError;
8
9#[derive(Debug, Clone, Args)]
10#[clap(group(ArgGroup::new("property-group")
11.required(true)
12.multiple(true)
13.args(&["property", "inherent", "gui"]),
14))]
15pub struct Cli {
16    /// Whether to show the Graphical User Interface.
17    #[arg(short, long, conflicts_with("property"), conflicts_with("inherent"))]
18    pub gui: bool,
19
20    /// Computation Tree Logic property to verify.
21    #[arg(long)]
22    pub property: Option<String>,
23
24    /// Whether to verify the inherent property instead of a supplied one.
25    #[arg(long)]
26    pub inherent: bool,
27
28    /// Where the machine crate should be created. Defaults to temporary directory.
29    #[arg(long)]
30    pub machine_path: Option<Utf8PathBuf>,
31
32    /// Location of preparation directory. Defaults to "machine-check-preparation" next to the executable.
33    #[arg(long)]
34    pub preparation_path: Option<Utf8PathBuf>,
35
36    /// Location of the system to verify.
37    pub system_path: Utf8PathBuf,
38
39    /// Whether state decay should be used. This can speed up or slow down verification depending on the system.
40    #[arg(long)]
41    pub use_decay: bool,
42}
43
44#[derive(Debug, Serialize, Deserialize)]
45pub struct VerifyResult {
46    pub exec: Option<ExecResult>,
47    pub stats: VerifyStats,
48}
49
50#[derive(Debug, Serialize, Deserialize)]
51pub struct VerifyStats {
52    pub transcription_time: Option<f64>,
53    pub build_time: Option<f64>,
54    pub execution_time: Option<f64>,
55    pub prepared: Option<bool>,
56}
57
58pub(crate) fn run(args: super::Cli, verify_args: Cli) -> Result<(), CheckError> {
59    let abstract_machine = process_machine(&verify_args.system_path)?;
60
61    // if no property is supplied, we will verify the inherent one
62
63    let config = machine_check_compile::VerifyConfig {
64        abstract_machine,
65        machine_path: verify_args.machine_path,
66        preparation_path: verify_args.preparation_path,
67        batch: args.batch,
68        gui: verify_args.gui,
69        property: verify_args.property,
70        verbose: args.verbose,
71        use_decay: verify_args.use_decay,
72    };
73    let verify_result = machine_check_compile::verify(config);
74    if let Err(machine_check_compile::Error::Gui) = verify_result {
75        return Ok(());
76    }
77
78    let exec_result = verify_result?;
79
80    // print interesting facts
81    info!(
82        "Used {} states and {} refinements.",
83        exec_result.stats.num_final_states, exec_result.stats.num_refinements
84    );
85    // print conclusion or return exec error
86    let conclusion = exec_result.result.map_err(CheckError::ExecError)?;
87    info!("Reached conclusion: {}", conclusion);
88    Ok(())
89}
90
91fn process_machine(system_path: &Utf8Path) -> Result<syn::File, CheckError> {
92    debug!("Constructing machine from path {:?}.", &system_path);
93    let machine_file = super::translate::translate(system_path)?;
94    Ok(machine_file)
95}
machine_check_hw/verify.rs

machine_check_hw/
verify.rs
