1 
use std::fmt;
2 

            

        

            

                3
            

            

                
            

            

                
use log::debug;

            

        

            

                4
            

            

                
            

            

                
use log::info;

            

        

            

                5
            

            

                
            

            

                
use log::trace;

            

        

            

                6
            

            

                
            

            

                
use oxidd::BooleanFunction;

            

        

            

                7
            

            

                
            

            

                
use oxidd::ManagerRef;

            

        

            

                8
            

            

                
            

            

                
use oxidd::bdd::BDDFunction;

            

        

            

                9
            

            

                
            

            

                
use oxidd::bdd::BDDManagerRef;

            

        

            

                10
            

            

                
            

            

                

            

        

            

                11
            

            

                
            

            

                
use merc_collections::IndexedSet;

            

        

            

                12
            

            

                
            

            

                
use merc_io::TimeProgress;

            

        

            

                13
            

            

                
            

            

                
use merc_lts::LTS;

            

        

            

                14
            

            

                
            

            

                
use merc_lts::StateIndex;

            

        

            

                15
            

            

                
            

            

                
use merc_syntax::ActFrm;

            

        

            

                16
            

            

                
            

            

                
use merc_syntax::ActFrmBinaryOp;

            

        

            

                17
            

            

                
            

            

                
use merc_syntax::Action;

            

        

            

                18
            

            

                
            

            

                
use merc_syntax::FixedPointOperator;

            

        

            

                19
            

            

                
            

            

                
use merc_syntax::ModalityOperator;

            

        

            

                20
            

            

                
            

            

                
use merc_syntax::MultiAction;

            

        

            

                21
            

            

                
            

            

                
use merc_syntax::RegFrm;

            

        

            

                22
            

            

                
            

            

                
use merc_syntax::StateFrm;

            

        

            

                23
            

            

                
            

            

                
use merc_syntax::StateFrmOp;

            

        

            

                24
            

            

                
            

            

                
use merc_utilities::MercError;

            

        

            

                25
            

            

                
            

            

                

            

        

            

                26
            

            

                
            

            

                
use crate::FeatureTransitionSystem;

            

        

            

                27
            

            

                
            

            

                
use crate::ModalEquationSystem;

            

        

            

                28
            

            

                
            

            

                
use crate::Player;

            

        

            

                29
            

            

                
            

            

                
use crate::Priority;

            

        

            

                30
            

            

                
            

            

                
use crate::VariabilityParityGame;

            

        

            

                31
            

            

                
            

            

                
use crate::VertexIndex;

            

        

            

                32
            

            

                
            

            

                
use crate::compute_reachable;

            

        

            

                33
            

            

                
            

            

                
use crate::make_vpg_total;

            

        

            

                34
            

            

                
            

            

                

            

        

            

                35
            

            

                
            

            

                
/// Translates a feature transition system into a variability parity game.

            

        

            

                36
            

            

                1
            

            

                
pub fn translate_vpg(

            

        

            

                37
            

            

                1
            

            

                
    manager_ref: &BDDManagerRef,

            

        

            

                38
            

            

                1
            

            

                
    fts: &FeatureTransitionSystem,

            

        

            

                39
            

            

                1
            

            

                
    configuration: BDDFunction,

            

        

            

                40
            

            

                1
            

            

                
    formula: &StateFrm,

            

        

            

                41
            

            

                1
            

            

                
) -> Result<VariabilityParityGame, MercError> {

            

        

            

                42
            

            

                
            

            

                
    // Parses all labels into MultiAction once

            

        

            

                43
            

            

                1
            

            

                
    let parsed_labels: Result<Vec<MultiAction>, MercError> =

            

        

            

                44
            

            

                5
            

            

                
        fts.labels().iter().map(|label| MultiAction::parse(label)).collect();

            

        

            

                45
            

            

                
            

            

                

            

        

            

                46
            

            

                
            

            

                
    // Simplify the labels by stripping BDD information

            

        

            

                47
            

            

                1
            

            

                
    let simplified_labels: Vec<MultiAction> = parsed_labels?

            

        

            

                48
            

            

                1
            

            

                
        .iter()

            

        

            

                49
            

            

                1
            

            

                
        .map(strip_feature_configuration_from_multi_action)

            

        

            

                50
            

            

                1
            

            

                
        .collect();

            

        

            

                51
            

            

                
            

            

                

            

        

            

                52
            

            

                1
            

            

                
    let equation_system = ModalEquationSystem::new(formula);

            

        

            

                53
            

            

                1
            

            

                
    debug!("{}", equation_system);

            

        

            

                54
            

            

                
            

            

                

            

        

            

                55
            

            

                2
            

            

                
    for i in 0..equation_system.len() {

            

        

            

                56
            

            

                2
            

            

                
        debug!("Alternation depth of {} is {}", i, equation_system.alternation_depth(i));

            

        

            

                57
            

            

                
            

            

                
    }

            

        

            

                58
            

            

                
            

            

                

            

        

            

                59
            

            

                1
            

            

                
    let mut algorithm = Translation::new(

            

        

            

                60
            

            

                1
            

            

                
        fts,

            

        

            

                61
            

            

                1
            

            

                
        &simplified_labels,

            

        

            

                62
            

            

                1
            

            

                
        &equation_system,

            

        

            

                63
            

            

                1
            

            

                
        manager_ref.with_manager_shared(|manager| BDDFunction::t(manager)),

            

        

            

                64
            

            

                
            

            

                
    );

            

        

            

                65
            

            

                
            

            

                

            

        

            

                66
            

            

                1
            

            

                
    algorithm.translate(fts.initial_state_index(), 0)?;

            

        

            

                67
            

            

                
            

            

                

            

        

            

                68
            

            

                
            

            

                
    // Convert the feature diagram (with names) to a VPG

            

        

            

                69
            

            

                1
            

            

                
    let variables: Vec<BDDFunction> = fts.features().values().cloned().collect();

            

        

            

                70
            

            

                
            

            

                

            

        

            

                71
            

            

                1
            

            

                
    let result = VariabilityParityGame::from_edges(

            

        

            

                72
            

            

                1
            

            

                
        manager_ref,

            

        

            

                73
            

            

                1
            

            

                
        VertexIndex::new(0),

            

        

            

                74
            

            

                1
            

            

                
        algorithm.vertices.iter().map(|(p, _)| p).cloned().collect(),

            

        

            

                75
            

            

                1
            

            

                
        algorithm.vertices.into_iter().map(|(_, pr)| pr).collect(),

            

        

            

                76
            

            

                1
            

            

                
        configuration,

            

        

            

                77
            

            

                1
            

            

                
        variables,

            

        

            

                78
            

            

                2
            

            

                
        || algorithm.edges.iter().cloned(),

            

        

            

                79
            

            

                
            

            

                
    );

            

        

            

                80
            

            

                
            

            

                

            

        

            

                81
            

            

                
            

            

                
    // Check that all vertices are reachable from the initial vertex. After

            

        

            

                82
            

            

                
            

            

                
    // totality it could be that the true or false nodes are not reachable.

            

        

            

                83
            

            

                1
            

            

                
    if cfg!(debug_assertions) {

            

        

            

                84
            

            

                1
            

            

                
        let (_, reachable_vertices) = compute_reachable(&result);

            

        

            

                85
            

            

                1
            

            

                
        debug_assert!(

            

        

            

                86
            

            

                23
            

            

                
            reachable_vertices.iter().all(|v| v.is_some()),

            

        

            

                87
            

            

                
            

            

                
            "Not all vertices are reachable from the initial vertex"

            

        

            

                88
            

            

                
            

            

                
        );

            

        

            

                89
            

            

                
            

            

                
    }

            

        

            

                90
            

            

                
            

            

                

            

        

            

                91
            

            

                
            

            

                
    // Ensure that the result is a total VPG.

            

        

            

                92
            

            

                1
            

            

                
    let total_result = if !result.is_total(manager_ref)? {

            

        

            

                93
            

            

                1
            

            

                
        make_vpg_total(manager_ref, &result)?

            

        

            

                94
            

            

                
            

            

                
    } else {

            

        

            

                95
            

            

                
            

            

                
        result

            

        

            

                96
            

            

                
            

            

                
    };

            

        

            

                97
            

            

                
            

            

                

            

        

            

                98
            

            

                1
            

            

                
    Ok(total_result)

            

        

            

                99
            

            

                1
            

            

                
}

            

        

            

                100
            

            

                
            

            

                

            

        

            

                101
            

            

                
            

            

                
/// Is used to distinguish between StateFrm and Equation vertices in the vertex map.

            

        

            

                102
            

            

                
            

            

                
#[derive(Clone, PartialEq, Eq, Hash)]

            

        

            

                103
            

            

                
            

            

                
enum Formula<'a> {

            

        

            

                104
            

            

                
            

            

                
    StateFrm(&'a StateFrm),

            

        

            

                105
            

            

                
            

            

                
    Equation(usize),

            

        

            

                106
            

            

                
            

            

                
}

            

        

            

                107
            

            

                
            

            

                

            

        

            

                108
            

            

                
            

            

                
impl fmt::Display for Formula<'_> {

            

        

            

                109
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            

        

            

                110
            

            

                
            

            

                
        match self {

            

        

            

                111
            

            

                
            

            

                
            Formula::StateFrm(state_frm) => write!(f, "{}", state_frm),

            

        

            

                112
            

            

                
            

            

                
            Formula::Equation(i) => write!(f, "Equation({})", i),

            

        

            

                113
            

            

                
            

            

                
        }

            

        

            

                114
            

            

                
            

            

                
    }

            

        

            

                115
            

            

                
            

            

                
}

            

        

            

                116
            

            

                
            

            

                

            

        

            

                117
            

            

                
            

            

                
/// Local struct to keep track of the translation state

            

        

            

                118
            

            

                
            

            

                
///

            

        

            

                119
            

            

                
            

            

                
/// Implements the translation from (s, Ψ) pairs to VPG vertices and edges.

            

        

            

                120
            

            

                
            

            

                
/// However, to avoid the complication of merging sub-results we immediately

            

        

            

                121
            

            

                
            

            

                
/// store the vertices and edges into mutable vectors. Furthermore, to avoid

            

        

            

                122
            

            

                
            

            

                
/// stack overflows we use a breadth-first search approach with a queue. This

            

        

            

                123
            

            

                
            

            

                
/// means that during queuing we immediately assign a fresh index to each (s, Ψ)

            

        

            

                124
            

            

                
            

            

                
/// pair (if it does not yet exist) and then queue it to assign its actual

            

        

            

                125
            

            

                
            

            

                
/// values later on.

            

        

            

                126
            

            

                
            

            

                
struct Translation<'a> {

            

        

            

                127
            

            

                
            

            

                
    vertex_map: IndexedSet<(StateIndex, Formula<'a>)>,

            

        

            

                128
            

            

                
            

            

                
    vertices: Vec<(Player, Priority)>,

            

        

            

                129
            

            

                
            

            

                
    edges: Vec<(VertexIndex, BDDFunction, VertexIndex)>,

            

        

            

                130
            

            

                
            

            

                

            

        

            

                131
            

            

                
            

            

                
    // Used for the breadth first search.

            

        

            

                132
            

            

                
            

            

                
    queue: Vec<(StateIndex, Formula<'a>, VertexIndex)>,

            

        

            

                133
            

            

                
            

            

                

            

        

            

                134
            

            

                
            

            

                
    /// The parsed labels of the FTS.

            

        

            

                135
            

            

                
            

            

                
    parsed_labels: &'a Vec<MultiAction>,

            

        

            

                136
            

            

                
            

            

                

            

        

            

                137
            

            

                
            

            

                
    /// The feature transition system being translated.

            

        

            

                138
            

            

                
            

            

                
    fts: &'a FeatureTransitionSystem,

            

        

            

                139
            

            

                
            

            

                

            

        

            

                140
            

            

                
            

            

                
    /// A reference to the modal equation system being translated.

            

        

            

                141
            

            

                
            

            

                
    equation_system: &'a ModalEquationSystem,

            

        

            

                142
            

            

                
            

            

                

            

        

            

                143
            

            

                
            

            

                
    /// The BDD representing the "true" feature configuration.

            

        

            

                144
            

            

                
            

            

                
    true_bdd: BDDFunction,

            

        

            

                145
            

            

                
            

            

                

            

        

            

                146
            

            

                
            

            

                
    /// Use to print progress information.

            

        

            

                147
            

            

                
            

            

                
    progress: TimeProgress<usize>,

            

        

            

                148
            

            

                
            

            

                
}

            

        

            

                149
            

            

                
            

            

                

            

        

            

                150
            

            

                
            

            

                
impl<'a> Translation<'a> {

            

        

            

                151
            

            

                
            

            

                
    /// Creates a new translation instance.

            

        

            

                152
            

            

                1
            

            

                
    fn new(

            

        

            

                153
            

            

                1
            

            

                
        fts: &'a FeatureTransitionSystem,

            

        

            

                154
            

            

                1
            

            

                
        parsed_labels: &'a Vec<MultiAction>,

            

        

            

                155
            

            

                1
            

            

                
        equation_system: &'a ModalEquationSystem,

            

        

            

                156
            

            

                1
            

            

                
        true_bdd: BDDFunction,

            

        

            

                157
            

            

                1
            

            

                
    ) -> Self {

            

        

            

                158
            

            

                1
            

            

                
        let progress: TimeProgress<usize> = TimeProgress::new(

            

        

            

                159
            

            

                
            

            

                
            |num_of_vertices: usize| {

            

        

            

                160
            

            

                
            

            

                
                info!("Translated {} vertices...", num_of_vertices);

            

        

            

                161
            

            

                
            

            

                
            },

            

        

            

                162
            

            

                
            

            

                
            1,

            

        

            

                163
            

            

                
            

            

                
        );

            

        

            

                164
            

            

                
            

            

                

            

        

            

                165
            

            

                1
            

            

                
        Self {

            

        

            

                166
            

            

                1
            

            

                
            vertex_map: IndexedSet::new(),

            

        

            

                167
            

            

                1
            

            

                
            vertices: Vec::new(),

            

        

            

                168
            

            

                1
            

            

                
            edges: Vec::new(),

            

        

            

                169
            

            

                1
            

            

                
            queue: Vec::new(),

            

        

            

                170
            

            

                1
            

            

                
            fts,

            

        

            

                171
            

            

                1
            

            

                
            parsed_labels,

            

        

            

                172
            

            

                1
            

            

                
            equation_system,

            

        

            

                173
            

            

                1
            

            

                
            true_bdd,

            

        

            

                174
            

            

                1
            

            

                
            progress,

            

        

            

                175
            

            

                1
            

            

                
        }

            

        

            

                176
            

            

                1
            

            

                
    }

            

        

            

                177
            

            

                
            

            

                

            

        

            

                178
            

            

                
            

            

                
    /// Perform the actual translation.

            

        

            

                179
            

            

                1
            

            

                
    fn translate(&mut self, initial_state: StateIndex, initial_equation_index: usize) -> Result<(), MercError> {

            

        

            

                180
            

            

                
            

            

                
        // We store (state, formula, N) into the queue, where N is the vertex number assigned to this pair. This means

            

        

            

                181
            

            

                
            

            

                
        // that during the traversal we can assume this N to exist.

            

        

            

                182
            

            

                1
            

            

                
        self.queue = vec![(

            

        

            

                183
            

            

                1
            

            

                
            initial_state,

            

        

            

                184
            

            

                1
            

            

                
            Formula::Equation(initial_equation_index),

            

        

            

                185
            

            

                1
            

            

                
            VertexIndex::new(0),

            

        

            

                186
            

            

                1
            

            

                
        )];

            

        

            

                187
            

            

                1
            

            

                
        self.vertex_map.insert((initial_state, Formula::Equation(initial_equation_index)));

            

        

            

                188
            

            

                1
            

            

                
        self.vertices.push((Player::Odd, Priority::new(0))); // Placeholder for the initial vertex

            

        

            

                189
            

            

                
            

            

                

            

        

            

                190
            

            

                24
            

            

                
        while let Some((s, formula, vertex_index)) = self.queue.pop() {

            

        

            

                191
            

            

                23
            

            

                
            debug!("Translating vertex {}: (s={}, formula={})", vertex_index, s, formula);

            

        

            

                192
            

            

                23
            

            

                
            self.progress.print(self.vertices.len());

            

        

            

                193
            

            

                23
            

            

                
            match formula {

            

        

            

                194
            

            

                19
            

            

                
                Formula::StateFrm(f) => {

            

        

            

                195
            

            

                19
            

            

                
                    self.translate_vertex(s, f, vertex_index);

            

        

            

                196
            

            

                19
            

            

                
                }

            

        

            

                197
            

            

                4
            

            

                
                Formula::Equation(i) => {

            

        

            

                198
            

            

                4
            

            

                
                    self.translate_equation(s, i, vertex_index);

            

        

            

                199
            

            

                4
            

            

                
                }

            

        

            

                200
            

            

                
            

            

                
            }

            

        

            

                201
            

            

                
            

            

                
        }

            

        

            

                202
            

            

                
            

            

                

            

        

            

                203
            

            

                1
            

            

                
        Ok(())

            

        

            

                204
            

            

                1
            

            

                
    }

            

        

            

                205
            

            

                
            

            

                

            

        

            

                206
            

            

                
            

            

                
    /// Translate a single vertex (s, Ψ) into the variability parity game vertex and its outgoing edges.

            

        

            

                207
            

            

                
            

            

                
    ///

            

        

            

                208
            

            

                
            

            

                
    /// The `fts` and `parsed_labels` are used to find the outgoing transitions matching the modalities in the formula.

            

        

            

                209
            

            

                
            

            

                
    ///

            

        

            

                210
            

            

                
            

            

                
    /// These are stored in the provided `vertices` and `edges` vectors.

            

        

            

                211
            

            

                
            

            

                
    /// The `vertex_map` is used to keep track of already translated vertices.

            

        

            

                212
            

            

                
            

            

                
    ///

            

        

            

                213
            

            

                
            

            

                
    /// This function is recursively called for subformulas.

            

        

            

                214
            

            

                19
            

            

                
    pub fn translate_vertex(&mut self, s: StateIndex, formula: &'a StateFrm, vertex_index: VertexIndex) {

            

        

            

                215
            

            

                19
            

            

                
        match formula {

            

        

            

                216
            

            

                
            

            

                
            StateFrm::True => {

            

        

            

                217
            

            

                
            

            

                
                // (s, true) → odd, 0

            

        

            

                218
            

            

                
            

            

                
                self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

            

        

            

                219
            

            

                
            

            

                
            }

            

        

            

                220
            

            

                
            

            

                
            StateFrm::False => {

            

        

            

                221
            

            

                
            

            

                
                // (s, false) → even, 0

            

        

            

                222
            

            

                
            

            

                
                self.vertices[vertex_index] = (Player::Even, Priority::new(0));

            

        

            

                223
            

            

                
            

            

                
            }

            

        

            

                224
            

            

                6
            

            

                
            StateFrm::Binary { op, lhs, rhs } => {

            

        

            

                225
            

            

                6
            

            

                
                match op {

            

        

            

                226
            

            

                6
            

            

                
                    StateFrmOp::Conjunction => {

            

        

            

                227
            

            

                6
            

            

                
                        // (s, Ψ_1 ∧ Ψ_2) →_P odd, (s, Ψ_1) and (s, Ψ_2), 0

            

        

            

                228
            

            

                6
            

            

                
                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

            

        

            

                229
            

            

                6
            

            

                
                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

            

        

            

                230
            

            

                6
            

            

                
                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

            

        

            

                231
            

            

                6
            

            

                

            

        

            

                232
            

            

                6
            

            

                
                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_1));

            

        

            

                233
            

            

                6
            

            

                
                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_2));

            

        

            

                234
            

            

                6
            

            

                
                    }

            

        

            

                235
            

            

                
            

            

                
                    StateFrmOp::Disjunction => {

            

        

            

                236
            

            

                
            

            

                
                        // (s, Ψ_1 ∨ Ψ_2) →_P even, (s, Ψ_1) and (s, Ψ_2), 0

            

        

            

                237
            

            

                
            

            

                
                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

            

        

            

                238
            

            

                
            

            

                
                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

            

        

            

                239
            

            

                
            

            

                
                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

            

        

            

                240
            

            

                
            

            

                

            

        

            

                241
            

            

                
            

            

                
                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_1));

            

        

            

                242
            

            

                
            

            

                
                        self.edges.push((vertex_index, self.true_bdd.clone(), s_psi_2));

            

        

            

                243
            

            

                
            

            

                
                    }

            

        

            

                244
            

            

                
            

            

                
                    _ => {

            

        

            

                245
            

            

                
            

            

                
                        unimplemented!("Cannot translate binary operator in {}", formula);

            

        

            

                246
            

            

                
            

            

                
                    }

            

        

            

                247
            

            

                
            

            

                
                }

            

        

            

                248
            

            

                
            

            

                
            }

            

        

            

                249
            

            

                4
            

            

                
            StateFrm::Id(identifier, _args) => {

            

        

            

                250
            

            

                4
            

            

                
                let (i, _equation) = self

            

        

            

                251
            

            

                4
            

            

                
                    .equation_system

            

        

            

                252
            

            

                4
            

            

                
                    .find_equation_by_identifier(identifier)

            

        

            

                253
            

            

                4
            

            

                
                    .expect("Variable must correspond to an equation");

            

        

            

                254
            

            

                4
            

            

                

            

        

            

                255
            

            

                4
            

            

                
                self.vertices[vertex_index] = (Player::Odd, Priority::new(0)); // The priority and owner do not matter here

            

        

            

                256
            

            

                4
            

            

                
                let equation_vertex = self.queue_vertex(s, Formula::Equation(i));

            

        

            

                257
            

            

                4
            

            

                
                self.edges.push((vertex_index, self.true_bdd.clone(), equation_vertex));

            

        

            

                258
            

            

                4
            

            

                
            }

            

        

            

                259
            

            

                
            

            

                
            StateFrm::Modality {

            

        

            

                260
            

            

                9
            

            

                
                operator,

            

        

            

                261
            

            

                9
            

            

                
                formula,

            

        

            

                262
            

            

                9
            

            

                
                expr,

            

        

            

                263
            

            

                
            

            

                
            } => {

            

        

            

                264
            

            

                9
            

            

                
                match operator {

            

        

            

                265
            

            

                
            

            

                
                    ModalityOperator::Box => {

            

        

            

                266
            

            

                
            

            

                
                        // (s, [a] Ψ) → odd, (s', Ψ) for all s' with s -a-> s', 0

            

        

            

                267
            

            

                9
            

            

                
                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

            

        

            

                268
            

            

                
            

            

                

            

        

            

                269
            

            

                12
            

            

                
                        for transition in self.fts.outgoing_transitions(s) {

            

        

            

                270
            

            

                12
            

            

                
                            let action = &self.parsed_labels[*transition.label];

            

        

            

                271
            

            

                
            

            

                

            

        

            

                272
            

            

                12
            

            

                
                            trace!("Matching action {} against formula {}", action, formula);

            

        

            

                273
            

            

                
            

            

                

            

        

            

                274
            

            

                12
            

            

                
                            if match_regular_formula(formula, action) {

            

        

            

                275
            

            

                4
            

            

                
                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

            

        

            

                276
            

            

                4
            

            

                

            

        

            

                277
            

            

                4
            

            

                
                                self.edges.push((

            

        

            

                278
            

            

                4
            

            

                
                                    vertex_index,

            

        

            

                279
            

            

                4
            

            

                
                                    self.fts.feature_label(transition.label).clone(),

            

        

            

                280
            

            

                4
            

            

                
                                    s_prime_psi,

            

        

            

                281
            

            

                4
            

            

                
                                ));

            

        

            

                282
            

            

                8
            

            

                
                            }

            

        

            

                283
            

            

                
            

            

                
                        }

            

        

            

                284
            

            

                
            

            

                
                    }

            

        

            

                285
            

            

                
            

            

                
                    ModalityOperator::Diamond => {

            

        

            

                286
            

            

                
            

            

                
                        // (s, <a> Ψ) → even, (s', Ψ) for all s' with s -a-> s', 0

            

        

            

                287
            

            

                
            

            

                
                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

            

        

            

                288
            

            

                
            

            

                

            

        

            

                289
            

            

                
            

            

                
                        for transition in self.fts.outgoing_transitions(s) {

            

        

            

                290
            

            

                
            

            

                
                            let action = &self.parsed_labels[*transition.label];

            

        

            

                291
            

            

                
            

            

                

            

        

            

                292
            

            

                
            

            

                
                            if match_regular_formula(formula, action) {

            

        

            

                293
            

            

                
            

            

                
                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

            

        

            

                294
            

            

                
            

            

                

            

        

            

                295
            

            

                
            

            

                
                                self.edges.push((

            

        

            

                296
            

            

                
            

            

                
                                    vertex_index,

            

        

            

                297
            

            

                
            

            

                
                                    self.fts.feature_label(transition.label).clone(),

            

        

            

                298
            

            

                
            

            

                
                                    s_prime_psi,

            

        

            

                299
            

            

                
            

            

                
                                ));

            

        

            

                300
            

            

                
            

            

                
                            }

            

        

            

                301
            

            

                
            

            

                
                        }

            

        

            

                302
            

            

                
            

            

                
                    }

            

        

            

                303
            

            

                
            

            

                
                }

            

        

            

                304
            

            

                
            

            

                
            }

            

        

            

                305
            

            

                
            

            

                
            _ => {

            

        

            

                306
            

            

                
            

            

                
                unimplemented!("Cannot translate formula {}", formula);

            

        

            

                307
            

            

                
            

            

                
            }

            

        

            

                308
            

            

                
            

            

                
        }

            

        

            

                309
            

            

                19
            

            

                
    }

            

        

            

                310
            

            

                
            

            

                

            

        

            

                311
            

            

                
            

            

                
    /// Applies the translation to the given (s, equation) vertex.

            

        

            

                312
            

            

                4
            

            

                
    fn translate_equation(&mut self, s: StateIndex, equation_index: usize, vertex_index: VertexIndex) {

            

        

            

                313
            

            

                4
            

            

                
        let equation = self.equation_system.equation(equation_index);

            

        

            

                314
            

            

                4
            

            

                
        match equation.operator() {

            

        

            

                315
            

            

                3
            

            

                
            FixedPointOperator::Least => {

            

        

            

                316
            

            

                3
            

            

                
                // (s, μ X. Ψ) →_P odd, (s, Ψ[x := μ X. Ψ]), 2 * floor(AD(Ψ)/2) + 1. In Rust division is already floor.

            

        

            

                317
            

            

                3
            

            

                
                self.vertices[vertex_index] = (

            

        

            

                318
            

            

                3
            

            

                
                    Player::Odd,

            

        

            

                319
            

            

                3
            

            

                
                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2) + 1),

            

        

            

                320
            

            

                3
            

            

                
                );

            

        

            

                321
            

            

                3
            

            

                
                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

            

        

            

                322
            

            

                3
            

            

                
                self.edges.push((vertex_index, self.true_bdd.clone(), s_psi));

            

        

            

                323
            

            

                3
            

            

                
            }

            

        

            

                324
            

            

                1
            

            

                
            FixedPointOperator::Greatest => {

            

        

            

                325
            

            

                1
            

            

                
                // (s, ν X. Ψ) →_P even, (s, Ψ[x := ν X. Ψ]), 2 * (AD(Ψ)/2). In Rust division is already floor.

            

        

            

                326
            

            

                1
            

            

                
                self.vertices[vertex_index] = (

            

        

            

                327
            

            

                1
            

            

                
                    Player::Even,

            

        

            

                328
            

            

                1
            

            

                
                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2)),

            

        

            

                329
            

            

                1
            

            

                
                );

            

        

            

                330
            

            

                1
            

            

                
                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

            

        

            

                331
            

            

                1
            

            

                
                self.edges.push((vertex_index, self.true_bdd.clone(), s_psi));

            

        

            

                332
            

            

                1
            

            

                
            }

            

        

            

                333
            

            

                
            

            

                
        }

            

        

            

                334
            

            

                4
            

            

                
    }

            

        

            

                335
            

            

                
            

            

                

            

        

            

                336
            

            

                
            

            

                
    /// Queues a new pair to be translated, returning its vertex index.

            

        

            

                337
            

            

                24
            

            

                
    fn queue_vertex(&mut self, s: StateIndex, formula: Formula<'a>) -> VertexIndex {

            

        

            

                338
            

            

                24
            

            

                
        let (index, inserted) = self.vertex_map.insert((s, formula.clone()));

            

        

            

                339
            

            

                24
            

            

                
        let vertex_index = VertexIndex::new(*index);

            

        

            

                340
            

            

                
            

            

                

            

        

            

                341
            

            

                24
            

            

                
        if inserted {

            

        

            

                342
            

            

                22
            

            

                
            // New vertex, assign placeholder values

            

        

            

                343
            

            

                22
            

            

                
            self.vertices.resize(*vertex_index + 1, (Player::Odd, Priority::new(0)));

            

        

            

                344
            

            

                22
            

            

                
            self.queue.push((s, formula, vertex_index));

            

        

            

                345
            

            

                22
            

            

                
        }

            

        

            

                346
            

            

                
            

            

                

            

        

            

                347
            

            

                24
            

            

                
        vertex_index

            

        

            

                348
            

            

                24
            

            

                
    }

            

        

            

                349
            

            

                
            

            

                
}

            

        

            

                350
            

            

                
            

            

                

            

        

            

                351
            

            

                
            

            

                
/// Removes the BDD information from the multi-action, i.e., only keeps the action labels.

            

        

            

                352
            

            

                5
            

            

                
fn strip_feature_configuration_from_multi_action(multi_action: &MultiAction) -> MultiAction {

            

        

            

                353
            

            

                
            

            

                
    MultiAction {

            

        

            

                354
            

            

                5
            

            

                
        actions: multi_action

            

        

            

                355
            

            

                5
            

            

                
            .actions

            

        

            

                356
            

            

                5
            

            

                
            .iter()

            

        

            

                357
            

            

                5
            

            

                
            .map(|action| Action {

            

        

            

                358
            

            

                5
            

            

                
                id: action.id.clone(),

            

        

            

                359
            

            

                5
            

            

                
                args: Vec::new(),

            

        

            

                360
            

            

                5
            

            

                
            })

            

        

            

                361
            

            

                5
            

            

                
            .collect(),

            

        

            

                362
            

            

                
            

            

                
    }

            

        

            

                363
            

            

                5
            

            

                
}

            

        

            

                364
            

            

                
            

            

                

            

        

            

                365
            

            

                
            

            

                
/// Returns true iff the given action matches the regular formula.

            

        

            

                366
            

            

                12
            

            

                
fn match_regular_formula(formula: &RegFrm, action: &MultiAction) -> bool {

            

        

            

                367
            

            

                12
            

            

                
    match formula {

            

        

            

                368
            

            

                12
            

            

                
        RegFrm::Action(action_formula) => match_action_formula(action_formula, action),

            

        

            

                369
            

            

                
            

            

                
        RegFrm::Choice { lhs, rhs } => match_regular_formula(lhs, action) || match_regular_formula(rhs, action),

            

        

            

                370
            

            

                
            

            

                
        _ => {

            

        

            

                371
            

            

                
            

            

                
            unimplemented!("Cannot translate regular formula {}", formula);

            

        

            

                372
            

            

                
            

            

                
        }

            

        

            

                373
            

            

                
            

            

                
    }

            

        

            

                374
            

            

                12
            

            

                
}

            

        

            

                375
            

            

                
            

            

                

            

        

            

                376
            

            

                
            

            

                
/// Returns true iff the given action matches the action formula.

            

        

            

                377
            

            

                12
            

            

                
fn match_action_formula(formula: &ActFrm, action: &MultiAction) -> bool {

            

        

            

                378
            

            

                12
            

            

                
    match formula {

            

        

            

                379
            

            

                
            

            

                
        ActFrm::True => true,

            

        

            

                380
            

            

                
            

            

                
        ActFrm::False => false,

            

        

            

                381
            

            

                12
            

            

                
        ActFrm::MultAct(expected_action) => expected_action == action,

            

        

            

                382
            

            

                
            

            

                
        ActFrm::Binary { op, lhs, rhs } => match op {

            

        

            

                383
            

            

                
            

            

                
            ActFrmBinaryOp::Union => match_action_formula(lhs, action) || match_action_formula(rhs, action),

            

        

            

                384
            

            

                
            

            

                
            ActFrmBinaryOp::Intersect => match_action_formula(lhs, action) && match_action_formula(rhs, action),

            

        

            

                385
            

            

                
            

            

                
            _ => {

            

        

            

                386
            

            

                
            

            

                
                unimplemented!("Cannot translate binary operator {}", formula);

            

        

            

                387
            

            

                
            

            

                
            }

            

        

            

                388
            

            

                
            

            

                
        },

            

        

            

                389
            

            

                
            

            

                
        ActFrm::Negation(expr) => !match_action_formula(expr, action),

            

        

            

                390
            

            

                
            

            

                
        _ => {

            

        

            

                391
            

            

                
            

            

                
            unimplemented!("Cannot translate action formula {}", formula);

            

        

            

                392
            

            

                
            

            

                
        }

            

        

            

                393
            

            

                
            

            

                
    }

            

        

            

                394
            

            

                12
            

            

                
}

            

        

            

                395
            

            

                
            

            

                

            

        

            

                396
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                397
            

            

                
            

            

                
mod tests {

            

        

            

                398
            

            

                
            

            

                
    use merc_macros::merc_test;

            

        

            

                399
            

            

                
            

            

                
    use merc_syntax::UntypedStateFrmSpec;

            

        

            

                400
            

            

                
            

            

                

            

        

            

                401
            

            

                
            

            

                
    use crate::FeatureDiagram;

            

        

            

                402
            

            

                
            

            

                
    use crate::read_fts;

            

        

            

                403
            

            

                
            

            

                

            

        

            

                404
            

            

                
            

            

                
    use super::*;

            

        

            

                405
            

            

                
            

            

                

            

        

            

                406
            

            

                
            

            

                
    #[merc_test]

            

        

            

                407
            

            

                
            

            

                
    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

            

        

            

                408
            

            

                
            

            

                
    fn test_running_example() {

            

        

            

                409
            

            

                
            

            

                
        let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

            

        

            

                410
            

            

                
            

            

                

            

        

            

                411
            

            

                
            

            

                
        let fd = FeatureDiagram::from_reader(

            

        

            

                412
            

            

                
            

            

                
            &manager_ref,

            

        

            

                413
            

            

                
            

            

                
            include_bytes!("../../../examples/vpg/running_example_fts.fd") as &[u8],

            

        

            

                414
            

            

                
            

            

                
        )

            

        

            

                415
            

            

                
            

            

                
        .unwrap();

            

        

            

                416
            

            

                
            

            

                
        let fts = read_fts(

            

        

            

                417
            

            

                
            

            

                
            &manager_ref,

            

        

            

                418
            

            

                
            

            

                
            include_bytes!("../../../examples/vpg/running_example_fts.aut") as &[u8],

            

        

            

                419
            

            

                
            

            

                
            fd.features().clone(),

            

        

            

                420
            

            

                
            

            

                
        )

            

        

            

                421
            

            

                
            

            

                
        .unwrap();

            

        

            

                422
            

            

                
            

            

                

            

        

            

                423
            

            

                
            

            

                
        let formula = UntypedStateFrmSpec::parse(include_str!("../../../examples/vpg/running_example.mcf")).unwrap();

            

        

            

                424
            

            

                
            

            

                

            

        

            

                425
            

            

                
            

            

                
        let _vpg = translate_vpg(&manager_ref, &fts, fd.configuration().clone(), &formula.formula).unwrap();

            

        

            

                426
            

            

                
            

            

                
    }

            

        

            

                427
            

            

                
            

            

                
}