Grcov report - combine

1

use std::fs::File;

2

use std::io::Write;

3

use std::path::Path;

4

use std::process::Command;

5

6

use itertools::Itertools;

7

use log::info;

8

use merc_collections::VecBag;

9

use merc_io::temp_dir;

10

use merc_io::traced_command;

11

use merc_lts::LTS;

12

use merc_lts::LtsAction;

13

use merc_lts::LtsBuilderFast;

14

use merc_lts::LtsMultiAction;

15

use merc_lts::StateIndex;

16

use merc_lts::TransitionLabel;

17

use merc_lts::random_lts;

18

use merc_lts::read_lts;

19

use merc_lts::write_mcrl2_aut;

20

use merc_reduction::Equivalence;

21

use merc_reduction::compare_lts;

22

use merc_syntax::CommExpr;

23

use merc_syntax::MultiActionLabel;

24

use merc_utilities::Timing;

25

use merc_utilities::random_test;

26

use rand::RngExt;

27

use rand::seq::IndexedRandom;

28

use rand::seq::IteratorRandom;

29

30

use merc_explore::combine_lts;

31

32

/// Returns a random multi-action label with action names sampled from the given list.

33

fn random_multi_action<R: rand::Rng>(rng: &mut R, actions: &[String], max_size: usize) -> MultiActionLabel {

34

    let max_size = usize::min(actions.len(), max_size);

35

    let size = rng.random_range(0..=max_size);

36

    let selected_actions = actions.sample(rng, size).cloned().collect::<Vec<_>>();

37

    MultiActionLabel::new(selected_actions)

38

39

40

#[test]

41

1

fn test_mcrl2_ltscombine() {

42

1

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

43

1

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

44

1

        return;

45

};

46

47

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

48

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

49

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

50

51

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

52

    let temp_dir = temp_dir("test_mcrl2_ltscombine").unwrap();

53

54

    let spec_path = temp_dir.path().join("spec.mcrl2");

55

    let lps_path = temp_dir.path().join("spec.lps");

56

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

57

58

    // Generate a dummy linear process specification to convert the .aut files to .lts format.

59

    writeln!(&mut File::create(&spec_path).unwrap(), "act a, b, c; init delta;").unwrap();

60

61

    let status = traced_command(Command::new(&mcrl2_mcrl22lps).arg(&spec_path).arg(&lps_path))

62

        .expect("Failed to run ltsconvert");

63

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

64

65

    random_test(100, |rng| {

66

        let left_lts = random_lts::<String, _>(rng, 1000, 3)

67

            .relabel(|label| Ok(LtsMultiAction::new(VecBag::singleton(LtsAction::new(label, vec![])))))

68

            .unwrap();

69

        let right_lts = random_lts::<String, _>(rng, 1000, 3)

70

            .relabel(|label| Ok(LtsMultiAction::new(VecBag::singleton(LtsAction::new(label, vec![])))))

71

            .unwrap();

72

73

        let left_path = temp_dir.path().join("left.aut");

74

        let right_path = temp_dir.path().join("right.aut");

75

        write_mcrl2_aut(&mut File::create(&left_path).unwrap(), &left_lts).unwrap();

76

        write_mcrl2_aut(&mut File::create(&right_path).unwrap(), &right_lts).unwrap();

77

78

        // For mCRL2's ltscombine we need to convert the inputs to the mCRL2 LTS format.

79

        let left_lts_path = temp_dir.path().join("left.lts");

80

        let right_lts_path = temp_dir.path().join("right.lts");

81

        let status = traced_command(

82

            Command::new(&mcrl2_ltsconvert)

83

                .arg("-enone")

84

                .arg(&left_path)

85

                .arg(&left_lts_path)

86

                .arg("-l")

87

                .arg(&lps_path),

88

89

        .expect("Failed to run ltsconvert");

90

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

91

92

        let status = traced_command(

93

            Command::new(&mcrl2_ltsconvert)

94

                .arg("-enone")

95

                .arg(&right_path)

96

                .arg(&right_lts_path)

97

                .arg("-l")

98

                .arg(&lps_path),

99

100

        .expect("Failed to run ltsconvert");

101

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

102

103

        // Allow an arbitrary subset of labels

104

        let labels = left_lts

105

            .labels()

106

            .iter()

107

            .chain(right_lts.labels().iter())

108

            .map(|l| l.to_string())

109

            .filter(|label| !label.is_tau_label())

110

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

111

112

        let num_of_allowed = rng.random_range(0..=labels.len());

113

        let allow = (0..num_of_allowed)

114

            .map(|_| random_multi_action(rng, &labels, 3))

115

            .filter(|a| !a.is_tau_label())

116

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

117

118

        let num_of_hidden = rng.random_range(0..=labels.len());

119

        let hide = labels

120

            .iter()

121

            .filter(|a| !a.is_tau_label())

122

            .cloned()

123

            .sample(rng, num_of_hidden);

124

125

        let num_of_comm = rng.random_range(0..=5);

126

        let mut comm = (0..num_of_comm)

127

            .map(|_| {

128

                let size = rng.random_range(2..=3);

129

                let actions = random_multi_action(rng, &labels, size);

130

                let to = labels.choose(rng).unwrap().clone();

131

                CommExpr::new(actions, to)

132

})

133

            .filter(|comm| {

134

                !comm.from.is_tau_label() && comm.from.actions.contains(&comm.to) && comm.from.actions.len() >= 2

135

})

136

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

137

138

        comm.sort_unstable();

139

        comm.dedup();

140

141

        // Remove communication expressions with overlapping left-hand sides.

142

        let comm = comm

143

            .iter()

144

            .filter(|&comm_i| {

145

                !comm.iter().any(|comm_j| {

146

                    comm_i != comm_j && comm_i.from.actions.iter().any(|a| comm_j.from.actions.contains(a))

147

})

148

})

149

            .cloned()

150

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

151

152

        info!("Allow set {{{}}}", allow.iter().format(", "));

153

        info!("Hide set {{{}}}", hide.iter().format(", "));

154

        info!("Comm set {{{}}}", comm.iter().format(", "));

155

156

        // Use ltscombine to compute the combined LTS, which we will compare against our implementation's result

157

        let mut command = Command::new(&mcrl2_ltscombine);

158

        command.arg(&left_lts_path).arg(&right_lts_path);

159

        if !allow.is_empty() {

160

            command.arg(format!("--allow={{{}}}", allow.iter().format(", ")));

161

162

        if !hide.is_empty() {

163

            command.arg(format!("--hide={{{}}}", hide.iter().format(", ")));

164

165

        if !comm.is_empty() {

166

            command.arg(format!("--comm={{{}}}", comm.iter().format(", ")));

167

168

        command.arg(&output_path);

169

170

        let status = traced_command(&mut command).expect("Failed to run ltscombine");

171

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

172

173

        let expected_lts = read_lts(&File::open(&output_path).unwrap(), false).unwrap();

174

        let expected_path = temp_dir.path().join("expected.aut");

175

        write_mcrl2_aut(&mut File::create(&expected_path).unwrap(), &expected_lts).unwrap();

176

177

        let mut result: LtsBuilderFast<LtsMultiAction<LtsAction>> = LtsBuilderFast::new(Vec::new(), Vec::new());

178

        combine_lts(

179

            &mut result,

180

            vec![left_lts, right_lts],

181

            &hide,

182

            &allow,

183

            &comm,

184

            &Timing::new(),

185

186

        .unwrap();

187

        let result_lts = result.finish(StateIndex::new(0), false);

188

189

        let result_path = temp_dir.path().join("result.aut");

190

        write_mcrl2_aut(&mut File::create(&result_path).unwrap(), &result_lts).unwrap();

191

192

        assert!(

193

            compare_lts(

194

                Equivalence::StrongBisim,

195

                expected_lts,

196

                result_lts,

197

                false,

198

                &Timing::new(),

199

),

200

            "The resulting LTSs are not bisimilar."

201

);

202

});

203

1