Grcov report - quotient.rs

1

#![forbid(unsafe_code)]

2

3

use log::trace;

4

use merc_collections::BlockIndex;

5

use merc_lts::LTS;

6

use merc_lts::LabelIndex;

7

use merc_lts::LabelledTransitionSystem;

8

use merc_lts::LtsBuilder;

9

use merc_lts::LtsBuilderFast;

10

use merc_lts::StateIndex;

11

use merc_lts::reachability;

12

13

use crate::BlockPartition;

14

use crate::Partition;

15

use crate::diverges;

16

17

/// Returns a new LTS based on the given partition.

18

///

19

/// Computes the existential quotient of the given LTS based on the given

20

/// partition:

21

///

22

/// > \[p\] -a-> \[q\] iff there exist states s in p and t in q such that s -a-> t

23

///

24

/// If `eliminate_inert_taus` is true then non self-loop tau steps \[p\] -tau-> \[p\] are eliminated.

25

/// If `eliminate_tau_loops` is true then tau self-loops s -tau-> s are eliminated.

26

/// The two parameters are independent: each controls a disjoint set of transitions.

27

6820

pub fn quotient_lts_naive<L: LTS, P: Partition>(

28

6820

    lts: &L,

29

6820

    partition: &P,

30

6820

    eliminate_inert_taus: bool,

31

6820

    eliminate_tau_loops: bool,

32

6820

) -> LabelledTransitionSystem<L::Label> {

33

    // Introduce the transitions based on the block numbers. Seed the capacity

34

    // with at least one transition per block; the builder grows as needed.

35

6820

    let mut builder = LtsBuilderFast::with_capacity(lts.labels().into(), Vec::new(), partition.num_of_blocks());

36

37

1972386

    for state_index in lts.iter_states() {

38

2012670

        for transition in lts.outgoing_transitions(state_index) {

39

2012670

            let block = partition.block_number(state_index);

40

2012670

            let to_block = partition.block_number(transition.to);

41

42

            // Eliminate non-self-loop inert taus and (independently) tau self-loops.

43

2012670

            if !(eliminate_inert_taus

44

1677650

                && lts.is_hidden_label(transition.label)

45

557009

                && block == to_block

46

46399

                && state_index != transition.to)

47

1967904

                && !(eliminate_tau_loops && lts.is_hidden_label(transition.label) && state_index == transition.to)

48

49

1966480

                debug_assert!(

50

1966480

                    partition.block_number(state_index) < partition.num_of_blocks(),

51

                    "Quotienting assumes that the block numbers do not exceed the number of blocks"

52

);

53

54

1966480

                builder

55

1966480

                    .add_transition(

56

1966480

                        StateIndex::new(block.value()),

57

1966480

                        &lts.labels()[transition.label],

58

1966480

                        StateIndex::new(to_block.value()),

59

60

1966480

                    .expect("Adding transitions does not fail");

61

46190

62

63

64

65

6820

    builder.require_num_of_states(partition.num_of_blocks());

66

6820

    builder.finish(

67

6820

        StateIndex::new(partition.block_number(lts.initial_state_index()).value()),

68

        true,

69

70

6820

71

72

/// Returns a weak bisimulation quotient that additionally removes transitions

73

/// subsumed by a one-hidden-step alternative.

74

///

75

/// If `eliminate_tau_loops` is true then tau self-loops are eliminated.

76

1200

pub fn quotient_lts_weak<L: LTS, P: Partition>(

77

1200

    lts: &L,

78

1200

    partition: &P,

79

1200

    eliminate_tau_loops: bool,

80

1200

) -> LabelledTransitionSystem<L::Label> {

81

1200

    let quotient = quotient_lts_naive(lts, partition, true, eliminate_tau_loops);

82

1200

    remove_redundant_transitions(&quotient)

83

1200

84

85

/// Weak bisimulation quotient that removes redundant transitions.

86

1200

fn remove_redundant_transitions<L: LTS>(lts: &L) -> LabelledTransitionSystem<L::Label> {

87

1200

    let mut builder = LtsBuilderFast::with_capacity(lts.labels().into(), Vec::new(), lts.num_of_transitions());

88

1200

    builder.require_num_of_states(lts.num_of_states());

89

90

114638

    for from in lts.iter_states() {

91

193531

        for transition in lts.outgoing_transitions(from) {

92

193531

            if !is_redundant_transition(lts, from, transition.label, transition.to) {

93

190300

                builder

94

190300

                    .add_transition(from, &lts.labels()[transition.label], transition.to)

95

190300

                    .expect("Adding transitions does not fail");

96

190300

            } else {

97

3231

                trace!(

98

                    "Removing redundant transition: {} -[{}]-> {}",

99

                    from,

100

                    lts.labels()[transition.label],

101

                    transition.to

102

);

103

104

105

106

107

1200

    builder.finish(lts.initial_state_index(), true)

108

1200

109

110

/// Returns true when transition `from -label-> target` is redundant.

111

///

112

/// A transition `s -a-> u` is redundant iff there exist states `t` and `v` such that:

113

/// - `s -tau*-> t`

114

/// - `t -a-> v` (for hidden `a`, any hidden transition)

115

/// - `v -tau*-> u`

116

///

117

/// The exact transition `s -a-> u` itself is not considered a witness.

118

193531

fn is_redundant_transition<L: LTS>(lts: &L, from: StateIndex, label: LabelIndex, target: StateIndex) -> bool {

119

193531

    let mut redundant = false;

120

121

193531

    reachability(

122

193531

        lts,

123

193531

        from,

124

496975

        |l| lts.is_hidden_label(l),

125

323270

        |middle| {

126

323270

            if redundant {

127

920

                return;

128

322350

129

130

495260

            for transition in lts.outgoing_transitions(middle) {

131

495260

                let same_action = if lts.is_hidden_label(label) {

132

194182

                    lts.is_hidden_label(transition.label)

133

                } else {

134

301078

                    transition.label == label

135

};

136

137

495260

                if !same_action {

138

212391

                    continue;

139

282869

140

141

                // Skip the exact transition being tested.

142

282869

                if middle == from && transition.label == label && transition.to == target {

143

193376

                    continue;

144

89493

145

146

                // Skip tau self-loops on the middle state, as they do not contribute to the redundancy.

147

89493

                if lts.is_hidden_label(transition.label) && middle == transition.to {

148

111

                    continue;

149

89382

150

151

89382

                reachability(

152

89382

                    lts,

153

89382

                    transition.to,

154

130216

                    |l| lts.is_hidden_label(l),

155

117431

                    |reached| {

156

117431

                        if reached == target {

157

3231

                            redundant = true;

158

114200

159

117431

},

160

);

161

162

89382

                if redundant {

163

3231

                    break;

164

86151

165

166

323270

},

167

);

168

169

193531

    redundant

170

193531

171

172

/// Optimised implementation for block partitions.

173

///

174

/// Chooses a single state in the block as representative. If `BRANCHING` then

175

/// the chosen state is a bottom state. For `BRANCHING` we only consider bottom

176

/// states as representatives.

177

///

178

/// If `eliminate_tau_loops` is true then tau self-loops are eliminated.

179

759

pub fn quotient_lts_block<L: LTS, const BRANCHING: bool>(

180

759

    lts: &L,

181

759

    partition: &BlockPartition,

182

759

    eliminate_tau_loops: bool,

183

759

) -> LabelledTransitionSystem<L::Label> {

184

759

    let mut builder = LtsBuilderFast::new(lts.labels().into(), Vec::new());

185

186

    // Reused across blocks to find bottom states when BRANCHING.

187

759

    let mut visited = vec![false; lts.num_of_states()];

188

    // Only touched states are reset to avoid clearing the entire visited vector.

189

759

    let mut touched = Vec::new();

190

191

48560

    for block in (0..partition.num_of_blocks()).map(BlockIndex::new) {

192

        // Pick any state in the block

193

48560

        let mut candidate = if let Some(state) = partition.iter_block(block).next() {

194

48560

            state

195

        } else {

196

            panic!("Blocks in the partition should not be empty {}", block);

197

};

198

199

48560

        if BRANCHING {

200

            // traverse any outgoing transition to find a bottom state.

201

            'outer: loop {

202

34114

                if visited[candidate] {

203

                    // No bottom state exists in this block. Stop early to avoid looping forever.

204

                    debug_assert!(

205

                        !diverges(lts, candidate),

206

                        "The states of the given LTS should be non-divergent."

207

);

208

                    break;

209

34114

210

34114

                visited[candidate] = true;

211

34114

                touched.push(candidate);

212

213

61272

                if let Some(trans) = lts.outgoing_transitions(candidate).find(|trans| {

214

61272

                    lts.is_hidden_label(trans.label)

215

16646

                        && candidate != trans.to // Ignore self loops for the bottom state search.

216

16499

                        && partition.block_number(trans.to) == block

217

61272

                }) {

218

224

                    candidate = trans.to;

219

224

                    continue 'outer;

220

33890

221

222

                // No outgoing tau transition to the same block, so we found a bottom state.

223

33890

                break;

224

225

226

            // Reset only the entries touched by this walk.

227

34114

            for state in touched.drain(..) {

228

34114

                visited[state] = false;

229

34114

230

14670

231

232

        // Add all transitions from the representative state (or the bottom state if BRANCHING) to the quotient LTS.

233

90526

        for transition in lts.outgoing_transitions(candidate) {

234

90526

            if BRANCHING {

235

61038

                debug_assert!(

236

61038

                    !(lts.is_hidden_label(transition.label)

237

16412

                        && candidate != transition.to

238

16265

                        && partition.block_number(transition.to) == block),

239

                    "The representative {} is not bottom state",

240

                    candidate

241

);

242

29488

243

244

90526

            if !(eliminate_tau_loops && lts.is_hidden_label(transition.label) && candidate == transition.to) {

245

90526

                builder

246

90526

                    .add_transition(

247

90526

                        StateIndex::new(*block),

248

90526

                        &lts.labels()[transition.label],

249

90526

                        StateIndex::new(*partition.block_number(transition.to)),

250

90526

251

90526

                    .expect("Adding transitions does not fail");

252

90526

253

254

255

256

759

    builder.require_num_of_states(partition.num_of_blocks());

257

759

    builder.finish(

258

759

        StateIndex::new(partition.block_number(lts.initial_state_index()).value()),

259

        true,

260

261

759

262

263

#[cfg(test)]

264

mod tests {

265

    use merc_io::DumpFiles;

266

    use merc_lts::random_lts;

267

    use merc_lts::write_aut;

268

    use merc_utilities::Timing;

269

    use merc_utilities::random_test;

270

    use rand::rngs::StdRng;

271

272

    use crate::Equivalence;

273

    use crate::compare_lts;

274

    use crate::reduce_lts;

275

276

    /// Generates a random LTS, reduces it under `equivalence`, and asserts

277

    /// that the original and reduced LTS are equivalent.

278

1400

    fn check_quotient_equivalence(rng: &mut StdRng, equivalence: Equivalence, test_name: &str) {

279

1400

        let timing = Timing::new();

280

1400

        let files = DumpFiles::new(test_name);

281

282

1400

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

283

284

1400

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

285

286

1400

        let reduced = reduce_lts(lts.clone(), equivalence, false, &timing);

287

1400

        files.dump("quotient.aut", |w| write_aut(w, &reduced)).unwrap();

288

289

1400

        assert!(

290

1400

            compare_lts(equivalence, lts, reduced, false, &timing),

291

            "Quotient is not equivalent under {equivalence:?}",

292

);

293

1400

294

295

    #[test]

296

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

297

1

    fn test_random_strong_bisim_quotient() {

298

100

        random_test(100, |rng| {

299

100

            check_quotient_equivalence(rng, Equivalence::StrongBisim, "test_random_strong_bisim_quotient");

300

100

});

301

1

302

303

    #[test]

304

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

305

1

    fn test_random_strong_bisim_naive_quotient() {

306

100

        random_test(100, |rng| {

307

100

            check_quotient_equivalence(

308

100

                rng,

309

100

                Equivalence::StrongBisimNaive,

310

100

                "test_random_strong_bisim_naive_quotient",

311

);

312

100

});

313

1

314

315

    #[test]

316

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

317

1

    fn test_random_branching_bisim_quotient() {

318

100

        random_test(100, |rng| {

319

100

            check_quotient_equivalence(rng, Equivalence::BranchingBisim, "test_random_branching_bisim_quotient");

320

100

});

321

1

322

323

    #[test]

324

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

325

1

    fn test_random_branching_bisim_naive_quotient() {

326

100

        random_test(100, |rng| {

327

100

            check_quotient_equivalence(

328

100

                rng,

329

100

                Equivalence::BranchingBisimNaive,

330

100

                "test_random_branching_bisim_naive_quotient",

331

);

332

100

});

333

1

334

335

    #[test]

336

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

337

1

    fn test_random_weak_bisim_quotient() {

338

100

        random_test(100, |rng| {

339

100

            check_quotient_equivalence(rng, Equivalence::WeakBisim, "test_random_weak_bisim_quotient");

340

100

});

341

1

342

343

    #[test]

344

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

345

1

    fn test_random_weak_bisim_parallel_quotient() {

346

100

        random_test(100, |rng| {

347

100

            check_quotient_equivalence(

348

100

                rng,

349

100

                Equivalence::WeakBisimParallel,

350

100

                "test_random_weak_bisim_parallel_quotient",

351

);

352

100

});

353

1

354

355

    #[test]

356

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

357

1

    fn test_random_weak_bisim_sigref_quotient() {

358

100

        random_test(100, |rng| {

359

100

            check_quotient_equivalence(

360

100

                rng,

361

100

                Equivalence::WeakBisimSigref,

362

100

                "test_random_weak_bisim_sigref_quotient",

363

);

364

100

});

365

1

366

367

    #[test]

368

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

369

1

    fn test_random_weak_bisim_sigref_naive_quotient() {

370

100

        random_test(100, |rng| {

371

100

            check_quotient_equivalence(

372

100

                rng,

373

100

                Equivalence::WeakBisimSigrefNaive,

374

100

                "test_random_weak_bisim_sigref_naive_quotient",

375

);

376

100

});

377

1

378

379

    #[test]

380

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

381

1

    fn test_random_weak_bisim_divergence_preserving_quotient() {

382

100

        random_test(100, |rng| {

383

100

            check_quotient_equivalence(

384

100

                rng,

385

100

                Equivalence::WeakBisimDivergencePreserving,

386

100

                "test_random_weak_bisim_divergence_preserving_quotient",

387

);

388

100

});

389

1

390

391

    #[test]

392

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

393

1

    fn test_random_weak_bisim_parallel_divergence_preserving_quotient() {

394

100

        random_test(100, |rng| {

395

100

            check_quotient_equivalence(

396

100

                rng,

397

100

                Equivalence::WeakBisimParallelDivergencePreserving,

398

100

                "test_random_weak_bisim_parallel_divergence_preserving_quotient",

399

);

400

100

});

401

1

402

403

    #[test]

404

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

405

1

    fn test_random_weak_bisim_sigref_divergence_preserving_quotient() {

406

100

        random_test(100, |rng| {

407

100

            check_quotient_equivalence(

408

100

                rng,

409

100

                Equivalence::WeakBisimSigrefDivergencePreserving,

410

100

                "test_random_weak_bisim_sigref_divergence_preserving_quotient",

411

);

412

100

});

413

1

414

415

    #[test]

416

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

417

1

    fn test_random_weak_bisim_sigref_naive_divergence_preserving_quotient() {

418

100

        random_test(100, |rng| {

419

100

            check_quotient_equivalence(

420

100

                rng,

421

100

                Equivalence::WeakBisimSigrefNaiveDivergencePreserving,

422

100

                "test_random_weak_bisim_sigref_naive_divergence_preserving_quotient",

423

);

424

100

});

425

1

426

427

    #[test]

428

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

429

1

    fn test_random_branching_bisim_divergence_preserving_quotient() {

430

100

        random_test(100, |rng| {

431

100

            check_quotient_equivalence(

432

100

                rng,

433

100

                Equivalence::BranchingBisimDivergencePreserving,

434

100

                "test_random_branching_bisim_divergence_preserving_quotient",

435

);

436

100

});

437

1

438

439

    #[test]

440

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

441

1

    fn test_random_branching_bisim_divergence_preserving_naive_quotient() {

442

100

        random_test(100, |rng| {

443

100

            check_quotient_equivalence(

444

100

                rng,

445

100

                Equivalence::BranchingBisimDivergencePreservingNaive,

446

100

                "test_random_branching_bisim_divergence_preserving_naive_quotient",

447

);

448

100

});

449

1

450