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

14

15

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

16

201

pub fn make_vpg_total(

17

201

    manager_ref: &BDDManagerRef,

18

201

    vpg: &VariabilityParityGame,

19

201

) -> Result<VariabilityParityGame, MercError> {

20

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

21

201

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

22

23

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

24

201

    let mut edges = Vec::new();

25

26

    // Add the true and false nodes.

27

201

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

28

201

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

29

30

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

31

201

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

32

201

    owners.push(Player::Even);

33

201

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

34

35

201

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

36

201

    owners.push(Player::Even);

37

201

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

38

39

201

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

40

201

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

41

42

4023

    for vertex in vpg.iter_vertices() {

43

4023

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

44

5353

        for edge in vpg.outgoing_conf_edges(vertex) {

45

            // Add the original edge.

46

5353

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

47

48

            // Keep track of the overall outgoing configuration.

49

5353

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

50

51

52

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

53

4023

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

54

4023

        if missing.satisfiable() {

55

643

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

56

309

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

57

309

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

58

334

            } else {

59

334

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

60

334

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

61

334

62

3380

63

64

65

201

    Ok(VariabilityParityGame::from_edges(

66

201

        manager_ref,

67

201

        vpg.initial_vertex(),

68

201

        owners,

69

201

        priorities,

70

201

        vpg.configuration().clone(),

71

201

        vpg.variables().clone(),

72

402

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

73

))

74

201