smc_scan_scxml 0.1.0

SCXML frontend for the Scan model checker.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

//! Parser and model builder for SCAN's CONVINCE-XML specification format.

mod builder;
mod parser;
mod print_trace;

use std::path::Path;

pub use builder::ScxmlModel;
use log::info;
pub use print_trace::TracePrinter;
pub use scan_core;
use scan_core::{CsModel, PmtlOracle, Scan};

pub type ScxmlScan = Scan<CsModel, PmtlOracle>;

pub fn load(
    path: &Path,
    properties: &[String],
    all_properties: bool,
) -> anyhow::Result<(ScxmlScan, ScxmlModel)> {
    let time = std::time::Instant::now();
    info!(target: "parser", "parse SCXML model");
    let parser = parser::Parser::parse(path)?;
    info!("parsing model completed in {:?}", time.elapsed());

    let time = std::time::Instant::now();
    info!(target: "build", "building SCXML model");
    let (cs, oracle, model) = builder::ModelBuilder::build(parser, properties, all_properties)?;
    info!("building model completed in {:?}", time.elapsed());
    let scan = Scan::new(cs, oracle);
    Ok((scan, model))
}