Grcov report - project

1

use log::debug;

2

use merc_lts::LtsBuilder;

3

use oxidd::BooleanFunction;

4

use oxidd::Function;

5

use oxidd::bdd::BDDFunction;

6

use oxidd::util::OptBool;

7

use oxidd::util::OutOfMemory;

8

9

use merc_lts::LTS;

10

use merc_lts::LabelledTransitionSystem;

11

use merc_lts::LtsBuilderFast;

12

use merc_lts::TransitionLabel;

13

use merc_symbolic::CubeIterAll;

14

use merc_symbolic::FormatConfigSet;

15

use merc_symbolic::bits_to_bdd;

16

use merc_utilities::MercError;

17

use merc_utilities::Timing;

18

19

use crate::FeatureDiagram;

20

use crate::FeatureTransitionSystem;

21

use crate::FeaturedLabel;

22

23

/// Projects all configurations of a featured transition system into standard labelled transition systems.

24

pub fn project_feature_transition_system_iter<'a, L: TransitionLabel>(

25

    fts: &'a FeatureTransitionSystem<L>,

26

    fd: &'a FeatureDiagram,

27

    timing: &'a Timing,

28

) -> impl Iterator<Item = Result<(ProjectedLts<FeaturedLabel<L>>, &'a Timing), MercError>> {

29

    let variables = fd

30

        .feature_names()

31

        .iter()

32

        .map(|name| {

33

            fd.features()

34

                .get(name)

35

                .expect("Feature diagram should contain all features defined in the feature names")

36

                .clone()

37

})

38

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

39

40

    CubeIterAll::new(fd.configuration()).map(move |cube| {

41

        let cube = cube?;

42

43

        let bdd = match bits_to_bdd(&fd.configuration().manager_ref(), &variables, &cube) {

44

            Ok(bdd) => bdd,

45

            Err(e) => return Err(MercError::from(e)),

46

};

47

48

        let lts = timing.measure("project", || -> Result<_, MercError> {

49

            project_feature_transition_system(fts, &bdd)

50

        })?;

51

52

        Ok((ProjectedLts { bits: cube, bdd, lts }, timing))

53

})

54

55

56

/// A projected configuration of a featured transition system.

57

pub struct ProjectedLts<L: TransitionLabel> {

58

    pub bits: Vec<OptBool>,

59

    pub bdd: BDDFunction,

60

    pub lts: LabelledTransitionSystem<L>,

61

62

63

/// Projects a featured transition system onto a specific feature selection, resulting in a standard labelled transition system.

64

pub fn project_feature_transition_system<L: TransitionLabel>(

65

    fts: &FeatureTransitionSystem<L>,

66

    feature_selection: &BDDFunction,

67

) -> Result<LabelledTransitionSystem<FeaturedLabel<L>>, MercError> {

68

    let mut builder = LtsBuilderFast::new(fts.labels().to_vec(), Vec::new());

69

70

    debug!("Projecting on feature selection {}", FormatConfigSet(feature_selection));

71

72

    let labels = fts

73

        .labels()

74

        .iter()

75

        .map(|label| -> Result<bool, OutOfMemory> {

76

            // Check if the edge is enabled by the feature selection, if so, include it.

77

            let result = feature_selection.and(label.feature_expr())?.satisfiable();

78

            debug!("Label {} is included: {}", label, result);

79

80

            Ok(result)

81

})

82

        .collect::<Result<Vec<_>, _>>()?;

83

84

    for v in fts.iter_states() {

85

        for edge in fts.outgoing_transitions(v) {

86

            if labels[edge.label] {

87

                builder.add_transition(v, &fts.labels()[edge.label], edge.to)?;

88

89

90

91

92

    Ok(builder.finish(fts.initial_state_index(), false))

93