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

3300

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

19

3300

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

20

3300

    drop(right); // No longer needed.

21

22

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

23

3300

    match equivalence {

24

        Equivalence::WeakBisim => {

25

200

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

26

200

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

27

28

        Equivalence::WeakBisimParallel => {

29

200

            let (lts, rhs_initial, partition) =

30

200

                weak_bisimulation_parallel(merged, rhs_initial, preprocess, false, timing);

31

200

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

32

33

        Equivalence::WeakBisimDivergencePreserving => {

34

200

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

35

200

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

36

37

        Equivalence::WeakBisimParallelDivergencePreserving => {

38

200

            let (lts, rhs_initial, partition) =

39

200

                weak_bisimulation_parallel(merged, rhs_initial, preprocess, true, timing);

40

200

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

41

42

        Equivalence::WeakBisimSigref => {

43

200

            let (lts, rhs_initial, partition) =

44

200

                weak_bisim_sigref_inductive_naive(merged, rhs_initial, preprocess, false, timing);

45

200

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

46

47

        Equivalence::WeakBisimSigrefNaive => {

48

200

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

49

200

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

50

51

        Equivalence::WeakBisimSigrefDivergencePreserving => {

52

200

            let (lts, rhs_initial, partition) =

53

200

                weak_bisim_sigref_inductive_naive(merged, rhs_initial, preprocess, true, timing);

54

200

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

55

56

        Equivalence::WeakBisimSigrefNaiveDivergencePreserving => {

57

200

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

58

200

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

59

60

        Equivalence::StrongBisim => {

61

700

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

62

700

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

63

64

        Equivalence::StrongBisimNaive => {

65

200

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

66

200

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

67

68

        Equivalence::BranchingBisim => {

69

200

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

70

200

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

71

72

        Equivalence::BranchingBisimNaive => {

73

200

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

74

200

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

75

76

        Equivalence::BranchingBisimDivergencePreserving => {

77

200

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

78

200

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

79

80

        Equivalence::BranchingBisimDivergencePreservingNaive => {

81

200

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

82

200

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

83

84

85

3300

86

87

#[cfg(test)]

88

mod tests {

89

    use merc_io::DumpFiles;

90

    use merc_lts::LTS;

91

    use merc_lts::LabelledTransitionSystem;

92

    use merc_lts::StateIndex;

93

    use merc_lts::random_lts;

94

    use merc_lts::write_aut;

95

    use merc_utilities::Timing;

96

    use merc_utilities::random_test;

97

    use rand::seq::IndexedRandom;

98

99

    use crate::compare;

100

    use crate::compare_lts;

101

102

    #[test]

103

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

104

1

    fn test_random_lts_permutation() {

105

100

        random_test(100, |rng| {

106

100

            let mut timing = Timing::new();

107

100

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

108

109

100

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

110

100

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

111

112

            // Generate a random permutation of the state indices.

113

100

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

114

100

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

115

100

                .sample(rng, lts.num_of_states())

116

100000

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

117

100

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

118

119

100

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

120

121

200004

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

122

100

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

123

124

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

125

100

            assert!(compare_lts(

126

100

                compare::Equivalence::StrongBisim,

127

100

                lts,

128

100

                permuted_lts,

129

                false,

130

100

                &mut timing

131

));

132

100

})

133

1

134

135

    #[test]

136

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

137

1

    fn test_random_compare_weak_bisim_variants() {

138

100

        random_test(100, |rng| {

139

100

            let mut timing = Timing::new();

140

100

            let lts1 = random_lts::<String, _>(rng, 100, 3);

141

100

            let lts2 = random_lts::<String, _>(rng, 100, 3);

142

143

            // All weak bisimulation variants should agree on whether two LTSs are equivalent

144

100

            let weak_bisim = compare_lts(

145

100

                compare::Equivalence::WeakBisim,

146

100

                lts1.clone(),

147

100

                lts2.clone(),

148

                false,

149

100

                &mut timing,

150

);

151

100

            let weak_bisim_parallel = compare_lts(

152

100

                compare::Equivalence::WeakBisimParallel,

153

100

                lts1.clone(),

154

100

                lts2.clone(),

155

                false,

156

100

                &mut timing,

157

);

158

100

            let weak_bisim_sigref = compare_lts(

159

100

                compare::Equivalence::WeakBisimSigref,

160

100

                lts1.clone(),

161

100

                lts2.clone(),

162

                false,

163

100

                &mut timing,

164

);

165

100

            let weak_bisim_sigref_naive = compare_lts(

166

100

                compare::Equivalence::WeakBisimSigrefNaive,

167

100

                lts1.clone(),

168

100

                lts2.clone(),

169

                false,

170

100

                &mut timing,

171

);

172

173

100

            assert_eq!(

174

                weak_bisim, weak_bisim_parallel,

175

                "WeakBisim and WeakBisimParallel should agree"

176

);

177

100

            assert_eq!(

178

                weak_bisim, weak_bisim_sigref,

179

                "WeakBisim and WeakBisimSigref should agree"

180

);

181

100

            assert_eq!(

182

                weak_bisim, weak_bisim_sigref_naive,

183

                "WeakBisim and WeakBisimSigrefNaive should agree"

184

);

185

100

})

186

1

187

188

    #[test]

189

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

190

1

    fn test_random_compare_weak_bisim_divergence_preserving_variants() {

191

100

        random_test(100, |rng| {

192

100

            let mut timing = Timing::new();

193

100

            let lts1 = random_lts::<String, _>(rng, 100, 3);

194

100

            let lts2 = random_lts::<String, _>(rng, 100, 3);

195

196

            // All weak bisimulation divergence-preserving variants should agree

197

100

            let weak_bisim_dp = compare_lts(

198

100

                compare::Equivalence::WeakBisimDivergencePreserving,

199

100

                lts1.clone(),

200

100

                lts2.clone(),

201

                false,

202

100

                &mut timing,

203

);

204

100

            let weak_bisim_dp_parallel = compare_lts(

205

100

                compare::Equivalence::WeakBisimParallelDivergencePreserving,

206

100

                lts1.clone(),

207

100

                lts2.clone(),

208

                false,

209

100

                &mut timing,

210

);

211

100

            let weak_bisim_dp_sigref = compare_lts(

212

100

                compare::Equivalence::WeakBisimSigrefDivergencePreserving,

213

100

                lts1.clone(),

214

100

                lts2.clone(),

215

                false,

216

100

                &mut timing,

217

);

218

100

            let weak_bisim_dp_sigref_naive = compare_lts(

219

100

                compare::Equivalence::WeakBisimSigrefNaiveDivergencePreserving,

220

100

                lts1.clone(),

221

100

                lts2.clone(),

222

                false,

223

100

                &mut timing,

224

);

225

226

100

            assert_eq!(

227

                weak_bisim_dp, weak_bisim_dp_parallel,

228

                "WeakBisimDivergencePreserving and WeakBisimParallelDivergencePreserving should agree"

229

);

230

100

            assert_eq!(

231

                weak_bisim_dp, weak_bisim_dp_sigref,

232

                "WeakBisimDivergencePreserving and WeakBisimSigrefDivergencePreserving should agree"

233

);

234

100

            assert_eq!(

235

                weak_bisim_dp, weak_bisim_dp_sigref_naive,

236

                "WeakBisimDivergencePreserving and WeakBisimSigrefNaiveDivergencePreserving should agree"

237

);

238

100

})

239

1

240

241

    #[test]

242

1

    fn test_random_compare_random_compare_strong_bisim_variants() {

243

100

        random_test(100, |rng| {

244

100

            let mut timing = Timing::new();

245

100

            let lts1 = random_lts::<String, _>(rng, 100, 3);

246

100

            let lts2 = random_lts::<String, _>(rng, 100, 3);

247

248

            // Strong bisimulation variants should agree

249

100

            let strong_bisim = compare_lts(

250

100

                compare::Equivalence::StrongBisim,

251

100

                lts1.clone(),

252

100

                lts2.clone(),

253

                false,

254

100

                &mut timing,

255

);

256

100

            let strong_bisim_naive = compare_lts(

257

100

                compare::Equivalence::StrongBisimNaive,

258

100

                lts1.clone(),

259

100

                lts2.clone(),

260

                false,

261

100

                &mut timing,

262

);

263

264

100

            assert_eq!(

265

                strong_bisim, strong_bisim_naive,

266

                "StrongBisim and StrongBisimNaive should agree"

267

);

268

100

})

269

1

270

271

    #[test]

272

1

    fn test_random_compare_branching_bisim_variants() {

273

100

        random_test(100, |rng| {

274

100

            let mut timing = Timing::new();

275

100

            let lts1 = random_lts::<String, _>(rng, 100, 3);

276

100

            let lts2 = random_lts::<String, _>(rng, 100, 3);

277

278

            // Branching bisimulation variants should agree

279

100

            let branching_bisim = compare_lts(

280

100

                compare::Equivalence::BranchingBisim,

281

100

                lts1.clone(),

282

100

                lts2.clone(),

283

                false,

284

100

                &mut timing,

285

);

286

100

            let branching_bisim_naive = compare_lts(

287

100

                compare::Equivalence::BranchingBisimNaive,

288

100

                lts1.clone(),

289

100

                lts2.clone(),

290

                false,

291

100

                &mut timing,

292

);

293

294

100

            assert_eq!(

295

                branching_bisim, branching_bisim_naive,

296

                "BranchingBisim and BranchingBisimNaive should agree"

297

);

298

100

})

299

1

300

301

    #[test]

302

1

    fn test_random_compare_branching_bisim_divergence_preserving_variants() {

303

100

        random_test(100, |rng| {

304

100

            let mut timing = Timing::new();

305

100

            let lts1 = random_lts::<String, _>(rng, 100, 3);

306

100

            let lts2 = random_lts::<String, _>(rng, 100, 3);

307

308

            // Branching bisimulation divergence-preserving variants should agree

309

100

            let branching_bisim_dp = compare_lts(

310

100

                compare::Equivalence::BranchingBisimDivergencePreserving,

311

100

                lts1.clone(),

312

100

                lts2.clone(),

313

                false,

314

100

                &mut timing,

315

);

316

100

            let branching_bisim_dp_naive = compare_lts(

317

100

                compare::Equivalence::BranchingBisimDivergencePreservingNaive,

318

100

                lts1.clone(),

319

100

                lts2.clone(),

320

                false,

321

100

                &mut timing,

322

);

323

324

100

            assert_eq!(

325

                branching_bisim_dp, branching_bisim_dp_naive,

326

                "BranchingBisimDivergencePreserving and BranchingBisimDivergencePreservingNaive should agree"

327

);

328

100

})

329

1

330