#![forbid(unsafe_code)]

use std::borrow::Borrow;

use std::collections::HashMap;

use std::fmt;

use std::hash::Hash;

use merc_collections::ByteCompressedVec;

use merc_collections::CompressedEntry;

use merc_utilities::MercError;

use crate::LabelIndex;

use crate::LabelledTransitionSystem;

use crate::StateIndex;

use crate::TransitionLabel;

/// A trait for building labelled transition systems incrementally.

///

/// # Details

///

/// Depending on the implementation this can be done in a memory efficient way,

/// or in a way that is optimized for speed. Alternatively, the resulting LTS is

/// immediately written to disk. The builder accumulates transitions using

/// `add_transition`, and once all transitions have been added, the labelled

/// transition system can be constructed with `finish`. An initial state can

/// also be specified during finalization.

pub trait LtsBuilder<L: TransitionLabel> {

    /// The result type of the builder once finalized.

    type LTS;

    /// Adds a transition to the builder. For efficiency reasons, we can use

    /// another type `Q` for the label.

    fn add_transition<Q>(&mut self, from: StateIndex, label: &Q, to: StateIndex) -> Result<(), MercError>

    where

        L: Borrow<Q>,

        Q: ?Sized + ToOwned<Owned = L> + Eq + Hash;

    /// Finalizes the builder and returns the constructed labelled transition system.

    fn finish(&mut self, initial_state: StateIndex) -> Result<Self::LTS, MercError>;

    /// Returns the number of transitions added to the builder.

    fn num_of_transitions(&self) -> usize;

    /// Returns the number of states added to the builder.

    fn num_of_states(&self) -> usize;

}

/// This struct helps in building a labelled transition system by accumulating

/// transitions in a memory efficient way.

///

/// # Details

///

/// Transitions can be added with `add_transition`, and once all transitions

/// have been added, the labelled transition system can be constructed with

/// `finish`. An initial state can also be specified during finalization.

///

pub struct LtsBuilderMem<L> {

    transition_from: ByteCompressedVec<StateIndex>,

    transition_labels: ByteCompressedVec<LabelIndex>,

    transition_to: ByteCompressedVec<StateIndex>,

    // This is used to keep track of the label to index mapping.

    labels_index: HashMap<L, LabelIndex>,

    labels: Vec<L>,

    /// The hidden labels that should be mapped to the hidden action.

    hidden_labels: Vec<String>,

    /// The number of states (derived from the transitions).

    num_of_states: usize,

}

impl<L: TransitionLabel> LtsBuilderMem<L> {

    /// Initializes a new empty builder.

    /// Initializes the builder with pre-allocated capacity for states and transitions. The number of labels

    /// can be used when labels are added dynamically.

        // Remove duplicates from the labels.

        // Introduce the fixed 0-indexed tau label.

        // Ensure that all hidden labels are mapped to the tau action.

        }

    /// Ensures that the builder has at least the given number of states.

    /// Returns an iterator over all transitions as (from, label, to) tuples.

}

impl<L: TransitionLabel> LtsBuilder<L> for LtsBuilderMem<L> {

    type LTS = LabelledTransitionSystem<L>;

    {

        } else {

            // Label was not yet added, so add it to the labels and the index.

            } else {

            };

        };

        // Update the number of states.

        ))

}

impl<Label: TransitionLabel> fmt::Debug for LtsBuilderMem<Label> {

        }

}