use itertools::Itertools;

use log::info;

use streaming_iterator::StreamingIterator;

use merc_collections::VecBag;

use merc_io::TimeProgress;

use merc_lts::LTS;

use merc_lts::LabelIndex;

use merc_lts::LtsAction;

use merc_lts::LtsBuilder;

use merc_lts::LtsMultiAction;

use merc_lts::SimpleAction;

use merc_lts::StateIndex;

use merc_lts::Transition;

use merc_lts::TransitionLabel;

use merc_syntax::CommExpr;

use merc_syntax::MultiActionLabel;

use merc_utilities::MercError;

use merc_utilities::Timing;

use crate::DiscoveredSet;

use crate::SequenceForestContext;

use crate::StateRef;

/// The trait for labels used in the composition operator.

pub trait CombineLabel: TransitionLabel + Ord {

    /// Returns true iff the data arguments of two actions are compatible for communication.

    /// Defaults to `true` for label types without structured arguments (e.g., `String`).

    /// Creates a new action as the result of a communication expression with the given `label`.

    /// `representative` is one of the matched input actions and provides argument values.

    fn from_comm(label: String, representative: &Self) -> Self;

}

impl CombineLabel for SimpleAction {

}

impl CombineLabel for LtsAction {

}

/// Computes the parallel composition hide(H, allow(A, comm(C, L1 || ... || Ln))).

///

/// The `builder` is used to construct the resulting LTS, which can also be

/// stored immediately in a file.

        // The left hand side of a communication cannot overlap with any other communication's left hand side. This is the definition used in mCRL2,

        // for example a|b -> a is a valid communication expression.

        }

        // The right hand side of a communication cannot be in another communication's left hand side.

        }

    }

    // Keep track of the discovered states in the combined LTS. State vectors

    // are stored as maximally shared sequences of raw `usize` indices in the

    // discovered set; we convert to/from `StateIndex` at the boundary.

        1,

    );

    // Pre-sort the allow set for efficient matching.

    // The working set of states that must still be explored.

    // Reusable buffers for reconstructing the current state vector from the

    // discovered set and for building target vectors prior to insertion.

    // Reused interning scratch buffers, avoiding a reallocation per inserted

    // state. This loop is single-threaded, so one context suffices.

            // Reconstruct the current state vector from the discovered set.

                "StateRef from working set must be valid"

            );

            // Loop over all subsets of LTSs and their outgoing transitions in the current state vector.

            loop {

                };

                // Build the combined multi-action alpha = alpha_{j_0} | ... | alpha_{j_m}.

                }

                // Apply communication: alpha = gamma_C(alpha).

                // Check allow: alpha in A ∪ {tau}.

                // Apply hide: alpha = tau_I(alpha).

                // Convert the target vector into raw indices for the discovered set.

            }

        }

        "Composition complete: {} states, {} transitions",

    );

/// Applies the communication operator to a multi-action according to the given

/// communication expressions.

///

/// # Details

/// Applies the communication operator $\gamma_C$ to a multi-action.

///

/// For each communication expression $a_1 | \cdots | a_n \rightarrow c$ in $C$,

/// repeatedly finds matching sub-multisets of actions (with equal arguments)

/// and replaces them with the result action $c$.

        // Try to find a matching sub-multiset for this communication expression.

    }

/// Tries to find actions matching a single communication expression

/// $a_1 | \cdots | a_n \rightarrow c$ within the given action list.

///

/// Returns the resulting action list with the matched actions replaced by the

/// communicated action, or `None` if no match was found.

    // For each action name in the communication expression's left-hand side,

    // find a matching action with the same label. All matched actions must

    // have the same arguments.

    //

    // We iterate over every candidate for the *first* required name so that we

    // do not greedily commit to a particular argument set.  Once the first

    // action is chosen its arguments fix the constraint for all remaining

    // names, so a single greedy pass over the rest is correct.

        // Attempt to complete the match using actions[first_idx] as the

        // argument reference.

            }

        }

        // Build the result: remove matched actions and add the communicated action.

    }

/// Returns true iff the given multi-action is allowed by the allow operator.

///

/// A multi-action is allowed if:

/// - The action is tau (always allowed), or

/// - The action label names, compared as sorted multisets, match one of the

///   entries in the allow set.

/// Applies the hide operator $\tau_I$ to a multi-action.

///

/// Removes all actions whose label is in the hide set $I$. If all actions are

/// hidden the result is the tau action (empty multi-action).

/// Reusable scratch buffers for [`CartesianProduct`].

///

/// Holding these buffers in a long-lived context avoids re-allocating per

/// iteration.

struct CartesianProductContext {

    /// The length of each factor.

    lengths: Vec<usize>,

    /// Current index into each factor.

    indices: Vec<usize>,

}

impl CartesianProductContext {

    /// Creates a fresh context with empty buffers.

    /// Advances the element by one step.

    ///

    /// Returns `Some(i)` where `i` is the leftmost position that was

    /// incremented (all positions to its right were reset to 0). Returns

    /// `None` when the product is exhausted.

        }

}

impl Default for CartesianProductContext {

}

/// A multi-action label with action names sorted, for proper multiset

/// comparison with [`SortedLtsMultiAction`].

struct SortedMultiActionLabel {

    /// Action names in sorted order.

    actions: Vec<String>,

}

impl SortedMultiActionLabel {

}

/// A view of an [`LtsMultiAction`] for multiset comparison with

/// [`SortedMultiActionLabel`].

///

/// `VecBag<L>` iterates in `L`'s sorted order, this only works if `L`'s `Ord`

/// implementation is consistent with the label-matching logic in `is_allowed`

/// and the communication matching in `find_communication_match`.

struct SortedLtsMultiAction<'a, L: Ord> {

    action: &'a LtsMultiAction<L>,

}

impl<'a, L: TransitionLabel> SortedLtsMultiAction<'a, L> {

        // Check if the L Ord is consistent.

            "LtsMultiAction's internal order must be consistent with the label-matching logic"

        );

}

/// The output of a parallel transition step: label indices from participating

/// LTSs and the combined target state vector.

struct ParallelTransition {

    /// Indices of LTSs participating in this transition's subset.

    pub subset_indices: Vec<usize>,

    /// Label indices from each participating LTS in the current subset.

    pub labels: Vec<LabelIndex>,

    /// Target state vector: for LTSs in the subset, the transition target;

    /// for others, the current state is retained.

    pub target: Vec<StateIndex>,

}

/// Reusable scratch buffers for [`ParallelTransitionIter`].

///

/// Holding these buffers in a long-lived context avoids re-allocating per

/// source state during a single `combine_lts` invocation.

struct ParallelTransitionContext {

    /// Indices of LTSs participating in the current subset.

    subset_indices: Vec<usize>,

    /// Snapshot of the current source state vector (one state per LTS).

    base_target: Vec<StateIndex>,

    /// Current transition for each LTS in `subset_indices`, in the same order.

    current: Vec<Transition>,

    /// Cartesian product context tracking the current offset and length for

    /// each LTS in `subset_indices`, in the same order.

    cartesian_product_context: CartesianProductContext,

    /// Output buffer surfaced via `StreamingIterator::get`.

    result: ParallelTransition,

}

impl ParallelTransitionContext {

    /// Creates a fresh context with empty buffers.

}

impl Default for ParallelTransitionContext {

}

/// A streaming iterator that lazily enumerates all parallel transitions from a

/// given state vector across multiple LTSs.

///

/// For each non-empty subset $J \subseteq \{0, \ldots, n-1\}$ of LTSs,

/// enumerates the Cartesian product of outgoing transitions from the LTSs in

/// $J$ without materialising all outgoing transitions ahead of time. Internal

/// buffers live in a [`ParallelTransitionContext`] that can be reused across

/// many source states.

struct ParallelTransitionIter<'ctx, 'a, L: LTS> {

    ctx: &'ctx mut ParallelTransitionContext,

    lts_list: &'a [L],

    /// Current subset bitmask (1 to 2^n - 1).

    current_subset: usize,

    /// Upper bound for subset enumeration (2^n).

    max_subset: usize,

    done: bool,

    started: bool,

}

impl<'ctx, 'a, L: LTS> ParallelTransitionIter<'ctx, 'a, L> {

    /// Creates a new iterator over parallel transitions for the given LTSs

    /// and current state vector, reusing the buffers held in `ctx`.

            "Number of LTSs exceeds maximum supported for subset enumeration"

        );

            "LTS slice and state vector must have the same length"

        );

        // Reset all reusable buffers while keeping their allocated capacity.

    /// Sets up the Cartesian product context and initial transitions for the

    /// current subset bitmask.

    ///

    /// Returns `true` if the subset has a non-empty Cartesian product (every

    /// participating LTS has at least one outgoing transition from its

    /// current state).

                };

        }

    /// Advances the Cartesian product odometer for the current subset.

    ///

    /// Returns `true` if a new combination is available; `false` if the

    /// subset is exhausted.

        // Advance the shared odometer; get the leftmost position that changed.

        // All positions to its right were reset to 0.

        };

        // Re-fetch transitions only for the positions whose offset changed.

    /// Materialises the next result into the context's output buffer.

}

impl<'a, L: LTS> StreamingIterator for ParallelTransitionIter<'_, 'a, L> {

    type Item = ParallelTransition;

        // Try to advance within the current Cartesian product.

        // Find the next subset with a non-empty Cartesian product.

        }

        } else {

        }

}

#[cfg(test)]

mod tests {

    use merc_collections::VecBag;

    use merc_lts::LtsMultiAction;

    use merc_lts::SimpleAction;

    use merc_syntax::CommExpr;

    use merc_syntax::MultiActionLabel;

    use super::SortedLtsMultiAction;

    use super::SortedMultiActionLabel;

    use super::find_communication_match;

    use super::is_allowed;

        )

    /// Builds the allow set from label-name multisets.

    /// Builds a multi-action from actions; `VecBag` orders them internally.

    /// The allow operator matches on label-name multisets only, independent of

    /// arguments. This locks in the name-primary ordering that [`is_allowed`]

    /// relies on: here `a`'s argument sorts *after* `b`'s, so an argument-first

    /// ordering of the bag would misalign the zip and wrongly reject `{a, b}`.

    #[test]

        // Arguments chosen so an argument-first sort would reorder the names.

        ));

        // Repeated names compare as a multiset, not a set.

        ));

        // A differing length or name is rejected; tau is always allowed.

    /// Regression: when the first candidate for the first required name has

    /// incompatible args, the function must try subsequent candidates.

    ///

    /// Multi-action: a(1) | a(2) | b(2)

    /// Comm: a | b -> c

    ///

    /// Greedy first-pick would choose a(1), then fail to match b because

    /// b(2) has different args.  The correct match is a(2) | b(2) -> c(2).

    #[test]

        // Remaining multi-action: a(1) and c(2)  (a(2) and b(2) consumed)

    /// When all candidates are genuinely incompatible, the function should

    /// still return `None`.

    #[test]

    /// Basic case with no data args still works.

    #[test]

}