Grcov report - variability

1

use log::debug;

2

use oxidd::BooleanFunction;

3

use oxidd::ManagerRef;

4

use oxidd::bdd::BDDFunction;

5

use oxidd::bdd::BDDManagerRef;

6

7

use merc_lts::LTS;

8

use merc_syntax::Action;

9

use merc_syntax::MultiAction;

10

use merc_syntax::StateFrm;

11

use merc_utilities::MercError;

12

13

use crate::FeatureTransitionSystem;

14

use crate::ModalEquationSystem;

15

use crate::Translation;

16

use crate::VariabilityParityGame;

17

use crate::VertexIndex;

18

use crate::compute_reachable;

19

use crate::make_vpg_total;

20

use crate::warn_unknown_action_labels;

21

22

/// Translates a feature transition system into a variability parity game.

23

1

pub fn translate_vpg(

24

1

    manager_ref: &BDDManagerRef,

25

1

    fts: &FeatureTransitionSystem<String>,

26

1

    configuration: BDDFunction,

27

1

    formula: &StateFrm,

28

1

) -> Result<VariabilityParityGame, MercError> {

29

    // Parses all labels into MultiAction once

30

1

    let parsed_labels: Result<Vec<MultiAction>, MercError> =

31

5

        fts.labels().iter().map(|label| MultiAction::parse(label.label())).collect();

32

33

    // Simplify the labels by stripping BDD information

34

1

    let simplified_labels: Vec<MultiAction> = parsed_labels?

35

1

        .iter()

36

1

        .map(strip_feature_configuration_from_multi_action)

37

1

        .collect();

38

39

    // Warn about any labels that are used in the formula but do not correspond to any label in the LTS.

40

1

    warn_unknown_action_labels(formula, &simplified_labels);

41

42

1

    let true_bdd = manager_ref.with_manager_shared(|manager| BDDFunction::t(manager));

43

44

1

    let equation_system = ModalEquationSystem::new(formula);

45

1

    debug!("{}", equation_system);

46

1

    let mut algorithm: Translation<'_, _, BDDFunction> = Translation::new(fts, &simplified_labels, &equation_system);

47

48

1

    algorithm.translate(

49

1

        fts.initial_state_index(),

50

0,

51

24

        |transition| match transition {

52

4

            Some(transition) => fts.labels()[transition.label].feature_expr().clone(),

53

20

            None => true_bdd.clone(), // The label does not matter, allow all configurations.

54

24

},

55

        |existing, new| {

56

            *existing = existing.or(&new)?;

57

            Ok(())

58

},

59

)?;

60

61

    // Convert the feature diagram (with names) to a VPG

62

1

    let variables: Vec<BDDFunction> = fts.features().values().cloned().collect();

63

64

1

    let vertices = algorithm.vertices();

65

1

    let result = VariabilityParityGame::from_edges(

66

1

        manager_ref,

67

1

        VertexIndex::new(0),

68

1

        vertices.iter().map(|vertex| vertex.0).collect(),

69

1

        vertices.iter().map(|vertex| vertex.1).collect(),

70

1

        configuration,

71

1

        variables,

72

2

        || algorithm.edges().iter().cloned(),

73

);

74

75

    // Check that all vertices are reachable from the initial vertex. After

76

    // totality it could be that the true or false nodes are not reachable.

77

1

    if cfg!(debug_assertions) {

78

1

        let (_, reachable_vertices) = compute_reachable(&result);

79

1

        debug_assert!(

80

23

            reachable_vertices.iter().all(|v| v.is_some()),

81

            "Not all vertices are reachable from the initial vertex"

82

);

83

84

85

    // Ensure that the result is a total VPG.

86

1

    let total_result = if !result.is_total(manager_ref)? {

87

1

        make_vpg_total(manager_ref, &result)?

88

    } else {

89

        result

90

};

91

92

1

    Ok(total_result)

93

1

94

95

/// Removes the BDD information from the multi-action, i.e., only keeps the action labels.

96

5

fn strip_feature_configuration_from_multi_action(multi_action: &MultiAction) -> MultiAction {

97

    MultiAction {

98

5

        actions: multi_action

99

5

            .actions

100

5

            .iter()

101

5

            .map(|action| Action {

102

5

                id: action.id.clone(),

103

5

                args: Vec::new(),

104

5

})

105

5

            .collect(),

106

107

5

108

109

#[cfg(test)]

110

mod tests {

111

    use merc_macros::merc_test;

112

    use merc_syntax::UntypedStateFrmSpec;

113

114

    use crate::FeatureDiagram;

115

    use crate::read_fts;

116

117

    use super::*;

118

119

    #[merc_test]

120

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

121

    fn test_vpg_running_example() {

122

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

123

124

        let fd = FeatureDiagram::from_reader(

125

            &manager_ref,

126

            include_bytes!("../../../examples/vpg/running_example_fts.fd") as &[u8],

127

128

        .unwrap();

129

        let fts = read_fts(

130

            &manager_ref,

131

            include_bytes!("../../../examples/vpg/running_example_fts.aut") as &[u8],

132

            fd.features().clone(),

133

134

        .unwrap();

135

136

        let formula = UntypedStateFrmSpec::parse(include_str!("../../../examples/vpg/running_example.mcf")).unwrap();

137

138

        let vpg = translate_vpg(&manager_ref, &fts, fd.configuration().clone(), &formula.formula).unwrap();

139

140

        assert!(vpg.is_total(&manager_ref).unwrap(), "The translated VPG should be total");

141

24

        assert!(compute_reachable(&vpg).1.iter().all(|v| v.is_some()), "All vertices should be reachable from the initial vertex");

142

143