Grcov report - io

1

//! Authors: Maurice Laveaux and Sjef van Loo

2

3

use std::io::BufWriter;

4

use std::io::Read;

5

use std::io::Write;

6

7

use itertools::Itertools;

8

use log::info;

9

use oxidd::BooleanFunction;

10

use oxidd::Manager;

11

use oxidd::ManagerRef;

12

use oxidd::bdd::BDDFunction;

13

use oxidd::bdd::BDDManagerRef;

14

use regex::Regex;

15

use streaming_iterator::StreamingIterator;

16

17

use merc_io::LineIterator;

18

use merc_io::TimeProgress;

19

use merc_symbolic::FormatConfigSet;

20

use merc_symbolic::minus;

21

use merc_utilities::MercError;

22

23

use crate::IOError;

24

use crate::PG;

25

use crate::Player;

26

use crate::Priority;

27

use crate::VariabilityParityGame;

28

use crate::VariabilityParityGameBuilder;

29

use crate::VertexIndex;

30

31

/// Reads a variability parity game in an extended PGSolver `.vpg` format from the given reader.

32

/// Note that the reader is buffered internally using a `BufReader`.

33

///

34

/// # Details

35

///

36

/// The format starts with a header, followed by the vertices

37

///

38

/// parity <num_of_vertices>;

39

/// `<index> <priority> <owner> <outgoing_vertex>,<outgoing_vertex>,...;`

40

/// Each outgoing edge is represented as `<to>|<configuration_set>`. For the

41

/// format of the configuration set see [parse_configuration_set]

42

1

pub fn read_vpg<R: Read>(manager: &BDDManagerRef, reader: R) -> Result<VariabilityParityGame, MercError> {

43

1

    info!("Reading variability parity game in .vpg format...");

44

45

1

    manager.with_manager_exclusive(|manager| {

46

1

        debug_assert_eq!(

47

1

            manager.num_vars(),

48

0,

49

            "A BDD manager can only hold the variables for a single variability parity game"

50

51

1

});

52

53

1

    let mut lines = LineIterator::new(reader);

54

1

    lines.advance();

55

1

    let header = lines

56

1

        .get()

57

1

        .ok_or(IOError::InvalidHeader("The first line should be the confs header"))?;

58

59

    // Read the confs <configurations> line

60

1

    let confs_regex = Regex::new(r#"confs\s+([+-01]*)\s*;"#).expect("Regex compilation should not fail");

61

1

    let (_, [configurations_txt]) = confs_regex

62

1

        .captures(header)

63

1

        .ok_or(IOError::InvalidHeader("header does not match confs <configurations>;"))?

64

1

        .extract();

65

1

    let (variables, configurations) = parse_configuration(manager, configurations_txt)?;

66

67

    // Read the parity header

68

1

    let header_regex = Regex::new(r#"parity\s+([0-9]+)\s*;"#).expect("Regex compilation should not fail");

69

1

    let header = lines

70

1

        .next()

71

1

        .ok_or(IOError::InvalidHeader("The second line should be the parity header"))?;

72

73

1

    let (_, [num_of_vertices_txt]) = header_regex

74

1

        .captures(header)

75

1

        .ok_or(IOError::InvalidHeader(

76

1

            "header does not match parity <num_of_vertices>;",

77

1

))?

78

1

        .extract();

79

80

1

    let num_of_vertices: usize = num_of_vertices_txt.parse()?;

81

82

    // Collect the data in a builder and remove duplicate edges at the end.

83

1

    let mut builder = VariabilityParityGameBuilder::with_capacity(VertexIndex::new(0), num_of_vertices);

84

1

    if num_of_vertices > 0 {

85

1

        builder.add_vertex(VertexIndex::new(num_of_vertices - 1), Player::Even, Priority::new(0));

86

1

87

88

    // Print progress messages

89

1

    let progress = TimeProgress::new(

90

        |(amount, total): (usize, usize)| info!("Read {} vertices ({}%)...", amount, amount * 100 / total),

91

1,

92

);

93

1

    let mut vertex_count = 0;

94

3003

    while let Some(line) = lines.next() {

95

        // Parse the line: <index> <priority> <owner> <outgoing_vertex>, <outgoing_vertex>, ...;

96

3002

        let mut parts = line.split_whitespace();

97

98

3002

        let index: usize = parts

99

3002

            .next()

100

3002

            .ok_or(IOError::InvalidLine("Expected at least <index> ...;"))?

101

3002

            .parse()?;

102

3002

        let vertex_priority: usize = parts

103

3002

            .next()

104

3002

            .ok_or(IOError::InvalidLine("Expected at least <index> <priority> ...;"))?

105

3002

            .parse()?;

106

3002

        let vertex_owner = Player::try_from_index(

107

3002

            parts

108

3002

                .next()

109

3002

                .ok_or(IOError::InvalidLine(

110

3002

                    "Expected at least <index> <priority> <owner> ...;",

111

3002

))?

112

3002

                .parse()?,

113

114

3002

        .ok_or(IOError::InvalidLine("owner must be 0 (even) or 1 (odd)"))?;

115

116

3002

        let vertex = VertexIndex::new(index);

117

3002

        builder.add_vertex(vertex, vertex_owner, Priority::new(vertex_priority));

118

119

3002

        for successors in parts {

120

            // Parse successors (remaining parts, removing trailing semicolon)

121

4409

            for successor in successors

122

3002

                .trim_end_matches(';')

123

3002

                .split(',')

124

4409

                .filter(|s| !s.trim().is_empty())

125

126

                // Each successor is `<to>` or `<to>|<configuration_set>`.

127

4409

                let (index_part, configuration_part) = match successor.trim().split_once('|') {

128

4409

                    Some((index, configuration)) => (index, Some(configuration)),

129

                    None => (successor.trim(), None),

130

};

131

4409

                let successor = VertexIndex::new(index_part.trim().parse()?);

132

133

4409

                let edge_configuration = match configuration_part {

134

4409

                    Some(configuration) => parse_configuration_set(manager, &variables, configuration.trim())?,

135

                    // No configuration specified, use true (all configurations)

136

                    None => manager.with_manager_shared(|m| BDDFunction::t(m)),

137

};

138

139

4409

                builder.add_edge(vertex, edge_configuration, successor);

140

141

142

143

3002

        progress.print((vertex_count + 1, num_of_vertices));

144

3002

        vertex_count += 1;

145

146

147

1

    Ok(builder.finish(manager, configurations, variables, true))

148

1

149

150

/// Parses a configuration set from a string representation into a BDD function, but also creates the necessary variables.

151

/// based on the length of the configurations.

152

1

fn parse_configuration(

153

1

    manager_ref: &BDDManagerRef,

154

1

    config: &str,

155

1

) -> Result<(Vec<BDDFunction>, BDDFunction), MercError> {

156

    // Check for existing variables

157

1

    if manager_ref.with_manager_shared(|manager| manager.num_vars()) != 0 {

158

        return Err("BDD manager must not contain any variables yet".into());

159

1

160

161

1

    if let Some(first_part) = config.split('+').next() {

162

1

        let variables = manager_ref.with_manager_exclusive(|manager| {

163

1

            manager

164

1

                .add_vars(first_part.len() as u32)

165

10

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

166

1

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

167

1

        })?;

168

169

1

        let configuration = parse_configuration_set(manager_ref, &variables, config)?;

170

1

        return Ok((variables.to_vec(), configuration));

171

};

172

173

    Err(MercError::from(IOError::InvalidHeader("Empty configuration string")))

174

1

175

176

/// Parses a configuration from a string representation into a BDD function.

177

///

178

/// # Details

179

///

180

/// A configuration is represented as a string \<entry\>+\<entry\>+..., where each entry is either

181

/// a sequence consisting of '-', '0', and '1', representing don't care, false, and true respectively.

182

/// The length of the sequence determines the number of boolean variables. So `-1--` represents a boolean

183

/// function over 4 variables.

184

///

185

/// The variables must be defined beforehand and are assumed to be in order, i.e., the first character

186

/// corresponds to variable 0, the second to variable 1, and so on.

187

4410

pub fn parse_configuration_set(

188

4410

    manager_ref: &BDDManagerRef,

189

4410

    variables: &[BDDFunction],

190

4410

    config: &str,

191

4410

) -> Result<BDDFunction, MercError> {

192

4410

    manager_ref.with_manager_shared(|manager| -> Result<BDDFunction, MercError> {

193

4410

        let mut result = BDDFunction::f(manager);

194

195

4418

        for part in config.split('+') {

196

4418

            let mut conjunction = BDDFunction::t(manager);

197

198

44180

            for (i, c) in part.chars().enumerate() {

199

44180

                let var = variables.get(i).ok_or(IOError::InvalidLine(

200

44180

                    "configuration entry has more characters than there are variables",

201

44180

                ))?;

202

44180

                match c {

203

474

                    '1' => conjunction = conjunction.and(var)?,

204

207

                    '0' => conjunction = minus(&conjunction, var)?,

205

43499

                    '-' => {} // don't care

206

                    _ => {

207

                        return Err(MercError::from(IOError::InvalidHeader(

208

                            "Invalid character in configuration",

209

                        )));

210

211

212

213

214

4418

            result = result.or(&conjunction)?;

215

216

217

4410

        Ok(result)

218

4410

})

219

4410

220

221

/// Writes the given parity game to the given writer in .vpg format.

222

/// Note that the writer is buffered internally using a `BufWriter`.

223

pub fn write_vpg<W: Write>(writer: &mut W, game: &VariabilityParityGame) -> Result<(), MercError> {

224

    info!("Writing variability parity game to .vpg format...");

225

    let mut writer = BufWriter::new(writer);

226

227

    writeln!(writer, "confs {};", FormatConfigSet(game.configuration()))?;

228

    writeln!(writer, "parity {};", game.num_of_vertices())?;

229

230

    let progress = TimeProgress::new(

231

        |(index, total): (usize, usize)| info!("Wrote {} vertices ({}%)...", index, index * 100 / total),

232

1,

233

);

234

    for v in game.iter_vertices() {

235

        let prio = game.priority(v);

236

        let owner = game.owner(v).to_index();

237

238

        write!(writer, "{} {} {} ", v.value(), prio.value(), owner)?;

239

        write!(

240

            writer,

241

            "{}",

242

            game.outgoing_edges(v).format_with(",", |edge, fmt| {

243

                fmt(&format_args!("{}|{}", edge.to(), FormatConfigSet(edge.label())))

244

})

245

)?;

246

247

        writeln!(writer, ";")?;

248

        progress.print((v.value() + 1, game.num_of_vertices()));

249

250

251

    Ok(())

252

253

254

#[cfg(test)]

255

mod tests {

256

    use super::PG;

257

    use super::read_vpg;

258

259

    #[test]

260

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

261

1

    fn test_read_vpg() {

262

1

        let manager = oxidd::bdd::new_manager(2048, 1024, 8);

263

264

1

        let parity_game = read_vpg(

265

1

            &manager,

266

1

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

267

268

1

        .unwrap();

269

270

1

        assert_eq!(parity_game.num_of_vertices(), 3002);

271

1

        assert_eq!(parity_game.num_of_edges(), 4408);

272

1

273