Grcov report - signature

1

use std::mem::swap;

2

3

use bumpalo::Bump;

4

use log::debug;

5

use log::info;

6

use log::log_enabled;

7

use log::trace;

8

use merc_io::TimeProgress;

9

use merc_lts::IncomingTransitions;

10

use merc_lts::LTS;

11

use merc_lts::LabelIndex;

12

use merc_lts::LabelledTransitionSystem;

13

use merc_lts::StateIndex;

14

use rustc_hash::FxHashMap;

15

use rustc_hash::FxHashSet;

16

17

use merc_collections::BlockIndex;

18

use merc_collections::IndexedPartition;

19

use merc_utilities::Timing;

20

21

use crate::BlockPartition;

22

use crate::BlockPartitionBuilder;

23

use crate::Equivalence;

24

use crate::Partition;

25

use crate::Signature;

26

use crate::SignatureBuilder;

27

use crate::branching_bisim_signature;

28

use crate::branching_bisim_signature_inductive;

29

use crate::branching_bisim_signature_sorted;

30

use crate::is_tau_hat;

31

use crate::longest_tau_path;

32

use crate::reduce_lts;

33

use crate::strong_bisim_signature;

34

use crate::tau_loop_elimination_and_reorder;

35

use crate::weak_bisim_presignature_sorted;

36

use crate::weak_bisim_signature_sorted;

37

use crate::weak_bisim_signature_sorted_full;

38

use crate::weak_bisim_signature_sorted_taus;

39

40

/// Computes a strong bisimulation partitioning using signature refinement

41

300

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

42

300

    let incoming = timing.measure("preprocess", || IncomingTransitions::new(&lts));

43

44

300

    let partition = timing.measure("reduction", || {

45

300

        signature_refinement::<_, _, false>(

46

300

            &lts,

47

300

            &incoming,

48

5533

            |state_index, partition, _, builder| {

49

5533

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

50

5533

},

51

            |_, _| None,

52

53

300

});

54

55

300

    (lts, partition)

56

300

57

58

/// Computes a strong bisimulation partitioning using signature refinement

59

200

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

60

200

    let partition = timing.measure("reduction", || {

61

9454

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

62

9454

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

63

9454

})

64

200

});

65

66

200

    (lts, partition)

67

200

68

69

/// Computes a branching bisimulation partitioning using signature refinement

70

100

pub fn branching_bisim_sigref<L: LTS>(lts: L, timing: &Timing) -> (LabelledTransitionSystem<L::Label>, BlockPartition) {

71

100

    let preprocessed_lts = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts));

72

100

    let incoming = timing.measure("preprocess", || IncomingTransitions::new(&preprocessed_lts));

73

74

100

    if log_enabled!(log::Level::Debug) {

75

        let path = longest_tau_path(&preprocessed_lts);

76

        debug!("longest_tau_path" = path.len(); "The longest tau path is {:?}", path);

77

100

78

79

100

    let mut expected_builder = SignatureBuilder::default();

80

100

    let mut visited = FxHashSet::default();

81

100

    let mut stack = Vec::new();

82

83

100

    let partition = timing.measure("reduction", || {

84

100

        signature_refinement::<_, _, true>(

85

100

            &preprocessed_lts,

86

100

            &incoming,

87

2047

            |state_index, partition, state_to_key, builder| {

88

2047

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

89

90

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

91

2047

                if cfg!(debug_assertions) {

92

2047

                    branching_bisim_signature(

93

2047

                        state_index,

94

2047

                        &preprocessed_lts,

95

2047

                        partition,

96

2047

                        &mut expected_builder,

97

2047

                        &mut visited,

98

2047

                        &mut stack,

99

);

100

2047

                    let expected_result = builder.clone();

101

102

2047

                    let signature = Signature::new(builder);

103

2047

                    debug_assert_eq!(

104

2047

                        signature.as_slice(),

105

                        expected_result,

106

                        "The sorted and expected signature should be the same"

107

);

108

109

2047

},

110

2047

            |signature, key_to_signature| {

111

                // Inductive signatures.

112

2113

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

113

2113

                    if is_tau_hat(*label, &preprocessed_lts)

114

1233

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

115

116

1006

                        return Some(*key);

117

1107

118

119

1107

                    if !is_tau_hat(*label, &preprocessed_lts) {

120

880

                        return None;

121

227

122

123

124

161

                None

125

2047

},

126

127

100

});

128

129

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

130

100

    (preprocessed_lts, partition)

131

100

132

133

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

134

300

pub fn branching_bisim_sigref_naive<L: LTS>(

135

300

    lts: L,

136

300

    timing: &Timing,

137

300

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

138

300

    let preprocessed_lts = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts));

139

140

300

    timing.measure("reduction", || {

141

300

        let mut expected_builder = SignatureBuilder::default();

142

300

        let mut visited = FxHashSet::default();

143

300

        let mut stack = Vec::new();

144

145

300

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

146

300

            &preprocessed_lts,

147

16204

            |state_index, partition, state_to_signature, builder| {

148

16204

                branching_bisim_signature_sorted(

149

16204

                    state_index,

150

16204

                    &preprocessed_lts,

151

16204

                    partition,

152

16204

                    state_to_signature,

153

16204

                    builder,

154

);

155

156

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

157

16204

                if cfg!(debug_assertions) {

158

16204

                    branching_bisim_signature(

159

16204

                        state_index,

160

16204

                        &preprocessed_lts,

161

16204

                        partition,

162

16204

                        &mut expected_builder,

163

16204

                        &mut visited,

164

16204

                        &mut stack,

165

);

166

16204

                    let expected_result = builder.clone();

167

168

16204

                    let signature = Signature::new(builder);

169

16204

                    debug_assert_eq!(

170

16204

                        signature.as_slice(),

171

                        expected_result,

172

                        "The sorted and expected signature should be the same"

173

);

174

175

16204

},

176

);

177

178

300

        (preprocessed_lts, partition)

179

300

})

180

300

181

182

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

183

200

pub fn weak_bisim_sigref_inductive_naive<L: LTS>(

184

200

    lts: L,

185

200

    preprocess: bool,

186

200

    timing: &Timing,

187

200

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

188

    // Preprocess the LTS if desired.

189

200

    if preprocess {

190

        let lts = timing.measure("preprocess", || {

191

            reduce_lts(lts, Equivalence::BranchingBisim, true, timing)

192

});

193

        weak_bisim_sigref_inductive_naive_impl(lts, timing)

194

    } else {

195

200

        weak_bisim_sigref_inductive_naive_impl(lts, timing)

196

197

200

198

199

/// Implementation of [weak bisimulation signature refinement] that deals with  both preprocessed and regular LTSs.

200

pub fn weak_bisim_sigref_inductive_naive_impl<L: LTS>(

201

200

    lts: L,

202

200

    timing: &Timing,

203

200

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

204

200

    let preprocessed_lts = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts));

205

200

    let partition = timing.measure("reduction", || signature_refinement_weak(&preprocessed_lts));

206

200

    (preprocessed_lts, partition)

207

200

208

209

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

210

200

pub fn weak_bisim_sigref_naive<L: LTS>(

211

200

    lts: L,

212

200

    preprocess: bool,

213

200

    timing: &Timing,

214

200

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

215

    // Preprocess the LTS if desired.

216

200

    if preprocess {

217

        let lts = timing.measure("preprocess", || {

218

            reduce_lts(lts, Equivalence::BranchingBisim, true, timing)

219

});

220

        weak_bisim_sigref_naive_impl(lts, timing)

221

    } else {

222

200

        weak_bisim_sigref_naive_impl(lts, timing)

223

224

200

225

226

/// Implementation of [weak bisimulation signature refinement] that deals with

227

/// both preprocessed and regular LTSs.

228

200

fn weak_bisim_sigref_naive_impl<L: LTS>(

229

200

    lts: L,

230

200

    timing: &Timing,

231

200

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

232

200

    let preprocessed_lts = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts));

233

200

    let partition = timing.measure("reduction", || {

234

200

        signature_refinement_naive::<_, _, true>(

235

200

            &preprocessed_lts,

236

10182

            |state_index, partition, state_to_signature, builder| {

237

10182

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

238

10182

},

239

240

200

});

241

242

200

    (preprocessed_lts, partition)

243

200

244

245

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

246

///

247

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

248

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

249

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

250

400

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

251

400

    lts: &impl LTS,

252

400

    incoming: &IncomingTransitions,

253

400

    mut signature: F,

254

400

    mut renumber: G,

255

400

) -> BlockPartition

256

400

where

257

400

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

258

400

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

259

260

    // Avoids reallocations when computing the signature.

261

400

    let mut arena = Bump::new();

262

400

    let mut builder = SignatureBuilder::default();

263

400

    let mut split_builder = BlockPartitionBuilder::default();

264

265

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

266

400

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

267

268

    // Assigns the signature to each state.

269

400

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

270

400

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

271

4380

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

272

400

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

273

274

    // Refine partitions until stable.

275

400

    let mut iteration = 0usize;

276

400

    let mut states = Vec::new();

277

278

    // Used to keep track of dirty blocks.

279

400

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

280

281

400

    let progress = TimeProgress::new(

282

        |(iteration, blocks)| {

283

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

284

},

285

5,

286

);

287

288

3463

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

289

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

290

3063

        id.clear();

291

292

        // Removes the existing signatures.

293

3063

        key_to_signature.clear();

294

295

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

296

3063

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

297

3063

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

298

299

3063

        arena.reset();

300

301

3063

        let block = partition.block(block_index);

302

3063

        debug_assert!(

303

3063

            block.has_marked(),

304

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

305

);

306

307

3063

        if BRANCHING {

308

367

            partition.mark_backward_closure(block_index, incoming);

309

2696

310

311

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

312

3063

        let num_blocks = partition.num_of_blocks();

313

314

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

315

3063

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

316

317

5537

        for new_block_index in

318

7580

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

319

7580

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

320

321

                // Compute the signature of a single state

322

7580

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

323

1006

key

324

6574

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

325

2972

                    *index

326

                } else {

327

3602

                    let slice = if builder.is_empty() {

328

210

                        empty_slice

329

                    } else {

330

3392

                        arena.alloc_slice_copy(&builder)

331

};

332

3602

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

333

3602

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

334

3602

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

335

336

3602

                    number

337

};

338

339

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

340

7580

                state_to_key[state_index] = index;

341

342

7580

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

343

7580

                index

344

7580

})

345

346

5537

            if block_index != new_block_index {

347

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

348

2474

                states.clear();

349

2474

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

350

351

4235

                for &state_index in &states {

352

9721

                    for transition in incoming.incoming_transitions(state_index) {

353

9721

                        if BRANCHING {

354

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

355

1623

                            if !lts.is_hidden_label(transition.label)

356

782

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

357

358

988

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

359

360

988

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

361

267

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

362

267

                                    worklist.push(other_block);

363

721

364

365

988

                                partition.mark_element(transition.to);

366

635

367

                        } else {

368

                            // In this case mark all incoming states.

369

8098

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

370

371

8098

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

372

2396

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

373

2396

                                worklist.push(other_block);

374

5702

375

376

8098

                            partition.mark_element(transition.to);

377

378

379

380

3063

381

382

383

3063

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

384

385

3063

        iteration += 1;

386

387

3063

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

388

389

390

400

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

391

400

    partition

392

400

393

394

/// Weak signature refinement algorithm, doing inductive signatures naively.

395

///

396

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

397

/// signature builder with the pre_signature of the state.

398

200

fn signature_refinement_weak<L: LTS>(lts: &L) -> IndexedPartition

399

200

where {

400

    // Avoids reallocations when computing the signature.

401

200

    let mut arena = Bump::new();

402

200

    let mut builder = SignatureBuilder::default();

403

404

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

405

200

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

406

407

    // Assigns the signature to each state.

408

200

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

409

200

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

410

200

    let mut state_to_signature: Vec<Option<usize>> = Vec::new();

411

200

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

412

200

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

413

414

200

    state_to_signature.resize_with(lts.num_of_states(), || None);

415

200

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

416

417

200

    let mut old_count = 1;

418

200

    let mut iteration = 0;

419

420

200

    let progress = TimeProgress::new(

421

        |(iteration, blocks)| {

422

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

423

},

424

5,

425

);

426

427

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

428

200

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

429

    // Refine partitions until stable.

430

431

669

    while old_count != id.len() {

432

469

        old_count = id.len();

433

469

        progress.print((iteration, old_count));

434

469

        swap(&mut partition, &mut next_partition);

435

436

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

437

469

        id.clear();

438

439

        // Remove the current signatures.

440

469

        arena.reset();

441

442

469

        state_to_signature.clear();

443

469

        key_to_signature.clear();

444

445

469

        state_to_signature.resize_with(lts.num_of_states(), || None);

446

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

447

469

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

448

469

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

449

469

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

450

469

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

451

452

        // Compute for each state its tau signature. This seems inefficient, but for now it works.

453

469

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

454

5034

        for state in lts.iter_states() {

455

5034

            weak_bisim_signature_sorted_taus(state, lts, &partition, state_to_taus, &mut builder);

456

457

5034

            let slice = if builder.is_empty() {

458

                empty_slice

459

            } else {

460

5034

                arena.alloc_slice_copy(&builder)

461

};

462

5034

            state_to_taus[state] = Signature::new(slice);

463

464

465

5034

        for state_index in lts.iter_states() {

466

            // Compute the Presignature of a single state

467

5034

            weak_bisim_presignature_sorted(

468

5034

                state_index,

469

5034

                lts,

470

5034

                &partition,

471

5034

                state_to_taus,

472

5034

                state_to_signature,

473

5034

                &mut builder,

474

);

475

476

            // Inductive step see if presig is a subset of a tau reachable state.

477

5034

            let mut inductive_key = None;

478

15586

            for keyvalue in builder.as_slice() {

479

15586

                if is_tau_hat(keyvalue.0, lts) {

480

3567

                    let tau_sig = &key_to_signature[keyvalue.1.value()];

481

3567

                    let presig = Signature::new(&builder);

482

483

3567

                    if tau_sig.is_subset_of(presig.as_slice(), *keyvalue) {

484

1902

                        inductive_key = Some(*keyvalue.1);

485

1902

                        break;

486

1665

487

12019

488

489

5034

            if let Some(inductive_key) = inductive_key {

490

1902

                trace!(

491

                    "State {state_index} with pre {:?} uses inductive key {inductive_key}:{:?}",

492

                    builder.as_slice(),

493

                    key_to_signature[inductive_key].as_slice()

494

);

495

1902

                state_to_signature[state_index] = Some(inductive_key);

496

1902

                next_partition.set_block(*state_index, BlockIndex::new(inductive_key));

497

            } else {

498

                // If not: expand the signature completely.

499

3132

                weak_bisim_signature_sorted_full(

500

3132

                    state_index,

501

3132

                    lts,

502

3132

                    &partition,

503

3132

                    state_to_taus,

504

3132

                    state_to_signature,

505

3132

                    key_to_signature,

506

3132

                    &mut builder,

507

);

508

3132

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

509

510

                // Keep track of the index for every state

511

3132

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

512

3132

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

513

1616

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

514

1616

                    state_to_signature[state_index] = Some(index.value());

515

1616

                    new_id = *index;

516

1616

                } else {

517

1516

                    let slice = if builder.is_empty() {

518

                        empty_slice

519

                    } else {

520

1516

                        arena.alloc_slice_copy(&builder)

521

};

522

1516

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

523

1516

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

524

525

1516

                    state_to_signature[state_index] = Some(new_id.value());

526

527

528

3132

                next_partition.set_block(*state_index, new_id);

529

};

530

531

532

469

        iteration += 1;

533

534

469

        debug_assert!(

535

469

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

536

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

537

);

538

539

540

200

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

541

    // debug_assert!(

542

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

543

    //         state_index,

544

    //         partition,

545

    //         &state_to_signature,

546

    //         builder

547

    //     )),

548

    //     "The resulting partition is not a valid partition."

549

    // );

550

200

    partition

551

200

552

553

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

554

///

555

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

556

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

557

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

558

700

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

559

700

where

560

700

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

561

562

    // Avoids reallocations when computing the signature.

563

700

    let mut arena = Bump::new();

564

700

    let mut builder = SignatureBuilder::default();

565

566

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

567

700

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

568

569

    // Assigns the signature to each state.

570

700

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

571

700

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

572

700

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

573

700

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

574

575

    // Refine partitions until stable.

576

700

    let mut old_count = 1;

577

700

    let mut iteration = 0;

578

579

700

    let progress = TimeProgress::new(

580

        |(iteration, blocks)| {

581

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

582

},

583

5,

584

);

585

586

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

587

700

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

588

589

2688

    while old_count != id.len() {

590

1988

        trace!("Iteration {} ({} blocks)", iteration, id.len());

591

592

1988

        old_count = id.len();

593

1988

        progress.print((iteration, old_count));

594

1988

        swap(&mut partition, &mut next_partition);

595

596

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

597

1988

        id.clear();

598

599

1988

        state_to_signature.clear();

600

1988

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

601

602

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

603

1988

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

604

1988

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

605

606

        // Remove the current signatures.

607

1988

        arena.reset();

608

609

1988

        if WEAK {

610

8108

            for state_index in lts.iter_states() {

611

8108

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

612

613

8108

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

614

615

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

616

8108

                let slice = if builder.is_empty() {

617

                    empty_slice

618

                } else {

619

8108

                    arena.alloc_slice_copy(&builder)

620

};

621

8108

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

622

623

1456

624

625

28886

        for state_index in lts.iter_states() {

626

            // Compute the signature of a single state

627

28886

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

628

629

28886

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

630

631

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

632

28886

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

633

28886

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

634

18660

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

635

18660

                state_to_signature[state_index] = unsafe {

636

18660

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

637

18660

};

638

18660

                new_id = *index;

639

18660

            } else {

640

10226

                let slice = if builder.is_empty() {

641

1171

                    empty_slice

642

                } else {

643

9055

                    arena.alloc_slice_copy(&builder)

644

};

645

10226

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

646

647

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

648

10226

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

649

650

651

28886

            next_partition.set_block(*state_index, new_id);

652

653

654

1988

        iteration += 1;

655

656

1988

        debug_assert!(

657

1988

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

658

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

659

);

660

661

662

700

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

663

700

    debug_assert!(

664

6954

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

665

6954

            state_index,

666

6954

            partition,

667

6954

            &state_to_signature,

668

6954

            builder

669

)),

670

        "The resulting partition is not a valid partition."

671

);

672

700

    partition

673

700

674

675

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

676

700

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

677

700

where

678

700

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

679

700

    P: Partition,

680

681

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

682

700

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

683

684

    // Avoids reallocations when computing the signature.

685

700

    let mut builder = SignatureBuilder::default();

686

687

6954

    for state_index in lts.iter_states() {

688

6954

        let block = partition.block_number(state_index);

689

690

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

691

6954

        compute_signature(state_index, partition, &mut builder);

692

6954

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

693

694

6954

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

695

3762

            if signature != *block_signature {

696

                trace!(

697

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

698

);

699

                return false;

700

3762

701

3192

        } else {

702

3192

            block_to_signature[block] = Some(signature);

703

3192

};

704

705

706

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

707

700

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

708

709

3192

    for (block_index, signature) in block_to_signature

710

700

        .iter()

711

3192

        .map(|signature: &Option<SignatureBuilder>| signature.as_ref().expect("Signature should be defined"))

712

700

        .enumerate()

713

714

3192

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

715

            if block_index != *other_block_index {

716

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

717

                return false;

718

719

3192

        } else {

720

3192

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

721

3192

722

723

724

700

    true

725

700

726

727

#[cfg(test)]

728

mod tests {

729

    use super::*;

730

731

    use merc_io::DumpFiles;

732

    use merc_lts::write_aut;

733

    use test_log::test;

734

735

    use merc_lts::random_lts;

736

    use merc_utilities::Timing;

737

    use merc_utilities::random_test;

738

739

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

740

300

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

741

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

742

        // the other partition.

743

1493

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

744

1493

            let mut other_block_index = None;

745

746

3324

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

747

1493

                .map(StateIndex::new)

748

44375

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

749

750

3324

                match other_block_index {

751

1493

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

752

1831

                    Some(other_block_index) => {

753

1831

                        if right.block_number(state_index) != other_block_index {

754

                            return false;

755

1831

756

757

758

759

760

761

1493

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

762

1493

            let mut other_block_index = None;

763

764

3324

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

765

1493

                .map(StateIndex::new)

766

44375

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

767

768

3324

                match other_block_index {

769

1493

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

770

1831

                    Some(other_block_index) => {

771

1831

                        if left.block_number(state_index) != other_block_index {

772

                            return false;

773

1831

774

775

776

777

778

779

300

        true

780

300

781

782

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

783

200

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

784

1815

        for state_index in lts.iter_states() {

785

57301

            for other_state_index in lts.iter_states() {

786

57301

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

787

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

788

9373

                    assert_eq!(

789

9373

                        branching_partition.block_number(state_index),

790

9373

                        branching_partition.block_number(other_state_index),

791

                        "The strong partition should be a refinement of the branching partition, but states {state_index} and {other_state_index} are in different strong blocks"

792

);

793

47928

794

795

796

200

797

798

    #[test]

799

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

800

    fn test_random_strong_bisim_sigref() {

801

100

        random_test(100, |rng| {

802

100

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

803

804

100

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

805

100

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

806

807

100

            let mut timing = Timing::new();

808

809

100

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

810

100

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

811

812

100

            files

813

100

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

814

100

                .unwrap();

815

100

            files

816

100

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

817

100

                .unwrap();

818

819

            // There is no preprocessing so this works.

820

100

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

821

100

});

822

823

824

    #[test]

825

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

826

    fn test_random_branching_bisim_sigref() {

827

100

        random_test(100, |rng| {

828

100

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

829

830

100

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

831

100

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

832

833

100

            let mut timing = Timing::new();

834

835

100

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

836

100

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

837

838

100

            files

839

100

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

840

100

                .unwrap();

841

100

            files

842

100

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

843

100

                .unwrap();

844

845

            // There is no preprocessing so this works.

846

100

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

847

100

});

848

849

850

    #[test]

851

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

852

    fn test_random_weak_bisim_sigref() {

853

100

        random_test(100, |rng| {

854

100

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

855

856

100

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

857

100

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

858

859

100

            let mut timing = Timing::new();

860

861

100

            let (result_lts, result_partition) = weak_bisim_sigref_naive(lts.clone(), false, &mut timing);

862

100

            let (expected_lts, expected_partition) = weak_bisim_sigref_inductive_naive(lts, false, &mut timing);

863

864

100

            files

865

100

                .dump("result.aut", |writer| write_aut(writer, &result_lts))

866

100

                .unwrap();

867

100

            files

868

100

                .dump("expected.aut", |writer| write_aut(writer, &expected_lts))

869

100

                .unwrap();

870

871

            // There is no preprocessing so this works.

872

100

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

873

100

});

874

875

876

    #[test]

877

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

878

    fn test_random_branching_bisim_sigref_naive() {

879

100

        random_test(100, |rng| {

880

100

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

881

882

100

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

883

100

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

884

885

100

            let mut timing = Timing::new();

886

887

100

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

888

100

            files

889

100

                .dump("preprocessed.aut", |writer| write_aut(writer, &preprocessed_lts))

890

100

                .unwrap();

891

892

100

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

893

100

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

894

100

});

895

896

897

    #[test]

898

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

899

    fn test_random_weak_bisim_sigref_naive() {

900

100

        random_test(100, |rng| {

901

100

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

902

903

100

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

904

100

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

905

906

100

            let mut timing = Timing::new();

907

908

100

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

909

100

            files

910

100

                .dump("preprocessed.aut", |writer| write_aut(writer, &preprocessed_lts))

911

100

                .unwrap();

912

913

100

            let branching_partition = branching_bisim_sigref_naive(preprocessed_lts.clone(), &mut timing).1;

914

100

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

915

100

});

916

917