Grcov report - 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 crate::PG;

8

use crate::Player;

9

use crate::Priority;

10

use crate::VariabilityParityGame;

11

use crate::VertexIndex;

12

use crate::variability_zielonka::minus;

13

14

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

15

201

pub fn make_vpg_total(

16

201

    manager_ref: &BDDManagerRef,

17

201

    vpg: &VariabilityParityGame,

18

201

) -> Result<VariabilityParityGame, MercError> {

19

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

20

201

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

21

22

    // For a total game we need to potentially add new edges to true/false nodes.

23

201

    let mut edges = Vec::new();

24

25

    // Add the true and false nodes.

26

201

    let mut owners = vpg.owners().clone();

27

201

    let mut priorities = vpg.priorities().clone();

28

29

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

30

201

    let true_node = VertexIndex::new(owners.len());

31

201

    owners.push(Player::Even);

32

201

    priorities.push(Priority::new(0)); // Even priority for true node

33

34

201

    let false_node = VertexIndex::new(owners.len());

35

201

    owners.push(Player::Even);

36

201

    priorities.push(Priority::new(1)); // Odd priority for false node

37

38

201

    edges.push((true_node, universe.clone(), true_node)); // Self-loop on true node

39

201

    edges.push((false_node, universe.clone(), false_node)); // Self-loop on false node

40

41

4023

    for vertex in vpg.iter_vertices() {

42

4023

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

43

5405

        for edge in vpg.outgoing_conf_edges(vertex) {

44

            // Add a new edge with a random configuration.

45

5405

            edges.push((vertex, edge.configuration().clone(), edge.to()));

46

47

            // Keep track of the overall outgoing configuration.

48

5405

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

49

50

51

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

52

4023

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

53

4023

        if missing.satisfiable() {

54

645

            if owners[*vertex] == Player::Even {

55

320

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

56

320

                edges.push((vertex, universe.clone(), true_node));

57

325

            } else {

58

325

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

59

325

                edges.push((vertex, universe.clone(), false_node));

60

325

61

3378

62

63

64

201

    Ok(VariabilityParityGame::from_edges(

65

201

        manager_ref,

66

201

        vpg.initial_vertex(),

67

201

        owners,

68

201

        priorities,

69

201

        vpg.configuration().clone(),

70

201

        vpg.variables().clone(),

71

402

        || edges.iter().cloned(),

72

))

73

201