1
use rand::Rng;
2
use rand::RngExt;
3
use rand::seq::IndexedRandom;
4
use rand::seq::IteratorRandom;
5

            
6
use merc_aterm::ATermString;
7
use merc_data::DataExpression;
8
use merc_data::DataSpecification;
9
use merc_data::DataVariable;
10
use merc_ldd::Storage;
11
use merc_ldd::from_iter;
12
use merc_ldd::random_vector_set;
13
use merc_lts::LtsMultiAction;
14
use merc_lts::TransitionLabel;
15
use merc_utilities::MercError;
16

            
17
use crate::SummandGroup;
18
use crate::SymbolicLts;
19

            
20
/// Generates random symbolic LTSs for testing purposes.
21
300
pub fn random_symbolic_lts<R: Rng>(
22
300
    rng: &mut R,
23
300
    storage: &mut Storage,
24
300
    num_state_variables: usize,
25
300
    num_action_labels: usize,
26
300
) -> Result<SymbolicLts, MercError> {
27
300
    let num_of_values = 5usize;
28

            
29
    // Determine the state set.
30
300
    let states = random_vector_set(rng, 100, num_state_variables, num_of_values as u32);
31
300
    let initial_state = states.iter().choose(rng).ok_or("at least one state generated")?;
32

            
33
    // The action labels
34
300
    let mut action_labels = Vec::new();
35
1500
    for i in 0..num_action_labels {
36
1500
        action_labels.push(LtsMultiAction::from_index(i));
37
1500
    }
38

            
39
    // The parameter values
40
300
    let mut parameter_values = Vec::new();
41
300
    let value = DataExpression::from_string("1")?;
42
3000
    for _ in 0..num_state_variables {
43
3000
        parameter_values.push(Vec::from_iter(std::iter::repeat_n(value.clone(), num_of_values)));
44
3000
    }
45

            
46
    // The parameter names
47
300
    let parameters = (0..num_state_variables)
48
3000
        .map(|i| DataVariable::new(ATermString::new(format!("p{i}"))))
49
300
        .collect::<Vec<_>>();
50

            
51
    // Determine the summand groups.
52
300
    let mut summand_groups = Vec::new();
53
300
    for _ in 0..5 {
54
1500
        let num_of_read_variables = rng.random_range(0..parameters.len());
55
1500
        let read_parameters = parameters
56
1500
            .sample(rng, num_of_read_variables)
57
1500
            .cloned()
58
1500
            .collect::<Vec<_>>();
59

            
60
1500
        let num_of_write_variables = rng.random_range(0..parameters.len());
61
1500
        let write_parameters = parameters
62
1500
            .sample(rng, num_of_write_variables)
63
1500
            .cloned()
64
1500
            .collect::<Vec<_>>();
65

            
66
        // Reserve additional space for action labels.
67
1500
        let relation = random_vector_set(rng, 10, read_parameters.len() + write_parameters.len() + 1, 5);
68
1500
        let relation_bdd = from_iter(storage, relation.iter());
69

            
70
1500
        summand_groups.push(SummandGroup::new(
71
1500
            storage,
72
1500
            &parameters,
73
1500
            read_parameters,
74
1500
            write_parameters,
75
1500
            relation_bdd,
76
        )?)
77
    }
78

            
79
300
    let initial_state_ldd = from_iter(storage, std::iter::once(initial_state));
80
300
    let states_ldd = from_iter(storage, states.iter());
81

            
82
300
    Ok(SymbolicLts::new(
83
300
        DataSpecification::default(),
84
300
        states_ldd,
85
300
        initial_state_ldd,
86
300
        summand_groups,
87
300
        action_labels,
88
300
        parameter_values,
89
300
    ))
90
300
}