scan/

lib.rs

//! # SCAN (StatistiCal ANalyzer)
//!
//! SCAN is a statistical model checker
//! designed to verify large concurrent systems
//! for which standard verification techniques do not scale.
//!
//! SCAN uses Channel Systems (CS) as models,[^1]
//! and Metric Temporal Logic (MTL) as property specification language.
//!
//! SCAN is being developed to accept models specified in multiple, rich modeling languages.
//! At the moment the following languages are planned or implemented:
//!
//! - [x] [State Chart XML (SCXML)](https://www.w3.org/TR/scxml/).
//! - [x] [Promela](https://spinroot.com/spin/Man/Manual.html)
//! - [x] [JANI](https://jani-spec.org/)
//!
//! This crate is part of the [SCAN statistical model checker](https://convince-project.github.io/scan/)
//!
//! [^1]: Baier, C., & Katoen, J. (2008). *Principles of model checking*. MIT Press.

#![warn(missing_docs)]
#![forbid(unsafe_code)]

mod progress;
mod report;
mod trace;
mod verify;

use std::{env::current_dir, path::PathBuf};

use anyhow::{anyhow, bail};
use clap::{Parser, Subcommand, ValueEnum};
use progress::Bar;
use report::Report;
use scan_core::{Oracle, Scan};
use trace::TraceArgs;
use verify::VerifyArgs;

/// Supported model specification formats.
///
/// SCAN supports different model specification formats.
///
/// WARNING: formats can have varying levels of supports
/// and may not be interpreted as expected.
#[deny(missing_docs)]
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum)]
enum Format {
    /// SCXML format, passed as either the path to the main file,
    /// if present, or the path of the directory sub-tree containing the model's files.
    ///
    /// SCXML models are composed by separate .scxml files for SCXML automaton,
    /// an .xml file for pMTL properties and,
    /// optionally, an .xml main file describing the model.
    ///
    /// The model can be passed to SCAN as either the path to the main file,
    /// if present, or the path of a directory.
    /// In the latter case, SCAN will attempt to process appropriately
    /// all files in the given directory and its sub-directories.
    #[cfg(feature = "scxml")]
    Scxml,
    /// JANI format, passed as the path to the .jani file.
    ///
    /// JANI models are composed by a single .jani file.
    ///
    /// The model has to be passed to SCAN as the path to the .jani file.
    ///
    /// WARNING: JANI support is still experimental.
    #[cfg(feature = "jani")]
    Jani,
    /// Promela format, passed as the path to the .pml or .prm file.
    ///
    /// Promela models are composed by a single .pml or .prm file.
    ///
    /// The model has to be passed to SCAN as the path to the .pml or .prm file.
    ///
    /// WARNING: Promela support is still experimental.
    #[cfg(feature = "promela")]
    Promela,
}

/// SCAN's available commands.
#[deny(missing_docs)]
#[derive(Subcommand)]
enum Commands {
    /// Validate the syntactical and semantical correctness of the model, without running it.
    ///
    /// Examples:
    /// 'scan PATH/TO/MODEL validate' validates the model.
    Validate,
    /// Verify properties of the given model.
    ///
    /// At least one property has to be verified.
    ///
    /// Examples:
    /// 'scan PATH/TO/MODEL verify PROPERTY' verifies the property PROPERTY over the model.
    /// 'scan PATH/TO/MODEL verify PROPERTY_1 PROPERTY_2' verifies the properties PROPERTY_1 and PROPERTY_2 together over the model.
    /// 'scan PATH/TO/MODEL verify --all' verifies all specified properties together over the model.
    #[clap(verbatim_doc_comment)]
    Verify {
        /// Args for model verification.
        #[clap(flatten)]
        args: VerifyArgs,
        /// Print progress bars during verification.
        ///
        /// By default, when it starts the verification process, SCAN only prints a terse message.
        /// For longer jobs, it is useful to have real-time feedback on how the verification is proceeding.
        /// This flag has SCAN print progress bars and current statistics on the verification process,
        /// and make a best-effort attempt in estimating how long it will take to completion.
        #[arg(long, value_enum)]
        progress: Option<Bar>,
        /// Print JSON-serialized final verification report.
        ///
        /// By default, SCAN prints a user-friendly report at the end of verification.
        /// This flag has the report printed in JSON format instead.
        #[arg(long)]
        json: bool,
    },
    /// Produce execution traces and save them to file in csv format..
    ///
    /// Executions are always run to completion, regardless of verification outcome.
    /// Executions that verify the given properties are separated from those that do not.
    /// It is possible to verify no property at all, in which case all executions are successful but still executed to completion.
    ///
    /// Examples:
    /// 'scan PATH/TO/MODEL trace' executes the model once and writes the trace to disk, without verifying any property.
    /// '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.
    /// '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.
    #[clap(verbatim_doc_comment)]
    Trace(TraceArgs),
}

const LONG_ABOUT: &str = "SCAN (StatistiCal ANalyzer) is a statistical model checker \
designed to verify large concurrent systems \
for which standard verification techniques do not scale.";

/// SCAN (StatistiCal ANalyzer) is a statistical model checker
/// designed to verify large concurrent systems
/// for which standard verification techniques do not scale.
#[derive(Parser)]
#[deny(missing_docs)]
#[command(version, about, long_about=LONG_ABOUT)]
pub struct Cli {
    /// Path of model's file or folder,
    /// depending on the used specification format.
    #[arg(value_hint = clap::ValueHint::AnyPath)]
    model: PathBuf,
    /// Format used to specify the model.
    ///
    /// SCAN supports different model specification formats,
    /// and, by default, it attempts to autodetect the correct one,
    /// but this can be specified to resolve ambiguity.
    ///
    /// WARNING: formats can have varying levels of supports
    /// and may not be interpreted as expected.
    #[arg(short, long, value_enum)]
    format: Option<Format>,
    /// Verbose output.
    ///
    /// Verbosity level corresponds to the log level that gets printed.
    /// Logging mostly concerns parsing and building of the model,
    /// so it is particularly useful when validating a model
    /// to check for errors.
    ///
    /// Verbosity levels: ERROR, WARNING, INFO, DEBUG, TRACE
    ///
    /// Examples:
    /// 'scan PATH/TO/MODEL validate -vvv' validates the model and prints ERROR, WARNING and INFO log entries.
    #[command(flatten)]
    pub verbosity: clap_verbosity_flag::Verbosity,
    /// Actions to execute on the model.
    #[command(subcommand)]
    command: Commands,
}

impl Cli {
    /// Run SCAN with the parameters passed via the CLI.
    pub fn run(self) -> anyhow::Result<()> {
        let model = std::path::absolute(&self.model)?
            .file_name()
            .and_then(std::ffi::OsStr::to_str)
            .unwrap_or("model")
            .to_owned();

        if let Some(format) = self.format {
            match format {
                #[cfg(feature = "scxml")]
                Format::Scxml => self.run_scxml(&model),
                #[cfg(feature = "jani")]
                Format::Jani => self.run_jani(&model),
                #[cfg(feature = "promela")]
                Format::Promela => self.run_promela(&model),
            }
        } else if self.model.is_dir() {
            self.run_scxml(&model)
        } else {
            let ext = self
                .model
                .extension()
                .ok_or(anyhow!("file extension unknown"))?;
            match ext
                .to_str()
                .ok_or(anyhow!("file extension not recognized"))?
            {
                #[cfg(feature = "scxml")]
                "xml" | "scxml" => self.run_scxml(&model),
                #[cfg(feature = "jani")]
                "jani" => self.run_jani(&model),
                #[cfg(feature = "promela")]
                "pml" | "prm" => self.run_promela(&model),
                _ => bail!("unsupported file format"),
            }
        }
    }

    #[cfg(feature = "scxml")]
    fn run_scxml(self, model: &str) -> anyhow::Result<()> {
        use scan_scxml::*;

        match self.command {
            Commands::Verify {
                mut args,
                progress,
                json,
            } => {
                args.validate()?;
                let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
                validate_properties(&args.properties, &scxml_model.guarantees)?;
                // Reorder properties as they appear in the model
                args.properties = scxml_model.guarantees.clone();
                run_verification::<_>(model, &args, progress, json, &scan_def).print(json);
            }
            Commands::Validate => {
                let (_scan, _scxml_model) = load(&self.model, &[], true)?;
                // At this point the model has been validated
                println!("model '{model}' successfully validated");
            }
            Commands::Trace(mut args) => {
                let (scan_def, scxml_model) = load(&self.model, &args.properties, args.all)?;
                validate_properties(&args.properties, &scxml_model.guarantees)?;
                // Reorder properties as they appear in the model
                args.properties = scxml_model.guarantees.clone();
                let path = new_traces_dir();
                args.trace::<_, TracePrinter>(&scan_def, path, &scxml_model);
                println!("trace computation for model '{model}' completed");
            }
        }
        Ok(())
    }

    #[cfg(feature = "jani")]
    fn run_jani(self, model: &str) -> anyhow::Result<()> {
        use scan_jani::*;

        match self.command {
            Commands::Verify {
                mut args,
                progress,
                json,
            } => {
                args.validate()?;
                let properties = args.properties.clone();
                let (scan, jani_model) = load(&self.model, &properties)?;
                validate_properties(&args.properties, &jani_model.guarantees)?;
                // Reorder properties as they appear in the model
                args.properties = jani_model.guarantees.clone();
                run_verification::<_>(model, &args, progress, json, &scan).print(json);
            }
            Commands::Validate => {
                let (_scan, _jani_model) = load(&self.model, &[])?;
                println!("model '{model}' successfully validated");
            }
            Commands::Trace(args) => {
                args.validate()?;
                let (scan, jani_model) = load(&self.model, &[])?;
                let path = new_traces_dir();
                args.trace::<_, TracePrinter>(&scan, path, &jani_model);
                println!("trace computation for model '{model}' completed");
            }
        }
        Ok(())
    }

    #[cfg(feature = "promela")]
    fn run_promela(self, model: &str) -> anyhow::Result<()> {
        use scan_promela::*;

        match self.command {
            Commands::Verify {
                args,
                progress,
                json,
            } => {
                args.validate()?;
                let properties = args.properties.clone();
                let (scan, _promela_model) = load(&self.model, &properties, args.all)?;
                run_verification::<_>(model, &args, progress, json, &scan).print(json);
            }
            Commands::Validate => {
                let (_scan, _jani_model) = load(&self.model, &[], true)?;
                println!("model '{model}' successfully validated");
            }
            Commands::Trace(args) => {
                args.validate()?;
                let (_scan, _promela_model) = load(&self.model, &[], args.all)?;
                println!("processing model '{model}' completed");
            }
        }
        Ok(())
    }
}

fn validate_properties(props: &[String], all_props: &[String]) -> anyhow::Result<()> {
    if let Some(prop) = props.iter().find(|prop| !all_props.contains(prop)) {
        Err(anyhow!(
            "no property named '{prop}' found in model.\n\nHint: maybe it is misspelled?"
        ))
    } else {
        Ok(())
    }
}

fn run_verification<'a, O>(
    model: &str,
    args: &VerifyArgs,
    progress: Option<Bar>,
    json: bool,
    scan: &'a Scan<O>,
) -> Report
where
    O: 'a + Oracle + Clone + Sync,
{
    if !json {
        println!(
            "Verifying {model} (-p {} -c {}) {:?}",
            args.precision, args.confidence, args.properties
        );
    }
    if let Some(bar) = progress {
        std::thread::scope(|s| {
            s.spawn(|| {
                bar.print_progress_bar::<O>(
                    args.confidence,
                    args.precision,
                    &args.properties,
                    scan,
                );
            });
            args.verify::<O>(model.to_owned(), scan)
        })
    } else {
        args.verify::<O>(model.to_owned(), scan)
    }
}

fn new_traces_dir() -> std::path::PathBuf {
    const FOLDER: &str = "traces";

    let mut path = current_dir().expect("current dir");
    for i in 0.. {
        path.push(format!("{}_{i:02}", FOLDER));
        if std::fs::exists(&path).is_ok_and(|exists| !exists) {
            break;
        } else {
            assert!(path.pop());
        }
    }
    path
}

// From Clap tutorial <https://docs.rs/clap/latest/clap/_derive/_tutorial/index.html#testing>
#[test]
fn verify_cli() {
    use clap::CommandFactory;
    Cli::command().debug_assert();
}