prismulti 0.1.0

A multi-threaded Rust implementation of a subset of the PRISM model checker.
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

use anyhow::Result;
use lalrpop_util::lalrpop_mod;

use crate::ast;
lalrpop_mod!(
    #[allow(clippy::all)]
    #[rustfmt::skip]
    parser,
    "/parser/parser.rs"
);

/// Parse a PRISM DTMC model string into the project AST.
///
/// On parse failure, this reports line/column-oriented diagnostics to make
/// grammar errors easier to locate.
pub fn parse_dtmc(input: &str) -> Result<ast::DTMCAst> {
    let parser = parser::DTMCParser::new();
    parser
        .parse(input)
        .map_err(|e| parse_error_to_anyhow(input, e))
}

/// Parsed DTMC property file payload: `(const_declarations, properties)`.
pub type ParsedProps = (Vec<(String, ast::ConstDecl)>, Vec<ast::Property>);

/// Parse a DTMC property file into property/query AST.
pub fn parse_dtmc_props(input: &str) -> Result<ParsedProps> {
    let parser = parser::DTMCPropsParser::new();
    parser
        .parse(input)
        .map_err(|e| parse_error_to_anyhow(input, e))
}

fn parse_error_to_anyhow<Tok, Err>(
    input: &str,
    e: lalrpop_util::ParseError<usize, Tok, Err>,
) -> anyhow::Error
where
    Tok: std::fmt::Display,
    Err: std::fmt::Display,
{
    let msg = match &e {
        lalrpop_util::ParseError::InvalidToken { location } => {
            let (line, col) = line_col(input, *location);
            format!("Invalid token at line {line}, col {col}")
        }
        lalrpop_util::ParseError::UnrecognizedToken {
            token: (start, tok, _),
            expected,
        } => {
            let (line, col) = line_col(input, *start);
            format!(
                "Unexpected token '{tok}' at line {line}, col {col}. Expected one of: {}",
                expected.join(", ")
            )
        }
        lalrpop_util::ParseError::UnrecognizedEof { expected, .. } => {
            format!(
                "Unexpected end of input. Expected one of: {}",
                expected.join(", ")
            )
        }
        lalrpop_util::ParseError::ExtraToken {
            token: (start, tok, _),
        } => {
            let (line, col) = line_col(input, *start);
            format!("Extra token '{tok}' at line {line}, col {col}")
        }
        lalrpop_util::ParseError::User { error } => format!("Parse error: {error}"),
    };
    anyhow::anyhow!(msg)
}

fn line_col(input: &str, byte_offset: usize) -> (usize, usize) {
    let line = input[..byte_offset].matches('\n').count() + 1;
    let col = byte_offset - input[..byte_offset].rfind('\n').map(|i| i + 1).unwrap_or(0) + 1;
    (line, col)
}