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

7

use crate::solve_solitaire_game;

8

use crate::Edge;

9

use crate::Player;

10

use crate::Priority;

11

use crate::Set;

12

use crate::Strategy;

13

use crate::VertexIndex;

14

use crate::PG;

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

100

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

24

100

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

25

26

100

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

27

100

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

28

29

100

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

30

100

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

31

32

    // The set of all vertices in the game.

33

100

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

34

35

    // Check that the input solution is a proper partitioning

36

100

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

37

38

    // We check both players' strategies

39

200

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

40

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

41

200

        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

200

        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

200

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

50

200

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

51

            panic!("The strategy for player {} is incorrect, expected solution {}, got {}", player, expected, solution[player.to_index()]);

52

200

53

54

100

55

56

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

57

/// given player into account.

58

struct Restricted<'a, G: PG> {

59

    /// The game that is being restricted.

60

    game: &'a G,

61

62

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

63

    strategy: &'a Strategy,

64

65

    /// The player that owns the strategy.

66

    player: Player,

67

68

69

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

70

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

71

200

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

72

200

        Restricted { game, player, strategy }

73

200

74

75

76

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

77

    type Label = G::Label;

78

79

20300

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

80

        // 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.

81

20300

        self.player.opponent()

82

20300

83

84

179858

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

85

232678

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

86

            // Only consider edges that follow the strategy.

87

232678

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

88

232678

})

89

179858

90

91

    fn is_total(&self) -> bool {

92

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

93

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

94

95

96

    delegate! {

97

        to self.game {

98

200

            fn initial_vertex(&self) -> VertexIndex;

99

37900

            fn num_of_vertices(&self) -> usize;

100

700

            fn num_of_edges(&self) -> usize;

101

1200

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

102

57003

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

103

200

            fn highest_priority(&self) -> Priority;

104

105

106