//! Authors: Maurice Laveaux and Sjef van Loo

use std::collections::HashMap;

use std::fmt;

use std::io::BufRead;

use std::io::BufReader;

use std::io::Read;

use log::debug;

use oxidd::BooleanFunction;

use oxidd::Manager;

use oxidd::ManagerRef;

use oxidd::bdd::BDDFunction;

use oxidd::bdd::BDDManagerRef;

use merc_lts::LabelIndex;

use merc_lts::LabelledTransitionSystem;

use merc_lts::LTS;

use merc_lts::read_aut;

use merc_lts::StateIndex;

use merc_lts::Transition;

use merc_lts::TransitionLabel;

use merc_symbolic::FormatConfigSet;

use merc_syntax::DataExpr;

use merc_syntax::MultiAction;

use merc_utilities::MercError;

/// Reads a .aut file as feature transition system by using the associated

/// feature diagram.

///

/// # Details

///

/// The action labels of a feature transition system are annotated with a

/// special `BDD` struct that is defined as:

///

/// > `struct BDD = node(var, true, false) | tt | ff`

///

/// The `features` map contains the mapping from variable names to their

/// corresponding BDD variable, which *must* be defined in the BDD manager.

    // Read the underlying LTS, where the labels are in plain text

    // Parse the labels as data expressions

            } else {

            }

        } else {

            // This is the tau action, is always enabled.

        }

    }

    // Find the associated feature for each label and relabel the LTS accordingly.

/// Converts the given data expression into a BDD function.

///

/// The input should be a data expression of the shape: expr = node(var, expr, expr) | tt | ff.

                // A node must be of the shape 'node(var, true_branch, false_branch)'

                    } else {

                    }

                }

            }

        }

            // Deal with the base cases.

            }

        }

    }

/// A feature diagram represented as a BDD.

pub struct FeatureDiagram {

    /// The mapping from feature names to their BDD variable.

    features: HashMap<String, BDDFunction>,

    /// The feature names in the order they are defined in the input.

    feature_names: Vec<String>,

    /// Stores the set of products as a BDD function.

    configuration: BDDFunction,

}

impl FeatureDiagram {

    /// Reads feature diagram from the input.

    ///

    /// # Details

    ///

    /// The first line is a list of variable names, separated by commas. The

    /// second line is the initial configuration, represented as a data

    /// expression. This function will initialize the BDD manager with the

    /// variables read from the first line, and assumes that the manager has no

    /// variables yet defined.

                0,

                "A BDD manager can only hold the variables for a single feature diagram"

            )

    /// Returns the configuration of the feature diagram.

    /// Returns the feature variables used in the feature diagram.

    /// Returns the feature names used in the feature diagram, in the order they are defined in the input.

}

impl fmt::Debug for FeatureDiagram {

}

/// A feature transition system, i.e., a labelled transition system

/// where each label is associated with a feature expression.

pub struct FeatureTransitionSystem<L: TransitionLabel> {

    /// The underlying labelled transition system.

    lts: LabelledTransitionSystem<FeaturedLabel<L>>,

    /// The features associated with this feature transition system.

    features: HashMap<String, BDDFunction>,

}

impl<L: TransitionLabel> FeatureTransitionSystem<L> {

    /// Creates a new feature transition system.

    /// Returns the features used in the feature diagram.

}

/// A transition label associated with a feature expression.

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

pub struct FeaturedLabel<L: TransitionLabel> {

    label: L,

    feature_expr: BDDFunction,

}

impl<L: TransitionLabel> FeaturedLabel<L> {

    /// Creates a new featured label with the given label and feature expression.

    /// Returns the label of this featured label.

    /// Returns the feature expression of this featured label.

}

impl<L: TransitionLabel> TransitionLabel for FeaturedLabel<L> {

    delegate::delegate! {

        to self.label {

        }

    }

    }

        // TODO: This is annoying, but we need a BDDManager to create the

        // feature label. Perhaps this should be refactored to not require the

        // tau label to be a constant.

    }

}

impl<L: TransitionLabel> fmt::Debug for FeaturedLabel<L> {

}

impl<L: TransitionLabel> fmt::Display for FeaturedLabel<L> {

        // This is also used for the output in .aut format, so should be valid labels.

}

impl<L: TransitionLabel> LTS for FeatureTransitionSystem<L> {

    type Label = FeaturedLabel<L>;

    }

    delegate::delegate! {

        to self.lts {

        }

    }

}

#[cfg(test)]

mod tests {

    use merc_macros::merc_test;

    use super::*;

    #[merc_test]

    #[cfg_attr(miri, ignore)] // Oxidd does not support miri (specifically the crossbeam-epoch dependency)

    fn test_read_minepump_fts() {

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

        let feature_diagram = FeatureDiagram::from_reader(

            &manager_ref,

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

        )

        .unwrap();

        let _result = read_fts(

            &manager_ref,

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

            feature_diagram.features,

        )

        .unwrap();

    }

}