pub fn from_symbolic_lts<L: SymbolicLTS>(

        storage: &mut Storage,

        manager_ref: &BDDManagerRef,

        lts: &L,

    ) -> Result<Self, MercError> {

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

        let mut state_highest = compute_highest(storage, lts.states());

        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.max(highest[group.action_label_index().ok_or("Action label index not found")?]);

            for (ldd_level, var) in group

                .read_indices()

                .iter()

                .merge(group.write_indices().iter())

                .enumerate()

            {

                let var = *var as usize;

                state_highest[var] = state_highest[var].max(highest[ldd_level]);

            }

        let state_bits = compute_bits(&state_highest);

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

        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 = ldd_to_bdd(storage, manager_ref, lts.states(), &bits_dd, &all_state_variables_bits)?;

        let initial_state = ldd_to_bdd(

            storage,

            manager_ref,

            lts.initial_state(),

            &bits_dd,

            &all_state_variables_bits,

        let mut transition_groups = Vec::new();

        for (index, group) in lts.transition_groups().iter().enumerate() {

            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 = ldd_to_bdd(storage, manager_ref, 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 with_transition_groups(lts: &Self, transition_groups: Vec<SummandGroupBdd>) -> Self {

        Self {

            states: lts.states.clone(),

            initial_state: lts.initial_state.clone(),

            state_variable_num_of_bits: lts.state_variable_num_of_bits.clone(),

            state_variable_indices: lts.state_variable_indices.clone(),

            next_state_variables_indices: lts.next_state_variables_indices.clone(),

            action_variable_indices: lts.action_variable_indices.clone(),

            action_labels: lts.action_labels.clone(),

            parameter_values: lts.parameter_values.clone(),

            transition_groups,

        }

    }

    pub fn with_quotient_state(

        lts: &Self,

        states: BDDFunction,

        initial_state: BDDFunction,

        transition_groups: Vec<SummandGroupBdd>,

        state_variable_indices: Vec<VarNo>,

        next_state_variables_indices: Vec<VarNo>,

        state_variable_num_of_bits: Vec<Value>,

    ) -> Self {

        Self {

            states,

            initial_state,

            transition_groups,

            state_variable_num_of_bits,

            state_variable_indices,

            next_state_variables_indices,

            action_variable_indices: lts.action_variable_indices.clone(),

            action_labels: lts.action_labels.clone(),

            parameter_values: Vec::new(),

        }

    }

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

        &self.states

    }

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

        &self.initial_state

    }

    pub fn state_variable_num_of_bits(&self) -> &[Value] {

        &self.state_variable_num_of_bits

    }

    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) -> &[SummandGroupBdd] {

        &self.transition_groups

    }

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

        &self.action_variable_indices

    }

    pub fn action_labels(&self) -> &[String] {

        &self.action_labels

    }

    pub fn new(relation: BDDFunction, read_variables: Vec<VarNo>, write_variables: Vec<VarNo>) -> Self {

        Self {

            relation,

            read_variables,

            write_variables,

        }

    }

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

        &self.relation

    }

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

        &self.read_variables

    }

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

        &self.write_variables

    }

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_from_symbolic_lts_bdd_abp() {

        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();

    }