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 feature diagram.

27

///

28

/// # Details

29

///

30

/// The action labels of a feature transition system are annotated with a special `BDD` struct that is defined as `struct BDD = node(var, true, false) | tt | ff`.

31

2

pub fn read_fts(

32

2

    manager_ref: &BDDManagerRef,

33

2

    reader: impl Read,

34

2

    features: HashMap<String, BDDFunction>,

35

2

) -> Result<FeatureTransitionSystem, MercError> {

36

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

37

2

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

38

39

    // Parse the labels as data expressions

40

2

    let mut feature_labels = Vec::new();

41

55

    for label in aut.labels() {

42

55

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

43

44

55

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

45

55

        if action.actions.len() > 1 {

46

            return Err(MercError::from(format!(

47

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

48

                label

49

            )));

50

55

51

52

55

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

53

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

54

44

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

55

            } else {

56

9

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

57

58

        } else {

59

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

60

2

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

61

62

63

64

2

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

65

2

66

67

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

68

///

69

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

70

186

fn data_expr_to_bdd(

71

186

    manager_ref: &BDDManagerRef,

72

186

    variables: &HashMap<String, BDDFunction>,

73

186

    expr: &DataExpr,

74

186

) -> Result<BDDFunction, MercError> {

75

186

    match expr {

76

70

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

77

70

            match function.as_ref() {

78

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

79

70

                DataExpr::Id(name) => {

80

70

                    if name == "node" {

81

70

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

82

70

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

83

70

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

84

70

                        Ok(variables

85

70

                            .get(&variable)

86

70

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

87

70

                            .ite(&then_branch, &else_branch)?)

88

                    } else {

89

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

90

91

92

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

93

94

95

116

        DataExpr::Id(name) => {

96

            // Deal with the base cases.

97

116

            match name.as_str() {

98

116

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

99

62

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

100

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

101

102

103

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

104

105

186

106

107

pub struct FeatureDiagram {

108

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

109

    features: HashMap<String, BDDFunction>,

110

111

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

112

    configuration: BDDFunction,

113

114

115

impl FeatureDiagram {

116

    /// Reads feature diagram from the input.

117

///

118

    /// # Details

119

///

120

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

121

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

122

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

123

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

124

    /// variables yet defined.

125

2

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

126

2

        manager_ref.with_manager_exclusive(|manager| {

127

2

            debug_assert_eq!(

128

2

                manager.num_vars(),

129

0,

130

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

131

132

2

});

133

134

2

        let input = BufReader::new(input);

135

2

        let mut line_iter = input.lines();

136

2

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

137

138

12

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

139

2

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

140

2

            Ok(manager

141

2

                .add_named_vars(variable_names.iter())

142

2

                .map_err(|e| format!("{}", e))?

143

12

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

144

2

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

145

2

        })?;

146

147

2

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

148

149

2

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

150

2

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

151

152

2

        Ok(Self {

153

2

            features: variables,

154

2

            configuration: initial_configuration,

155

2

})

156

2

157

158

    /// Returns the configuration of the feature diagram.

159

1

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

160

1

        &self.configuration

161

1

162

163

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

164

1

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

165

1

        &self.features

166

1

167

168

169

impl fmt::Debug for FeatureDiagram {

170

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

171

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

172

173

174

175

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

176

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

177

pub struct FeatureTransitionSystem {

178

    /// The underlying labelled transition system.

179

    lts: LabelledTransitionSystem<String>,

180

181

    /// The feature expression associated with each label.

182

    feature_labels: Vec<BDDFunction>,

183

184

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

185

    features: HashMap<String, BDDFunction>,

186

187

188

impl FeatureTransitionSystem {

189

    /// Creates a new feature transition system.

190

2

    pub fn new(

191

2

        lts: LabelledTransitionSystem<String>,

192

2

        feature_labels: Vec<BDDFunction>,

193

2

        features: HashMap<String, BDDFunction>,

194

2

    ) -> Self {

195

2

        Self {

196

2

            lts,

197

2

            feature_labels,

198

2

            features,

199

2

200

2

201

202

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

203

4

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

204

4

        &self.feature_labels[label_index]

205

4

206

207

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

208

1

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

209

1

        &self.features

210

1

211

212

213

impl LTS for FeatureTransitionSystem {

214

    type Label = String;

215

216

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

217

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

218

219

220

    delegate::delegate! {

221

        to self.lts {

222

1

            fn initial_state_index(&self) -> StateIndex;

223

            fn num_of_states(&self) -> usize;

224

            fn num_of_labels(&self) -> usize;

225

            fn num_of_transitions(&self) -> usize;

226

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

227

1

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

228

9

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

229

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

230

231

232

233

234

#[cfg(test)]

235

mod tests {

236

    use merc_macros::merc_test;

237

238

    use super::*;

239

240

    #[merc_test]

241

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

242

    fn test_read_minepump_fts() {

243

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

244

245

        let feature_diagram = FeatureDiagram::from_reader(

246

            &manager_ref,

247

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

248

249

        .unwrap();

250

251

        let _result = read_fts(

252

            &manager_ref,

253

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

254

            feature_diagram.features,

255

256

        .unwrap();

257

258