Grcov report - verify.rs

1

use bitvec::bitvec;

2

use bitvec::order::Lsb0;

3

use delegate::delegate;

4

use log::trace;

5

6

use crate::Edge;

7

use crate::PG;

8

use crate::Player;

9

use crate::Priority;

10

use crate::Set;

11

use crate::Strategy;

12

use crate::VertexIndex;

13

use crate::check_partition;

14

use crate::solve_solitaire_game;

15

16

/// Verifies that a proposed solution is valid for the given parity game and

17

/// strategies.

18

///

19

/// # Details

20

///

21

/// This is done by restricting the `pg` according to the strategy for each

22

/// player, and computing the solution for the induced solitaire game.

23

200

pub fn verify_solution<G: PG>(pg: &G, solution: &[Set; 2], strategy: &[Strategy; 2]) {

24

200

    debug_assert!(pg.is_total(), "Verifying requires a total parity game");

25

26

200

    trace!("Solution for even: {}", solution[Player::Even.to_index()]);

27

200

    trace!("Solution for odd: {}", solution[Player::Odd.to_index()]);

28

29

200

    trace!("Strategy for even: {:?}", strategy[Player::Even.to_index()]);

30

200

    trace!("Strategy for odd: {:?}", strategy[Player::Odd.to_index()]);

31

32

    // The set of all vertices in the game.

33

200

    let vertices = bitvec![usize, Lsb0; 1; pg.num_of_vertices()];

34

35

    // Check that the input solution is a proper partitioning

36

200

    check_partition(&solution[0], &solution[1], &vertices);

37

38

    // We check both players' strategies

39

400

    for player in [Player::Even, Player::Odd] {

40

        // Check that the strategies are consistent with the ownership of the vertices

41

400

        strategy[player.to_index()].check_consistent(pg, &solution[player.to_index()], player);

42

43

        // Restricted game according to the strategy for the current player

44

400

        let restricted = Restricted::new(pg, player, &strategy[player.to_index()]);

45

46

        // The opponent is the solitaire player, so invert the solution.

47

        // Furthermore, only consider the vertices that are in the solution for

48

        // the current player.

49

400

        let expected = !solve_solitaire_game(&restricted) & solution[player.to_index()].clone();

50

400

        if expected != solution[player.to_index()] {

51

            panic!(

52

                "The strategy for player {} is incorrect, expected solution {}, got {}",

53

                player,

54

                expected,

55

                solution[player.to_index()]

56

);

57

400

58

59

200

60

61

/// A subgame of a parity game that is induced by taking the strategy for the

62

/// given player into account.

63

struct Restricted<'a, G: PG> {

64

    /// The game that is being restricted.

65

    game: &'a G,

66

67

    /// The strategy that is applied to the game.

68

    strategy: &'a Strategy,

69

70

    /// The player that owns the strategy.

71

    player: Player,

72

73

74

impl<G: PG> Restricted<'_, G> {

75

    /// Create a new sub-game induced by the given strategy on the given game.

76

400

    pub fn new<'a>(game: &'a G, player: Player, strategy: &'a Strategy) -> Restricted<'a, G> {

77

400

        Restricted { game, player, strategy }

78

400

79

80

81

impl<G: PG> PG for Restricted<'_, G> {

82

    type Label = G::Label;

83

84

40600

    fn owner(&self, _vertex_index: VertexIndex) -> Player {

85

        // We know that player only makes moves according to the strategy, so we can treat all vertices in the game as if they were owned by the opponent.

86

40600

        self.player.opponent()

87

40600

88

89

220167

    fn outgoing_edges<'a>(&'a self, vertex_index: VertexIndex) -> impl Iterator<Item = Edge<'a, G::Label>> + 'a {

90

285503

        self.game.outgoing_edges(vertex_index).filter(move |edge| {

91

            // Only consider edges that follow the strategy.

92

285503

            self.game.owner(vertex_index) != self.player || self.strategy.get(vertex_index) == Some(&edge.to())

93

285503

})

94

220167

95

96

    fn is_total(&self) -> bool {

97

        // The sub-game is total if every vertex in the restricted set has at least one outgoing edge.

98

        self.iter_vertices().all(|v| self.outgoing_edges(v).next().is_some())

99

100

101

    delegate! {

102

        to self.game {

103

400

            fn initial_vertex(&self) -> VertexIndex;

104

76036

            fn num_of_vertices(&self) -> usize;

105

400

            fn num_of_edges(&self) -> usize;

106

2400

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

107

114024

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

108

400

            fn highest_priority(&self) -> Priority;

109

110

111