1 
//!
2 
//! Safe abstraction for the LPS library,
3 
//!
4 

            

        

            

                5
            

            

                
            

            

                
use std::error::Error;

            

        

            

                6
            

            

                
            

            

                
use std::fmt;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use mcrl2_sys::cxx::UniquePtr;

            

        

            

                9
            

            

                
            

            

                
use mcrl2_sys::lps::ffi;

            

        

            

                10
            

            

                
            

            

                

            

        

            

                11
            

            

                
            

            

                
use crate::data::DataSpecification;

            

        

            

                12
            

            

                
            

            

                

            

        

            

                13
            

            

                
            

            

                
/// Rust representation of a lps::linear_process_specification.

            

        

            

                14
            

            

                
            

            

                
pub struct LinearProcessSpecification {

            

        

            

                15
            

            

                
            

            

                
    lps: UniquePtr<ffi::specification>,

            

        

            

                16
            

            

                
            

            

                
}

            

        

            

                17
            

            

                
            

            

                

            

        

            

                18
            

            

                
            

            

                
impl LinearProcessSpecification {

            

        

            

                19
            

            

                
            

            

                
    /// Reads the linear process specification from the given path.

            

        

            

                20
            

            

                1
            

            

                
    pub fn read(filename: &str) -> Result<LinearProcessSpecification, Box<dyn Error>> {

            

        

            

                21
            

            

                1
            

            

                
        Ok(LinearProcessSpecification {

            

        

            

                22
            

            

                1
            

            

                
            lps: ffi::read_linear_process_specification(filename)?,

            

        

            

                23
            

            

                
            

            

                
        })

            

        

            

                24
            

            

                1
            

            

                
    }

            

        

            

                25
            

            

                
            

            

                

            

        

            

                26
            

            

                
            

            

                
    /// Returns the underlying data specification.

            

        

            

                27
            

            

                1
            

            

                
    pub fn data_specification(&self) -> DataSpecification {

            

        

            

                28
            

            

                1
            

            

                
        DataSpecification {

            

        

            

                29
            

            

                1
            

            

                
            data_spec: ffi::get_data_specification(&self.lps),

            

        

            

                30
            

            

                1
            

            

                
        }

            

        

            

                31
            

            

                1
            

            

                
    }

            

        

            

                32
            

            

                
            

            

                
}

            

        

            

                33
            

            

                
            

            

                

            

        

            

                34
            

            

                
            

            

                
impl fmt::Display for LinearProcessSpecification {

            

        

            

                35
            

            

                1
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            

        

            

                36
            

            

                1
            

            

                
        write!(f, "{}", ffi::print_linear_process_specification(&self.lps))

            

        

            

                37
            

            

                1
            

            

                
    }

            

        

            

                38
            

            

                
            

            

                
}

            

        

            

                39
            

            

                
            

            

                

            

        

            

                40
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                41
            

            

                
            

            

                
mod tests {

            

        

            

                42
            

            

                
            

            

                
    use super::*;

            

        

            

                43
            

            

                
            

            

                

            

        

            

                44
            

            

                
            

            

                
    #[test]

            

        

            

                45
            

            

                1
            

            

                
    fn test_read_linear_process_specification() {

            

        

            

                46
            

            

                1
            

            

                
        let lps = LinearProcessSpecification::read("../../examples/lps/abp.lps").unwrap();

            

        

            

                47
            

            

                1
            

            

                

            

        

            

                48
            

            

                1
            

            

                
        let _data_spec = lps.data_specification();

            

        

            

                49
            

            

                1
            

            

                

            

        

            

                50
            

            

                1
            

            

                
        println!("{}", lps);

            

        

            

                51
            

            

                1
            

            

                
    }

            

        

            

                52
            

            

                
            

            

                
}