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 Validate,
79 /// Verify properties of the given model.
80 /// At least one property has to be verified.
81 ///
82 /// Examples:
83 /// 'scan PATH/TO/MODEL verify PROPERTY' verifies the property PROPERTY over the model.
84 /// 'scan PATH/TO/MODEL verify PROPERTY_1 PROPERTY_2' verifies the properties PROPERTY_1 and PROPERTY_2 together over the model.
85 /// 'scan PATH/TO/MODEL verify --all' verifies all specified properties together over the model.
86 #[clap(verbatim_doc_comment)]
87 Verify {
88 /// Args for model verification.
89 #[clap(flatten)]
90 args: VerifyArgs,
91 /// Print progress bars during verification.
92 ///
93 /// By default, when it starts the verification process, SCAN only prints a terse message.
94 /// For longer computations, it might be nice to see in real-time how the verification is proceeding.
95 /// This flag has SCAN print progress bars and current statistics on the verification process,
96 /// and make a best-effort attempt to estimate how long it will take to completion.
97 #[arg(long, value_enum)]
98 progress: Option<Bar>,
99 /// Print JSON-serialized final verification report.
100 ///
101 /// By default, SCAN prints a user-friendly report at the end of verification.
102 /// This flag has the report printed in JSON format instead.
103 #[arg(long)]
104 json: bool,
105 },
106 /// Produce execution traces and save them to file in csv format, separating executions that verify the given properties from those that do not.
107 /// Executions are always run to completion, regardless of verification outcome.
108 /// It is possible to verify no property at all, in which case all executions are successful but still executed to completion.
109 ///
110 /// Examples:
111 /// 'scan PATH/TO/MODEL trace' executes the model once and writes the trace to disk, without verifying any property.
112 /// '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.
113 /// '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.
114 #[clap(verbatim_doc_comment)]
115 Trace(TraceArgs),
116}
117
118const LONG_ABOUT: &str = "SCAN (StatistiCal ANalyzer) is a statistical model checker \
119designed to verify large concurrent systems \
120for which standard verification techniques do not scale.";
121
122/// SCAN (StatistiCal ANalyzer) is a statistical model checker
123/// designed to verify large concurrent systems
124/// for which standard verification techniques do not scale.
125#[derive(Parser)]
126#[deny(missing_docs)]
127#[command(version, about, long_about=LONG_ABOUT)]
128pub struct Cli {
129 /// Path of model's file or folder,
130 /// depending on the used specification format.
131 #[arg(value_hint = clap::ValueHint::AnyPath)]
132 model: PathBuf,
133 /// Format used to specify the model.
134 ///
135 /// SCAN supports different model specification formats,
136 /// and, by default, it attempts to autodetect the correct one,
137 /// but this can be specified to resolve ambiguity.
138 ///
139 /// WARNING: formats can have varying levels of supports
140 /// and may not be interpreted as expected.
141 #[arg(short, long, value_enum)]
142 format: Option<Format>,
143 /// Verbose output
144 #[command(flatten)]
145 pub verbosity: clap_verbosity_flag::Verbosity,
146 /// Actions to execute on the model.
147 #[command(subcommand)]
148 command: Commands,
149}
150
151impl Cli {
152 pub fn run(self) -> anyhow::Result<()> {
153 let model = std::path::absolute(&self.model)?
154 .file_name()
155 .and_then(std::ffi::OsStr::to_str)
156 .unwrap_or("model")
157 .to_owned();
158
159 if let Some(format) = self.format {
160 match format {
161 Format::Scxml => self.run_scxml(&model),
162 Format::Promela => self.run_promela(&model),
163 Format::Jani => self.run_jani(&model),
164 }
165 } else if self.model.is_dir() {
166 self.run_scxml(&model)
167 } else {
168 let ext = self
169 .model
170 .extension()
171 .ok_or(anyhow!("file extension unknown"))?;
172 match ext
173 .to_str()
174 .ok_or(anyhow!("file extension not recognized"))?
175 {
176 "xml" => self.run_scxml(&model),
177 "jani" => self.run_jani(&model),
178 "pml" | "prm" => self.run_promela(&model),
179 _ => bail!("unsupported file format"),
180 }
181 }
182 }
183
184 fn run_scxml(self, model: &str) -> anyhow::Result<()> {
185 use scan_scxml::*;
186
187 match self.command {
188 Commands::Verify {
189 mut args,
190 progress,
191 json,
192 } => {
193 args.validate()?;
194 println!("processing model '{model}' started");
195 let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
196 println!("processing model '{model}' completed successfully");
197 validate_properties(&args.properties, &scxml_model.guarantees)?;
198 // Reorder properties as they appear in the model
199 args.properties = scxml_model.guarantees.clone();
200 run_verification::<CsModel, PmtlOracle>(model, &args, progress, &scan_def)
201 .print(json);
202 }
203 Commands::Validate => {
204 println!("processing model '{model}' started");
205 let (_scan, _scxml_model) = load(&self.model, &[], true)?;
206 // At this point the model has been validated
207 println!("model '{model}' successfully validated");
208 }
209 Commands::Trace(mut args) => {
210 println!("processing model '{model}' started");
211 let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
212 println!("processing model '{model}' completed");
213 validate_properties(&args.properties, &scxml_model.guarantees)?;
214 // Reorder properties as they appear in the model
215 args.properties = scxml_model.guarantees.clone();
216 let scxml_model = Arc::new(scxml_model);
217 let tracer = TracePrinter::new(&scxml_model);
218 println!("trace computation started");
219 args.trace::<CsModel, PmtlOracle, _>(&scan_def, tracer);
220 println!("trace computation completed");
221 }
222 }
223 Ok(())
224 }
225
226 fn run_jani(self, model: &str) -> anyhow::Result<()> {
227 use scan_jani::*;
228
229 match self.command {
230 Commands::Verify {
231 mut args,
232 progress,
233 json,
234 } => {
235 args.validate()?;
236 println!("processing model '{model}' started");
237 let properties = args.properties.clone();
238 let (scan, jani_model) = load(&self.model, &properties)?;
239 println!("processing model '{model}' completed successfully");
240 validate_properties(&args.properties, &jani_model.guarantees)?;
241 // Reorder properties as they appear in the model
242 args.properties = jani_model.guarantees.clone();
243 run_verification::<PgModel, MtlOracle>(model, &args, progress, &scan).print(json);
244 }
245 Commands::Validate => {
246 println!("processing model '{model}' started");
247 let (_scan, _jani_model) = load(&self.model, &[])?;
248 println!("model '{model}' successfully validated");
249 }
250 Commands::Trace(args) => {
251 args.validate()?;
252 println!("processing model '{model}' started");
253 let (scan, jani_model) = load(&self.model, &[])?;
254 println!("processing model '{model}' completed successfully");
255 let jani_model = Arc::new(jani_model);
256 let tracer = TracePrinter::new(jani_model);
257 println!("trace computation started");
258 args.trace::<PgModel, MtlOracle, _>(&scan, tracer);
259 println!("trace computation completed");
260 }
261 }
262 Ok(())
263 }
264
265 fn run_promela(self, model: &str) -> anyhow::Result<()> {
266 use scan_promela::*;
267
268 match self.command {
269 Commands::Verify {
270 args,
271 progress,
272 json,
273 } => {
274 args.validate()?;
275 println!("processing model '{model}' started");
276 let properties = args.properties.clone();
277 let (scan, _promela_model) = load(&self.model, &properties, args.all)?;
278 println!("processing model '{model}' completed");
279 run_verification::<CsModel, PmtlOracle>(model, &args, progress, &scan).print(json);
280 }
281 Commands::Validate => {
282 println!("processing model '{model}' started");
283 let (_scan, _jani_model) = load(&self.model, &[], true)?;
284 println!("model '{model}' successfully validated");
285 }
286 Commands::Trace(args) => {
287 args.validate()?;
288 println!("processing model '{model}' started");
289 let (_scan, _promela_model) = load(&self.model, &[], args.all)?;
290 println!("processing model '{model}' completed");
291 }
292 }
293 Ok(())
294 }
295}
296
297fn validate_properties(props: &[String], all_props: &[String]) -> anyhow::Result<()> {
298 if let Some(prop) = props.iter().find(|prop| !all_props.contains(prop)) {
299 Err(anyhow!(
300 "no property named '{prop}' found in model.\n\nHint: maybe it is misspelled?"
301 ))
302 } else {
303 Ok(())
304 }
305}
306
307fn run_verification<'a, Ts, O>(
308 model: &str,
309 args: &VerifyArgs,
310 progress: Option<Bar>,
311 scan: &'a Scan<Ts, O>,
312) -> Report
313where
314 Ts: 'a + TransitionSystemGenerator + Sync,
315 O: 'a + Oracle + Clone + Sync,
316 Ts::Ts<'a>: Clone + Sync,
317{
318 println!(
319 "Verifying {model} (-p {} -c {} -d {}) {:?}",
320 args.precision, args.confidence, args.duration, args.properties
321 );
322 if let Some(bar) = progress {
323 std::thread::scope(|s| {
324 s.spawn(|| {
325 bar.print_progress_bar::<Ts, O>(
326 args.confidence,
327 args.precision,
328 &args.properties,
329 scan,
330 );
331 });
332 args.verify::<Ts, O>(model.to_owned(), scan)
333 })
334 } else {
335 args.verify::<Ts, O>(model.to_owned(), scan)
336 }
337}
338
339// From Clap tutorial <https://docs.rs/clap/latest/clap/_derive/_tutorial/index.html#testing>
340#[test]
341fn verify_cli() {
342 use clap::CommandFactory;
343 Cli::command().debug_assert();
344}