taco_cli/
main.rs

1//! TACO Command Line Interface
2//!
3//! This crate contains the TACO CLI that can be used to verify, translate and
4//! visualize different flavors of threshold automata. Consult the TACO
5//! documentation for more information on how to use the tool, what
6//! specification formats are supported etc.
7
8use ::config::Config;
9
10use clap::Parser;
11use cli::get_bdd_manager_cfg;
12#[cfg(feature = "dot")]
13use cli::visualize_ta;
14use cli::{Cli, initialize_logger, parse_input_file};
15use human_panic::setup_panic;
16use log::{debug, info};
17use taco_model_checker::eltl::ELTLSpecificationBuilder;
18use taco_threshold_automaton::ThresholdAutomaton;
19
20use crate::cli::{
21    create_coverability_expression, create_reachability_expression, get_smt_solver,
22    parse_coverability, parse_reachability, translate_ta,
23};
24mod cli;
25mod taco_config;
26
27fn main() -> Result<(), Box<dyn std::error::Error>> {
28    setup_panic!();
29
30    // parse the cli arguments
31    let cli = Cli::parse();
32    initialize_logger(cli.log_config)?;
33    info!("Welcome to the TACO model checker!");
34    match cli.command {
35        cli::Commands::Check {
36            input,
37            config_file,
38            model_checker,
39            bdd,
40            smt_solver,
41            compact_out,
42            abort_on_violation,
43            mode,
44        } => {
45            let (mut ta, mut spec) = parse_input_file(input)?;
46
47            info!(
48                "Parsed threshold automaton with the name '{}' from the input file",
49                ta.name()
50            );
51            debug!("Parsed threshold automaton: {ta}");
52
53            let n_loc = ta.locations().count();
54            let n_rules = ta.rules().count();
55            info!("Threshold automaton has {n_loc} locations and {n_rules} rules");
56
57            // Check whether a configuration file was supplied
58            let mut settings = Config::builder();
59            if let Some(config_file) = config_file {
60                if !config_file.exists() {
61                    return Err(anyhow::anyhow!(
62                        "Specified configuration file '{}' does not exist.",
63                        config_file.display()
64                    )
65                    .into());
66                }
67
68                settings = settings.add_source(config::File::from(config_file));
69            }
70
71            // Parse configuration from environment variables
72            settings = settings.add_source(config::Environment::with_prefix("TACO"));
73            let mut config = settings
74                .build()?
75                .try_deserialize::<taco_config::TACOConfig>()?;
76
77            // Check whether the smt solver was overridden via CLI
78            if let Some(solver) = smt_solver {
79                let solver_cfg = get_smt_solver(solver);
80                config.set_smt_solver_builder_cfg(solver_cfg);
81            }
82
83            // Check whether the bdd manager was overridden via CLI
84            if let Some(bdd) = bdd {
85                let bdd_cfg = get_bdd_manager_cfg(bdd);
86                config.set_bdd_config(bdd_cfg);
87            }
88
89            // Check whether we want a check based on the input file or a quick
90            // coverability or reachability check through the CLI
91            match mode {
92                cli::CheckMode::Coverability => {
93                    // Parse coverability
94                    let loc_to_be_covered = parse_coverability(&mut ta);
95                    // Build expression for specification and add it to the TA
96                    let expression = create_coverability_expression(loc_to_be_covered);
97
98                    let mut builder = ELTLSpecificationBuilder::new(&ta);
99                    builder
100                        .add_expression(String::from("coverability"), expression)
101                        .unwrap();
102                    spec = builder.build();
103                }
104                cli::CheckMode::Reachability => {
105                    // Parse reachability
106                    let (populated_locs, unpopulated_locs) = parse_reachability(&mut ta);
107                    // Build expression for specification and add it to the TA
108                    let expression =
109                        create_reachability_expression(populated_locs, unpopulated_locs);
110                    let mut builder = ELTLSpecificationBuilder::new(&ta);
111                    builder
112                        .add_expression(String::from("reachability"), expression)
113                        .unwrap();
114                    spec = builder.build();
115                }
116                _ => (),
117            }
118
119            cli::display_result(
120                ta,
121                spec,
122                model_checker,
123                config,
124                abort_on_violation,
125                mode,
126                compact_out,
127            );
128
129            info!("Finished model checking. Goodbye!");
130            Ok(())
131        }
132
133        #[cfg(feature = "dot")]
134        cli::Commands::Visualize { input, output } => {
135            let (ta, _) = parse_input_file(input)?;
136            visualize_ta(&ta, output)?;
137            Ok(())
138        }
139        cli::Commands::Translate { input, output } => {
140            let (ta, spec) = parse_input_file(input)?;
141            translate_ta(&ta, &spec, output)?;
142            Ok(())
143        }
144    }
145}
taco_cli/main.rs

taco_cli/
main.rs
