1 
#![forbid(unsafe_code)]
2 

            

        

            

                3
            

            

                
            

            

                
use merc_lts::LTS;

            

        

            

                4
            

            

                
            

            

                
use merc_lts::LabelledTransitionSystem;

            

        

            

                5
            

            

                
            

            

                
use merc_utilities::Timing;

            

        

            

                6
            

            

                
            

            

                

            

        

            

                7
            

            

                
            

            

                
use crate::branching_bisim_sigref;

            

        

            

                8
            

            

                
            

            

                
use crate::branching_bisim_sigref_naive;

            

        

            

                9
            

            

                
            

            

                
use crate::quotient_lts_block;

            

        

            

                10
            

            

                
            

            

                
use crate::quotient_lts_naive;

            

        

            

                11
            

            

                
            

            

                
use crate::strong_bisim_sigref;

            

        

            

                12
            

            

                
            

            

                
use crate::strong_bisim_sigref_naive;

            

        

            

                13
            

            

                
            

            

                
use crate::weak_bisim_sigref_inductive_naive;

            

        

            

                14
            

            

                
            

            

                
use crate::weak_bisim_sigref_naive;

            

        

            

                15
            

            

                
            

            

                
use crate::weak_bisimulation;

            

        

            

                16
            

            

                
            

            

                

            

        

            

                17
            

            

                
            

            

                
#[derive(Copy, Clone, Debug)]

            

        

            

                18
            

            

                
            

            

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

            

        

            

                19
            

            

                
            

            

                
pub enum Equivalence {

            

        

            

                20
            

            

                
            

            

                
    /// Partition based refinement algorithms.

            

        

            

                21
            

            

                
            

            

                
    WeakBisim,

            

        

            

                22
            

            

                
            

            

                
    /// Various signature based reduction algorithms.

            

        

            

                23
            

            

                
            

            

                
    WeakBisimSigref,

            

        

            

                24
            

            

                
            

            

                
    WeakBisimSigrefNaive,

            

        

            

                25
            

            

                
            

            

                
    StrongBisim,

            

        

            

                26
            

            

                
            

            

                
    StrongBisimNaive,

            

        

            

                27
            

            

                
            

            

                
    BranchingBisim,

            

        

            

                28
            

            

                
            

            

                
    BranchingBisimNaive,

            

        

            

                29
            

            

                
            

            

                
}

            

        

            

                30
            

            

                
            

            

                

            

        

            

                31
            

            

                
            

            

                
/// Reduces the given LTS modulo the given equivalence using signature refinement

            

        

            

                32
            

            

                300
            

            

                
pub fn reduce_lts<L: LTS>(

            

        

            

                33
            

            

                300
            

            

                
    lts: L,

            

        

            

                34
            

            

                300
            

            

                
    equivalence: Equivalence,

            

        

            

                35
            

            

                300
            

            

                
    preprocess: bool,

            

        

            

                36
            

            

                300
            

            

                
    timing: &Timing,

            

        

            

                37
            

            

                300
            

            

                
) -> LabelledTransitionSystem<L::Label> {

            

        

            

                38
            

            

                300
            

            

                
    match equivalence {

            

        

            

                39
            

            

                
            

            

                
        Equivalence::WeakBisim => {

            

        

            

                40
            

            

                100
            

            

                
            let (lts, partition) = weak_bisimulation(lts, preprocess, timing);

            

        

            

                41
            

            

                100
            

            

                
            timing.measure("quotient", || quotient_lts_naive(&lts, &partition, true))

            

        

            

                42
            

            

                
            

            

                
        }

            

        

            

                43
            

            

                
            

            

                
        Equivalence::WeakBisimSigref => {

            

        

            

                44
            

            

                100
            

            

                
            let (lts, partition) = weak_bisim_sigref_inductive_naive(lts, preprocess, timing);

            

        

            

                45
            

            

                100
            

            

                
            timing.measure("quotient", || quotient_lts_naive(&lts, &partition, true))

            

        

            

                46
            

            

                
            

            

                
        }

            

        

            

                47
            

            

                
            

            

                
        Equivalence::WeakBisimSigrefNaive => {

            

        

            

                48
            

            

                
            

            

                
            let (lts, partition) = weak_bisim_sigref_naive(lts, preprocess, timing);

            

        

            

                49
            

            

                
            

            

                
            timing.measure("quotient", || quotient_lts_naive(&lts, &partition, true))

            

        

            

                50
            

            

                
            

            

                
        }

            

        

            

                51
            

            

                
            

            

                
        Equivalence::StrongBisim => {

            

        

            

                52
            

            

                100
            

            

                
            let (lts, partition) = strong_bisim_sigref(lts, timing);

            

        

            

                53
            

            

                100
            

            

                
            timing.measure("quotient", || quotient_lts_block::<_, false>(&lts, &partition))

            

        

            

                54
            

            

                
            

            

                
        }

            

        

            

                55
            

            

                
            

            

                
        Equivalence::StrongBisimNaive => {

            

        

            

                56
            

            

                
            

            

                
            let (lts, partition) = strong_bisim_sigref_naive(lts, timing);

            

        

            

                57
            

            

                
            

            

                
            timing.measure("quotient", || quotient_lts_naive(&lts, &partition, false))

            

        

            

                58
            

            

                
            

            

                
        }

            

        

            

                59
            

            

                
            

            

                
        Equivalence::BranchingBisim => {

            

        

            

                60
            

            

                
            

            

                
            let (lts, partition) = branching_bisim_sigref(lts, timing);

            

        

            

                61
            

            

                
            

            

                
            timing.measure("quotient", || quotient_lts_block::<_, true>(&lts, &partition))

            

        

            

                62
            

            

                
            

            

                
        }

            

        

            

                63
            

            

                
            

            

                
        Equivalence::BranchingBisimNaive => {

            

        

            

                64
            

            

                
            

            

                
            let (lts, partition) = branching_bisim_sigref_naive(lts, timing);

            

        

            

                65
            

            

                
            

            

                
            timing.measure("quotient", || quotient_lts_naive(&lts, &partition, true))

            

        

            

                66
            

            

                
            

            

                
        }

            

        

            

                67
            

            

                
            

            

                
    }

            

        

            

                68
            

            

                300
            

            

                
}