Grcov report - ltsconvert

1

use std::fs::File;

2

use std::path::Path;

3

use std::process::Command;

4

5

use log::info;

6

use merc_lts::LTS;

7

use merc_lts::random_lts;

8

use merc_lts::reachable_lts;

9

use merc_lts::read_mcrl2_aut;

10

use merc_lts::write_mcrl2_aut;

11

use merc_reduction::Equivalence;

12

use merc_reduction::compare_lts;

13

use merc_reduction::reduce_lts;

14

use merc_utilities::Timing;

15

use merc_utilities::random_test;

16

17

/// Compares our reduction against mCRL2's `ltsconvert` on random inputs.

18

7

fn test_mcrl2_sigref_vs_ltsconvert(name: &str, equivalence: Equivalence, argument: &str) {

19

7

    let Ok(mcrl2_path) = std::env::var("MCRL2_PATH") else {

20

7

        println!("Skipping test: MCRL2_PATH not set");

21

7

        return;

22

};

23

24

    let ltsconvert = Path::new(&mcrl2_path).join("ltsconvert");

25

26

    // Write the random LTS to a temp file for ltsconvert to process.

27

    let temp_dir = tempfile::tempdir().unwrap();

28

    let input_path = temp_dir.path().join("input.aut");

29

    let output_path = temp_dir.path().join("output.aut");

30

31

    random_test(100, |rng| {

32

        let mut files = merc_io::DumpFiles::new(name);

33

34

        // ltsconvert only works on the reachable part, so restrict our random LTS as well.

35

        let lts = reachable_lts(&random_lts::<String, _>(rng, 10, 3));

36

        info!(

37

            "Generated random LTS with {} states and {} transitions",

38

            lts.num_of_states(),

39

            lts.num_of_transitions()

40

);

41

42

        let mut input_file = File::create(&input_path).unwrap();

43

        write_mcrl2_aut(&mut input_file, &lts).unwrap();

44

        files.dump("input.aut", |writer| write_mcrl2_aut(writer, &lts)).unwrap();

45

46

        let status = Command::new(&ltsconvert)

47

            .arg(format!("-e{}", argument))

48

            .arg(&input_path)

49

            .arg(&output_path)

50

            .status()

51

            .expect("Failed to run ltsconvert");

52

        assert!(status.success(), "ltsconvert failed with status: {status}");

53

54

        let ltsconvert_reduced = read_mcrl2_aut(File::open(&output_path).unwrap()).unwrap();

55

56

        let mut timing = Timing::new();

57

        let our_reduced = reduce_lts(lts, equivalence, false, &timing);

58

59

        files

60

            .dump("reduced.aut", |writer| write_mcrl2_aut(writer, &our_reduced))

61

            .unwrap();

62

        files

63

            .dump("ltsconvert_reduced.aut", |writer| {

64

                write_mcrl2_aut(writer, &ltsconvert_reduced)

65

})

66

            .unwrap();

67

68

        assert!(

69

            compare_lts(

70

                Equivalence::StrongBisim,

71

                our_reduced,

72

                ltsconvert_reduced,

73

                false,

74

                &mut timing

75

),

76

            "The reduced LTSs are not strongly bisimilar"

77

);

78

79

        // assert_eq!(

80

        //     our_reduced.num_of_states(),

81

        //     ltsconvert_reduced.num_of_states(),

82

        //     "Number of states differs",

83

        // );

84

        // assert_eq!(

85

        //     our_reduced.num_of_transitions(),

86

        //     ltsconvert_reduced.num_of_transitions(),

87

        //     "Number of transitions differs",

88

        // );

89

});

90

7

91

92

#[test]

93

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

94

1

fn test_mcrl2_branching_bisim_sigref_vs_ltsconvert() {

95

1

    test_mcrl2_sigref_vs_ltsconvert(

96

1

        "test_mcrl2_branching_bisim_sigref_vs_ltsconvert",

97

1

        Equivalence::BranchingBisim,

98

1

        "branching-bisim",

99

);

100

1

101

102

#[test]

103

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

104

1

fn test_mcrl2_divergence_preserving_branching_bisim_sigref_vs_ltsconvert() {

105

1

    test_mcrl2_sigref_vs_ltsconvert(

106

1

        "test_mcrl2_divergence_preserving_branching_bisim_sigref_vs_ltsconvert",

107

1

        Equivalence::BranchingBisimDivergencePreserving,

108

1

        "dpbranching-bisim",

109

);

110

1

111

112

#[test]

113

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

114

1

fn test_mcrl2_strong_bisim_sigref_vs_ltsconvert() {

115

1

    test_mcrl2_sigref_vs_ltsconvert(

116

1

        "test_mcrl2_strong_bisim_sigref_vs_ltsconvert",

117

1

        Equivalence::StrongBisim,

118

1

        "bisim",

119

);

120

1

121

122

#[test]

123

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

124

1

fn test_mcrl2_weak_bisim_sigref_vs_ltsconvert() {

125

1

    test_mcrl2_sigref_vs_ltsconvert(

126

1

        "test_mcrl2_weak_bisim_sigref_vs_ltsconvert",

127

1

        Equivalence::WeakBisim,

128

1

        "weak-bisim",

129

);

130

1

131

132

#[test]

133

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

134

1

fn test_mcrl2_divergence_preserving_weak_bisim_sigref_vs_ltsconvert() {

135

1

    test_mcrl2_sigref_vs_ltsconvert(

136

1

        "test_mcrl2_divergence_preserving_weak_bisim_sigref_vs_ltsconvert",

137

1

        Equivalence::WeakBisimDivergencePreserving,

138

1

        "dpweak-bisim",

139

);

140

1

141

142

#[test]

143

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

144

1

fn test_mcrl2_weak_bisimulation_vs_ltsconvert() {

145

1

    test_mcrl2_sigref_vs_ltsconvert(

146

1

        "test_mcrl2_weak_bisimulation_vs_ltsconvert",

147

1

        Equivalence::WeakBisim,

148

1

        "weak-bisim",

149

);

150

1

151

152

#[test]

153

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

154

1

fn test_mcrl2_divergence_preserving_weak_bisimulation_vs_ltsconvert() {

155

1

    test_mcrl2_sigref_vs_ltsconvert(

156

1

        "test_mcrl2_divergence_preserving_weak_bisimulation_vs_ltsconvert",

157

1

        Equivalence::WeakBisimDivergencePreserving,

158

1

        "dpweak-bisim",

159

);

160

1