use itertools::Itertools;

use log::debug;

use log::trace;

use merc_lts::LTS;

use merc_lts::StateIndex;

use merc_reduction::Equivalence;

use merc_reduction::Partition;

use merc_reduction::branching_bisim_sigref;

use merc_reduction::quotient_lts_block;

use merc_reduction::quotient_lts_naive;

use merc_reduction::strong_bisim_sigref;

use merc_reduction::tau_scc_decomposition;

use merc_utilities::Timing;

use crate::CounterExample;

use crate::CounterExampleConstructor;

use crate::ImpossibleFuturesResult;

use crate::InnerCe;

use crate::is_failures_refinement;

use crate::is_impossible_futures_refinement;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

#[cfg_attr(feature = "clap", derive(clap::ValueEnum))]

pub enum RefinementType {

    /// Checks for (strong) trace inclusion, i.e., whether all traces of the implementation are also traces of the specification.

    Trace,

    /// Checks for weak trace inclusion, i.e., whether all weak traces of the implementation are also weak traces of the specification.

    Weaktrace,

    /// Checks for stable failures inclusion, i.e., whether all stable failures of the implementation are also stable failures of the specification.

    StableFailures,

    /// Check for failures-divergences inclusion, i.e., whether all failures and divergences of the implementation are also failures and divergences of the specification.

    FailuresDivergences,

    /// Checks for impossible futures inclusion, i.e., whether all impossible futures of the implementation are also impossible futures of the specification.

    ImpossibleFutures,

}

/// Determines the exploration strategy for the failures refinement algorithm.

///

/// Typically `BFS` is more suited for counter examples, but `DFS` can be more efficient

/// in practice when a counter example is not required.

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

pub enum ExplorationStrategy {

    /// Breadth-first search; better suited for finding short counter examples.

    BFS,

    /// Depth-first search; often uses less memory when no counter example is required.

    DFS,

}

/// Checks whether `impl_lts` refines `spec_lts` according to the given

/// `refinement` relation.

///

/// # Details

///

/// The `refinement_type` determines (weak) trace inclusions, failures inclusion

/// and divergence failures inclusion etc.

///

/// The `strategy` parameter determines whether a breadth-first search

/// or depth-first search is used to explore the state space. Breadth-first search

/// is often better suited for finding short counter examples, while depth-first

/// search often uses less memory.

///

/// The `preprocess` flag indicates whether preprocessing should be applied to

/// the LTSs. The refinement checks often involve product constructions, and

/// reducing the state space beforehand can lead to significant performance

/// improvements. However, for quick failing checks the preprocessing could cause

/// unnecessary overhead.

        // Note that for impossible futures we use branching bisimulation, which also removes tau loops.

        RefinementType::StableFailures | RefinementType::FailuresDivergences => {

        }

    };

    // For the preprocessing/quotienting step it makes sense to merge both LTSs

    // together in case that some states are equivalent. So we do this in all branches.

        // Reduce all states in the merged LTS.

            Equivalence::StrongBisim => {

                    // The initial states are already in the same block, so we can skip the refinement check.

                        "Initial states are in the same block after strong bisimulation reduction, skipping refinement check."

                    );

                // After partitioning the block becomes the state in the reduced_lts.

            }

            Equivalence::BranchingBisim | Equivalence::BranchingBisimDivergencePreserving => {

                    // The initial states are already in the same block, so we can skip the refinement check.

                        "Initial states are in the same block after branching bisimulation reduction, skipping refinement check."

                    );

                );

            }

        }

        // For impossible futures we need to remove tau loops from the implementation.

    } else {

    };

    // Print the labels of the merged LTS for debugging purposes.

        "Merged LTS labels: {:?}",

    );

            // Construct a counter example tree, and return a trace.

                RefinementType::Trace

                | RefinementType::Weaktrace

                | RefinementType::StableFailures

                | RefinementType::FailuresDivergences => {

                        // Reconstruct a trace from the counter example tree, relabelling the indices to their actual labels.

                        (

                                RefinementType::StableFailures | RefinementType::FailuresDivergences => {

                                            ),

                                        }

                                    } else {

                                        // The stable failures failed because of a weak trace difference.

                                    }

                                }

                            }),

                        )

                    } else {

                    }

                }

                RefinementType::ImpossibleFutures => {

                    let ImpossibleFuturesResult {

                        // Reconstruct a trace from the counter example tree, relabelling the indices to their actual labels.

                        (

                            } else {

                                // The impossible futures failed because of a weak trace.

                            }),

                        )

                    } else {

                    }

                }

            };

        } else {

            // Run without constructing a counter example.

                RefinementType::Trace

                | RefinementType::Weaktrace

                | RefinementType::StableFailures

                | RefinementType::FailuresDivergences => {

                }

                RefinementType::ImpossibleFutures => {

                }

            }

        }

#[cfg(test)]

mod tests {

    use std::fs::File;

    use std::path::Path;

    use std::process::Command;

    use merc_io::DumpFiles;

    use merc_lts::mutate_lts;

    use merc_lts::random_lts;

    use merc_lts::write_mcrl2_aut;

    use merc_utilities::Timing;

    use merc_utilities::random_test;

    use crate::ExplorationStrategy;

    use crate::RefinementType;

    use crate::refines;

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow

        );

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow

        );

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow

        );

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow

        );

    /// Compares our approach to the one implemented in mCRL2's ltscompare

        };

        // Write the random LTS to a temp file for ltscompare to process.

            // Reduce the LTS using ltsconvert with branching bisimulation.

                "ltscompare failed with status: {}",

                process.status

            );

            // Check that the result is the same.

                expected_result, result,

                "Mismatch between ltsconvert and our implementation"

            );

}