pub fn from_symbolic_lts(

        storage: &mut Storage,

        manager_ref: &BDDManagerRef,

        lts: &impl SymbolicLTS,

    ) -> Result<Self, MercError> {

        info!("Converting symbolic LTS from LDD to BDD representation...");

        let state_bits = compute_bits(&compute_highest(storage, lts.states()));

        debug!("Determined number of bits for state variables: {:?}", state_bits);

        let mut action_label_highest = 0u32;

        for group in lts.transition_groups() {

            let highest = compute_highest(storage, group.relation());

            if !highest.is_empty() {

                action_label_highest = action_label_highest

                    .max(highest[group.action_label_index().ok_or("Action label index not found")?]);

        let action_label_bits = required_bits(action_label_highest);

        debug!(

        let mut vars = Vec::new();

        let mut state_variables_bits: Vec<Vec<VarNo>> = Vec::new();

        let mut next_state_variables_bits: Vec<Vec<VarNo>> = Vec::new();

        for (i, &bits) in state_bits.iter().enumerate() {

            let mut state_var_bits = Vec::new();

            let mut next_state_var_bits = Vec::new();

            for k in 0..bits {

                // Add variable for the state variable

                state_var_bits.push(vars.len() as VarNo);

                vars.push(format!("s{}_{}", i, k));

                // Add a primed version for the write parameters

                next_state_var_bits.push(vars.len() as VarNo);

                vars.push(format!("s{}'_{}", i, k));

            }

            state_variables_bits.push(state_var_bits);

            next_state_variables_bits.push(next_state_var_bits);

        let mut action_labels_vars = Vec::new();

        for k in 0..action_label_bits {

            action_labels_vars.push(vars.len() as VarNo);

            vars.push(format!("a_{}", k));

        }

        if manager_ref.with_manager_shared(|manager| manager.num_vars()) != 0 {

        }

        manager_ref.with_manager_exclusive(|manager| {

            debug_assert_eq!(

                manager.num_vars(),

        });

        let number_of_vars = vars.len();

        let variables = manager_ref

            .with_manager_exclusive(|manager| -> Result<Range<VarNo>, DuplicateVarName> {

                manager.add_named_vars(vars)

            })

            .map_err(|e| format!("Failed to create variables: {e}"))?;

        assert!(variables.clone().is_sorted(), "Variables must be added in sorted order");

        assert!(

            variables.len() == number_of_vars,

        let bits_dd = singleton(storage, &state_bits);

        let all_state_variables_bits: Vec<VarNo> = state_variables_bits.iter().flatten().cloned().collect();

        let states = manager_ref.with_manager_shared(|manager| ldd_to_bdd(storage, manager, lts.states(), &bits_dd, &all_state_variables_bits))?;

        let initial_state = manager_ref.with_manager_shared(|manager| ldd_to_bdd(

            storage,

            manager,

            lts.initial_state(),

            &bits_dd,

            &all_state_variables_bits,

        let mut transition_groups = Vec::new();

        for group in lts.transition_groups() {

            let mut relation_bits = Vec::new();

            let mut variables = Vec::new();

            let mut read_variable_indices: Vec<VarNo> = Vec::new();

            let mut write_variable_indices: Vec<VarNo> = Vec::new();

            for (var, bits) in state_bits.iter().enumerate() {

                if group.read_indices().contains(&(var as VarNo)) {

                    relation_bits.push(*bits);

                    variables.extend(state_variables_bits[var].iter());

                    read_variable_indices.extend(state_variables_bits[var].iter())

                }

                if group.write_indices().contains(&(var as VarNo)) {

                    relation_bits.push(*bits);

                    variables.extend(next_state_variables_bits[var].iter());

                    write_variable_indices.extend(next_state_variables_bits[var].iter())

                }

            if let Some(_action_index) = group.action_label_index() {

                // TODO: This currently assumes that action label bits are at the end.

                variables.extend(action_labels_vars.iter());

            }

            relation_bits.push(action_label_bits);

            debug!(

            let bits_dd = singleton(storage, &relation_bits);

            let relation_bdd = manager_ref.with_manager_shared(|manager| ldd_to_bdd(storage, manager, group.relation(), &bits_dd, &variables))?;

            transition_groups.push(SummandGroupBdd::new(

                relation_bdd,

                read_variable_indices,

                write_variable_indices,

        let all_next_state_variables_bits = next_state_variables_bits

            .iter()

            .flatten()

            .cloned()

            .collect::<Vec<VarNo>>();

        debug!("State bits {all_state_variables_bits:?}, and next state bits {all_next_state_variables_bits:?}");

        info!("Finished conversion.");

        Ok(Self {

            action_variable_indices: action_labels_vars,

            states,

            initial_state,

            transition_groups,

            state_variable_num_of_bits: state_bits,

            state_variable_indices: all_state_variables_bits,

            next_state_variables_indices: all_next_state_variables_bits,

            action_labels: lts.action_labels().to_vec(),

            parameter_values: lts.parameter_values().to_vec(),

        })

    }

    pub fn states(&self) -> &BDDFunction {

        &self.states

    }

    pub fn initial_state(&self) -> &BDDFunction {

        &self.initial_state

    }

    pub fn state_variables(&self) -> &[VarNo] {

        &self.state_variable_indices

    }

    pub fn next_state_variables(&self) -> &[VarNo] {

        &self.next_state_variables_indices

    }

    pub fn transition_groups(&self) -> &Vec<SummandGroupBdd> {

        &self.transition_groups

    }

    pub fn action_variables(&self) -> &[VarNo] {

        &self.action_variable_indices

    }

    pub fn new(

        relation: BDDFunction,

        read_variable: Vec<VarNo>,

        write_variable: Vec<VarNo>,

    ) -> Self {

        Self {

            relation,

            read_variable,

            write_variable,

        }

    }

    pub fn relation(&self) -> &BDDFunction {

        &self.relation

    }

    pub fn write_variables(&self) -> &Vec<VarNo> {

        &self.write_variable

    }

pub fn compute_vars_bdd(manager_ref: &BDDManagerRef, vars: &[VarNo]) -> Result<(Vec<BDDFunction>, BDDFunction), OutOfMemory> {

    manager_ref.with_manager_shared(|manager| -> Result<_, OutOfMemory> {

        let mut vector = Vec::new();

        let mut bdd: BDDFunction = BDDFunction::t(manager);

        for var in vars {

            let var = BDDFunction::var(manager, *var)?;

            vector.push(var.clone());

            bdd = bdd.and(&var)?;

        Ok((vector, bdd))

    })

}

    fn test_symbolic_lts_bdd() {

        test_logger();

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

        let mut storage = Storage::new();

        let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

        let symbolic_lts = read_symbolic_lts(&mut storage, &input[..]).unwrap();

        SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &symbolic_lts).unwrap();

    }