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

use crate::ast::{Expr, VarDecl, VarType};

/// Returns the folded integer encoding of a variable's single initial value.
///
/// For bool variables, `false -> 0` and `true -> 1`.
/// This helper assumes analysis has already folded initial expressions to
/// literals compatible with their declared type.
pub fn init_value(var_decl: &VarDecl) -> i32 {
    match (&var_decl.var_type, &*var_decl.init) {
        (VarType::BoundedInt { .. }, Expr::IntLit(v)) => *v,
        (VarType::Bool, Expr::BoolLit(b)) => {
            if *b {
                1
            } else {
                0
            }
        }
        (VarType::Bool, Expr::IntLit(v)) if *v == 0 || *v == 1 => *v,
        _ => panic!(
            "Unsupported folded init expression for variable '{}': {:?}",
            var_decl.name, var_decl.init
        ),
    }
}