1 
use clap::ValueEnum;
2 
use merc_lts::LTS;
3 
use merc_utilities::Timing;
4 

            

        

            

                5
            

            

                
            

            

                
use crate::ExplorationStrategy;

            

        

            

                6
            

            

                
            

            

                
use crate::is_failures_refinement;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
#[derive(Clone, Copy, Debug, ValueEnum)]

            

        

            

                9
            

            

                
            

            

                
pub enum RefinementType {

            

        

            

                10
            

            

                
            

            

                
    Trace,

            

        

            

                11
            

            

                
            

            

                
}

            

        

            

                12
            

            

                
            

            

                

            

        

            

                13
            

            

                
            

            

                
pub fn refines<L: LTS>(impl_lts: L, spec_lts: L, preorder: RefinementType, timing: &mut Timing) -> bool {

            

        

            

                14
            

            

                
            

            

                
    match preorder {

            

        

            

                15
            

            

                
            

            

                
        RefinementType::Trace => is_failures_refinement::<L, false>(

            

        

            

                16
            

            

                
            

            

                
            impl_lts,

            

        

            

                17
            

            

                
            

            

                
            spec_lts,

            

        

            

                18
            

            

                
            

            

                
            RefinementType::Trace,

            

        

            

                19
            

            

                
            

            

                
            ExplorationStrategy::BFS,

            

        

            

                20
            

            

                
            

            

                
            false,

            

        

            

                21
            

            

                
            

            

                
            timing,

            

        

            

                22
            

            

                
            

            

                
        ),

            

        

            

                23
            

            

                
            

            

                
    }

            

        

            

                24
            

            

                
            

            

                
}