Grcov report - random_symbolic

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

use merc_utilities::Timing;

17

18

use crate::SummandGroup;

19

use crate::SymbolicLts;

20

use crate::reachability;

21

22

/// Generates random symbolic LTSs for testing purposes.

23

300

pub fn random_symbolic_lts<R: Rng>(

24

300

    rng: &mut R,

25

300

    storage: &mut Storage,

26

300

    num_state_variables: usize,

27

300

    num_action_labels: usize,

28

300

) -> Result<SymbolicLts, MercError> {

29

300

    let num_of_values = 5usize;

30

31

    // Determine the state set.

32

300

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

33

300

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

34

35

    // The action labels

36

300

    let mut action_labels = Vec::new();

37

1500

    for i in 0..num_action_labels {

38

1500

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

39

1500

40

41

    // The parameter values

42

300

    let mut parameter_values = Vec::new();

43

300

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

44

3000

    for _ in 0..num_state_variables {

45

3000

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

46

3000

47

48

    // The parameter names

49

300

    let parameters = (0..num_state_variables)

50

3000

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

51

300

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

52

53

    // Determine the summand groups.

54

300

    let mut summand_groups = Vec::new();

55

300

    for _ in 0..5 {

56

1500

        let num_of_read_variables = rng.random_range(0..parameters.len());

57

1500

        let read_parameters = parameters

58

1500

            .sample(rng, num_of_read_variables)

59

1500

            .cloned()

60

1500

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

61

62

1500

        let num_of_write_variables = rng.random_range(0..parameters.len());

63

1500

        let write_parameters = parameters

64

1500

            .sample(rng, num_of_write_variables)

65

1500

            .cloned()

66

1500

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

67

68

        // Reserve additional space for action labels.

69

1500

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

70

1500

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

71

72

1500

        summand_groups.push(SummandGroup::new(

73

1500

            storage,

74

1500

            &parameters,

75

1500

            read_parameters,

76

1500

            write_parameters,

77

1500

            relation_bdd,

78

)?)

79

80

81

300

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

82

83

    // Compute the actual reachable state set, since the randomly generated transitions are not

84

    // restricted to the random state set above.

85

300

    let mut lts = SymbolicLts::new(

86

300

        DataSpecification::default(),

87

300

        initial_state_ldd.clone(),

88

300

        initial_state_ldd,

89

300

        summand_groups,

90

300

        action_labels,

91

300

        parameter_values,

92

);

93

94

300

    let reachable = reachability(storage, &mut lts, &Timing::new())?;

95

300

    lts.set_states(reachable);

96

97

300

    Ok(lts)

98

300