Grcov report - signature

1

use std::mem::swap;

2

3

use bumpalo::Bump;

4

use log::debug;

5

use log::info;

6

use log::trace;

7

use merc_io::TimeProgress;

8

use merc_lts::IncomingTransitions;

9

use merc_lts::LTS;

10

use merc_lts::LabelIndex;

11

use merc_lts::LabelledTransitionSystem;

12

use merc_lts::StateIndex;

13

use rustc_hash::FxHashMap;

14

use rustc_hash::FxHashSet;

15

16

use merc_utilities::Timing;

17

18

use crate::BlockIndex;

19

use crate::BlockPartition;

20

use crate::BlockPartitionBuilder;

21

use crate::IndexedPartition;

22

use crate::Partition;

23

use crate::Signature;

24

use crate::SignatureBuilder;

25

use crate::branching_bisim_signature;

26

use crate::branching_bisim_signature_inductive;

27

use crate::branching_bisim_signature_sorted;

28

use crate::is_tau_hat;

29

use crate::preprocess_branching;

30

use crate::strong_bisim_signature;

31

use crate::weak_bisim_signature_sorted;

32

use crate::weak_bisim_signature_sorted_taus;

33

34

/// Computes a strong bisimulation partitioning using signature refinement

35

300

pub fn strong_bisim_sigref<L: LTS>(lts: L, timing: &mut Timing) -> (L, BlockPartition) {

36

300

    let mut timepre = timing.start("preprocess");

37

300

    let incoming = IncomingTransitions::new(&lts);

38

300

    timepre.finish();

39

40

300

    let mut time = timing.start("reduction");

41

300

    let partition = signature_refinement::<_, _, false>(

42

300

        &lts,

43

300

        &incoming,

44

28577

        |state_index, partition, _, builder| {

45

28577

            strong_bisim_signature(state_index, &lts, partition, builder);

46

28577

},

47

        |_, _| None,

48

);

49

300

    time.finish();

50

51

300

    (lts, partition)

52

300

53

54

/// Computes a strong bisimulation partitioning using signature refinement

55

300

pub fn strong_bisim_sigref_naive<L: LTS>(lts: L, timing: &mut Timing) -> (L, IndexedPartition) {

56

300

    let mut time = timing.start("reduction");

57

18582

    let partition = signature_refinement_naive::<_, _, false>(&lts, |state_index, partition, _, builder| {

58

18582

        strong_bisim_signature(state_index, &lts, partition, builder);

59

18582

});

60

61

300

    time.finish();

62

300

    (lts, partition)

63

300

64

65

/// Computes a branching bisimulation partitioning using signature refinement

66

100

pub fn branching_bisim_sigref<L: LTS>(

67

100

    lts: L,

68

100

    timing: &mut Timing,

69

100

) -> (LabelledTransitionSystem<L::Label>, BlockPartition) {

70

100

    let mut timepre = timing.start("preprocess");

71

100

    let preprocessed_lts = preprocess_branching(lts);

72

100

    let incoming = IncomingTransitions::new(&preprocessed_lts);

73

100

    timepre.finish();

74

75

100

    let mut time = timing.start("reduction");

76

100

    let mut expected_builder = SignatureBuilder::default();

77

100

    let mut visited = FxHashSet::default();

78

100

    let mut stack = Vec::new();

79

80

100

    let partition = signature_refinement::<_, _, true>(

81

100

        &preprocessed_lts,

82

100

        &incoming,

83

2381

        |state_index, partition, state_to_key, builder| {

84

2381

            branching_bisim_signature_inductive(state_index, &preprocessed_lts, partition, state_to_key, builder);

85

86

            // Compute the expected signature, only used in debugging.

87

2381

            if cfg!(debug_assertions) {

88

2381

                branching_bisim_signature(

89

2381

                    state_index,

90

2381

                    &preprocessed_lts,

91

2381

                    partition,

92

2381

                    &mut expected_builder,

93

2381

                    &mut visited,

94

2381

                    &mut stack,

95

);

96

2381

                let expected_result = builder.clone();

97

98

2381

                let signature = Signature::new(builder);

99

2381

                debug_assert_eq!(

100

2381

                    signature.as_slice(),

101

                    expected_result,

102

                    "The sorted and expected signature should be the same"

103

);

104

105

2381

},

106

2381

        |signature, key_to_signature| {

107

            // Inductive signatures.

108

2439

            for (label, key) in signature.iter().rev() {

109

2439

                if is_tau_hat(*label, &preprocessed_lts)

110

1486

                    && key_to_signature[*key].is_subset_of(signature, (*label, *key))

111

112

1312

                    return Some(*key);

113

1127

114

115

1127

                if !is_tau_hat(*label, &preprocessed_lts) {

116

953

                    return None;

117

174

118

119

120

116

            None

121

2381

},

122

);

123

124

100

    time.finish();

125

126

    // Combine the SCC partition with the branching bisimulation partition.

127

100

    (preprocessed_lts, partition)

128

100

129

130

/// Computes a branching bisimulation partitioning using signature refinement without dirty blocks.

131

200

pub fn branching_bisim_sigref_naive<L: LTS>(

132

200

    lts: L,

133

200

    timing: &mut Timing,

134

200

) -> (LabelledTransitionSystem<L::Label>, IndexedPartition) {

135

200

    let mut timepre = timing.start("preprocess");

136

200

    let preprocessed_lts = preprocess_branching(lts);

137

200

    timepre.finish();

138

139

200

    let mut time = timing.start("reduction");

140

200

    let mut expected_builder = SignatureBuilder::default();

141

200

    let mut visited = FxHashSet::default();

142

200

    let mut stack = Vec::new();

143

144

200

    let partition = signature_refinement_naive::<_, _, false>(

145

200

        &preprocessed_lts,

146

14408

        |state_index, partition, state_to_signature, builder| {

147

14408

            branching_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder);

148

149

            // Compute the expected signature, only used in debugging.

150

14408

            if cfg!(debug_assertions) {

151

14408

                branching_bisim_signature(

152

14408

                    state_index,

153

14408

                    &preprocessed_lts,

154

14408

                    partition,

155

14408

                    &mut expected_builder,

156

14408

                    &mut visited,

157

14408

                    &mut stack,

158

);

159

14408

                let expected_result = builder.clone();

160

161

14408

                let signature = Signature::new(builder);

162

14408

                debug_assert_eq!(

163

14408

                    signature.as_slice(),

164

                    expected_result,

165

                    "The sorted and expected signature should be the same"

166

);

167

168

14408

},

169

);

170

200

    time.finish();

171

172

200

    (preprocessed_lts, partition)

173

200

174

175

/// Computes a branching bisimulation partitioning using signature refinement without dirty blocks.

176

200

pub fn weak_bisim_sigref_naive<L: LTS>(

177

200

    lts: L,

178

200

    timing: &mut Timing,

179

200

) -> (LabelledTransitionSystem<L::Label>, IndexedPartition) {

180

200

    let mut timepre = timing.start("preprocess");

181

200

    let preprocessed_lts = preprocess_branching(lts);

182

200

    timepre.finish();

183

184

200

    let mut time = timing.start("reduction");

185

186

200

    let partition = signature_refinement_naive::<_, _, true>(

187

200

        &preprocessed_lts,

188

5399

        |state_index, partition, state_to_signature, builder| {

189

5399

            weak_bisim_signature_sorted(state_index, &preprocessed_lts, partition, state_to_signature, builder)

190

5399

},

191

);

192

200

    time.finish();

193

194

200

    (preprocessed_lts, partition)

195

200

196

197

/// General signature refinement algorithm that accepts an arbitrary signature

198

///

199

/// The signature function is called for each state and should fill the

200

/// signature builder with the signature of the state. It consists of the

201

/// current partition, the signatures per state for the next partition.

202

400

fn signature_refinement<F, G, const BRANCHING: bool>(

203

400

    lts: &impl LTS,

204

400

    incoming: &IncomingTransitions,

205

400

    mut signature: F,

206

400

    mut renumber: G,

207

400

) -> BlockPartition

208

400

where

209

400

    F: FnMut(StateIndex, &BlockPartition, &[BlockIndex], &mut SignatureBuilder),

210

400

    G: FnMut(&[(LabelIndex, BlockIndex)], &Vec<Signature>) -> Option<BlockIndex>,

211

212

    // Avoids reallocations when computing the signature.

213

400

    let mut arena = Bump::new();

214

400

    let mut builder = SignatureBuilder::default();

215

400

    let mut split_builder = BlockPartitionBuilder::default();

216

217

    // Put all the states in the initial partition { S }.

218

400

    let mut id: FxHashMap<Signature<'_>, BlockIndex> = FxHashMap::default();

219

220

    // Assigns the signature to each state.

221

400

    let mut partition = BlockPartition::new(lts.num_of_states());

222

400

    let mut state_to_key: Vec<BlockIndex> = Vec::new();

223

18955

    state_to_key.resize_with(lts.num_of_states(), || BlockIndex::new(0));

224

400

    let mut key_to_signature: Vec<Signature> = Vec::new();

225

226

    // Refine partitions until stable.

227

400

    let mut iteration = 0usize;

228

400

    let mut states = Vec::new();

229

230

    // Used to keep track of dirty blocks.

231

400

    let mut worklist = vec![BlockIndex::new(0)];

232

233

400

    let progress = TimeProgress::new(

234

        |(iteration, blocks)| {

235

            info!("Iteration {iteration}, found {blocks} blocks...");

236

},

237

5,

238

);

239

240

21199

    while let Some(block_index) = worklist.pop() {

241

        // Clear the current partition to start the next blocks.

242

20799

        id.clear();

243

244

        // Removes the existing signatures.

245

20799

        key_to_signature.clear();

246

247

        // Safety: The current signatures have been removed, so it safe to reuse the memory.

248

20799

        let id: &'_ mut FxHashMap<Signature<'_>, BlockIndex> = unsafe { std::mem::transmute(&mut id) };

249

20799

        let key_to_signature: &'_ mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut key_to_signature) };

250

251

20799

        arena.reset();

252

253

20799

        let block = partition.block(block_index);

254

20799

        debug_assert!(

255

20799

            block.has_marked(),

256

            "Every block in the worklist should have at least one marked state"

257

);

258

259

20799

        if BRANCHING {

260

366

            partition.mark_backward_closure(block_index, incoming);

261

20433

262

263

        // Blocks above this number are new in this iteration.

264

20799

        let num_blocks = partition.num_of_blocks();

265

266

        // This is a workaround for a data race in bumpalo for zero-sized slices.

267

20799

        let empty_slice: &[(LabelIndex, BlockIndex)] = &[];

268

269

35126

        for new_block_index in

270

30958

            partition.partition_marked_with(block_index, &mut split_builder, |state_index, partition| {

271

30958

                signature(state_index, partition, &state_to_key, &mut builder);

272

273

                // Compute the signature of a single state

274

30958

                let index = if let Some(key) = renumber(&builder, key_to_signature) {

275

1312

key

276

29646

                } else if let Some((_, index)) = id.get_key_value(&Signature::new(&builder)) {

277

10924

                    *index

278

                } else {

279

18722

                    let slice = if builder.is_empty() {

280

204

                        empty_slice

281

                    } else {

282

18518

                        arena.alloc_slice_copy(&builder)

283

};

284

18722

                    let number = BlockIndex::new(key_to_signature.len());

285

18722

                    id.insert(Signature::new(slice), number);

286

18722

                    key_to_signature.push(Signature::new(slice));

287

288

18722

                    number

289

};

290

291

                // (branching) Keep track of the signature for every block in the next partition.

292

30958

                state_to_key[state_index] = index;

293

294

30958

                trace!("State {state_index} signature {builder:?} index {index}");

295

30958

                index

296

30958

})

297

298

35126

            if block_index != new_block_index {

299

                // If this is a new block, mark the incoming states as dirty

300

14327

                states.clear();

301

14327

                states.extend(partition.iter_block(new_block_index));

302

303

21037

                for &state_index in &states {

304

107571

                    for transition in incoming.incoming_transitions(state_index) {

305

107571

                        if BRANCHING {

306

                            // Mark incoming states into old blocks, or visible actions.

307

1692

                            if !lts.is_hidden_label(transition.label)

308

681

                                || partition.block_number(transition.to) < num_blocks

309

310

1091

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

311

312

1091

                                if !partition.block(other_block).has_marked() {

313

266

                                    // If block was not already marked then add it to the worklist.

314

266

                                    worklist.push(other_block);

315

825

316

317

1091

                                partition.mark_element(transition.to);

318

601

319

                        } else {

320

                            // In this case mark all incoming states.

321

105879

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

322

323

105879

                            if !partition.block(other_block).has_marked() {

324

20133

                                // If block was not already marked then add it to the worklist.

325

20133

                                worklist.push(other_block);

326

85746

327

328

105879

                            partition.mark_element(transition.to);

329

330

331

332

20799

333

334

335

20799

        trace!("Iteration {iteration} partition {partition}");

336

337

20799

        iteration += 1;

338

339

20799

        progress.print((iteration, partition.num_of_blocks()));

340

341

342

400

    trace!("Refinement partition {partition}");

343

400

    partition

344

400

345

346

/// General signature refinement algorithm that accepts an arbitrary signature

347

///

348

/// The signature function is called for each state and should fill the

349

/// signature builder with the signature of the state. It consists of the

350

/// current partition, the signatures per state for the next partition.

351

700

fn signature_refinement_naive<F, L: LTS, const WEAK: bool>(lts: &L, mut signature: F) -> IndexedPartition

352

700

where

353

700

    F: FnMut(StateIndex, &IndexedPartition, &Vec<Signature<'_>>, &mut SignatureBuilder),

354

355

    // Avoids reallocations when computing the signature.

356

700

    let mut arena = Bump::new();

357

700

    let mut builder = SignatureBuilder::default();

358

359

    // Put all the states in the initial partition { S }.

360

700

    let mut id: FxHashMap<Signature<'_>, BlockIndex> = FxHashMap::default();

361

362

    // Assigns the signature to each state.

363

700

    let mut partition = IndexedPartition::new(lts.num_of_states());

364

700

    let mut next_partition = IndexedPartition::new(lts.num_of_states());

365

700

    let mut state_to_signature: Vec<Signature<'_>> = Vec::new();

366

700

    state_to_signature.resize_with(lts.num_of_states(), Signature::default);

367

368

    // Refine partitions until stable.

369

700

    let mut old_count = 1;

370

700

    let mut iteration = 0;

371

372

700

    let progress = TimeProgress::new(

373

        |(iteration, blocks)| {

374

            debug!("Iteration {iteration}, found {blocks} blocks...",);

375

},

376

5,

377

);

378

379

    // This is a workaround for a data race in bumpalo for zero-sized slices.

380

700

    let empty_slice: &[(LabelIndex, BlockIndex)] = &[];

381

382

2676

    while old_count != id.len() {

383

1976

        old_count = id.len();

384

1976

        progress.print((iteration, old_count));

385

1976

        swap(&mut partition, &mut next_partition);

386

387

        // Clear the current partition to start the next blocks.

388

1976

        id.clear();

389

390

1976

        state_to_signature.clear();

391

1976

        state_to_signature.resize_with(lts.num_of_states(), Signature::default);

392

393

        // Safety: The current signatures have been removed, so it safe to reuse the memory.

394

1976

        let id: &'_ mut FxHashMap<Signature<'_>, BlockIndex> = unsafe { std::mem::transmute(&mut id) };

395

1976

        let state_to_signature: &mut Vec<Signature<'_>> = unsafe { std::mem::transmute(&mut state_to_signature) };

396

397

        // Remove the current signatures.

398

1976

        arena.reset();

399

400

1976

        if WEAK {

401

4224

            for state_index in lts.iter_states() {

402

4224

                weak_bisim_signature_sorted_taus(state_index, lts, &partition, state_to_signature, &mut builder);

403

404

4224

                trace!("State {state_index} signature {:?}", builder);

405

406

                // Keep track of the index for every state, either use the arena to allocate space or simply borrow the value.

407

4224

                let slice = if builder.is_empty() {

408

                    empty_slice

409

                } else {

410

4224

                    arena.alloc_slice_copy(&builder)

411

};

412

4224

                state_to_signature[state_index] = Signature::new(slice);

413

414

1499

415

416

31188

        for state_index in lts.iter_states() {

417

            // Compute the signature of a single state

418

31188

            signature(state_index, &partition, state_to_signature, &mut builder);

419

420

31188

            trace!("State {state_index} signature {builder:?}");

421

422

            // Keep track of the index for every state, either use the arena to allocate space or simply borrow the value.

423

31188

            let mut new_id = BlockIndex::new(id.len());

424

31188

            if let Some((signature, index)) = id.get_key_value(&Signature::new(&builder)) {

425

19290

                // SAFETY: We know that the signature lives as long as the arena

426

19290

                state_to_signature[state_index] = unsafe {

427

19290

                    std::mem::transmute::<Signature<'_>, Signature<'_>>(Signature::new(signature.as_slice()))

428

19290

};

429

19290

                new_id = *index;

430

19290

            } else {

431

11898

                let slice = if builder.is_empty() {

432

1188

                    empty_slice

433

                } else {

434

10710

                    arena.alloc_slice_copy(&builder)

435

};

436

11898

                id.insert(Signature::new(slice), new_id);

437

438

                // (branching) Keep track of the signature for every block in the next partition.

439

11898

                state_to_signature[state_index] = Signature::new(slice);

440

441

442

31188

            next_partition.set_block(state_index, new_id);

443

444

445

1976

        iteration += 1;

446

447

1976

        debug_assert!(

448

1976

            iteration <= lts.num_of_states().max(2),

449

            "There can never be more splits than number of states, but at least two iterations for stability"

450

);

451

452

453

700

    trace!("Refinement partition {partition}");

454

700

    debug_assert!(

455

7201

        is_valid_refinement(lts, &partition, |state_index, partition, builder| signature(

456

7201

            state_index,

457

7201

            partition,

458

7201

            &state_to_signature,

459

7201

            builder

460

)),

461

        "The resulting partition is not a valid partition."

462

);

463

700

    partition

464

700

465

466

/// Returns true iff the given partition is a strong bisimulation partition

467

700

pub fn is_valid_refinement<F, P>(lts: &impl LTS, partition: &P, mut compute_signature: F) -> bool

468

700

where

469

700

    F: FnMut(StateIndex, &P, &mut SignatureBuilder),

470

700

    P: Partition,

471

472

    // Check that the partition is indeed stable and as such is a quotient of strong bisimulation

473

700

    let mut block_to_signature: Vec<Option<SignatureBuilder>> = vec![None; partition.num_of_blocks()];

474

475

    // Avoids reallocations when computing the signature.

476

700

    let mut builder = SignatureBuilder::default();

477

478

7201

    for state_index in lts.iter_states() {

479

7201

        let block = partition.block_number(state_index);

480

481

        // Compute the flat signature, which has Hash and is more compact.

482

7201

        compute_signature(state_index, partition, &mut builder);

483

7201

        let signature: Vec<(LabelIndex, BlockIndex)> = builder.clone();

484

485

7201

        if let Some(block_signature) = &block_to_signature[block] {

486

3560

            if signature != *block_signature {

487

                trace!(

488

                    "State {state_index} has a different signature {signature:?} then the block {block} which has signature {block_signature:?}"

489

);

490

                return false;

491

3560

492

3641

        } else {

493

3641

            block_to_signature[block] = Some(signature);

494

3641

};

495

496

497

    // Check if there are two blocks with the same signature

498

700

    let mut signature_to_block: FxHashMap<Signature, usize> = FxHashMap::default();

499

500

3641

    for (block_index, signature) in block_to_signature

501

700

        .iter()

502

3641

        .map(|signature| signature.as_ref().unwrap())

503

700

        .enumerate()

504

505

3641

        if let Some(other_block_index) = signature_to_block.get(&Signature::new(signature)) {

506

            if block_index != *other_block_index {

507

                trace!("Block {block_index} and {other_block_index} have the same signature {signature:?}");

508

                return false;

509

510

3641

        } else {

511

3641

            signature_to_block.insert(Signature::new(signature), block_index);

512

3641

513

514

515

700

    true

516

700

517

518

#[cfg(test)]

519

mod tests {

520

    use super::*;

521

522

    use test_log::test;

523

524

    use merc_lts::random_lts;

525

    use merc_utilities::Timing;

526

    use merc_utilities::random_test;

527

528

    /// Returns true iff the partitions are equal, runs in O(n^2).

529

200

    fn equal_partitions(left: &impl Partition, right: &impl Partition) -> bool {

530

        // Check that states in the same block, have a single (unique) number in

531

        // the other partition.

532

1296

        for block_index in (0..left.num_of_blocks()).map(BlockIndex::new) {

533

1296

            let mut other_block_index = None;

534

535

2655

            for state_index in (0..left.len())

536

1296

                .map(StateIndex::new)

537

56690

                .filter(|&state_index| left.block_number(state_index) == block_index)

538

539

2655

                match other_block_index {

540

1296

                    None => other_block_index = Some(right.block_number(state_index)),

541

1359

                    Some(other_block_index) => {

542

1359

                        if right.block_number(state_index) != other_block_index {

543

                            return false;

544

1359

545

546

547

548

549

550

1296

        for block_index in (0..right.num_of_blocks()).map(BlockIndex::new) {

551

1296

            let mut other_block_index = None;

552

553

2655

            for state_index in (0..left.len())

554

1296

                .map(StateIndex::new)

555

56690

                .filter(|&state_index| right.block_number(state_index) == block_index)

556

557

2655

                match other_block_index {

558

1296

                    None => other_block_index = Some(left.block_number(state_index)),

559

1359

                    Some(other_block_index) => {

560

1359

                        if left.block_number(state_index) != other_block_index {

561

                            return false;

562

1359

563

564

565

566

567

568

200

        true

569

200

570

571

    #[test]

572

    fn test_random_strong_bisim_sigref() {

573

100

        random_test(100, |rng| {

574

100

            let lts = random_lts(rng, 10, 3, 3);

575

100

            let mut timing = Timing::new();

576

577

100

            let (_result_lts, result_partition) = strong_bisim_sigref(lts.clone(), &mut timing);

578

100

            let (_expected_lts, expected_partition) = strong_bisim_sigref_naive(lts, &mut timing);

579

580

            // There is no preprocessing so this works.

581

100

            assert!(equal_partitions(&result_partition, &expected_partition));

582

100

});

583

584

585

    #[test]

586

    fn test_random_branching_bisim_sigref() {

587

100

        random_test(100, |rng| {

588

100

            let lts = random_lts(rng, 10, 3, 3);

589

100

            let mut timing = Timing::new();

590

591

100

            let (_result_lts, result_partition) = branching_bisim_sigref(lts.clone(), &mut timing);

592

100

            let (_expected_lts, expected_partition) = branching_bisim_sigref_naive(lts, &mut timing);

593

594

            // There is no preprocessing so this works.

595

100

            assert!(equal_partitions(&result_partition, &expected_partition));

596

100

});

597

598

599

    /// Checks that the branching bisimulation partition is a refinement of the strong bisimulation partition.

600

200

    fn is_refinement(lts: &impl LTS, strong_partition: &impl Partition, branching_partition: &impl Partition) {

601

2152

        for state_index in lts.iter_states() {

602

71400

            for other_state_index in lts.iter_states() {

603

71400

                if strong_partition.block_number(state_index) == strong_partition.block_number(other_state_index) {

604

                    // If the states are together according to branching bisimilarity, then they should also be together according to strong bisimilarity.

605

5714

                    assert_eq!(

606

5714

                        branching_partition.block_number(state_index),

607

5714

                        branching_partition.block_number(other_state_index),

608

                        "The branching partition should be a refinement of the strong partition,

609

                        but states {state_index} and {other_state_index} are in different blocks"

610

);

611

65686

612

613

614

200

615

616

    #[test]

617

    #[cfg_attr(miri, ignore)]

618

    fn test_random_branching_bisim_sigref_naive() {

619

100

        random_test(100, |rng| {

620

100

            let lts = random_lts(rng, 10, 3, 3);

621

100

            let mut timing = Timing::new();

622

623

100

            let (preprocessed_lts, branching_partition) = branching_bisim_sigref_naive(lts, &mut timing);

624

100

            let strong_partition = strong_bisim_sigref_naive(preprocessed_lts.clone(), &mut timing).1;

625

100

            is_refinement(&preprocessed_lts, &strong_partition, &branching_partition);

626

100

});

627

628

629

    #[test]

630

    #[cfg_attr(miri, ignore)]

631

    fn test_random_weak_bisim_sigref_naive() {

632

100

        random_test(100, |rng| {

633

100

            let lts = random_lts(rng, 10, 3, 3);

634

100

            let mut timing = Timing::new();

635

636

100

            let (preprocessed_lts, weak_partition) = weak_bisim_sigref_naive(lts, &mut timing);

637

100

            let strong_partition = strong_bisim_sigref_naive(preprocessed_lts.clone(), &mut timing).1;

638

100

            is_refinement(&preprocessed_lts, &strong_partition, &weak_partition);

639

100

});

640

641