Grcov report - weak_bisimulation.rs

1

//! Authors: Maurice Laveaux, Eduardo Costa Martins

2

//!

3

//! Implements the weak bisimulation algorithm by Eduardo Costa Martins.

4

#![forbid(unsafe_code)]

5

6

use std::iter;

7

8

use bitvec::bitvec;

9

use bitvec::order::Lsb0;

10

11

use bitvec::vec::BitVec;

12

use log::info;

13

use log::trace;

14

use merc_collections::BlockIndex;

15

use merc_io::TimeProgress;

16

use merc_lts::IncomingTransitions;

17

use merc_lts::LTS;

18

use merc_lts::LabelIndex;

19

use merc_lts::LabelledTransitionSystem;

20

use merc_lts::StateIndex;

21

use merc_utilities::Timing;

22

23

use crate::DivergencePreservingLts;

24

use crate::Equivalence;

25

use crate::MarkedBlockPartition;

26

use crate::reduce_lts;

27

use crate::tau_cycle_elimination_and_reorder;

28

29

/// Type alias because we use bitvec for marking states

30

type BitArray = BitVec<u64, Lsb0>;

31

32

/// Apply weak bisimulation reduction

33

///

34

/// # Details

35

///

36

/// The `preprocess` flag indicates whether to preprocess the LTS using

37

/// branching bisimulation.

38

///

39

/// The `state` is any state for which we return the equivalent state in the

40

/// preprocessed LTS.

41

800

pub fn weak_bisimulation<L: LTS>(

42

800

    lts: L,

43

800

    state: StateIndex,

44

800

    preprocess: bool,

45

800

    divergence_preserving: bool,

46

800

    timing: &Timing,

47

800

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

48

    // Preprocess the LTS if desired.

49

800

    if preprocess {

50

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

51

            if divergence_preserving {

52

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

53

            } else {

54

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

55

56

});

57

        weak_bisimulation_preprocessed(lts, state, divergence_preserving, timing)

58

    } else {

59

800

        weak_bisimulation_preprocessed(lts, state, divergence_preserving, timing)

60

61

800

62

63

/// Apply weak bisimulation reduction using the parallel variant of the

64

/// algorithm

65

///

66

/// # Details

67

///

68

/// The `preprocess` flag indicates whether to preprocess the LTS using

69

/// branching bisimulation.

70

///

71

/// The `state` is any state for which we return the equivalent state in the

72

/// preprocessed LTS.

73

700

pub fn weak_bisimulation_parallel<L: LTS>(

74

700

    lts: L,

75

700

    state: StateIndex,

76

700

    preprocess: bool,

77

700

    divergence_preserving: bool,

78

700

    timing: &Timing,

79

700

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

80

    // Preprocess the LTS if desired.

81

700

    if preprocess {

82

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

83

            if divergence_preserving {

84

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

85

            } else {

86

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

87

88

});

89

        weak_bisimulation_parallel_preprocessed(lts, state, divergence_preserving, timing)

90

    } else {

91

700

        weak_bisimulation_parallel_preprocessed(lts, state, divergence_preserving, timing)

92

93

700

94

95

/// Core weak bisimulation algorithm implementation.

96

800

fn weak_bisimulation_preprocessed<L: LTS>(

97

800

    lts: L,

98

800

    state: StateIndex,

99

800

    divergence_preserving: bool,

100

800

    timing: &Timing,

101

800

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

102

800

    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || {

103

800

        tau_cycle_elimination_and_reorder(lts, state, !divergence_preserving)

104

800

});

105

106

800

    timing.measure("reduction", || {

107

800

        let blocks = if divergence_preserving {

108

300

            let divergence_preserving_lts = DivergencePreservingLts::new(&tau_loop_free_lts);

109

300

            weak_bisimulation_impl(&divergence_preserving_lts)

110

        } else {

111

500

            weak_bisimulation_impl(&tau_loop_free_lts)

112

};

113

800

        (tau_loop_free_lts, mapped_state, blocks)

114

800

})

115

800

116

117

/// The implementation of [weak_bisimulation_parallel] that assumes the LTS has already been preprocessed.

118

700

fn weak_bisimulation_parallel_preprocessed<L: LTS>(

119

700

    lts: L,

120

700

    state: StateIndex,

121

700

    divergence_preserving: bool,

122

700

    timing: &Timing,

123

700

) -> (LabelledTransitionSystem<L::Label>, StateIndex, MarkedBlockPartition) {

124

700

    let (tau_loop_free_lts, mapped_state) = timing.measure("preprocess", || {

125

700

        tau_cycle_elimination_and_reorder(lts, state, !divergence_preserving)

126

700

});

127

128

700

    timing.measure("reduction", || {

129

700

        let blocks = if divergence_preserving {

130

300

            let divergence_preserving_lts = DivergencePreservingLts::new(&tau_loop_free_lts);

131

300

            weak_bisimulation_parallel_impl(&divergence_preserving_lts)

132

        } else {

133

400

            weak_bisimulation_parallel_impl(&tau_loop_free_lts)

134

};

135

700

        (tau_loop_free_lts, mapped_state, blocks)

136

700

})

137

700

138

139

/// The implementation of [weak_bisimulation].

140

800

fn weak_bisimulation_impl<L: LTS>(lts: &L) -> MarkedBlockPartition {

141

800

    let mut blocks = MarkedBlockPartition::new(lts.num_of_states());

142

143

800

    let mut act_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

144

800

    let mut tau_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

145

146

800

    let incoming = IncomingTransitions::new(lts);

147

148

800

    let progress = TimeProgress::new(

149

406

        |num_of_blocks: usize| {

150

406

            info!("Found {} blocks...", num_of_blocks);

151

406

},

152

1,

153

);

154

155

    loop {

156

5856

        let mut stable = true;

157

415555

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

158

415555

            progress.print(blocks.num_of_blocks());

159

415555

            if *blocks.block(block_index).annotation() {

160

327123

                continue;

161

88432

162

163

88432

            trace!("Stabilising block {:?}", block_index);

164

88432

            stable = false;

165

88432

            blocks.mark_block_stable(block_index);

166

167

            // tau is the first label.

168

285367

            for label in lts.labels().iter().enumerate().map(|(i, _)| LabelIndex::new(i)) {

169

285367

                compute_weak_act(

170

285367

                    &mut act_mark,

171

285367

                    &mut tau_mark,

172

285367

                    lts,

173

285367

                    &blocks,

174

285367

                    &incoming,

175

285367

                    block_index,

176

285367

                    label,

177

);

178

179

                // Note that we cannot use the block references here, and instead uses indices, because stabilise

180

                // also modifies the blocks structure.

181

38649115

                for block_prime in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

182

38649115

                    stabilise(block_prime, &mut act_mark, &mut blocks);

183

38649115

184

185

186

187

5856

        if stable {

188

800

            trace!("Partition is stable!");

189

800

            break;

190

5056

191

192

193

800

    blocks

194

800

195

196

/// The implementation of [weak_bisimulation_parallel].

197

700

fn weak_bisimulation_parallel_impl<L: LTS>(lts: &L) -> MarkedBlockPartition {

198

700

    let progress = TimeProgress::new(

199

        |num_of_blocks: usize| {

200

            info!("Found {} blocks...", num_of_blocks);

201

},

202

1,

203

);

204

205

700

    let mut blocks = MarkedBlockPartition::new(lts.num_of_states());

206

207

    // Represents the s.marked[a] from the pseudocode.

208

700

    let mut marked = Vec::from_iter(iter::repeat_n(

209

700

        bitvec![u64, Lsb0; 0; lts.labels().len()],

210

700

        lts.num_of_states(),

211

));

212

213

700

    let incoming = IncomingTransitions::new(lts);

214

215

    loop {

216

4739

        let mut stable = true;

217

165228

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

218

165228

            progress.print(blocks.num_of_blocks());

219

165228

            if *blocks.block(block_index).annotation() {

220

118718

                continue;

221

46510

222

223

46510

            trace!("Stabilising block {:?}", block_index);

224

46510

            stable = false;

225

46510

            blocks.mark_block_stable(block_index);

226

227

            // marked := 0 for all states and actions

228

7103586

            for act_mark in &mut marked {

229

7103586

                act_mark.fill(false);

230

7103586

231

232

46510

            compute_weak_acts(&mut marked, lts, &incoming, &blocks, block_index);

233

234

68464

            while let Some(label) = find_act(lts, &blocks, &mut marked) {

235

749936

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

236

749936

                    stabilise_act(block_index, label, &mut marked, &mut blocks);

237

749936

238

239

240

241

4739

        if stable {

242

700

            trace!("Partition is stable!");

243

700

            break;

244

4039

245

246

247

700

    blocks

248

700

249

250

/// Sets s.act_mark to true iff exists t: S. s =\not{a}=> t

251

/// If a = tau, then also updates s.tau_mark

252

445401

fn compute_weak_act<L: LTS>(

253

445401

    act_mark: &mut BitArray,

254

445401

    tau_mark: &mut BitArray,

255

445401

    lts: &L,

256

445401

    blocks: &MarkedBlockPartition,

257

445401

    incoming: &IncomingTransitions,

258

445401

    block: BlockIndex,

259

445401

    label: LabelIndex,

260

445401

) {

261

177330790

    for s in lts.iter_states() {

262

        // s.act_mark := true iff s in B && a == tau

263

177330790

        act_mark.set(

264

177330790

*s,

265

274138438

            lts.is_hidden_label(label) && blocks.iter_block(block).any(|state| state == *s),

266

);

267

268

179906486

        for transition in lts.outgoing_transitions(s) {

269

179906486

            if transition.label == label {

270

                // s.act_mark := true iff a != tau && tau_mark[t]

271

57706133

                if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {

272

616339

                    act_mark.set(*s, true);

273

57089794

274

122200353

275

276

277

278

177330790

    for t in lts.iter_states() {

279

        // t.tau_mark := t.act_mark if a == tau

280

177330790

        if lts.is_hidden_label(label) {

281

56952082

            tau_mark.set(*t, act_mark[*t]);

282

120378708

283

284

177330790

        if act_mark[*t] {

285

1712887

            for transition in incoming.incoming_silent_transitions(t) {

286

564484

                act_mark.set(*transition.from, true);

287

564484

288

175617903

289

290

445401

291

292

/// Computing weak reachability for all actions at once. The `marked` array contains |Act| entries per state.

293

///

294

/// # Details

295

///

296

/// Requires s.tau_mark iff s ->> B.

297

/// For all a in A sets s.marked[a] iff s =[a]> B.

298

///

299

/// Note that `B` is only used for debugging checks, and is not used in the actual algorithm.

300

46510

fn compute_weak_acts<L: LTS>(

301

46510

    marked: &mut [BitArray],

302

46510

    lts: &L,

303

46510

    incoming: &IncomingTransitions<'_>,

304

46510

    blocks: &MarkedBlockPartition,

305

46510

    block: BlockIndex,

306

46510

) {

307

46510

    if cfg!(debug_assertions) {

308

        // Check that compute_weak_act results in the same markings as the optimised compute_weak_acts procedure.

309

310

        // Determine the tau_mark first, the act_mark result is ignored.

311

46510

        let mut tau_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

312

7103586

        for s in lts.iter_states() {

313

7103586

            tau_mark.set(*s, marked[*s][0]);

314

7103586

315

316

        // Determine the act_mark for every label that is not tau

317

46510

        let act_mark = (0..lts.labels().len())

318

160034

            .map(|label| {

319

160034

                let mut act_mark = bitvec![u64, Lsb0; 0; lts.num_of_states()];

320

321

24580404

                for s in lts.iter_states() {

322

24580404

                    act_mark.set(*s, marked[*s][label]);

323

24580404

324

325

160034

                compute_weak_act(

326

160034

                    &mut act_mark,

327

160034

                    &mut tau_mark,

328

160034

                    lts,

329

160034

                    blocks,

330

160034

                    incoming,

331

160034

                    block,

332

160034

                    LabelIndex::new(label),

333

);

334

160034

                act_mark

335

160034

})

336

46510

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

337

338

        // Compute the markings using the optimised procedure.

339

46510

        compute_weak_acts_inner(marked, lts, incoming, blocks, block);

340

341

        // Check that the markings are the same for all labels, except tau

342

113524

        for label in 1..lts.labels().len() {

343

            // The act_mark array starts at the first action, because we skip the tau action (index 0).

344

113524

            debug_assert!(

345

17476818

                act_mark[label].iter().zip(marked.iter()).all(|(a, m)| a == m[label]),

346

                "The act mark should be the same as the corresponding column in marked"

347

);

348

349

    } else {

350

        // No checking for correctness.

351

        compute_weak_acts_inner(marked, lts, incoming, blocks, block);

352

353

46510

354

355

/// The inner implementation of [compute_weak_acts]. For all action a, sets s.marked[a] iff s =[a]> B, where B is the given block.

356

///

357

/// # Details

358

///

359

/// Requires that marked = 0 for all states.

360

46510

fn compute_weak_acts_inner<L: LTS>(

361

46510

    marked: &mut [BitArray],

362

46510

    lts: &L,

363

46510

    incoming: &IncomingTransitions<'_>,

364

46510

    blocks: &MarkedBlockPartition,

365

46510

    block: BlockIndex,

366

46510

) {

367

46510

    debug_assert!(

368

7103586

        marked.iter().all(|m| m.not_any()),

369

        "The marked array should be empty when calling compute_weak_acts_inner"

370

);

371

372

    // TODO: This should probably not be hardcoded.

373

46510

    let tau_index = LabelIndex::new(0);

374

46510

    debug_assert!(

375

46510

        lts.is_hidden_label(tau_index),

376

        "The first label should be the tau action"

377

);

378

379

    // For t in B: t.marked[tau] := true

380

249341

    for t in blocks.iter_block(block) {

381

249341

        marked[t].set(*tau_index, true);

382

249341

383

384

7103586

    for t in lts.iter_states() {

385

7103586

        if marked[*t][*tau_index] {

386

            // For each s -[tau]-> t do

387

286553

            for transition in incoming.incoming_silent_transitions(t) {

388

96120

                // s.marked[tau] := True if t.marked[tau]

389

96120

                marked[transition.from].set(*tau_index, true);

390

96120

391

6817033

392

393

394

7103586

    for t in lts.iter_states() {

395

        // For each t -[a]-> u do

396

7465882

        for transition in lts.outgoing_transitions(t) {

397

            // If u.marked[tau] then t.marked[a] := true

398

7465882

            if marked[*transition.to][*tau_index] {

399

300006

                marked[*t].set(*transition.label, true);

400

7165876

401

402

403

        // For each s -[tau]-> t do

404

7103586

        for transition in incoming.incoming_silent_transitions(t) {

405

            // Computes s.marked[a] := s.marked[a] | t.marked[a] in place.

406

2415315

            let [marked_s, marked_t] = marked

407

2415315

                .get_disjoint_mut([*transition.from, *t])

408

2415315

                .expect("The indices are disjoint");

409

2415315

            for (i, number) in marked_s.as_raw_mut_slice().iter_mut().enumerate() {

410

2415315

                *number |= marked_t.as_raw_slice()[i];

411

2415315

412

413

414

46510

415

416

/// Finding an action that can be used to perform a refinement step.

417

68464

fn find_act<L: LTS>(_lts: &L, blocks: &MarkedBlockPartition, marked: &mut [BitArray]) -> Option<LabelIndex> {

418

2685362

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

419

        // Pick a representative state s from the block

420

2685362

        let s = blocks.iter_block(block).next().expect("Block is non-empty");

421

8940921

        for t in blocks.iter_block(block) {

422

8940921

            if marked[s] != marked[t] {

423

                // Find an action a such that s.marked[a] != t.marked[a]

424

51904

                for (label, marked_s) in marked[s].iter().enumerate() {

425

51904

                    if marked_s != marked[t][label] {

426

21954

                        return Some(LabelIndex::new(label));

427

29950

428

429

8918967

430

431

432

433

46510

    None

434

68464

435

436

/// Splits the given block according to the given marking.

437

38649115

fn stabilise(block: BlockIndex, act_mark: &mut BitArray, blocks: &mut MarkedBlockPartition) {

438

152750386

    blocks.split_block(block, |state| act_mark[*state]);

439

38649115

440

441

/// Splits the given block according to the given marking.

442

749936

fn stabilise_act(block: BlockIndex, act: LabelIndex, marked: &mut [BitArray], blocks: &mut MarkedBlockPartition) {

443

3338942

    blocks.split_block(block, |state| marked[*state][*act]);

444

749936

445

446

#[cfg(test)]

447

mod tests {

448

    use merc_io::DumpFiles;

449

    use merc_lts::LTS;

450

    use merc_lts::random_lts;

451

    use merc_lts::write_aut;

452

    use merc_utilities::Timing;

453

    use merc_utilities::random_test;

454

455

    use crate::Equivalence;

456

    use crate::compare_lts;

457

    use crate::reduce_lts;

458

    // use crate::signature_refinement::test_mcrl2_sigref_vs_ltsconvert_impl;

459

460

    #[test]

461

    #[cfg_attr(miri, ignore)]

462

1

    fn test_weak_bisimulation() {

463

100

        random_test(100, |rng| {

464

100

            let files = DumpFiles::new("test_weak_bisimulation");

465

466

100

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

467

100

            let timing = Timing::new();

468

100

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

469

470

100

            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &timing);

471

100

            let expected = reduce_lts(lts, Equivalence::WeakBisimSigref, false, &timing);

472

473

100

            assert_eq!(result.num_of_states(), expected.num_of_states());

474

100

            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

475

476

100

            files.dump("result.aut", |f| write_aut(f, &result)).unwrap();

477

100

            files.dump("expected.aut", |f| write_aut(f, &expected)).unwrap();

478

479

100

            assert!(compare_lts(Equivalence::StrongBisim, result, expected, false, &timing));

480

100

})

481

1

482

483

    #[test]

484

    #[cfg_attr(miri, ignore)]

485

1

    fn test_weak_bisimulation_parallel() {

486

100

        random_test(100, |rng| {

487

100

            let files = DumpFiles::new("test_weak_bisimulation_parallel");

488

489

100

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

490

100

            let timing = Timing::new();

491

100

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

492

493

100

            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &timing);

494

100

            let expected = reduce_lts(lts, Equivalence::WeakBisimParallel, false, &timing);

495

496

100

            assert_eq!(result.num_of_states(), expected.num_of_states());

497

100

            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

498

499

100

            files.dump("result.aut", |f| write_aut(f, &result)).unwrap();

500

100

            files.dump("expected.aut", |f| write_aut(f, &expected)).unwrap();

501

502

100

            assert!(compare_lts(Equivalence::StrongBisim, result, expected, false, &timing));

503

100

})

504

1

505