Grcov report - variability

1

use log::debug;

2

use merc_lts::TransitionLabel;

3

use oxidd::BooleanFunction;

4

use oxidd::ManagerRef;

5

use oxidd::bdd::BDDFunction;

6

use oxidd::bdd::BDDManagerRef;

7

8

use merc_lts::LTS;

9

use merc_syntax::Action;

10

use merc_syntax::MultiAction;

11

use merc_syntax::StateFrm;

12

use merc_utilities::MercError;

13

14

use crate::FeatureTransitionSystem;

15

use crate::ModalEquationSystem;

16

use crate::Translation;

17

use crate::VariabilityParityGame;

18

use crate::VertexIndex;

19

use crate::compute_reachable;

20

use crate::make_vpg_total;

21

use crate::warn_unknown_action_labels;

22

23

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

24

1

pub fn translate_vpg(

25

1

    manager_ref: &BDDManagerRef,

26

1

    fts: &FeatureTransitionSystem<String>,

27

1

    configuration: BDDFunction,

28

1

    formula: &StateFrm,

29

1

) -> Result<VariabilityParityGame, MercError> {

30

    // Parses all labels into MultiAction once

31

1

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

32

1

        .labels()

33

1

        .iter()

34

5

        .map(|label| {

35

5

            if label.is_tau_label() {

36

1

                Ok(MultiAction::tau())

37

            } else {

38

4

                MultiAction::parse(label.label())

39

40

5

})

41

1

        .collect();

42

43

    // Simplify the labels by stripping BDD information

44

1

    let simplified_labels: Vec<MultiAction> = parsed_labels?

45

1

        .iter()

46

1

        .map(strip_feature_configuration_from_multi_action)

47

1

        .collect();

48

49

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

50

1

    warn_unknown_action_labels(formula, &simplified_labels);

51

52

1

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

53

54

1

    let equation_system = ModalEquationSystem::new(formula);

55

1

    debug!("{}", equation_system);

56

1

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

57

58

1

    algorithm.translate(

59

1

        fts.initial_state_index(),

60

0,

61

24

        |transition| match transition {

62

4

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

63

20

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

64

24

},

65

        |existing, new| {

66

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

67

            Ok(())

68

},

69

)?;

70

71

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

72

1

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

73

74

1

    let vertices = algorithm.vertices();

75

1

    let result = VariabilityParityGame::from_edges(

76

1

        manager_ref,

77

1

        VertexIndex::new(0),

78

1

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

79

1

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

80

1

        configuration,

81

1

        variables,

82

2

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

83

);

84

85

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

86

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

87

1

    if cfg!(debug_assertions) {

88

1

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

89

1

        debug_assert!(

90

23

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

91

            "Not all vertices are reachable from the initial vertex"

92

);

93

94

95

    // Ensure that the result is a total VPG.

96

1

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

97

1

        make_vpg_total(manager_ref, &result)?

98

    } else {

99

        result

100

};

101

102

1

    Ok(total_result)

103

1

104

105

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

106

5

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

107

    MultiAction {

108

5

        actions: multi_action

109

5

            .actions

110

5

            .iter()

111

5

            .map(|action| Action {

112

4

                id: action.id.clone(),

113

4

                args: Vec::new(),

114

4

})

115

5

            .collect(),

116

117

5

118

119

#[cfg(test)]

120

mod tests {

121

    use merc_macros::merc_test;

122

    use merc_syntax::UntypedStateFrmSpec;

123

124

    use crate::FeatureDiagram;

125

    use crate::compute_reachable;

126

    use crate::read_fts;

127

    use crate::translate_vpg;

128

129

    #[merc_test]

130

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

131

    fn test_vpg_running_example() {

132

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

133

134

        let fd = FeatureDiagram::from_reader(

135

            &manager_ref,

136

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

137

138

        .unwrap();

139

        let fts = read_fts(

140

            &manager_ref,

141

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

142

            fd.features().clone(),

143

144

        .unwrap();

145

146

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

147

148

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

149

150

        assert!(

151

            vpg.is_total(&manager_ref).unwrap(),

152

            "The translated VPG should be total"

153

);

154

        assert!(

155

24

            compute_reachable(&vpg).1.iter().all(|v| v.is_some()),

156

            "All vertices should be reachable from the initial vertex"

157

);

158

159