Grcov report - compare.rs

1

#![forbid(unsafe_code)]

2

3

use merc_lts::LTS;

4

use merc_utilities::Timing;

5

6

use crate::Equivalence;

7

use crate::Partition;

8

use crate::branching_bisim_sigref;

9

use crate::branching_bisim_sigref_naive;

10

use crate::strong_bisim_sigref;

11

use crate::strong_bisim_sigref_naive;

12

use crate::weak_bisim_sigref_inductive_naive;

13

use crate::weak_bisim_sigref_naive;

14

use crate::weak_bisimulation;

15

use crate::weak_bisimulation_parallel;

16

17

// Compare two LTSs for equivalence using the given algorithm.

18

1100

pub fn compare_lts<L: LTS>(equivalence: Equivalence, left: L, right: L, preprocess: bool, timing: &mut Timing) -> bool {

19

1100

    let (merged, rhs_initial) = timing.measure("merge lts", || left.merge_disjoint(&right));

20

1100

    drop(right); // No longer needed.

21

22

    // Reduce the merged LTS modulo the given equivalence and return the partition

23

1100

    match equivalence {

24

        Equivalence::WeakBisim => {

25

100

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

26

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

27

28

        Equivalence::WeakBisimParallel => {

29

100

            let (lts, rhs_initial, partition) = weak_bisimulation_parallel(merged, rhs_initial, preprocess, timing);

30

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

31

32

        Equivalence::WeakBisimSigref => {

33

100

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

34

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

35

36

        Equivalence::WeakBisimSigrefNaive => {

37

100

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

38

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

39

40

        Equivalence::StrongBisim => {

41

400

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

42

400

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

43

44

        Equivalence::StrongBisimNaive => {

45

100

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

46

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

47

48

        Equivalence::BranchingBisim => {

49

100

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

50

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

51

52

        Equivalence::BranchingBisimNaive => {

53

100

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

54

100

            partition.block_number(lts.initial_state_index()) == partition.block_number(rhs_initial)

55

56

57

1100

58

59

#[cfg(test)]

60

mod tests {

61

    use merc_io::DumpFiles;

62

    use merc_lts::LTS;

63

    use merc_lts::LabelledTransitionSystem;

64

    use merc_lts::StateIndex;

65

    use merc_lts::random_lts;

66

    use merc_lts::write_aut;

67

    use merc_utilities::Timing;

68

    use merc_utilities::random_test;

69

    use rand::seq::IndexedRandom;

70

71

    use crate::compare;

72

    use crate::compare_lts;

73

74

    #[test]

75

    #[cfg_attr(miri, ignore)] // Test is too slow under miri

76

1

    fn test_random_lts_permutation() {

77

100

        random_test(100, |rng| {

78

100

            let mut timing = Timing::new();

79

100

            let mut files = DumpFiles::new("test_random_lts_permutation");

80

81

100

            let lts = random_lts(rng, 10, 3, 3);

82

100

            files.dump("input.aut", |w| write_aut(w, &lts)).unwrap();

83

84

            // Generate a random permutation of the state indices.

85

100

            let permutation = (0..lts.num_of_states())

86

100

                .collect::<Vec<_>>()

87

100

                .sample(rng, lts.num_of_states())

88

1038

                .map(|state| StateIndex::new(*state))

89

100

                .collect::<Vec<_>>();

90

91

100

            println!("Permutation: {:?}", permutation);

92

93

3178

            let permuted_lts = LabelledTransitionSystem::new_from_permutation(lts.clone(), |i| permutation[i]);

94

100

            files.dump("permuted.aut", |w| write_aut(w, &permuted_lts)).unwrap();

95

96

            // Check that the original and permuted LTS are bisimilar.

97

100

            assert!(compare_lts(

98

100

                compare::Equivalence::StrongBisim,

99

100

                lts,

100

                permuted_lts,

101

                false,

102

100

                &mut timing

103

));

104

100

})

105

1

106