1
//! Authors: Maurice Laveaux and Sjef van Loo
2

            
3
use merc_collections::ByteCompressedVec;
4
use merc_collections::bytevec;
5

            
6
use crate::PG;
7
use crate::ParityGame;
8
use crate::VertexIndex;
9

            
10
/// Stores the predecessors for a given parity game.
11
pub struct Predecessors {
12
    edges_from: ByteCompressedVec<VertexIndex>,
13
    vertex_to_predecessors: ByteCompressedVec<usize>,
14
}
15

            
16
impl Predecessors {
17
    /// Creates the predecessors structure for the given parity game.
18
853
    pub fn new(game: &ParityGame) -> Self {
19
853
        let mut edges_from = bytevec![VertexIndex::new(0); game.num_of_edges()];
20
853
        let mut state2incoming = bytevec![0; game.num_of_vertices()];
21

            
22
        // Count the number of incoming transitions for each state
23
13691
        for state_index in game.iter_vertices() {
24
18360
            for to in game.outgoing_edges(state_index) {
25
18360
                state2incoming.update(to.value(), |start| *start += 1);
26
            }
27
        }
28

            
29
        // Compute the start offsets (prefix sum)
30
13691
        state2incoming.fold(0, |offset, start| {
31
13691
            let new_offset = offset + *start;
32
13691
            *start = offset;
33
13691
            new_offset
34
13691
        });
35

            
36
        // Place the transitions
37
13691
        for state_index in game.iter_vertices() {
38
18360
            for to in game.outgoing_edges(state_index) {
39
18360
                state2incoming.update(to.value(), |start| {
40
18360
                    edges_from.set(*start, state_index);
41
18360
                    *start += 1;
42
18360
                });
43
            }
44
        }
45

            
46
13691
        state2incoming.fold(0, |previous, start| {
47
13691
            let result = *start;
48
13691
            *start = previous;
49
13691
            result
50
13691
        });
51

            
52
        // Add sentinel state
53
853
        state2incoming.push(edges_from.len());
54

            
55
853
        Self {
56
853
            edges_from,
57
853
            vertex_to_predecessors: state2incoming,
58
853
        }
59
853
    }
60

            
61
    /// Returns an iterator over the predecessors the given vertex.
62
56211
    pub fn predecessors(&self, state_index: VertexIndex) -> impl Iterator<Item = VertexIndex> + '_ {
63
56211
        let start = self.vertex_to_predecessors.index(state_index.value());
64
56211
        let end = self.vertex_to_predecessors.index(state_index.value() + 1);
65
82607
        (start..end).map(move |i| self.edges_from.index(i))
66
56211
    }
67
}