pub fn random_symbolic_lts<R: Rng>(

    rng: &mut R,

    manager: &LDDManagerRef,

    num_state_variables: usize,

    num_action_labels: usize,

) -> Result<SymbolicLts, MercError> {

    let num_of_values = 5usize;

    let states = random_vector_set(rng, 100, num_state_variables, num_of_values as u32);

    let initial_state = states.iter().choose(rng).ok_or("at least one state generated")?;

    let mut action_labels = Vec::new();

    for i in 0..num_action_labels {

        action_labels.push(LtsMultiAction::from_index(i));

    }

    let mut parameter_values = Vec::new();

    let value = DataExpression::from_string("1")?;

    for _ in 0..num_state_variables {

        parameter_values.push(Vec::from_iter(std::iter::repeat_n(value.clone(), num_of_values)));

    }

    let parameters = (0..num_state_variables)

        .map(|i| DataVariable::new(ATermString::new(format!("p{i}"))))

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

    let mut summand_groups = Vec::new();

    for _ in 0..5 {

        let num_of_read_variables = if parameters.is_empty() {

            rng.random_range(0..parameters.len())

        let read_parameters = parameters

            .sample(rng, num_of_read_variables)

            .cloned()

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

        let num_of_write_variables = if parameters.is_empty() {

            rng.random_range(0..parameters.len())

        let write_parameters = parameters

            .sample(rng, num_of_write_variables)

            .cloned()

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

        let relation = random_vector_set(rng, 10, read_parameters.len() + write_parameters.len() + 1, 5);

        let relation_bdd = from_iter(manager, relation.iter());

        summand_groups.push(SummandGroup::new(

            manager,

            &parameters,

            read_parameters,

            write_parameters,

            relation_bdd,

    let initial_state_ldd = from_iter(manager, std::iter::once(initial_state));

    let mut lps = ExplorationLps {

        initial_state: initial_state_ldd.clone(),

        summand_groups,

    };

    let reachable = reachability(manager, &mut lps, &Timing::new())?;

    Ok(SymbolicLts::new(

        DataSpecification::default(),

        reachable,

        initial_state_ldd,

        lps.summand_groups,

        action_labels,

        parameter_values,

    ))

}

    fn initial_state(&self) -> &LDDFunction {

        &self.initial_state

    }

    fn transition_groups_mut(&mut self) -> &mut [Self::Group] {

        &mut self.summand_groups

    }

    fn create_context(&self) {}