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

            

        

            

                3
            

            

                
            

            

                
use oxidd::BooleanFunction;

            

        

            

                4
            

            

                
            

            

                
use oxidd::ManagerRef;

            

        

            

                5
            

            

                
            

            

                
use oxidd::bdd::BDDFunction;

            

        

            

                6
            

            

                
            

            

                
use oxidd::bdd::BDDManagerRef;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use merc_collections::ByteCompressedVec;

            

        

            

                9
            

            

                
            

            

                
use merc_collections::bytevec;

            

        

            

                10
            

            

                
            

            

                

            

        

            

                11
            

            

                
            

            

                
use crate::PG;

            

        

            

                12
            

            

                
            

            

                
use crate::VariabilityParityGame;

            

        

            

                13
            

            

                
            

            

                
use crate::VertexIndex;

            

        

            

                14
            

            

                
            

            

                

            

        

            

                15
            

            

                
            

            

                
/// Stores the incoming transitions for a given variability parity game.

            

        

            

                16
            

            

                
            

            

                
pub struct VariabilityPredecessors {

            

        

            

                17
            

            

                
            

            

                
    edges_from: ByteCompressedVec<VertexIndex>,

            

        

            

                18
            

            

                
            

            

                
    edges_configuration: Vec<BDDFunction>,

            

        

            

                19
            

            

                
            

            

                
    vertex_to_predecessors: ByteCompressedVec<usize>,

            

        

            

                20
            

            

                
            

            

                
}

            

        

            

                21
            

            

                
            

            

                

            

        

            

                22
            

            

                
            

            

                
impl VariabilityPredecessors {

            

        

            

                23
            

            

                
            

            

                
    /// Creates the predecessors structure for the given parity game.

            

        

            

                24
            

            

                300
            

            

                
    pub fn new(manager_ref: &BDDManagerRef, game: &VariabilityParityGame) -> Self {

            

        

            

                25
            

            

                300
            

            

                
        let mut edges_from = bytevec![VertexIndex::new(0); game.num_of_edges()];

            

        

            

                26
            

            

                300
            

            

                
        let mut edges_configuration =

            

        

            

                27
            

            

                300
            

            

                
            manager_ref.with_manager_shared(|manager| vec![BDDFunction::f(manager); game.num_of_edges()]);

            

        

            

                28
            

            

                300
            

            

                
        let mut state2incoming = bytevec![0; game.num_of_vertices()];

            

        

            

                29
            

            

                
            

            

                

            

        

            

                30
            

            

                
            

            

                
        // Count the number of incoming transitions for each state

            

        

            

                31
            

            

                6600
            

            

                
        for state_index in game.iter_vertices() {

            

        

            

                32
            

            

                9611
            

            

                
            for edge in game.outgoing_conf_edges(state_index) {

            

        

            

                33
            

            

                9611
            

            

                
                state2incoming.update(*edge.to(), |start| *start += 1);

            

        

            

                34
            

            

                
            

            

                
            }

            

        

            

                35
            

            

                
            

            

                
        }

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
        // Compute the start offsets (prefix sum)

            

        

            

                38
            

            

                6600
            

            

                
        state2incoming.fold(0, |offset, start| {

            

        

            

                39
            

            

                6600
            

            

                
            let new_offset = offset + *start;

            

        

            

                40
            

            

                6600
            

            

                
            *start = offset;

            

        

            

                41
            

            

                6600
            

            

                
            new_offset

            

        

            

                42
            

            

                6600
            

            

                
        });

            

        

            

                43
            

            

                
            

            

                

            

        

            

                44
            

            

                
            

            

                
        // Place the transitions

            

        

            

                45
            

            

                6600
            

            

                
        for state_index in game.iter_vertices() {

            

        

            

                46
            

            

                9611
            

            

                
            for edge in game.outgoing_conf_edges(state_index) {

            

        

            

                47
            

            

                9611
            

            

                
                state2incoming.update(*edge.to(), |start| {

            

        

            

                48
            

            

                9611
            

            

                
                    edges_from.set(*start, state_index);

            

        

            

                49
            

            

                9611
            

            

                
                    edges_configuration[*start] = edge.configuration().clone();

            

        

            

                50
            

            

                9611
            

            

                
                    *start += 1;

            

        

            

                51
            

            

                9611
            

            

                
                });

            

        

            

                52
            

            

                
            

            

                
            }

            

        

            

                53
            

            

                
            

            

                
        }

            

        

            

                54
            

            

                
            

            

                

            

        

            

                55
            

            

                6600
            

            

                
        state2incoming.fold(0, |previous, start| {

            

        

            

                56
            

            

                6600
            

            

                
            let result = *start;

            

        

            

                57
            

            

                6600
            

            

                
            *start = previous;

            

        

            

                58
            

            

                6600
            

            

                
            result

            

        

            

                59
            

            

                6600
            

            

                
        });

            

        

            

                60
            

            

                
            

            

                

            

        

            

                61
            

            

                
            

            

                
        // Add sentinel state

            

        

            

                62
            

            

                300
            

            

                
        state2incoming.push(edges_from.len());

            

        

            

                63
            

            

                
            

            

                

            

        

            

                64
            

            

                300
            

            

                
        Self {

            

        

            

                65
            

            

                300
            

            

                
            edges_from,

            

        

            

                66
            

            

                300
            

            

                
            edges_configuration,

            

        

            

                67
            

            

                300
            

            

                
            vertex_to_predecessors: state2incoming,

            

        

            

                68
            

            

                300
            

            

                
        }

            

        

            

                69
            

            

                300
            

            

                
    }

            

        

            

                70
            

            

                
            

            

                

            

        

            

                71
            

            

                
            

            

                
    /// Returns an iterator over the incoming transitions for the given state.

            

        

            

                72
            

            

                20863
            

            

                
    pub fn predecessors(&self, state_index: VertexIndex) -> impl Iterator<Item = (VertexIndex, &BDDFunction)> + '_ {

            

        

            

                73
            

            

                20863
            

            

                
        let start = self.vertex_to_predecessors.index(state_index.value());

            

        

            

                74
            

            

                20863
            

            

                
        let end = self.vertex_to_predecessors.index(state_index.value() + 1);

            

        

            

                75
            

            

                31260
            

            

                
        (start..end).map(move |i| (self.edges_from.index(i), &self.edges_configuration[i]))

            

        

            

                76
            

            

                20863
            

            

                
    }

            

        

            

                77
            

            

                
            

            

                
}