Grcov report - variability_parity

1

//! Authors: Maurice Laveaux and Sjef van Loo

2

3

use std::fmt;

4

5

use delegate::delegate;

6

use oxidd::BooleanFunction;

7

use oxidd::ManagerRef;

8

use oxidd::bdd::BDDFunction;

9

use oxidd::bdd::BDDManagerRef;

10

11

use merc_symbolic::FormatConfigSet;

12

use merc_symbolic::minus;

13

use merc_utilities::MercError;

14

15

use crate::PG;

16

use crate::ParityGame;

17

use crate::Player;

18

use crate::Priority;

19

use crate::VertexIndex;

20

21

/// A variability parity game is an extension of a parity game where each edge is

22

/// associated with a BDD function representing the configurations in which the

23

/// edge is enabled.

24

///

25

/// # Details

26

///

27

/// This is also a max-priority parity game. There is also a configuration set associated

28

/// with the variability parity game, representing the overall configurations.

29

pub struct VariabilityParityGame {

30

    /// The underlying normal parity game.

31

    game: ParityGame,

32

33

    /// The overall configurations for the variability parity game.

34

    configuration: BDDFunction,

35

36

    /// The variables used in the configuration BDD.

37

    variables: Vec<BDDFunction>,

38

39

    /// Every edge has an associated BDD function representing the configurations

40

    /// in which the edge is enabled.

41

    edges_configuration: Vec<BDDFunction>,

42

43

44

/// Represents an edge in the parity game along with its configuration BDD.

45

pub struct Edge<'a> {

46

    to: VertexIndex,

47

    configuration: &'a BDDFunction,

48

49

50

impl<'a> Edge<'a> {

51

    /// Returns the target vertex of the edge.

52

120740

    pub fn to(&self) -> VertexIndex {

53

120740

        self.to

54

120740

55

56

    /// Returns the configuration BDD associated with the edge.

57

103395

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

58

103395

        self.configuration

59

103395

60

61

62

impl VariabilityParityGame {

63

    /// Construct a new variability parity game from an iterator over edges.

64

301

    pub fn new(

65

301

        parity_game: ParityGame,

66

301

        configuration: BDDFunction,

67

301

        variables: Vec<BDDFunction>,

68

301

        edges_configuration: Vec<BDDFunction>,

69

301

    ) -> Self {

70

        // Check that the sizes are consistent

71

301

        debug_assert_eq!(

72

301

            edges_configuration.len(),

73

301

            parity_game.num_of_edges(),

74

            "There should be a configuration BDD for every edge"

75

);

76

77

301

        Self {

78

301

            game: parity_game,

79

301

            configuration,

80

301

            variables,

81

301

            edges_configuration,

82

301

83

301

84

85

    /// Constructs a new variability parity game from an iterator over edges.

86

///

87

    /// The vertices are given by their owner and priority.

88

    /// The `edges` iterator should yield tuples of the form (from, configuration, to).

89

202

    pub fn from_edges<F, I>(

90

202

        manager_ref: &BDDManagerRef,

91

202

        initial_vertex: VertexIndex,

92

202

        owner: Vec<Player>,

93

202

        priority: Vec<Priority>,

94

202

        configuration: BDDFunction,

95

202

        variables: Vec<BDDFunction>,

96

202

        mut edges: F,

97

202

    ) -> Self

98

202

    where

99

202

        F: FnMut() -> I,

100

202

        I: Iterator<Item = (VertexIndex, BDDFunction, VertexIndex)>,

101

102

202

        let num_of_vertices = owner.len();

103

202

        debug_assert_eq!(

104

202

            priority.len(),

105

            num_of_vertices,

106

            "Owner and priority vectors should have the same length"

107

);

108

109

202

        let mut vertices = Vec::new();

110

202

        vertices.resize_with(num_of_vertices, Default::default);

111

202

        debug_assert!(

112

202

            initial_vertex.value() < num_of_vertices,

113

            "Initial vertex index {} out of bounds {num_of_vertices}",

114

            initial_vertex.value()

115

);

116

117

        // Count the number of transitions for every state

118

202

        let mut num_of_edges = 0;

119

6422

        for (from, _, to) in edges() {

120

            // Ensure that the states vector is large enough.

121

6422

            if vertices.len() <= *from.max(to) {

122

                vertices.resize_with(*from.max(to) + 1, || 0);

123

6422

124

125

6422

            vertices[*from] += 1;

126

6422

            num_of_edges += 1;

127

128

6422

            debug_assert!(

129

6422

                *from < num_of_vertices && *to < num_of_vertices,

130

                "Vertex index out of bounds: from {:?}, to {:?}, num_of_vertices {}",

131

                from,

132

to,

133

                num_of_vertices

134

);

135

136

137

202

        if initial_vertex.value() >= vertices.len() {

138

            // Ensure that the initial state is a valid state (and all states before it exist).

139

            vertices.resize_with(initial_vertex.value() + 1, Default::default);

140

202

141

142

        // Sets the offset for every state into the edge arrays.

143

4448

        vertices.iter_mut().fold(0, |count, start| {

144

4448

            let result = count + *start;

145

4448

            *start = count;

146

4448

            result

147

4448

});

148

149

        // Place the transitions, and increment the end for every state.

150

202

        let mut edges_to = vec![VertexIndex::new(0); num_of_edges];

151

202

        let mut edges_configuration =

152

202

            manager_ref.with_manager_shared(|manager| vec![BDDFunction::f(manager); num_of_edges]);

153

6422

        for (from, config, to) in edges() {

154

6422

            let start = &mut vertices[*from];

155

6422

            edges_to[*start] = to;

156

6422

            edges_configuration[*start] = config;

157

6422

            *start += 1;

158

6422

159

160

        // Reset the offset to the start.

161

4448

        vertices.iter_mut().fold(0, |previous, start| {

162

4448

            let result = *start;

163

4448

            *start = previous;

164

4448

            result

165

4448

});

166

167

202

        vertices.push(num_of_edges); // Sentinel vertex

168

169

202

        Self {

170

202

            game: ParityGame::new(initial_vertex, owner, priority, vertices, edges_to),

171

202

            configuration,

172

202

            variables,

173

202

            edges_configuration,

174

202

175

202

176

177

    /// Returns an iterator over the outgoing edges of the given vertex.

178

56920

    pub fn outgoing_conf_edges(&self, state_index: VertexIndex) -> impl Iterator<Item = Edge<'_>> + '_ {

179

56920

        let start = self.game.vertices()[*state_index];

180

56920

        let end = self.game.vertices()[*state_index + 1];

181

56920

        self.edges_configuration[start..end]

182

56920

            .iter()

183

56920

            .zip(self.game.edges_to()[start..end].iter())

184

83289

            .map(|(configuration, &to)| Edge { to, configuration })

185

56920

186

187

    /// Returns true iff the parity game is total, checks all vertices have at least one outgoing edge.

188

301

    pub fn is_total(&self, manager_ref: &BDDManagerRef) -> Result<bool, MercError> {

189

        // Check that every vertex has at least one outgoing edge.

190

6607

        for v in self.iter_vertices() {

191

6607

            if self.outgoing_edges(v).next().is_none() {

192

1

                return Ok(false);

193

6606

194

195

196

        // Check that the configurations of the outgoing edges cover the overall configuration.

197

6600

        for v in self.iter_vertices() {

198

            // Compute the disjunction of all outgoing edge configurations.

199

6600

            let covered = self.outgoing_conf_edges(v).try_fold(

200

6600

                manager_ref.with_manager_shared(|manager| BooleanFunction::f(manager)),

201

9544

                |acc: BDDFunction, edge| acc.or(edge.configuration()),

202

)?;

203

204

            // If there are configurations not covered by the outgoing edges, the game is not total.

205

6600

            if minus(&self.configuration, &covered)?.satisfiable() {

206

                return Ok(false);

207

6600

208

209

210

300

        Ok(true)

211

301

212

213

    /// Returns the overall configuration BDD of the variability parity game.

214

25921

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

215

25921

        &self.configuration

216

25921

217

218

    /// Returns the variables used in the configuration BDD.

219

946

    pub fn variables(&self) -> &Vec<BDDFunction> {

220

946

        &self.variables

221

946

222

223

    /// Returns the owners of the vertices in the variability parity game.

224

946

    pub(crate) fn owners(&self) -> &Vec<Player> {

225

946

        self.game.owners()

226

946

227

228

    /// Returns the priorities of the vertices in the variability parity game.

229

946

    pub(crate) fn priorities(&self) -> &Vec<Priority> {

230

946

        self.game.priorities()

231

946

232

233

234

impl PG for VariabilityParityGame {

235

    delegate! {

236

        to self.game {

237

947

            fn initial_vertex(&self) -> VertexIndex;

238

4520

            fn num_of_vertices(&self) -> usize;

239

601

            fn num_of_edges(&self) -> usize;

240

3192

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

241

25111

            fn owner(&self, vertex: VertexIndex) -> Player;

242

29369

            fn priority(&self, vertex: VertexIndex) -> Priority;

243

6630

            fn outgoing_edges(&self, state_index: VertexIndex) -> impl Iterator<Item = VertexIndex> + '_;

244

            fn is_total(&self) -> bool;

245

            fn highest_priority(&self) -> Priority;

246

247

248

249

250

impl fmt::Display for VariabilityParityGame {

251

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

252

        writeln!(f, "Variability Parity Game:")?;

253

        writeln!(f, "Configuration BDD: {}", FormatConfigSet(self.configuration()))?;

254

255

        for v in self.iter_vertices() {

256

            write!(

257

f,

258

                "v{}: {:?}, priority={}, edges=[",

259

v,

260

                self.owner(v).to_index(),

261

                self.priority(v)

262

)?;

263

264

            let mut first = true;

265

            for edge in self.outgoing_conf_edges(v) {

266

                if !first {

267

                    write!(f, ", ")?;

268

269

                write!(f, "(v{}, {})", edge.to(), FormatConfigSet(edge.configuration()))?;

270

                first = false;

271

272

273

            writeln!(f, "]")?;

274

275

276

        Ok(())

277

278