machine_check/
args.rs

1use clap::{ArgGroup, Args, Parser, ValueEnum};
2
3/// Arguments for executing machine-check.
4#[derive(Parser, Debug)]
5#[clap(group(ArgGroup::new("property-group")
6.required(true)
7.multiple(true)
8.args(&["property", "inherent","gui"]),
9))]
10#[clap(group(ArgGroup::new("verbosity-group")
11.required(false)
12.multiple(false)
13.args(&["silent", "verbose"]),
14))]
15pub struct ExecArgs {
16    /// Whether the execution should be completely silent.
17    ///
18    /// This will prevent standard logging to stderr and writing the result to stdout.
19    #[arg(long)]
20    pub silent: bool,
21    /// Adds debug and trace messages depending of the number of flags used.
22    #[arg(short, long, action = clap::ArgAction::Count)]
23    pub verbose: u8,
24
25    /// Outputs the result to stdout in a machine-readable format.
26    ///
27    /// The format is not stabilised yet.
28    #[arg(short, long)]
29    pub batch: bool,
30
31    /// Opens the Graphical User Interface.
32    ///
33    /// The `gui` feature of **machine-check** must be enabled for this to work.
34    #[arg(
35        short,
36        long,
37        conflicts_with("batch"),
38        conflicts_with("assume_inherent")
39    )]
40    pub gui: bool,
41
42    /// Verifies the inherent property.
43    #[arg(long)]
44    pub inherent: bool,
45    /// Assumes that the inherent property holds.
46    ///
47    /// The verification result will be meaningless if it does not.
48    #[arg(long, conflicts_with("inherent"))]
49    pub assume_inherent: bool,
50    /// Verifies a given property.
51    ///
52    /// It will be first verified that the inherent property holds unless `assume_inherent` is given.
53    #[arg(long, conflicts_with("inherent"))]
54    pub property: Option<String>,
55
56    /// The verification strategy.
57    #[arg(long, default_value("default"))]
58    pub strategy: ExecStrategy,
59}
60
61/// Verification strategy.
62///
63/// This can considerably alter how the verification proceeds,
64/// with potential drastic change in verification time and memory needed.
65#[derive(Debug, Clone, ValueEnum)]
66pub enum ExecStrategy {
67    /// The default verification strategy.
68    ///
69    /// Currently makes inputs imprecise at first, but keeps the states precise.
70    Default,
71    /// A naïve verification strategy, essentially brute-force model checking.
72    ///
73    /// Makes the inputs and states completely precise, with no advantage gained
74    /// by abstraction and no refinements necessary.
75    ///
76    /// This strategy is only reasonable for comparison, not for serious use.
77    Naive,
78    /// A verification strategy that additionally decays state precision.
79    ///
80    /// Both inputs and newly generated states will be imprecise before refinement.
81    /// This can make the verification faster or slower depending on the system.
82    Decay,
83}
84
85#[derive(Parser, Debug)]
86pub struct ProgramArgs<A: Args> {
87    #[clap(flatten)]
88    pub run_args: ExecArgs,
89    #[clap(flatten)]
90    pub system_args: A,
91}
machine_check/args.rs

machine_check/
args.rs
