Lines
70.21 %
Functions
47.37 %
Branches
100 %
use std::error::Error;
use mcrl2_sys::cxx::UniquePtr;
use mcrl2_sys::cxx::{self};
use mcrl2_sys::data::ffi;
use utilities::lock_global;
use crate::aterm::ATerm;
use crate::aterm::ATermList;
use crate::aterm::ATermRef;
use super::DataExpression;
use super::DataFunctionSymbol;
use super::DataVariable;
use super::SortExpressionRef;
/// A safe abstraction for the mCRL2 data specification.
pub struct DataSpecification {
pub(crate) data_spec: UniquePtr<ffi::data_specification>,
}
impl DataSpecification {
/// Parses the given text into a data specification
pub fn new(text: &str) -> Result<Self, cxx::Exception> {
let _guard = lock_global();
let data_spec = ffi::parse_data_specification(text)?;
Ok(DataSpecification { data_spec })
/// Parses the given text as a data expression for the spec.
pub fn parse(&self, text: &str) -> Result<DataExpression, Box<dyn Error>> {
let term: ATerm = ffi::parse_data_expression(text, &self.data_spec)?.into();
Ok(term.into())
/// Parses the given text as a data variable for the spec.
pub fn parse_variable(&self, text: &str) -> Result<DataVariable, Box<dyn Error>> {
let term: ATerm = ffi::parse_variable(text, &self.data_spec)?.into();
/// Returns the equations of the data specification.
pub fn equations(&self) -> Vec<DataEquation> {
ffi::get_data_specification_equations(&self.data_spec)
.iter()
.map(|x| ATerm::from(x).into())
.collect()
/// Returns the constructors for the given sort expression.
pub fn constructors(&self, sort: &SortExpressionRef<'_>) -> Vec<DataFunctionSymbol> {
let t: ATermRef<'_> = sort.copy().into();
unsafe {
ffi::get_data_specification_constructors(&self.data_spec, t.get())
impl Clone for DataSpecification {
fn clone(&self) -> Self {
DataSpecification {
data_spec: ffi::data_specification_clone(&self.data_spec),
#[derive(PartialEq, Eq, Hash, Clone, PartialOrd, Ord, Debug)]
pub struct DataEquation {
pub variables: Vec<DataVariable>,
pub condition: DataExpression,
pub lhs: DataExpression,
pub rhs: DataExpression,
impl From<ATerm> for DataEquation {
fn from(value: ATerm) -> Self {
let variables: ATermList<DataVariable> = value.arg(0).into();
DataEquation {
variables: variables.iter().collect(),
condition: value.arg(1).protect().into(),
lhs: value.arg(2).protect().into(),
rhs: value.arg(3).protect().into(),
#[cfg(test)]
mod tests {
use test_log::test;
use super::*;
#[test]
fn test_parse_data_specification() {
let text = "
sort Xbool = struct
Xfalse
| Xtrue ;
sort Bit = struct
x0
| x1 ;
sort Octet = struct
buildOctet (Bit, Bit, Bit, Bit, Bit, Bit, Bit, Bit) ;
sort OctetSum = struct
buildOctetSum (Bit, Octet) ;
sort Half = struct
buildHalf (Octet, Octet) ;
sort HalfSum = struct
buildHalfSum (Bit, Half) ;
map
notBool : Xbool -> Xbool ;
andBool : Xbool # Xbool -> Xbool ;";
let _data_spec = DataSpecification::new(text).unwrap();