1 
use merc_lts::LabelledTransitionSystem;
2 
use merc_lts::LtsBuilderFast;
3 
use merc_lts::LTS;
4 
use oxidd::bdd::BDDFunction;
5 
use oxidd::BooleanFunction;
6 
use oxidd::Function;
7 

            

        

            

                8
            

            

                
            

            

                
use merc_symbolic::bits_to_bdd;

            

        

            

                9
            

            

                
            

            

                
use merc_symbolic::CubeIterAll;

            

        

            

                10
            

            

                
            

            

                
use merc_utilities::MercError;

            

        

            

                11
            

            

                
            

            

                
use merc_utilities::Timing;

            

        

            

                12
            

            

                
            

            

                
use oxidd::util::OptBool;

            

        

            

                13
            

            

                
            

            

                

            

        

            

                14
            

            

                
            

            

                
use crate::FeatureDiagram;

            

        

            

                15
            

            

                
            

            

                
use crate::FeatureTransitionSystem;

            

        

            

                16
            

            

                
            

            

                

            

        

            

                17
            

            

                
            

            

                
/// Projects a variability parity game into a standard parity game by removing

            

        

            

                18
            

            

                
            

            

                
/// edges that are not enabled by the given feature selection.

            

        

            

                19
            

            

                
            

            

                
pub fn project_feature_transition_system(

            

        

            

                20
            

            

                
            

            

                
    fts: &FeatureTransitionSystem,

            

        

            

                21
            

            

                
            

            

                
    feature_selection: &BDDFunction,

            

        

            

                22
            

            

                
            

            

                
) -> Result<LabelledTransitionSystem<String>, MercError> {

            

        

            

                23
            

            

                
            

            

                
    let mut builder = LtsBuilderFast::new(fts.labels().to_vec(), Vec::new());

            

        

            

                24
            

            

                
            

            

                

            

        

            

                25
            

            

                
            

            

                
    for v in fts.iter_states() {

            

        

            

                26
            

            

                
            

            

                
        for edge in fts.outgoing_transitions(v) {

            

        

            

                27
            

            

                
            

            

                
            // Check if the edge is enabled by the feature selection, if so, include it.

            

        

            

                28
            

            

                
            

            

                
            if feature_selection.and(fts.feature_label(edge.label))?.satisfiable() {

            

        

            

                29
            

            

                
            

            

                
                builder.add_transition(v, &fts.labels()[edge.label], edge.to);

            

        

            

                30
            

            

                
            

            

                
            }

            

        

            

                31
            

            

                
            

            

                
        }

            

        

            

                32
            

            

                
            

            

                
    }

            

        

            

                33
            

            

                
            

            

                

            

        

            

                34
            

            

                
            

            

                
    Ok(builder.finish(fts.initial_state_index(), false))

            

        

            

                35
            

            

                
            

            

                
}

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
/// A projected configuration of a featured transition system.

            

        

            

                38
            

            

                
            

            

                
pub struct ProjectedLts {

            

        

            

                39
            

            

                
            

            

                
    pub bits: Vec<OptBool>,

            

        

            

                40
            

            

                
            

            

                
    pub bdd: BDDFunction,

            

        

            

                41
            

            

                
            

            

                
    pub lts: LabelledTransitionSystem<String>,

            

        

            

                42
            

            

                
            

            

                
}

            

        

            

                43
            

            

                
            

            

                

            

        

            

                44
            

            

                
            

            

                
/// Projects all configurations of a variability parity game into standard parity games.

            

        

            

                45
            

            

                
            

            

                
pub fn project_feature_transition_system_iter<'a>(

            

        

            

                46
            

            

                
            

            

                
    fts: &'a FeatureTransitionSystem,

            

        

            

                47
            

            

                
            

            

                
    fd: &'a FeatureDiagram,

            

        

            

                48
            

            

                
            

            

                
    timing: &'a Timing,

            

        

            

                49
            

            

                
            

            

                
) -> impl Iterator<Item = Result<(ProjectedLts, &'a Timing), MercError>> {

            

        

            

                50
            

            

                
            

            

                
    CubeIterAll::new(fd.configuration()).map(move |cube| {

            

        

            

                51
            

            

                
            

            

                
        let cube = cube?;

            

        

            

                52
            

            

                
            

            

                
        let variables = fd.features().values().cloned().collect::<Vec<_>>();

            

        

            

                53
            

            

                
            

            

                

            

        

            

                54
            

            

                
            

            

                
        let bdd = match bits_to_bdd(&fd.configuration().manager_ref(), &variables, &cube) {

            

        

            

                55
            

            

                
            

            

                
            Ok(bdd) => bdd,

            

        

            

                56
            

            

                
            

            

                
            Err(e) => return Err(MercError::from(e)),

            

        

            

                57
            

            

                
            

            

                
        };

            

        

            

                58
            

            

                
            

            

                

            

        

            

                59
            

            

                
            

            

                
        let lts = timing.measure("project", || -> Result<_, MercError> {

            

        

            

                60
            

            

                
            

            

                
            project_feature_transition_system(fts, &bdd)

            

        

            

                61
            

            

                
            

            

                
        })?;

            

        

            

                62
            

            

                
            

            

                

            

        

            

                63
            

            

                
            

            

                
        Ok((

            

        

            

                64
            

            

                
            

            

                
            ProjectedLts {

            

        

            

                65
            

            

                
            

            

                
                bits: cube,

            

        

            

                66
            

            

                
            

            

                
                bdd,

            

        

            

                67
            

            

                
            

            

                
                lts,

            

        

            

                68
            

            

                
            

            

                
            },

            

        

            

                69
            

            

                
            

            

                
            timing,

            

        

            

                70
            

            

                
            

            

                
        ))

            

        

            

                71
            

            

                
            

            

                
    })

            

        

            

                72
            

            

                
            

            

                
}