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::quotient_lts_weak;

12

use crate::strong_bisim_sigref;

13

use crate::strong_bisim_sigref_naive;

14

use crate::weak_bisim_sigref_inductive_naive;

15

use crate::weak_bisim_sigref_naive;

16

use crate::weak_bisimulation;

17

use crate::weak_bisimulation_parallel;

18

19

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

20

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

21

pub enum Equivalence {

22

    /// An O(|Act|mn) algorithmn for weak bisimulation equivalence.

23

    WeakBisim,

24

    /// An O(|Act|mn) algorithmn for weak bisimulation equivalence that computes |Act| in parallel.

25

    WeakBisimParallel,

26

    /// A variant of the O(|Act|mn) algorithmn for weak bisimulation equivalence that preserves divergence.

27

    #[cfg_attr(feature = "clap", clap(alias = "dp-weak-bisim"))]

28

    /// A variant of the parallel O(|Act|mn) algorithmn for weak bisimulation equivalence that preserves divergence.

29

    WeakBisimDivergencePreserving,

30

    #[cfg_attr(feature = "clap", clap(alias = "dp-weak-bisim-parallel"))]

31

    WeakBisimParallelDivergencePreserving,

32

    /// A signature based weak bisimulation algorithm that uses inductive signatures.

33

    WeakBisimSigref,

34

    /// A naive signature based weak bisimulation algorithm.

35

    WeakBisimSigrefNaive,

36

    /// A signature based weak bisimulation algorithm that uses inductive signatures and preserves divergence.

37

    #[cfg_attr(feature = "clap", clap(alias = "dp-weak-bisim-sigref"))]

38

    WeakBisimSigrefDivergencePreserving,

39

    /// A naive signature based weak bisimulation algorithm that preserves divergence.

40

    #[cfg_attr(feature = "clap", clap(alias = "dp-weak-bisim-sigref-naive"))]

41

    WeakBisimSigrefNaiveDivergencePreserving,

42

    /// A signature based strong bisimulation algorithm.

43

    StrongBisim,

44

    /// A naive signature based strong bisimulation algorithm.

45

    StrongBisimNaive,

46

    /// A signature based branching bisimulation algorithm that uses inductive signatures.

47

    BranchingBisim,

48

    /// A naive signature based branching bisimulation algorithm.

49

    BranchingBisimNaive,

50

    /// A signature based branching bisimulation algorithm that uses inductive signatures and preserves divergence.

51

    #[cfg_attr(feature = "clap", clap(alias = "dp-branching-bisim"))]

52

    BranchingBisimDivergencePreserving,

53

    /// A naive signature based branching bisimulation algorithm that preserves divergence.

54

    #[cfg_attr(feature = "clap", clap(alias = "dp-branching-bisim-naive"))]

55

    BranchingBisimDivergencePreservingNaive,

56

57

58

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

59

1800

pub fn reduce_lts<L: LTS>(

60

1800

    lts: L,

61

1800

    equivalence: Equivalence,

62

1800

    preprocess: bool,

63

1800

    timing: &Timing,

64

1800

) -> LabelledTransitionSystem<L::Label> {

65

1800

    let state = lts.initial_state_index();

66

1800

    match equivalence {

67

        Equivalence::WeakBisim => {

68

300

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

69

300

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

70

71

        Equivalence::WeakBisimDivergencePreserving => {

72

100

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

73

100

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

74

75

        Equivalence::WeakBisimParallel => {

76

200

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

77

200

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

78

79

        Equivalence::WeakBisimParallelDivergencePreserving => {

80

100

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

81

100

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

82

83

        Equivalence::WeakBisimSigref => {

84

200

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

85

200

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

86

87

        Equivalence::WeakBisimSigrefNaive => {

88

100

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

89

100

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

90

91

        Equivalence::WeakBisimSigrefDivergencePreserving => {

92

100

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

93

100

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

94

95

        Equivalence::WeakBisimSigrefNaiveDivergencePreserving => {

96

100

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

97

100

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

98

99

        Equivalence::StrongBisim => {

100

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

101

100

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

102

103

        Equivalence::StrongBisimNaive => {

104

100

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

105

100

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

106

107

        Equivalence::BranchingBisim => {

108

100

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

109

100

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

110

111

        Equivalence::BranchingBisimNaive => {

112

100

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

113

100

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

114

115

        Equivalence::BranchingBisimDivergencePreserving => {

116

100

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

117

100

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

118

119

        Equivalence::BranchingBisimDivergencePreservingNaive => {

120

100

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

121

100

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

122

123

124

1800