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

6804

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

28

6804

    lts: &L,

29

6804

    partition: &P,

30

6804

    eliminate_inert_taus: bool,

31

6804

    eliminate_tau_loops: bool,

32

6804

) -> LabelledTransitionSystem<L::Label> {

33

    // Introduce the transitions based on the block numbers, the number of blocks is a decent approximation for the number of transitions.

34

6804

    let mut builder = LtsBuilderFast::with_capacity(

35

6804

        lts.labels().into(),

36

6804

        Vec::new(),

37

6804

        partition.num_of_blocks(), // We expect one transition per state.

38

);

39

40

1972598

    for state_index in lts.iter_states() {

41

2012155

        for transition in lts.outgoing_transitions(state_index) {

42

2012155

            let block = partition.block_number(state_index);

43

2012155

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

44

45

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

46

2012155

            if !(eliminate_inert_taus

47

1676519

                && lts.is_hidden_label(transition.label)

48

555058

                && block == to_block

49

46177

                && state_index != transition.to)

50

1967547

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

51

52

1966187

                debug_assert!(

53

1966187

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

54

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

55

);

56

57

1966187

                builder

58

1966187

                    .add_transition(

59

1966187

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

60

1966187

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

61

1966187

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

62

63

1966187

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

64

45968

65

66

67

68

6804

    builder.require_num_of_states(partition.num_of_blocks());

69

6804

    builder.finish(

70

6804

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

71

        true,

72

73

6804

74

75

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

76

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

77

///

78

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

79

1200

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

80

1200

    lts: &L,

81

1200

    partition: &P,

82

1200

    eliminate_tau_loops: bool,

83

1200

) -> LabelledTransitionSystem<L::Label> {

84

1200

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

85

1200

    remove_redundant_transitions(&quotient)

86

1200

87

88

/// Weak bisimulation quotient that removes redundant transitions.

89

1200

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

90

1200

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

91

1200

    builder.require_num_of_states(lts.num_of_states());

92

93

114824

    for from in lts.iter_states() {

94

194085

        for transition in lts.outgoing_transitions(from) {

95

194085

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

96

190702

                builder

97

190702

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

98

190702

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

99

190702

            } else {

100

3383

                trace!(

101

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

102

                    from,

103

                    lts.labels()[transition.label],

104

                    transition.to

105

);

106

107

108

109

110

1200

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

111

1200

112

113

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

114

///

115

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

116

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

117

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

118

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

119

///

120

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

121

194085

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

122

194085

    let mut redundant = false;

123

124

194085

    reachability(

125

194085

        lts,

126

194085

        from,

127

500757

        |l| lts.is_hidden_label(l),

128

325962

        |middle| {

129

325962

            if redundant {

130

1125

                return;

131

324837

132

133

498782

            for transition in lts.outgoing_transitions(middle) {

134

498782

                let same_action = if lts.is_hidden_label(label) {

135

196707

                    lts.is_hidden_label(transition.label)

136

                } else {

137

302075

                    transition.label == label

138

};

139

140

498782

                if !same_action {

141

214330

                    continue;

142

284452

143

144

                // Skip the exact transition being tested.

145

284452

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

146

193948

                    continue;

147

90504

148

149

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

150

90504

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

151

93

                    continue;

152

90411

153

154

90411

                reachability(

155

90411

                    lts,

156

90411

                    transition.to,

157

131292

                    |l| lts.is_hidden_label(l),

158

118847

                    |reached| {

159

118847

                        if reached == target {

160

3383

                            redundant = true;

161

115464

162

118847

},

163

);

164

165

90411

                if redundant {

166

3383

                    break;

167

87028

168

169

325962

},

170

);

171

172

194085

    redundant

173

194085

174

175

/// Optimised implementation for block partitions.

176

///

177

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

178

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

179

/// states as representatives.

180

///

181

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

182

687

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

183

687

    lts: &L,

184

687

    partition: &BlockPartition,

185

687

    eliminate_tau_loops: bool,

186

687

) -> LabelledTransitionSystem<L::Label> {

187

687

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

188

189

49654

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

190

        // Pick any state in the block

191

49654

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

192

49654

            state

193

        } else {

194

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

195

};

196

197

49654

        if BRANCHING {

198

35957

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

199

200

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

201

            'outer: loop {

202

36222

                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

36222

210

36222

                visited[candidate] = true;

211

212

65720

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

213

65720

                    lts.is_hidden_label(trans.label)

214

17769

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

215

17584

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

216

65720

                }) {

217

265

                    candidate = trans.to;

218

265

                    continue 'outer;

219

35957

220

221

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

222

35957

                break;

223

224

13697

225

226

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

227

88448

        for transition in lts.outgoing_transitions(candidate) {

228

88448

            if BRANCHING {

229

65449

                debug_assert!(

230

65449

                    !(lts.is_hidden_label(transition.label)

231

17498

                        && candidate != transition.to

232

17313

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

233

                    "The representative {} is not bottom state",

234

                    candidate

235

);

236

22999

237

238

88448

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

239

88448

                builder

240

88448

                    .add_transition(

241

88448

                        StateIndex::new(*block),

242

88448

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

243

88448

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

244

88448

245

88448

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

246

88448

247

248

249

250

687

    builder.require_num_of_states(partition.num_of_blocks());

251

687

    builder.finish(

252

687

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

253

        true,

254

255

687

256

257

#[cfg(test)]

258

mod tests {

259

    use merc_io::DumpFiles;

260

    use merc_lts::random_lts;

261

    use merc_lts::write_aut;

262

    use merc_utilities::Timing;

263

    use merc_utilities::random_test;

264

    use rand::rngs::StdRng;

265

266

    use crate::Equivalence;

267

    use crate::compare_lts;

268

    use crate::reduce_lts;

269

270

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

271

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

272

1400

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

273

1400

        let mut timing = Timing::new();

274

1400

        let mut files = DumpFiles::new(test_name);

275

276

1400

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

277

278

1400

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

279

280

1400

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

281

1400

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

282

283

1400

        assert!(

284

1400

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

285

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

286

);

287

1400

288

289

    #[test]

290

1

    fn test_random_strong_bisim_quotient() {

291

100

        random_test(100, |rng| {

292

100

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

293

100

});

294

1

295

296

    #[test]

297

1

    fn test_random_strong_bisim_naive_quotient() {

298

100

        random_test(100, |rng| {

299

100

            check_quotient_equivalence(

300

100

                rng,

301

100

                Equivalence::StrongBisimNaive,

302

100

                "test_random_strong_bisim_naive_quotient",

303

);

304

100

});

305

1

306

307

    #[test]

308

1

    fn test_random_branching_bisim_quotient() {

309

100

        random_test(100, |rng| {

310

100

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

311

100

});

312

1

313

314

    #[test]

315

1

    fn test_random_branching_bisim_naive_quotient() {

316

100

        random_test(100, |rng| {

317

100

            check_quotient_equivalence(

318

100

                rng,

319

100

                Equivalence::BranchingBisimNaive,

320

100

                "test_random_branching_bisim_naive_quotient",

321

);

322

100

});

323

1

324

325

    #[test]

326

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

327

1

    fn test_random_weak_bisim_quotient() {

328

100

        random_test(100, |rng| {

329

100

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

330

100

});

331

1

332

333

    #[test]

334

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

335

1

    fn test_random_weak_bisim_parallel_quotient() {

336

100

        random_test(100, |rng| {

337

100

            check_quotient_equivalence(

338

100

                rng,

339

100

                Equivalence::WeakBisimParallel,

340

100

                "test_random_weak_bisim_parallel_quotient",

341

);

342

100

});

343

1

344

345

    #[test]

346

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

347

1

    fn test_random_weak_bisim_sigref_quotient() {

348

100

        random_test(100, |rng| {

349

100

            check_quotient_equivalence(

350

100

                rng,

351

100

                Equivalence::WeakBisimSigref,

352

100

                "test_random_weak_bisim_sigref_quotient",

353

);

354

100

});

355

1

356

357

    #[test]

358

1

    fn test_random_weak_bisim_sigref_naive_quotient() {

359

100

        random_test(100, |rng| {

360

100

            check_quotient_equivalence(

361

100

                rng,

362

100

                Equivalence::WeakBisimSigrefNaive,

363

100

                "test_random_weak_bisim_sigref_naive_quotient",

364

);

365

100

});

366

1

367

368

    #[test]

369

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

370

1

    fn test_random_weak_bisim_divergence_preserving_quotient() {

371

100

        random_test(100, |rng| {

372

100

            check_quotient_equivalence(

373

100

                rng,

374

100

                Equivalence::WeakBisimDivergencePreserving,

375

100

                "test_random_weak_bisim_divergence_preserving_quotient",

376

);

377

100

});

378

1

379

380

    #[test]

381

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

382

1

    fn test_random_weak_bisim_parallel_divergence_preserving_quotient() {

383

100

        random_test(100, |rng| {

384

100

            check_quotient_equivalence(

385

100

                rng,

386

100

                Equivalence::WeakBisimParallelDivergencePreserving,

387

100

                "test_random_weak_bisim_parallel_divergence_preserving_quotient",

388

);

389

100

});

390

1

391

392

    #[test]

393

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

394

1

    fn test_random_weak_bisim_sigref_divergence_preserving_quotient() {

395

100

        random_test(100, |rng| {

396

100

            check_quotient_equivalence(

397

100

                rng,

398

100

                Equivalence::WeakBisimSigrefDivergencePreserving,

399

100

                "test_random_weak_bisim_sigref_divergence_preserving_quotient",

400

);

401

100

});

402

1

403

404

    #[test]

405

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

406

1

    fn test_random_weak_bisim_sigref_naive_divergence_preserving_quotient() {

407

100

        random_test(100, |rng| {

408

100

            check_quotient_equivalence(

409

100

                rng,

410

100

                Equivalence::WeakBisimSigrefNaiveDivergencePreserving,

411

100

                "test_random_weak_bisim_sigref_naive_divergence_preserving_quotient",

412

);

413

100

});

414

1

415

416

    #[test]

417

1

    fn test_random_branching_bisim_divergence_preserving_quotient() {

418

100

        random_test(100, |rng| {

419

100

            check_quotient_equivalence(

420

100

                rng,

421

100

                Equivalence::BranchingBisimDivergencePreserving,

422

100

                "test_random_branching_bisim_divergence_preserving_quotient",

423

);

424

100

});

425

1

426

427

    #[test]

428

1

    fn test_random_branching_bisim_divergence_preserving_naive_quotient() {

429

100

        random_test(100, |rng| {

430

100

            check_quotient_equivalence(

431

100

                rng,

432

100

                Equivalence::BranchingBisimDivergencePreservingNaive,

433

100

                "test_random_branching_bisim_divergence_preserving_naive_quotient",

434

);

435

100

});

436

1

437