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::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

115

3002

        let vertex = VertexIndex::new(index);

116

3002

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

117

118

3002

        for successors in parts {

119

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

120

4409

            for successor in successors

121

3002

                .trim_end_matches(';')

122

3002

                .split(',')

123

4409

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

124

125

4409

                let parts: Vec<&str> = successor.trim().split('|').collect();

126

4409

                let successor_index: usize = parts[0].trim().parse()?;

127

4409

                let successor = VertexIndex::new(successor_index);

128

129

4409

                let edge_configuration = if parts.len() > 1 {

130

4409

                    parse_configuration_set(manager, &variables, parts[1].trim())?

131

                } else {

132

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

133

                    manager.with_manager_shared(|m| BDDFunction::t(m))

134

};

135

136

4409

                builder.add_edge(vertex, edge_configuration, successor);

137

138

139

140

3002

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

141

3002

        vertex_count += 1;

142

143

144

1

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

145

1

146

147

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

148

/// based on the length of the configurations.

149

1

fn parse_configuration(

150

1

    manager_ref: &BDDManagerRef,

151

1

    config: &str,

152

1

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

153

    // Check for existing variables

154

1

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

155

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

156

1

157

158

1

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

159

1

        let variables = manager_ref.with_manager_exclusive(|manager| {

160

1

            manager

161

1

                .add_vars(first_part.len() as u32)

162

10

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

163

1

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

164

1

        })?;

165

166

1

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

167

1

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

168

};

169

170

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

171

1

172

173

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

174

///

175

/// # Details

176

///

177

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

178

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

179

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

180

/// function over 4 variables.

181

///

182

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

183

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

184

4410

pub fn parse_configuration_set(

185

4410

    manager_ref: &BDDManagerRef,

186

4410

    variables: &[BDDFunction],

187

4410

    config: &str,

188

4410

) -> Result<BDDFunction, MercError> {

189

4410

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

190

4410

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

191

192

4418

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

193

4418

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

194

195

44180

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

196

44180

                let var = &variables[i];

197

44180

                match c {

198

474

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

199

207

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

200

43499

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

201

                    _ => {

202

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

203

                            "Invalid character in configuration",

204

                        )));

205

206

207

208

209

4418

            result = result.or(&conjunction)?;

210

211

212

4410

        Ok(result)

213

4410

})

214

4410

215

216

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

217

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

218

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

219

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

220

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

221

222

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

223

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

224

225

    let progress = TimeProgress::new(

226

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

227

1,

228

);

229

    for v in game.iter_vertices() {

230

        let prio = game.priority(v);

231

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

232

233

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

234

        write!(

235

            writer,

236

            "{}",

237

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

238

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

239

})

240

)?;

241

242

        writeln!(writer, ";")?;

243

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

244

245

246

    Ok(())

247

248

249

#[cfg(test)]

250

mod tests {

251

    use super::*;

252

253

    #[test]

254

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

255

1

    fn test_read_vpg() {

256

1

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

257

258

1

        let parity_game = read_vpg(

259

1

            &manager,

260

1

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

261

262

1

        .unwrap();

263

264

1

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

265

1

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

266

1

267