Grcov report - project

1

use log::debug;

2

use oxidd::bdd::BDDFunction;

3

use oxidd::BooleanFunction;

4

use oxidd::Function;

5

use oxidd::util::OptBool;

6

use oxidd::util::OutOfMemory;

7

8

use merc_lts::LabelledTransitionSystem;

9

use merc_lts::LTS;

10

use merc_lts::LtsBuilderFast;

11

use merc_lts::TransitionLabel;

12

use merc_symbolic::bits_to_bdd;

13

use merc_symbolic::CubeIterAll;

14

use merc_symbolic::FormatConfigSet;

15

use merc_utilities::MercError;

16

use merc_utilities::Timing;

17

18

use crate::FeatureDiagram;

19

use crate::FeatureTransitionSystem;

20

use crate::FeaturedLabel;

21

22

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

23

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

24

    fts: &'a FeatureTransitionSystem<L>,

25

    fd: &'a FeatureDiagram,

26

    timing: &'a Timing,

27

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

28

    let variables = fd.feature_names().iter().map(|name| {

29

        fd.features()

30

            .get(name)

31

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

32

            .clone()

33

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

34

35

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

36

        let cube = cube?;

37

38

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

39

            Ok(bdd) => bdd,

40

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

41

};

42

43

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

44

            project_feature_transition_system(fts, &bdd)

45

        })?;

46

47

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

48

})

49

50

51

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

52

pub struct ProjectedLts<L: TransitionLabel> {

53

    pub bits: Vec<OptBool>,

54

    pub bdd: BDDFunction,

55

    pub lts: LabelledTransitionSystem<L>,

56

57

58

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

59

pub fn project_feature_transition_system<L: TransitionLabel>(

60

    fts: &FeatureTransitionSystem<L>,

61

    feature_selection: &BDDFunction,

62

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

63

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

64

65

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

66

67

    let labels = fts

68

        .labels()

69

        .iter()

70

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

71

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

72

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

73

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

74

75

            Ok(result)

76

})

77

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

78

79

    for v in fts.iter_states() {

80

        for edge in fts.outgoing_transitions(v) {

81

            if labels[edge.label] {

82

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

83

84

85

86

87

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

88