pub fn read_symbolic_lts<R: Read>(manager: &LDDManagerRef, reader: R) -> Result<SymbolicLts, MercError> {

    info!("Reading symbolic LTS in the mCRL2 symbolic format...");

    let aterm_stream = BinaryATermReader::new(BufReader::new(reader))?;

    let mut stream = BinaryLddReader::new(manager, aterm_stream)?;

    if ATermRead::read_aterm(&mut stream)? != Some(symbolic_labelled_transition_system_mark()) {

    }

    let data_spec = DataSpecification::read(&mut stream)?;

    let process_parameters: ATermList<DataVariable> = stream.read_aterm()?.ok_or("Expected process parameters")?.into();

    let process_parameters: Vec<DataVariable> = process_parameters.to_vec();

    let initial_state = stream.read_ldd(manager)?;

    let states = stream.read_ldd(manager)?;

    let mut parameter_values: Vec<Vec<DataExpression>> = Vec::with_capacity(process_parameters.len());

    for parameter in &process_parameters {

        let num_of_entries = stream.read_integer()?;

        debug!(

        let mut values = Vec::with_capacity(num_of_entries as usize);

        for i in 0..num_of_entries {

            let value = stream.read_aterm()?.ok_or("Unexpected end of stream")?;

            let expr: DataExpression = value.into();

            debug!("  {i}:  {}", expr);

            values.push(expr);

        parameter_values.push(values);

    let num_of_action_labels = stream.read_integer()?;

    let mut action_labels = Vec::with_capacity(num_of_action_labels as usize);

    for _ in 0..num_of_action_labels {

        let action_label = stream.read_aterm()?.ok_or("Unexpected end of stream")?;

        let action = LtsMultiAction::from_mcrl2_aterm(action_label)?;

        debug!("Action {}: {}", action_labels.len(), action);

        action_labels.push(action);

    let mut summand_groups = Vec::new();

    let num_of_groups = stream.read_integer()?;

    for _ in 0..num_of_groups {

        let num_of_reads = stream.read_integer()?;

        let mut read_parameters: Vec<DataVariable> = Vec::with_capacity(num_of_reads as usize);

        for _ in 0..num_of_reads {

            read_parameters.push(stream.read_aterm()?.ok_or("Unexpected end of stream")?.into());

        let num_of_writes = stream.read_integer()?;

        let mut write_parameters: Vec<DataVariable> = Vec::with_capacity(num_of_writes as usize);

        for _ in 0..num_of_writes {

            write_parameters.push(stream.read_aterm()?.ok_or("Unexpected end of stream")?.into());

        let relation = stream.read_ldd(manager)?;

        summand_groups.push(SummandGroup::new(

            manager,

            &process_parameters,

            read_parameters,

            write_parameters,

            relation,

    info!("Finished reading symbolic LTS.");

    Ok(SymbolicLts::new(

        data_spec,

        states,

        initial_state,

        summand_groups,

        action_labels,

        parameter_values,

    ))

}

fn symbolic_labelled_transition_system_mark() -> ATerm {

    ATerm::constant(&Symbol::new("symbolic_labelled_transition_system", 0))

}

    fn test_read_symbolic_lts_wms_sym() {

        test_logger();

        let input = include_bytes!("../../../../examples/lts/WMS.sym");

        let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

        let _lts = read_symbolic_lts(&ldd_manager, &input[..]).unwrap();

    }