Grcov report - feature_transition

1

//! Authors: Maurice Laveaux and Sjef van Loo

2

3

use std::collections::HashMap;

4

use std::fmt;

5

use std::io::BufRead;

6

use std::io::BufReader;

7

use std::io::Read;

8

9

use log::debug;

10

use merc_lts::LabelIndex;

11

use merc_lts::StateIndex;

12

use merc_lts::Transition;

13

use oxidd::BooleanFunction;

14

use oxidd::Manager;

15

use oxidd::ManagerRef;

16

use oxidd::bdd::BDDFunction;

17

use oxidd::bdd::BDDManagerRef;

18

19

use merc_lts::LTS;

20

use merc_lts::LabelledTransitionSystem;

21

use merc_lts::read_aut;

22

use merc_syntax::DataExpr;

23

use merc_syntax::MultiAction;

24

use merc_utilities::MercError;

25

26

/// Reads a .aut file as feature transition system by using the associated

27

/// feature diagram.

28

///

29

/// # Details

30

///

31

/// The action labels of a feature transition system are annotated with a

32

/// special `BDD` struct that is defined as `struct BDD = node(var, true, false)

33

/// | tt | ff`. The `features` map contains the mapping from variable names to

34

/// their corresponding BDD variable, which *must* be defined in the BDD

35

/// manager.

36

2

pub fn read_fts(

37

2

    manager_ref: &BDDManagerRef,

38

2

    reader: impl Read,

39

2

    features: HashMap<String, BDDFunction>,

40

2

) -> Result<FeatureTransitionSystem, MercError> {

41

    // Read the underlying LTS, where the labels are in plain text

42

2

    let aut = read_aut(reader, Vec::new())?;

43

44

    // Parse the labels as data expressions

45

2

    let mut feature_labels = Vec::new();

46

55

    for label in aut.labels() {

47

55

        let action = MultiAction::parse(label)?;

48

49

55

        debug!("Parsed action: {}", action);

50

55

        if action.actions.len() > 1 {

51

            return Err(MercError::from(format!(

52

                "Cannot read feature transition system: action \"{}\" has multiple actions",

53

                label

54

            )));

55

56

57

55

        if let Some(action) = action.actions.first() {

58

55

            if let Some(arg) = action.args.first() {

59

44

                feature_labels.push(data_expr_to_bdd(manager_ref, &features, arg)?);

60

            } else {

61

11

                feature_labels.push(manager_ref.with_manager_shared(|manager| BDDFunction::t(manager)));

62

63

        } else {

64

            // This is the tau action, is always enabled.

65

            feature_labels.push(manager_ref.with_manager_shared(|manager| BDDFunction::t(manager)));

66

67

68

69

2

    Ok(FeatureTransitionSystem::new(aut, feature_labels, features))

70

2

71

72

/// Converts the given data expression into a BDD function.

73

///

74

/// The input should be a data expression of the shape: expr = node(var, expr, expr) | tt | ff.

75

186

fn data_expr_to_bdd(

76

186

    manager_ref: &BDDManagerRef,

77

186

    variables: &HashMap<String, BDDFunction>,

78

186

    expr: &DataExpr,

79

186

) -> Result<BDDFunction, MercError> {

80

186

    match expr {

81

70

        DataExpr::Application { function, arguments } => {

82

70

            match function.as_ref() {

83

                // A node must be of the shape 'node(var, true_branch, false_branch)'

84

70

                DataExpr::Id(name) => {

85

70

                    if name == "node" {

86

70

                        let variable = format!("{}", arguments[0]);

87

70

                        let then_branch = data_expr_to_bdd(manager_ref, variables, &arguments[1])?;

88

70

                        let else_branch = data_expr_to_bdd(manager_ref, variables, &arguments[2])?;

89

70

                        Ok(variables

90

70

                            .get(&variable)

91

70

                            .ok_or(format!("Variable \"{}\" not found in feature diagram", variable))?

92

70

                            .ite(&then_branch, &else_branch)?)

93

                    } else {

94

                        unimplemented!("Conversion of data expression to BDD not implemented for this function");

95

96

97

                _ => unimplemented!("Conversion of data expression to BDD not implemented for this function"),

98

99

100

116

        DataExpr::Id(name) => {

101

            // Deal with the base cases.

102

116

            match name.as_str() {

103

116

                "tt" => Ok(manager_ref.with_manager_shared(|manager| BDDFunction::t(manager))),

104

62

                "ff" => Ok(manager_ref.with_manager_shared(|manager| BDDFunction::f(manager))),

105

                _ => unimplemented!("Cannot convert data expression \"{expr}\" to BDD"),

106

107

108

        _ => unimplemented!("Cannot convert data expression \"{expr}\" to BDD"),

109

110

186

111

112

pub struct FeatureDiagram {

113

    /// The mapping from variable names to their BDD variable.

114

    features: HashMap<String, BDDFunction>,

115

116

    /// Stores the set of products as a BDD function.

117

    configuration: BDDFunction,

118

119

120

impl FeatureDiagram {

121

    /// Reads feature diagram from the input.

122

///

123

    /// # Details

124

///

125

    /// The first line is a list of variable names, separated by commas. The

126

    /// second line is the initial configuration, represented as a data

127

    /// expression. This function will initialize the BDD manager with the

128

    /// variables read from the first line, and assumes that the manager has no

129

    /// variables yet defined.

130

2

    pub fn from_reader(manager_ref: &BDDManagerRef, input: impl Read) -> Result<Self, MercError> {

131

2

        manager_ref.with_manager_exclusive(|manager| {

132

2

            debug_assert_eq!(

133

2

                manager.num_vars(),

134

0,

135

                "A BDD manager can only hold the variables for a single feature diagram"

136

137

2

});

138

139

2

        let input = BufReader::new(input);

140

2

        let mut line_iter = input.lines();

141

2

        let first_line = line_iter.next().ok_or("Expected variable names line")??;

142

143

12

        let variable_names: Vec<String> = first_line.split(',').map(|s| s.trim().to_string()).collect();

144

2

        let variables = manager_ref.with_manager_exclusive(|manager| -> Result<Vec<BDDFunction>, MercError> {

145

2

            Ok(manager

146

2

                .add_named_vars(variable_names.iter())

147

2

                .map_err(|e| format!("Failed to create variables: {e}"))?

148

12

                .map(|i| BDDFunction::var(manager, i))

149

2

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

150

2

        })?;

151

152

2

        let variables = HashMap::from_iter(variable_names.into_iter().zip(variables));

153

154

2

        let second_line = line_iter.next().ok_or("Expected initial configuration line")??;

155

2

        let initial_configuration = data_expr_to_bdd(manager_ref, &variables, &DataExpr::parse(&second_line)?)?;

156

157

2

        Ok(Self {

158

2

            features: variables,

159

2

            configuration: initial_configuration,

160

2

})

161

2

162

163

    /// Returns the configuration of the feature diagram.

164

1

    pub fn configuration(&self) -> &BDDFunction {

165

1

        &self.configuration

166

1

167

168

    /// Returns the feature variables used in the feature diagram.

169

1

    pub fn features(&self) -> &HashMap<String, BDDFunction> {

170

1

        &self.features

171

1

172

173

174

impl fmt::Debug for FeatureDiagram {

175

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

176

        write!(f, "variables = {:?}", self.features.keys())

177

178

179

180

/// A feature transition system, i.e., a labelled transition system

181

/// where each label is associated with a feature expression.

182

pub struct FeatureTransitionSystem {

183

    /// The underlying labelled transition system.

184

    lts: LabelledTransitionSystem<String>,

185

186

    /// The feature expression associated with each label.

187

    feature_labels: Vec<BDDFunction>,

188

189

    /// The features associated with this feature transition system.

190

    features: HashMap<String, BDDFunction>,

191

192

193

impl FeatureTransitionSystem {

194

    /// Creates a new feature transition system.

195

2

    pub fn new(

196

2

        lts: LabelledTransitionSystem<String>,

197

2

        feature_labels: Vec<BDDFunction>,

198

2

        features: HashMap<String, BDDFunction>,

199

2

    ) -> Self {

200

2

        Self {

201

2

            lts,

202

2

            feature_labels,

203

2

            features,

204

2

205

2

206

207

    /// Returns the feature label BDD for the given label index.

208

4

    pub fn feature_label(&self, label_index: LabelIndex) -> &BDDFunction {

209

4

        &self.feature_labels[label_index]

210

4

211

212

    /// Returns the features used in the feature diagram.

213

1

    pub fn features(&self) -> &HashMap<String, BDDFunction> {

214

1

        &self.features

215

1

216

217

218

impl LTS for FeatureTransitionSystem {

219

    type Label = String;

220

221

    fn merge_disjoint<L>(self, _other: &L) -> (LabelledTransitionSystem<String>, StateIndex) {

222

        unimplemented!("Merging feature transition systems is not yet implemented")

223

224

225

    delegate::delegate! {

226

        to self.lts {

227

1

            fn initial_state_index(&self) -> StateIndex;

228

            fn num_of_states(&self) -> usize;

229

            fn num_of_labels(&self) -> usize;

230

            fn num_of_transitions(&self) -> usize;

231

            fn is_hidden_label(&self, label_index: LabelIndex) -> bool;

232

1

            fn labels(&self) -> &[String];

233

9

            fn outgoing_transitions(&self, state_index: StateIndex) -> impl Iterator<Item = Transition>;

234

            fn iter_states(&self) -> impl Iterator<Item = StateIndex> + '_;

235

236

237

238

239

#[cfg(test)]

240

mod tests {

241

    use merc_macros::merc_test;

242

243

    use super::*;

244

245

    #[merc_test]

246

    #[cfg_attr(miri, ignore)] // Oxidd does not support miri (specifically the crossbeam-epoch dependency)

247

    fn test_read_minepump_fts() {

248

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

249

250

        let feature_diagram = FeatureDiagram::from_reader(

251

            &manager_ref,

252

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

253

254

        .unwrap();

255

256

        let _result = read_fts(

257

            &manager_ref,

258

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

259

            feature_diagram.features,

260

261

        .unwrap();

262

263