Grcov report - variability_make

1

use merc_utilities::MercError;

2

use oxidd::BooleanFunction;

3

use oxidd::ManagerRef;

4

use oxidd::bdd::BDDFunction;

5

use oxidd::bdd::BDDManagerRef;

6

7

use merc_symbolic::minus;

8

9

use crate::PG;

10

use crate::Player;

11

use crate::Priority;

12

use crate::VariabilityParityGame;

13

use crate::VariabilityParityGameBuilder;

14

use crate::VertexIndex;

15

16

/// Makes the given variability parity game total by adding edges to true/false nodes as needed.

17

301

pub fn make_vpg_total(

18

301

    manager_ref: &BDDManagerRef,

19

301

    vpg: &VariabilityParityGame,

20

301

) -> Result<VariabilityParityGame, MercError> {

21

    // The universe for totality is the game's overall configuration, not global true.

22

301

    let universe = manager_ref.with_manager_shared(|manager| BDDFunction::t(manager));

23

24

301

    let mut builder = VariabilityParityGameBuilder::with_capacity(

25

301

        vpg.initial_vertex(),

26

301

        vpg.num_of_edges() + vpg.num_of_vertices() + 2,

27

);

28

29

5023

    for vertex in vpg.iter_vertices() {

30

5023

        builder.add_vertex(vertex, vpg.owner(vertex), vpg.priority(vertex));

31

5023

32

33

    // Owner does not matter, priority must be even for true node and odd for false node.

34

301

    let mut true_node = None;

35

301

    let mut false_node = None;

36

37

5023

    for vertex in vpg.iter_vertices() {

38

5023

        let mut all_outgoing = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

39

6612

        for edge in vpg.outgoing_edges(vertex) {

40

            // Add the original edge.

41

6612

            builder.add_edge(vertex, edge.label().clone(), edge.to());

42

43

            // Keep track of the overall outgoing configuration.

44

6612

            all_outgoing = all_outgoing.or(edge.label())?;

45

46

47

        // Missing configurations are those in the universe not covered by any outgoing edge.

48

5023

        let missing = minus(&universe, &all_outgoing)?;

49

5023

        if missing.satisfiable() {

50

4882

            if vpg.owner(vertex) == Player::Odd {

51

                // Odd player deadlock: add edge to true node for the remaining configurations.

52

2411

                let node = if let Some(node) = true_node {

53

2110

                    node

54

                } else {

55

301

                    let node = VertexIndex::new(builder.num_of_vertices());

56

301

                    builder.add_vertex(node, Player::Even, Priority::new(0));

57

301

                    true_node = Some(node);

58

301

                    node

59

};

60

2411

                builder.add_edge(vertex, universe.clone(), node);

61

            } else {

62

                // Even player deadlock: add edge to false node for the remaining configurations.

63

2471

                let node = if let Some(node) = false_node {

64

2171

                    node

65

                } else {

66

300

                    let node = VertexIndex::new(builder.num_of_vertices());

67

300

                    builder.add_vertex(node, Player::Even, Priority::new(1));

68

300

                    false_node = Some(node);

69

300

                    node

70

};

71

2471

                builder.add_edge(vertex, universe.clone(), node);

72

73

141

74

75

76

    // Add self-loops for sink nodes if they were created

77

301

    if let Some(node) = true_node {

78

301

        builder.add_edge(node, universe.clone(), node);

79

301

80

301

    if let Some(node) = false_node {

81

300

        builder.add_edge(node, universe.clone(), node);

82

300

83

84

301

    Ok(builder.finish(

85

301

        manager_ref,

86

301

        vpg.configuration().clone(),

87

301

        vpg.variables().clone(),

88

301

        false,

89

301

))

90

301