Grcov report - reduce.rs

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

use crate::weak_bisimulation_parallel;

17

18

#[derive(Copy, Clone, Debug)]

19

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

20

pub enum Equivalence {

21

    /// Partition based refinement algorithms.

22

    WeakBisim,

23

    WeakBisimParallel,

24

    /// Various signature based reduction algorithms.

25

    WeakBisimSigref,

26

    WeakBisimSigrefNaive,

27

    StrongBisim,

28

    StrongBisimNaive,

29

    BranchingBisim,

30

    BranchingBisimNaive,

31

32

33

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

34

1200

pub fn reduce_lts<L: LTS>(

35

1200

    lts: L,

36

1200

    equivalence: Equivalence,

37

1200

    preprocess: bool,

38

1200

    timing: &Timing,

39

1200

) -> LabelledTransitionSystem<L::Label> {

40

1200

    let state = lts.initial_state_index();

41

1200

    match equivalence {

42

        Equivalence::WeakBisim => {

43

300

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

44

300

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

45

46

        Equivalence::WeakBisimParallel => {

47

200

            let (lts, _, partition) = weak_bisimulation_parallel(lts, state, preprocess, timing);

48

200

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

49

50

        Equivalence::WeakBisimSigref => {

51

200

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

52

200

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

53

54

        Equivalence::WeakBisimSigrefNaive => {

55

100

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

56

100

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

57

58

        Equivalence::StrongBisim => {

59

100

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

60

100

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

61

62

        Equivalence::StrongBisimNaive => {

63

100

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

64

100

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

65

66

        Equivalence::BranchingBisim => {

67

100

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

68

100

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

69

70

        Equivalence::BranchingBisimNaive => {

71

100

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

72

100

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

73

74

75

1200