mcrl2/
lps.rs

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
//!
//! Safe abstraction for the LPS library,
//!

use std::error::Error;
use std::fmt;

use mcrl2_sys::cxx::UniquePtr;
use mcrl2_sys::lps::ffi;

use crate::data::DataSpecification;

/// Rust representation of a lps::linear_process_specification.
pub struct LinearProcessSpecification {
    lps: UniquePtr<ffi::specification>,
}

impl LinearProcessSpecification {
    /// Reads the linear process specification from the given path.
    pub fn read(filename: &str) -> Result<LinearProcessSpecification, Box<dyn Error>> {
        Ok(LinearProcessSpecification {
            lps: ffi::read_linear_process_specification(filename)?,
        })
    }

    /// Returns the underlying data specification.
    pub fn data_specification(&self) -> DataSpecification {
        DataSpecification {
            data_spec: ffi::get_data_specification(&self.lps),
        }
    }
}

impl fmt::Display for LinearProcessSpecification {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", ffi::print_linear_process_specification(&self.lps))
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_read_linear_process_specification() {
        let lps = LinearProcessSpecification::read("../../examples/lps/abp.lps").unwrap();

        let _data_spec = lps.data_specification();

        println!("{}", lps);
    }
}