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

//! This file contains an implementation of

//! 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 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::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, in the

/// sense of trace inclusions, failures inclusion and divergence failures

/// inclusion.

    };

    // 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 trace remains valid.

        } else {

            // Reduce all states in the merged LTS.

                Equivalence::StrongBisim => {

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

                }

            }

        }

    } else {

    };

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

        // pop (impl,spec) from working;

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

                }

            }

                // if spec' = {} then

        }

    }

#[cfg(test)]

mod tests {

    use merc_io::DumpFiles;

    use merc_lts::random_lts;

    use merc_lts::write_aut;

    use merc_reduction::Equivalence;

    use merc_reduction::reduce_lts;

    use merc_utilities::Timing;

    use merc_utilities::random_test;

    use crate::ExplorationStrategy;

    use crate::RefinementType;

    use crate::is_failures_refinement;

    #[test]

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

                    false,

                ),

                "Strong bisimulation implies trace refinement."

            );

}