scan/lib.rs
1//! # SCAN (StatistiCal ANalyzer)
2//!
3//! SCAN is a statistical model checker
4//! designed to verify large concurrent systems
5//! for which standard verification techniques do not scale.
6//!
7//! SCAN uses Channel Systems (CS) as models,[^1]
8//! and Metric Temporal Logic (MTL) as property specification language.
9//!
10//! SCAN is being developed to accept models specified in multiple, rich modeling languages.
11//! At the moment the following languages are planned or implemented:
12//!
13//! - [x] [State Chart XML (SCXML)](https://www.w3.org/TR/scxml/).
14//! - [x] [Promela](https://spinroot.com/spin/Man/Manual.html)
15//! - [x] [JANI](https://jani-spec.org/)
16//!
17//! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.
18
19mod progress;
20mod report;
21mod trace;
22mod verify;
23
24use std::{path::PathBuf, sync::Arc};
25
26use anyhow::{anyhow, bail};
27use clap::{Parser, Subcommand, ValueEnum};
28use progress::Bar;
29use report::Report;
30use scan_core::{CsModel, MtlOracle, Oracle, PgModel, PmtlOracle, Scan, TransitionSystemGenerator};
31use trace::TraceArgs;
32use verify::VerifyArgs;
33
34/// Supported model specification formats.
35///
36/// SCAN supports different model specification formats.
37///
38/// WARNING: formats can have varying levels of supports
39/// and may not be interpreted as expected.
40#[deny(missing_docs)]
41#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum)]
42enum Format {
43 /// SCXML format, passed as either the path to the main file,
44 /// if present, or the path of the directory sub-tree containing the model's files.
45 ///
46 /// SCXML models are composed by separate .scxml files for SCXML automaton,
47 /// an .xml file for pMTL properties and,
48 /// optionally, an .xml main file describing the model.
49 ///
50 /// The model can be passed to SCAN as either the path to the main file,
51 /// if present, or the path of a directory.
52 /// In the latter case, SCAN will attempt to process appropriately
53 /// all files in the given directory and its sub-directories.
54 Scxml,
55 /// JANI format, passed as the path to the .jani file.
56 ///
57 /// JANI models are composed by a single .jani file.
58 ///
59 /// The model has to be passed to SCAN as the path to the .jani file.
60 ///
61 /// WARNING: JANI support is still experimental.
62 Jani,
63 /// Promela format, passed as the path to the .pml or .prm file.
64 ///
65 /// Promela models are composed by a single .pml or .prm file.
66 ///
67 /// The model has to be passed to SCAN as the path to the .pml or .prm file.
68 ///
69 /// WARNING: Promela support is still experimental.
70 Promela,
71}
72
73/// SCAN's available commands.
74#[deny(missing_docs)]
75#[derive(Subcommand)]
76enum Commands {
77 /// Validate the syntactical and semantical correctness of the model, without running it.
78 ///
79 /// Examples:
80 /// 'scan PATH/TO/MODEL validate' validates the model.
81 Validate,
82 /// Verify properties of the given model.
83 ///
84 /// At least one property has to be verified.
85 ///
86 /// Examples:
87 /// 'scan PATH/TO/MODEL verify PROPERTY' verifies the property PROPERTY over the model.
88 /// 'scan PATH/TO/MODEL verify PROPERTY_1 PROPERTY_2' verifies the properties PROPERTY_1 and PROPERTY_2 together over the model.
89 /// 'scan PATH/TO/MODEL verify --all' verifies all specified properties together over the model.
90 #[clap(verbatim_doc_comment)]
91 Verify {
92 /// Args for model verification.
93 #[clap(flatten)]
94 args: VerifyArgs,
95 /// Print progress bars during verification.
96 ///
97 /// By default, when it starts the verification process, SCAN only prints a terse message.
98 /// For longer jobs, it is useful to have real-time feedback on how the verification is proceeding.
99 /// This flag has SCAN print progress bars and current statistics on the verification process,
100 /// and make a best-effort attempt in estimating how long it will take to completion.
101 #[arg(long, value_enum)]
102 progress: Option<Bar>,
103 /// Print JSON-serialized final verification report.
104 ///
105 /// By default, SCAN prints a user-friendly report at the end of verification.
106 /// This flag has the report printed in JSON format instead.
107 #[arg(long)]
108 json: bool,
109 },
110 /// Produce execution traces and save them to file in csv format..
111 ///
112 /// Executions are always run to completion, regardless of verification outcome.
113 /// Executions that verify the given properties are separated from those that do not.
114 /// It is possible to verify no property at all, in which case all executions are successful but still executed to completion.
115 ///
116 /// Examples:
117 /// 'scan PATH/TO/MODEL trace' executes the model once and writes the trace to disk, without verifying any property.
118 /// 'scan PATH/TO/MODEL verify PROPERTY_1 PROPERTY_2' executes the model once and writes the trace to disk, classifying it according to verification outcome of the properties PROPERTY_1 and PROPERTY_2 together over the model.
119 /// 'scan PATH/TO/MODEL verify --all' executes the model once and writes the trace to disk, and classifying it according to verification outcome of all specified properties together over the model.
120 #[clap(verbatim_doc_comment)]
121 Trace(TraceArgs),
122}
123
124const LONG_ABOUT: &str = "SCAN (StatistiCal ANalyzer) is a statistical model checker \
125designed to verify large concurrent systems \
126for which standard verification techniques do not scale.";
127
128/// SCAN (StatistiCal ANalyzer) is a statistical model checker
129/// designed to verify large concurrent systems
130/// for which standard verification techniques do not scale.
131#[derive(Parser)]
132#[deny(missing_docs)]
133#[command(version, about, long_about=LONG_ABOUT)]
134pub struct Cli {
135 /// Path of model's file or folder,
136 /// depending on the used specification format.
137 #[arg(value_hint = clap::ValueHint::AnyPath)]
138 model: PathBuf,
139 /// Format used to specify the model.
140 ///
141 /// SCAN supports different model specification formats,
142 /// and, by default, it attempts to autodetect the correct one,
143 /// but this can be specified to resolve ambiguity.
144 ///
145 /// WARNING: formats can have varying levels of supports
146 /// and may not be interpreted as expected.
147 #[arg(short, long, value_enum)]
148 format: Option<Format>,
149 /// Verbose output.
150 ///
151 /// Verbosity level corresponds to the log level that gets printed.
152 /// Logging mostly concerns parsing and building of the model,
153 /// so it is particularly useful when validating a model
154 /// to check for errors.
155 ///
156 /// Verbosity levels: ERROR, WARNING, INFO, DEBUG, TRACE
157 ///
158 /// Examples:
159 /// 'scan PATH/TO/MODEL validate -vvv' validates the model and prints ERROR, WARNING and INFO log entries.
160 #[command(flatten)]
161 pub verbosity: clap_verbosity_flag::Verbosity,
162 /// Actions to execute on the model.
163 #[command(subcommand)]
164 command: Commands,
165}
166
167impl Cli {
168 pub fn run(self) -> anyhow::Result<()> {
169 let model = std::path::absolute(&self.model)?
170 .file_name()
171 .and_then(std::ffi::OsStr::to_str)
172 .unwrap_or("model")
173 .to_owned();
174
175 if let Some(format) = self.format {
176 match format {
177 Format::Scxml => self.run_scxml(&model),
178 Format::Promela => self.run_promela(&model),
179 Format::Jani => self.run_jani(&model),
180 }
181 } else if self.model.is_dir() {
182 self.run_scxml(&model)
183 } else {
184 let ext = self
185 .model
186 .extension()
187 .ok_or(anyhow!("file extension unknown"))?;
188 match ext
189 .to_str()
190 .ok_or(anyhow!("file extension not recognized"))?
191 {
192 "xml" => self.run_scxml(&model),
193 "jani" => self.run_jani(&model),
194 "pml" | "prm" => self.run_promela(&model),
195 _ => bail!("unsupported file format"),
196 }
197 }
198 }
199
200 fn run_scxml(self, model: &str) -> anyhow::Result<()> {
201 use scan_scxml::*;
202
203 match self.command {
204 Commands::Verify {
205 mut args,
206 progress,
207 json,
208 } => {
209 args.validate()?;
210 let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
211 validate_properties(&args.properties, &scxml_model.guarantees)?;
212 // Reorder properties as they appear in the model
213 args.properties = scxml_model.guarantees.clone();
214 run_verification::<CsModel, PmtlOracle>(model, &args, progress, json, &scan_def)
215 .print(json);
216 }
217 Commands::Validate => {
218 let (_scan, _scxml_model) = load(&self.model, &[], true)?;
219 // At this point the model has been validated
220 println!("model '{model}' successfully validated");
221 }
222 Commands::Trace(mut args) => {
223 let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
224 validate_properties(&args.properties, &scxml_model.guarantees)?;
225 // Reorder properties as they appear in the model
226 args.properties = scxml_model.guarantees.clone();
227 let scxml_model = Arc::new(scxml_model);
228 let tracer = TracePrinter::new(&scxml_model);
229 args.trace::<CsModel, PmtlOracle, _>(&scan_def, tracer);
230 println!("trace computation for model '{model}' completed");
231 }
232 }
233 Ok(())
234 }
235
236 fn run_jani(self, model: &str) -> anyhow::Result<()> {
237 use scan_jani::*;
238
239 match self.command {
240 Commands::Verify {
241 mut args,
242 progress,
243 json,
244 } => {
245 args.validate()?;
246 let properties = args.properties.clone();
247 let (scan, jani_model) = load(&self.model, &properties)?;
248 validate_properties(&args.properties, &jani_model.guarantees)?;
249 // Reorder properties as they appear in the model
250 args.properties = jani_model.guarantees.clone();
251 run_verification::<PgModel, MtlOracle>(model, &args, progress, json, &scan)
252 .print(json);
253 }
254 Commands::Validate => {
255 let (_scan, _jani_model) = load(&self.model, &[])?;
256 println!("model '{model}' successfully validated");
257 }
258 Commands::Trace(args) => {
259 args.validate()?;
260 let (scan, jani_model) = load(&self.model, &[])?;
261 let jani_model = Arc::new(jani_model);
262 let tracer = TracePrinter::new(jani_model);
263 args.trace::<PgModel, MtlOracle, _>(&scan, tracer);
264 println!("trace computation for model '{model}' completed");
265 }
266 }
267 Ok(())
268 }
269
270 fn run_promela(self, model: &str) -> anyhow::Result<()> {
271 use scan_promela::*;
272
273 match self.command {
274 Commands::Verify {
275 args,
276 progress,
277 json,
278 } => {
279 args.validate()?;
280 let properties = args.properties.clone();
281 let (scan, _promela_model) = load(&self.model, &properties, args.all)?;
282 run_verification::<CsModel, PmtlOracle>(model, &args, progress, json, &scan)
283 .print(json);
284 }
285 Commands::Validate => {
286 let (_scan, _jani_model) = load(&self.model, &[], true)?;
287 println!("model '{model}' successfully validated");
288 }
289 Commands::Trace(args) => {
290 args.validate()?;
291 let (_scan, _promela_model) = load(&self.model, &[], args.all)?;
292 println!("processing model '{model}' completed");
293 }
294 }
295 Ok(())
296 }
297}
298
299fn validate_properties(props: &[String], all_props: &[String]) -> anyhow::Result<()> {
300 if let Some(prop) = props.iter().find(|prop| !all_props.contains(prop)) {
301 Err(anyhow!(
302 "no property named '{prop}' found in model.\n\nHint: maybe it is misspelled?"
303 ))
304 } else {
305 Ok(())
306 }
307}
308
309fn run_verification<'a, Ts, O>(
310 model: &str,
311 args: &VerifyArgs,
312 progress: Option<Bar>,
313 json: bool,
314 scan: &'a Scan<Ts, O>,
315) -> Report
316where
317 Ts: 'a + TransitionSystemGenerator + Sync,
318 O: 'a + Oracle + Clone + Sync,
319 Ts::Ts<'a>: Clone + Sync,
320{
321 if !json {
322 println!(
323 "Verifying {model} (-p {} -c {} -d {}) {:?}",
324 args.precision, args.confidence, args.duration, args.properties
325 );
326 }
327 if let Some(bar) = progress {
328 std::thread::scope(|s| {
329 s.spawn(|| {
330 bar.print_progress_bar::<Ts, O>(
331 args.confidence,
332 args.precision,
333 &args.properties,
334 scan,
335 );
336 });
337 args.verify::<Ts, O>(model.to_owned(), scan)
338 })
339 } else {
340 args.verify::<Ts, O>(model.to_owned(), scan)
341 }
342}
343
344// From Clap tutorial <https://docs.rs/clap/latest/clap/_derive/_tutorial/index.html#testing>
345#[test]
346fn verify_cli() {
347 use clap::CommandFactory;
348 Cli::command().debug_assert();
349}