//! Authors: Jan Friso Groote, Maurice Laveaux, Wieger Wesselink and Tim A.C.

//! Willemse

//!

//! > M. Laveaux, J.F. Groote and T.A.C. Willemse. Correct and Efficient

//! > Antichain Algorithms for Refinement Checking. Logical Methods in Computer

//! > Science 17(1) 2021

//!

//! There are six algorithms. One for trace inclusion, one for failures

//! inclusion and one for failures-divergence inclusion. All algorithms come in

//! a variant with and without internal steps. It is possible to generate a

//! counter transition system in case the inclusion is answered by no.

use std::collections::HashSet;

use std::collections::VecDeque;

use log::trace;

use merc_collections::VecSet;

use merc_lts::LTS;

use merc_lts::StateIndex;

use merc_reduction::Equivalence;

use merc_reduction::Partition;

use merc_reduction::quotient_lts_block;

use merc_reduction::reduce_lts;

use merc_reduction::strong_bisim_sigref;

use merc_utilities::Timing;

use crate::Antichain;

use crate::CounterExample;

use crate::CounterExampleConstructor;

use crate::CounterExampleTree;

use crate::RefinementType;

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

pub enum ExplorationStrategy {

    BFS,

    DFS,

}

/// This function checks using algorithms in the paper mentioned above whether

/// transition system l1 is included in transition system l2.

///

/// # 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.

    };

    // 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.

            // If a counter example is to be generated, we only reduce the

            // specification LTS such that the resulting counter example remains valid.

        } else {

            // Reduce all states in the merged LTS.

                Equivalence::StrongBisim => {

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

                }

            }

        }

    } else {

    };

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

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

                (

                        CounterExample::Trace(

                        )

                    } else {

                        // The resulting trace is a weak trace.

                        CounterExample::WeakTrace(

                        )

                    }),

                )

            } else {

            }

        } else {

            // Run without constructing a counter example.

        }

/// The inner loop for checking refinement.

///

/// # Details

///

/// This is mostly used internally. The `CE` type parameter indicates the type

/// of counter example tree that is used to construct counter examples. If no

/// counter examples are required, this can be set to `()`. Avoiding the cost

/// for keeping track of counter example information.

    // The antichain data structure is used for storing explored states. However, as opposed to a discovered set it

    // allows for pruning additional pairs based on the `antichain` property.

    // Cache used for the tau-closure computations.

        // pop (impl,spec) from working;

        // for all impl-e->impl' do

                    // spec' := spec if e == tau

                } else {

                    // spec' := {s' | exists s in spec. s-e->s'};

                        // For weak trace refinement we need to consider tau-closures s -->* s1 -e-> s2 -*-> s'

                            }

                        }

                    } else {

                        // Otherwise, simply consider direct transitions.

                            }

                        }

                    }

                };

                // if spec' = {} then

                // if antichain_insert(impl,spec') then

                }

        }

    }

/// A cache that is used to reuse allocations during tau-closure computations.

pub struct ClosureCache {

    /// States that are still to be explored.

    working: Vec<StateIndex>,

    /// Set of already visited states.

    visited: HashSet<StateIndex>,

}

impl ClosureCache {

    /// Creates a new closure cache.

}

impl Default for ClosureCache {

}

/// Returns the tau closure for a set of states in the given LTS.

///

/// # Details

///

/// The `states` parameter indicates the initial set of states for which the

/// tau-closure is to be computed. The `extend` parameter indicates whether the

/// closure should include the original states as well. The `cache` parameter is

/// used to avoid repeated allocations.

    // Keep track of states that are already in the closure.

        }

    }

    // Clear the cache for the next use, the working set is empty by now.

#[cfg(test)]

mod tests {

    use merc_io::DumpFiles;

    use merc_lts::random_lts;

    use merc_lts::write_aut;

    use merc_utilities::Timing;

    use merc_utilities::random_test;

    use merc_vpg::solve_zielonka;

    use merc_vpg::translate;

    use crate::ExplorationStrategy;

    use crate::RefinementType;

    use crate::generate_formula;

    use crate::is_failures_refinement;

    #[test]

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

                            "Refinement returned false, but the counter example is not distinguishing."

                        );

                    } else {

                    }

            }

}