Grcov report - sigref.rs

1

use std::fmt;

2

use std::ops::Range;

3

4

use itertools::Itertools;

5

use log::debug;

6

use log::info;

7

use log::trace;

8

use merc_io::TimeProgress;

9

use merc_utilities::MercError;

10

use merc_utilities::Timing;

11

use oxidd::BooleanFunction;

12

use oxidd::BooleanFunctionQuant;

13

use oxidd::BooleanOperator;

14

use oxidd::Edge;

15

use oxidd::Function;

16

use oxidd::HasLevel;

17

use oxidd::Manager;

18

use oxidd::ManagerRef;

19

use oxidd::Node;

20

use oxidd::VarNo;

21

use oxidd::bdd::BDDFunction;

22

use oxidd::bdd::BDDManagerRef;

23

use oxidd::error::DuplicateVarName;

24

use oxidd::util::Borrowed;

25

use oxidd::util::OptBool;

26

use oxidd::util::OutOfMemory;

27

use oxidd_core::function::EdgeOfFunc;

28

use oxidd_core::util::EdgeDropGuard;

29

use oxidd_dump::Visualizer;

30

use oxidd_rules_bdd::simple::BDDTerminal;

31

use rustc_hash::FxHashMap;

32

use rustc_hash::FxHashSet;

33

34

use crate::CubeIterAll;

35

use crate::SatCountCache;

36

use crate::SummandGroupBdd;

37

use crate::SymbolicLtsBdd;

38

use crate::ValuesIter;

39

use crate::approx_satcount;

40

use crate::collect_children;

41

use crate::compute_vars_bdd;

42

use crate::reduce;

43

use crate::required_bits_64;

44

use crate::to_value;

45

use crate::variable_rename;

46

47

/// Computes the reduction of the given symbolic LTS using symbolic signature

48

/// refinement.

49

///

50

/// # Details

51

///

52

/// The implementation is based on the following paper:

53

///

54

/// > Tom van Dijk and Jaco van de Pol. Multi-core Symbolic Bisimulation

55

/// > Minimization.

56

302

pub fn sigref_symbolic(

57

302

    manager_ref: &BDDManagerRef,

58

302

    lts: &SymbolicLtsBdd,

59

302

    timing: &Timing,

60

302

    split_signature: bool,

61

302

    extend_relation: bool,

62

302

    merge_transitions: bool,

63

302

    visualize: bool,

64

302

) -> Result<(BDDFunction, Vec<VarNo>, usize), MercError> {

65

302

    if merge_transitions && !extend_relation {

66

        debug!("merge_transitions requires full-domain transition relations; enabling relation extension");

67

302

68

69

302

    let use_extended_relations = extend_relation || merge_transitions;

70

302

    let use_split_signature = split_signature && !merge_transitions;

71

72

302

    let preprocessed_lts = preprocess_lts(manager_ref, lts, use_extended_relations, merge_transitions)?;

73

74

302

    sigref_symbolic_impl(manager_ref, &preprocessed_lts, timing, use_split_signature, visualize)

75

302

76

77

/// Preprocess the LTS based on the input options.

78

///

79

/// # Details

80

///

81

/// When `extend_relations` is set, each transition relation is extended with `x = x'`

82

/// for every state variable that is not written by the relation; the group's read

83

/// and write variables then cover the full state domain. When `merge_transitions`

84

/// is set, the (extended) relations are then combined into a single transition

85

/// group covering the full state domain.

86

302

fn preprocess_lts(

87

302

    manager_ref: &BDDManagerRef,

88

302

    lts: &SymbolicLtsBdd,

89

302

    extend_relations: bool,

90

302

    merge_transitions: bool,

91

302

) -> Result<SymbolicLtsBdd, MercError> {

92

302

    if !extend_relations && !merge_transitions {

93

302

        let groups = lts

94

302

            .transition_groups()

95

302

            .iter()

96

1562

            .map(|group| {

97

1562

                SummandGroupBdd::new(

98

1562

                    group.relation().clone(),

99

1562

                    group.read_variables().to_vec(),

100

1562

                    group.write_variables().to_vec(),

101

102

1562

})

103

302

            .collect();

104

302

        return Ok(SymbolicLtsBdd::with_transition_groups(lts, groups));

105

106

107

    // Extend each transition relation to the full state/next-state domain.

108

    let mut groups: Vec<SummandGroupBdd> = lts

109

        .transition_groups()

110

        .iter()

111

        .map(|group| -> Result<SummandGroupBdd, MercError> {

112

            let relation = extend_relation(

113

                manager_ref,

114

                group.relation(),

115

                lts.state_variables(),

116

                lts.next_state_variables(),

117

                group.write_variables(),

118

)?;

119

            Ok(SummandGroupBdd::new(

120

                relation,

121

                lts.state_variables().to_vec(),

122

                lts.next_state_variables().to_vec(),

123

))

124

})

125

        .collect::<Result<Vec<_>, MercError>>()?;

126

127

    if merge_transitions && !groups.is_empty() {

128

        let mut merged_relation = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

129

        for group in &groups {

130

            merged_relation = merged_relation.or(group.relation())?;

131

132

        groups = vec![SummandGroupBdd::new(

133

            merged_relation,

134

            lts.state_variables().to_vec(),

135

            lts.next_state_variables().to_vec(),

136

)];

137

138

139

    Ok(SymbolicLtsBdd::with_transition_groups(lts, groups))

140

302

141

142

/// Implementation of [sigref_symbolic] on an already preprocessed LTS.

143

302

fn sigref_symbolic_impl(

144

302

    manager_ref: &BDDManagerRef,

145

302

    lts: &SymbolicLtsBdd,

146

302

    timing: &Timing,

147

302

    split_signature: bool,

148

302

    visualize: bool,

149

302

) -> Result<(BDDFunction, Vec<VarNo>, usize), MercError> {

150

302

    let split_partition_groups = if split_signature {

151

100

        combine_transition_groups(manager_ref, lts)?

152

    } else {

153

202

        Vec::new()

154

};

155

156

302

    let mut satcount_cache = SatCountCache::new();

157

302

    let num_of_states = approx_satcount(lts.states(), lts.state_variables().len() as VarNo, &mut satcount_cache);

158

302

    let num_of_block_bits = (num_of_states.as_f64().log2().ceil() as u32).max(1);

159

302

    debug!("Number of block bits: {}", num_of_block_bits);

160

161

302

    let block_variable_names = (0..num_of_block_bits)

162

1165

        .map(|i| format!("b_{}", i))

163

302

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

164

165

    // Create variables in the BDD manager

166

302

    let block_variable_indices: Vec<VarNo> = manager_ref

167

302

        .with_manager_exclusive(|manager| -> Result<Range<VarNo>, DuplicateVarName> {

168

302

            manager.add_named_vars(block_variable_names)

169

302

})

170

302

        .map_err(|e| format!("Failed to create variables: {e}"))?

171

302

        .collect();

172

173

    // Create BDD functions for the block variables

174

302

    let block_variables_bdds = compute_vars_bdd(manager_ref, &block_variable_indices)?.0;

175

176

    // Caches for [refine]. `refine_cache` is the BDD-level memo and its allocation is reused across

177

    // iterations (cleared each iteration). `claimed_blocks` records which old block ids have already

178

    // been claimed (reused as-is) this iteration; `next_fresh_id` is the persistent counter handing

179

    // out new block ids for splits, so num_of_blocks == next_fresh_id once refine returns.

180

302

    let mut refine_cache: FxHashMap<(BDDFunction, BDDFunction), BDDFunction> = FxHashMap::default();

181

302

    let mut claimed_blocks: FxHashSet<u64> = FxHashSet::default();

182

302

    let mut next_fresh_id: u64 = 1;

183

184

    // Substitution to replace state variables with next state variables.

185

302

    let state_substitution: Vec<(VarNo, VarNo)> = lts

186

302

        .state_variables()

187

302

        .iter()

188

302

        .cloned()

189

302

        .zip(lts.next_state_variables().iter().cloned())

190

302

        .collect();

191

192

    // Determine the variables in the support of a signature function.

193

302

    let signature_variables = lts

194

302

        .next_state_variables()

195

302

        .iter()

196

302

        .chain(lts.action_variables())

197

302

        .chain(block_variable_indices.iter())

198

302

        .cloned()

199

302

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

200

201

    // Determine the variables in the support of a partition function.

202

302

    let partition_variables = lts

203

302

        .next_state_variables()

204

302

        .iter()

205

302

        .chain(block_variable_indices.iter())

206

302

        .cloned()

207

302

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

208

209

    // Stores the partition of the states as BDD.

210

302

    let mut partition = lts.states().and(&manager_ref.with_manager_shared(

211

302

        |manager| -> Result<BDDFunction, OutOfMemory> {

212

302

            Ok(BDDFunction::from_edge(

213

302

                manager,

214

302

                encode_block(manager, &block_variables_bdds, 0)?,

215

))

216

302

},

217

    )?)?;

218

219

    // In the sigref algorithm, the partition is defined over the next state. When we compute the signature

220

    // we then get (s, a, b), since in the signature we need to consider the block of the next state.

221

302

    partition = variable_rename(manager_ref, &partition, &state_substitution)?;

222

223

    // Keep track of local information.

224

302

    let mut num_of_blocks = 0;

225

302

    let mut iteration = 0usize;

226

227

302

    let progress = TimeProgress::new(

228

31

        |(iterations, num_of_blocks): (usize, usize)| {

229

31

            info!("iteration {}: {} blocks", iterations, num_of_blocks);

230

31

},

231

1,

232

);

233

234

302

    if visualize {

235

        // Visualize the initial partition.

236

        manager_ref.with_manager_shared(|manager| {

237

            Visualizer::new()

238

                .add("initial_partition", manager, [&partition])

239

                .serve()

240

        })?;

241

302

242

243

302

    trace!(

244

        "Initial partition: {}",

245

        PartitionDisplay::new(

246

            &partition,

247

            &partition_variables,

248

            lts.state_variable_num_of_bits(),

249

            num_of_block_bits

250

251

);

252

253

    // Quantification BDD per transition group, derived from the (already

254

    // preprocessed) write variables of that group.

255

302

    let relation_quantified_next_state_vars: Vec<BDDFunction> = lts

256

302

        .transition_groups()

257

302

        .iter()

258

1562

        .map(|group| -> Result<_, MercError> { Ok(compute_vars_bdd(manager_ref, group.write_variables())?.1) })

259

302

        .collect::<Result<Vec<_>, MercError>>()?;

260

261

302

    let mut signature_index = 0;

262

302

    let mut changed_in_cycle = false;

263

    loop {

264

        // No fixed point reached yet, so keep refining.

265

738

        let old_num_of_blocks = num_of_blocks;

266

738

        trace!("Iteration {} ({} blocks)", iteration, num_of_blocks);

267

268

        // Compute the new signatures w.r.t. the previous partition.

269

738

        let signature = timing.measure("signature", || -> Result<BDDFunction, OutOfMemory> {

270

738

            let mut signature = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));

271

272

            // Select which transition groups to combine in this iteration: either a single

273

            // partition class (split signature) or all groups at once.

274

738

            let group_indices: Box<dyn Iterator<Item = usize>> =

275

738

                if split_signature && !split_partition_groups.is_empty() {

276

236

                    Box::new(split_partition_groups[signature_index].iter().copied())

277

                } else {

278

502

                    Box::new(0..lts.transition_groups().len())

279

};

280

281

4331

            for index in group_indices {

282

                // We explicitly do not quantify over next-state variables that are not written

283

                // by the transition group. Otherwise these s' would become unconstrained and,

284

                // after the s -> s' rename below, would conflate states.

285

4331

                let group_signature = timing.measure(&format!("group_signature_{}", index), || {

286

4331

                    signature_strong(

287

4331

                        &partition,

288

4331

                        lts.transition_groups()[index].relation(),

289

4331

                        &relation_quantified_next_state_vars[index],

290

291

4331

                })?;

292

293

4331

                let group_signature = variable_rename(manager_ref, &group_signature, &state_substitution)?;

294

4331

                signature = timing.measure("signature_or", || signature.or(&group_signature))?;

295

296

297

738

            Ok(signature)

298

738

        })?;

299

300

738

        trace!(

301

            "Signature at iteration {}: {}",

302

            iteration,

303

            SignatureDisplay::new(

304

                &signature,

305

                &signature_variables,

306

                lts.state_variable_num_of_bits(),

307

                lts.action_variables().len() as u32,

308

                num_of_block_bits

309

310

);

311

312

738

        if visualize {

313

            // Visualize the computed signature.

314

            manager_ref.with_manager_shared(|manager| {

315

                Visualizer::new()

316

                    .add(&format!("signature_{iteration}"), manager, [&signature])

317

                    .serve()

318

            })?;

319

738

320

321

        // Build the new partition based on the signatures.

322

738

        partition = timing.measure("refine", || {

323

738

            refine(

324

738

                manager_ref,

325

738

                &mut refine_cache,

326

738

                &mut claimed_blocks,

327

738

                &mut next_fresh_id,

328

738

                &block_variables_bdds,

329

738

                lts.next_state_variables(),

330

738

                &signature,

331

738

                &partition,

332

333

738

        })?;

334

335

738

        if visualize {

336

            // Visualize the current partition.

337

            manager_ref.with_manager_shared(|manager| {

338

                Visualizer::new()

339

                    .add(&format!("partition_{iteration}"), manager, [&partition])

340

                    .serve()

341

            })?;

342

738

343

344

738

        trace!(

345

            "Partition at iteration {}: {}",

346

            iteration,

347

            PartitionDisplay::new(

348

                &partition,

349

                &partition_variables,

350

                lts.state_variable_num_of_bits(),

351

                num_of_block_bits

352

353

);

354

355

738

        num_of_blocks = next_fresh_id as usize;

356

738

        progress.print((iteration, num_of_blocks));

357

738

        iteration += 1;

358

359

738

        if split_signature {

360

236

            if num_of_blocks != old_num_of_blocks {

361

136

                changed_in_cycle = true;

362

136

363

364

236

            signature_index += 1;

365

236

            if signature_index >= split_partition_groups.len() {

366

                // Completed a full sweep over every partition class: we have a fixed point

367

                // only if not a single class refined the partition during this sweep.

368

236

                if !changed_in_cycle {

369

100

                    break;

370

136

371

136

                changed_in_cycle = false;

372

136

                signature_index = 0;

373

374

502

        } else if num_of_blocks == old_num_of_blocks {

375

202

            break;

376

300

377

378

        // Per-iteration state is rebuilt; `next_fresh_id` is persistent so new ids never collide

379

        // with ids carried over from the previous partition.

380

436

        claimed_blocks.clear();

381

436

        refine_cache.clear();

382

383

384

302

    info!(

385

        "Signature refinement completed in {} iterations with {} blocks",

386

        iteration, num_of_blocks

387

);

388

389

302

    Ok((partition, block_variable_indices, num_of_blocks))

390

302

391

392

/// Computes a partitioning of the transition groups for the given LTS based on the split signature option.

393

///

394

/// # Details

395

///

396

/// Two transition groups are combined if they share action labels, this ensures that in split signature mode

397

/// the action labels of all transition groups are disjoint.

398

100

fn combine_transition_groups(manager_ref: &BDDManagerRef, lts: &SymbolicLtsBdd) -> Result<Vec<Vec<usize>>, MercError> {

399

    // In split signature mode we must ensure that the action labels of all transition groups are disjoint. We do this by merging

400

    // transition groups that share action labels.

401

402

    // Cube over the state and next-state variables; quantifying these out of a relation leaves

403

    // only the action labels.

404

100

    let state_and_next_state_vars = manager_ref.with_manager_shared(|manager| -> Result<_, OutOfMemory> {

405

100

        let mut bdd: BDDFunction = BDDFunction::t(manager);

406

407

5996

        for var in lts.state_variables().iter().chain(lts.next_state_variables().iter()) {

408

5996

            let var = BDDFunction::var(manager, *var)?;

409

5996

            bdd = bdd.and(&var)?;

410

411

412

100

        Ok(bdd)

413

100

    })?;

414

415

    // Compute the action labels for all transition groups.

416

100

    let representatives = lts

417

100

        .transition_groups()

418

100

        .iter()

419

500

        .map(|group| group.relation().exists(&state_and_next_state_vars))

420

100

        .collect::<Result<Vec<BDDFunction>, OutOfMemory>>()?;

421

422

    // Build connected components under "shares an action label". For each class we cache the

423

    // union of its members' action-label BDDs so the overlap test stays a single `and` per

424

    // pair, and we absorb every overlapping class — the relation is not transitive, so a

425

    // single-pass check against one representative per class would miss merges that chain

426

    // through other groups.

427

100

    let mut classes: Vec<(Vec<usize>, BDDFunction)> = Vec::new();

428

429

500

    for (i, representative) in representatives.iter().enumerate().take(lts.transition_groups().len()) {

430

500

        let mut merged_members = vec![i];

431

500

        let mut merged_rep = representative.clone();

432

433

500

        let mut j = 0;

434

900

        while j < classes.len() {

435

400

            if classes[j].1.and(&merged_rep)?.satisfiable() {

436

400

                let (members, rep) = classes.remove(j);

437

400

                merged_members.extend(members);

438

400

                merged_rep = merged_rep.or(&rep)?;

439

            } else {

440

                j += 1;

441

442

443

444

500

        classes.push((merged_members, merged_rep));

445

446

447

100

    let result: Vec<Vec<usize>> = classes.into_iter().map(|(members, _)| members).collect();

448

449

100

    debug!("Combined transition groups: {:?}", result);

450

100

    Ok(result)

451

100

452

453

/// Computes the strong signature refinement of the given partition and

454

/// relation.

455

///

456

/// # Details

457

///

458

/// For strong bisimulation the signature is defined as follows, where `P` is

459

/// the previous partition defined over the next state variables, and `relation` is defined

460

/// over the states, next states and the action label bits.

461

///

462

/// > ∃ s'. (relation(s, s', a) ∧ P(s', b))

463

4331

fn signature_strong(

464

4331

    partition: &BDDFunction,

465

4331

    relation: &BDDFunction,

466

4331

    next_state_vars: &BDDFunction,

467

4331

) -> Result<BDDFunction, OutOfMemory> {

468

4331

    partition.apply_exists(BooleanOperator::And, relation, next_state_vars)

469

4331

470

471

/// Refines the partition w.r.t. the given signature by assigning block numbers

472

/// to signatures.

473

///

474

/// # Details

475

///

476

/// This function assumes that in the partition only a single block number is

477

/// assigned to each state, which should be by definition.

478

///

479

/// This function computes the new partition `P` such that:

480

///

481

/// > For all states s, t it holds that P(s) == P(t) iff signature(s) == signature(t)

482

#[allow(clippy::too_many_arguments)]

483

738

fn refine(

484

738

    manager_ref: &BDDManagerRef,

485

738

    cache: &mut FxHashMap<(BDDFunction, BDDFunction), BDDFunction>,

486

738

    claimed_blocks: &mut FxHashSet<u64>,

487

738

    next_fresh_id: &mut u64,

488

738

    block_variables_bdds: &[BDDFunction],

489

738

    next_state_variables: &[VarNo],

490

738

    signature: &BDDFunction,

491

738

    partition: &BDDFunction,

492

738

) -> Result<BDDFunction, MercError> {

493

738

    debug_assert!(

494

738

        check_partition_function(manager_ref, partition, next_state_variables)?,

495

        "The given partition function is not a valid partition function"

496

);

497

498

738

    manager_ref.with_manager_shared(|manager| {

499

738

        let mut ctx = RefineContext {

500

738

            manager,

501

738

            cache,

502

738

            claimed_blocks,

503

738

            next_fresh_id,

504

738

            block_variables_bdds,

505

738

            next_state_variables,

506

738

};

507

508

738

        Ok(BDDFunction::from_edge(

509

738

            manager,

510

738

            refine_edge(

511

738

                &mut ctx,

512

738

                signature.as_edge(manager).borrowed(),

513

738

                partition.as_edge(manager).borrowed(),

514

)?,

515

))

516

738

})

517

738

518

519

/// Shared state threaded through the [refine_edge] recursion.

520

struct RefineContext<'a, 'id: 'a> {

521

    manager: &'a <BDDFunction as Function>::Manager<'id>,

522

    cache: &'a mut FxHashMap<(BDDFunction, BDDFunction), BDDFunction>,

523

    /// Old block ids already claimed by some signature this iteration; their states' partition BDD

524

    /// is returned as-is so the id is reused without reallocation.

525

    claimed_blocks: &'a mut FxHashSet<u64>,

526

    /// Strictly increasing counter for block ids allocated due to splits. Persisted across

527

    /// iterations so fresh ids never collide with ids carried over from the previous partition.

528

    next_fresh_id: &'a mut u64,

529

    block_variables_bdds: &'a [BDDFunction],

530

    next_state_variables: &'a [VarNo],

531

532

533

/// Recursive implementation of the [refine] function.

534

1990764

fn refine_edge<'id>(

535

1990764

    ctx: &mut RefineContext<'_, 'id>,

536

1990764

    signature: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

537

1990764

    partition: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

538

1990764

) -> Result<EdgeOfFunc<'id, BDDFunction>, OutOfMemory> {

539

1990764

    let manager = ctx.manager;

540

541

1990764

    let plevel = match manager.get_node(&partition) {

542

883349

        Node::Terminal(terminal) => {

543

883349

            if terminal == BDDTerminal::False {

544

                // In this case the state is not part of the partition function, so return empty.

545

883349

                return Ok(manager.clone_edge(&partition));

546

547

548

            unreachable!("There are always block variables, so cannot be true terminal");

549

550

1107415

        Node::Inner(node) => node.level(),

551

};

552

553

1107415

    if let Some(cached) = ctx.cache.get(&(

554

1107415

        BDDFunction::from_edge(manager, manager.clone_edge(&signature)),

555

1107415

        BDDFunction::from_edge(manager, manager.clone_edge(&partition)),

556

1107415

    )) {

557

82193

        return Ok(manager.clone_edge(cached.as_edge(manager)));

558

1025222

559

560

    // topVar

561

1025222

    let lowest_level = {

562

1025222

        let slevel = match manager.get_node(&signature) {

563

6112

            Node::Terminal(_) => plevel,

564

1019110

            Node::Inner(node) => node.level(),

565

};

566

1025222

        plevel.min(slevel)

567

};

568

569

1025222

    let result = if ctx.next_state_variables.contains(&lowest_level) {

570

        // Match paths on the level s'_i, for irrelevant variables we take both paths.

571

995013

        let (s_high, s_low) = match manager.get_node(&signature) {

572

989122

            Node::Inner(node) if node.level() == lowest_level => collect_children(node),

573

111831

            _ => (signature.borrowed(), signature.borrowed()),

574

};

575

995013

        let (p_high, p_low) = match manager.get_node(&partition) {

576

995013

            Node::Inner(node) if node.level() == lowest_level => collect_children(node),

577

5369

            _ => (partition.borrowed(), partition.borrowed()),

578

};

579

580

995013

        let low = refine_edge(ctx, s_low, p_low)?;

581

995013

        let high = refine_edge(ctx, s_high, p_high)?;

582

583

        // 7. result := BDDnode(topVar, high, low)

584

995013

        Ok(reduce(manager, lowest_level, high, low)?)

585

    } else {

586

        // Leaf: \sigma encodes the (action, target block) signature and P encodes the old block id.

587

        // Reuse the old id for the first signature that claims it (returning the partition edge

588

        // unchanged); any further signatures sharing that old block are splits and get a fresh id

589

        // from the persistent counter. The outer BDD memo above keys by (sig, partition) so

590

        // repeated (sig, partition) pairs reuse this assignment without re-decoding.

591

30209

        let block_index = decode_block(manager, partition.borrowed());

592

30209

        if ctx.claimed_blocks.insert(block_index) {

593

26533

            trace!("Reusing old block {block_index}");

594

26533

            Ok(manager.clone_edge(&partition))

595

        } else {

596

3676

            let new_block_index = *ctx.next_fresh_id;

597

3676

            *ctx.next_fresh_id += 1;

598

3676

            trace!("Allocating fresh block {new_block_index} (split from {block_index})");

599

3676

            Ok(encode_block(manager, ctx.block_variables_bdds, new_block_index)?)

600

601

}?;

602

603

1025222

    ctx.cache.insert(

604

1025222

605

1025222

            BDDFunction::from_edge(manager, manager.clone_edge(&signature)),

606

1025222

            BDDFunction::from_edge(manager, manager.clone_edge(&partition)),

607

1025222

),

608

1025222

        BDDFunction::from_edge(manager, manager.clone_edge(&result)),

609

);

610

611

1025222

    Ok(result)

612

1990764

613

614

/// Checks if the given BDD contains a function from `domain` to `range`.

615

///

616

/// # Details

617

///

618

/// Assumes that the domain variables all occur strictly before the range

619

/// variables.

620

738

fn check_partition_function(

621

738

    manager_ref: &BDDManagerRef,

622

738

    bdd: &BDDFunction,

623

738

    domain: &[VarNo],

624

738

) -> Result<bool, MercError> {

625

738

    manager_ref.with_manager_shared(|manager| {

626

738

        let mut cache = FxHashMap::default();

627

628

738

        check_partition_function_edge(manager, &mut cache, bdd.as_edge(manager).borrowed(), domain)

629

738

})

630

738

631

632

/// The recursive implementation of [check_partition_function] on edges.

633

1625653

fn check_partition_function_edge<'id>(

634

1625653

    manager: &<BDDFunction as Function>::Manager<'id>,

635

1625653

    cache: &mut FxHashMap<BDDFunction, bool>,

636

1625653

    bdd: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

637

1625653

    domain: &[VarNo],

638

1625653

) -> Result<bool, MercError> {

639

1625653

    if let Some(result) = cache.get(&BDDFunction::from_edge(manager, manager.clone_edge(&bdd))) {

640

67692

        return Ok(*result);

641

1557961

642

643

1557961

    let bdd_level = match manager.get_node(&bdd) {

644

717902

        Node::Terminal(_terminal) => {

645

717902

            return Ok(true);

646

647

840059

        Node::Inner(node) => node.level(),

648

};

649

650

840059

    let result = if let Some(domain_var) = domain.first() {

651

813526

        if bdd_level > *domain_var {

652

            // Skipped levels, so catch up in the domain.

653

2137

            check_partition_function_edge(manager, cache, bdd.borrowed(), &domain[1..])

654

811389

        } else if bdd_level == *domain_var {

655

811389

            let (high, low) = collect_children(manager.get_node(&bdd).unwrap_inner());

656

657

811389

            let high_result = check_partition_function_edge(manager, cache, high, &domain[1..])?;

658

811389

            let low_result = check_partition_function_edge(manager, cache, low, &domain[1..])?;

659

811389

            Ok(high_result && low_result)

660

        } else {

661

            // There are variables in the range that are not in the domain, so this cannot be a function from domain to range.

662

            return Ok(false);

663

664

    } else {

665

        // The domain was completely visited, so now we check whether there is

666

        // exactly one assignment to the range variables.

667

26533

        is_bdd_cube_edge(manager, bdd.borrowed())

668

}?;

669

670

840059

    cache.insert(BDDFunction::from_edge(manager, manager.clone_edge(&bdd)), result);

671

840059

    Ok(result)

672

1625653

673

674

/// Checks if the given BDD is a cube, i.e., it represents a single bitvector over the given variables.

675

593317

fn is_bdd_cube_edge<'id>(

676

593317

    manager: &<BDDFunction as Function>::Manager<'id>,

677

593317

    bdd: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

678

593317

) -> Result<bool, MercError> {

679

593317

    match manager.get_node(&bdd) {

680

309925

        Node::Terminal(terminal) => match terminal {

681

26533

            BDDTerminal::True => Ok(true),

682

283392

            BDDTerminal::False => Ok(false),

683

},

684

283392

        Node::Inner(node) => {

685

283392

            let (high, low) = collect_children(node);

686

687

283392

            let high_is_cube = is_bdd_cube_edge(manager, high)?;

688

283392

            let low_is_cube = is_bdd_cube_edge(manager, low)?;

689

690

283392

            Ok(high_is_cube ^ low_is_cube) // Exactly one of them should be a cube.

691

692

693

593317

694

695

/// Extend a transition relation to a larger domain by introducing x = x' for

696

/// the irrelevant variables.

697

///

698

/// # Details

699

///

700

/// The resulting transition can then be used without considering the support

701

/// explicitly.

702

500

pub(crate) fn extend_relation(

703

500

    manager_ref: &BDDManagerRef,

704

500

    relation: &BDDFunction,

705

500

    state_variables: &[VarNo],

706

500

    next_state_variables: &[VarNo],

707

500

    write_variables: &[VarNo],

708

500

) -> Result<BDDFunction, OutOfMemory> {

709

500

    manager_ref.with_manager_shared(|manager| {

710

500

        Ok(BDDFunction::from_edge(

711

500

            manager,

712

500

            extend_relation_edge(

713

500

                manager,

714

500

                relation.as_edge(manager).borrowed(),

715

500

                state_variables,

716

500

                next_state_variables,

717

500

                write_variables,

718

)?,

719

))

720

500

})

721

500

722

723

/// Extends a transition relation to the full domain by adding x = x' for every

724

/// state variable that is not written by the transition group.

725

500

fn extend_relation_edge<'id>(

726

500

    manager: &<BDDFunction as Function>::Manager<'id>,

727

500

    relation: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

728

500

    state_variables: &[VarNo],

729

500

    next_state_variables: &[VarNo],

730

500

    write_variables: &[VarNo],

731

500

) -> Result<EdgeOfFunc<'id, BDDFunction>, OutOfMemory> {

732

500

    debug_assert_eq!(

733

500

        state_variables.len(),

734

500

        next_state_variables.len(),

735

        "state and next-state domains should have matching arity"

736

);

737

738

    // Build a single BDD encoding x = x' for all non-written variables.

739

500

    let mut eq = EdgeDropGuard::new(manager, BDDFunction::t_edge(manager));

740

500

    let f_edge = EdgeDropGuard::new(manager, BDDFunction::f_edge(manager));

741

742

14985

    for (state_var, next_state_var) in state_variables.iter().zip(next_state_variables.iter()).rev() {

743

14985

        if write_variables.contains(next_state_var) {

744

6973

            continue;

745

8012

746

747

8012

        let low = EdgeDropGuard::new(

748

8012

            manager,

749

8012

            reduce(

750

8012

                manager,

751

8012

                *next_state_var,

752

8012

                manager.clone_edge(&eq),

753

8012

                manager.clone_edge(&f_edge),

754

)?,

755

);

756

8012

        let high = EdgeDropGuard::new(

757

8012

            manager,

758

8012

            reduce(

759

8012

                manager,

760

8012

                *next_state_var,

761

8012

                manager.clone_edge(&f_edge),

762

8012

                manager.clone_edge(&eq),

763

)?,

764

);

765

8012

        eq = EdgeDropGuard::new(manager, reduce(manager, *state_var, low.into_edge(), high.into_edge())?);

766

767

768

500

    BDDFunction::and_edge(manager, &relation, &eq)

769

500

770

771

/// Encodes the given block number into a BDD using the given variables as bits.

772

///

773

/// # Details

774

///

775

/// Encodes the bits starting with the least significant bit, which is the

776

/// inverse of the encoding used in [crate::ldd_to_bdd]. The intuition is

777

/// (potentially) that the block numbers are often small numbers, so the most

778

/// significant bits are more likely to be 0 and these will collapse to singular

779

/// nodes at the bottom layers.

780

4078

fn encode_block<'id>(

781

4078

    manager: &<BDDFunction as Function>::Manager<'id>,

782

4078

    variables: &[BDDFunction],

783

4078

    block_no: u64,

784

4078

) -> Result<EdgeOfFunc<'id, BDDFunction>, OutOfMemory> {

785

4078

    debug_assert!(

786

4078

        variables.len() >= required_bits_64(block_no) as usize,

787

        "Not enough variables to encode block number {}",

788

        block_no

789

);

790

791

4078

    let mut result = EdgeDropGuard::new(manager, BDDFunction::t_edge(manager));

792

4078

    let f_edge = EdgeDropGuard::new(manager, BDDFunction::f_edge(manager));

793

794

45870

    for (i, var) in variables.iter().enumerate() {

795

45870

        if block_no & (1 << i) != 0 {

796

            // bit is 1

797

18455

            result = EdgeDropGuard::new(

798

18455

                manager,

799

18455

                BDDFunction::ite_edge(manager, var.as_edge(manager), &result, &f_edge)?,

800

);

801

        } else {

802

            // bit is 0

803

27415

            result = EdgeDropGuard::new(

804

27415

                manager,

805

27415

                BDDFunction::ite_edge(manager, var.as_edge(manager), &f_edge, &result)?,

806

);

807

808

809

810

4078

    Ok(result.into_edge())

811

4078

812

813

/// Decodes the given block number from a BDD using the given variables as bits.

814

///

815

/// # Details

816

///

817

/// Should be the inverse of [encode_block].

818

30309

fn decode_block<'id>(

819

30309

    manager: &<BDDFunction as Function>::Manager<'id>,

820

30309

    block: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

821

30309

) -> u64 {

822

30309

    let mut result = 0u64;

823

30309

    let mut mask = 1u64;

824

30309

    let mut block = block.borrowed();

825

826

30309

    let f_edge = EdgeDropGuard::new(manager, BDDFunction::f_edge(manager));

827

30309

    debug_assert!(*block != *f_edge, "decode_block called on the false terminal");

828

358406

    while let Node::Inner(node) = manager.get_node(&block) {

829

328097

        let (b_high, b_low) = collect_children(node);

830

        // For a cube exactly one child is false; the other branch encodes the bit.

831

328097

        if *b_low != *f_edge {

832

195822

            debug_assert!(*b_high == *f_edge, "decode_block input is not a cube");

833

195822

            block = b_low;

834

        } else {

835

132275

            debug_assert!(*b_high != *f_edge, "decode_block input is not a cube");

836

132275

            result |= mask;

837

132275

            block = b_high;

838

839

328097

        mask <<= 1;

840

841

842

30309

    result

843

30309

844

845

/// Display helper that prints all vectors represented by the given signature BDD as numbers, by decoding

846

/// the BDD layers as `bits`, see [crate::ldd_to_bdd].

847

pub struct SignatureDisplay<'a> {

848

    signature: &'a BDDFunction,

849

850

    /// The number of bits per state variable, the action bits and block bits.

851

    num_of_bits: &'a [u32],

852

    action_bits: u32,

853

    block_bits: u32,

854

855

    /// The variables that contribute to the signature.

856

    variables: &'a [VarNo],

857

858

859

impl<'a> SignatureDisplay<'a> {

860

    /// Creates a new partition display helper.

861

    fn new(

862

        signature: &'a BDDFunction,

863

        variables: &'a [VarNo],

864

        num_of_bits: &'a [u32],

865

        action_bits: u32,

866

        block_bits: u32,

867

    ) -> Self {

868

        Self {

869

            signature,

870

            num_of_bits,

871

            action_bits,

872

            block_bits,

873

            variables,

874

875

876

877

878

/// Display helper that prints all vectors represented by the given signature BDD as numbers, by decoding

879

/// the BDD layers as `bits`, see [crate::ldd_to_bdd].

880

pub struct PartitionDisplay<'a> {

881

    signature: &'a BDDFunction,

882

883

    /// The number of bits per state variable and block bits.

884

    num_of_bits: &'a [u32],

885

    block_bits: u32,

886

887

    /// The variables that contribute to the signature.

888

    variables: &'a Vec<VarNo>,

889

890

891

impl<'a> PartitionDisplay<'a> {

892

    /// Creates a new partition display helper.

893

    fn new(signature: &'a BDDFunction, variables: &'a Vec<VarNo>, num_of_bits: &'a [u32], block_bits: u32) -> Self {

894

        Self {

895

            signature,

896

            num_of_bits,

897

            block_bits,

898

            variables,

899

900

901

902

903

impl fmt::Display for PartitionDisplay<'_> {

904

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

905

        // Total number of bits for the state variables.

906

        let total_num_of_bits: u32 = self.num_of_bits.iter().sum();

907

908

        // We ignore the output cube, so just pass no variables.

909

        let mut first = true;

910

        for cube in CubeIterAll::with_variables(self.signature, self.variables) {

911

            let cube = cube.map_err(|_| fmt::Error)?;

912

913

            debug_assert_eq!(

914

                cube.len(),

915

                (total_num_of_bits + self.block_bits) as usize,

916

                "Unexpected number of bits found"

917

);

918

919

            if !first {

920

                writeln!(f)?;

921

922

            first = false;

923

924

            let (state_bits, block_bits) = cube.split_at(total_num_of_bits as usize);

925

            debug_assert_eq!(

926

                block_bits.len(),

927

                self.block_bits as usize,

928

                "Unexpected number of block bits found"

929

);

930

931

            write!(

932

f,

933

                "[{}] -> {}",

934

                ValuesIter::new(state_bits, self.num_of_bits).format(", "),

935

                to_block_index(block_bits)

936

)?;

937

938

939

        Ok(())

940

941

942

943

impl fmt::Display for SignatureDisplay<'_> {

944

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

945

        // Total number of bits for the state variables.

946

        let total_num_of_bits: u32 = self.num_of_bits.iter().sum();

947

948

        // We ignore the output cube, so just pass no variables.

949

        let mut first = true;

950

        for cube in CubeIterAll::with_variables(self.signature, self.variables) {

951

            let cube = cube.map_err(|_| fmt::Error)?;

952

953

            debug_assert_eq!(

954

                cube.len(),

955

                (total_num_of_bits + self.action_bits + self.block_bits) as usize,

956

                "Unexpected number of bits found"

957

);

958

959

            if !first {

960

                writeln!(f)?;

961

962

            first = false;

963

964

            let (state_bits, rest) = cube.split_at(total_num_of_bits as usize);

965

            let (action_bits, block_bits) = rest.split_at(self.action_bits as usize);

966

            debug_assert_eq!(

967

                block_bits.len(),

968

                self.block_bits as usize,

969

                "Unexpected number of block bits found"

970

);

971

972

            write!(

973

f,

974

                "[{}] -> ({}, {})",

975

                ValuesIter::new(state_bits, self.num_of_bits).format(", "),

976

                to_value(action_bits),

977

                to_block_index(block_bits)

978

)?;

979

980

981

        Ok(())

982

983

984

985

/// Reconstruct the block index represented by the bits, this uses the same encoding

986

/// as [encode_block]. This is least significant bit first.

987

fn to_block_index(bits: &[OptBool]) -> u64 {

988

    let mut value = 0u64;

989

    for (i, bit) in bits.iter().enumerate() {

990

        if *bit == OptBool::True {

991

            value |= 1 << i;

992

993

994

995

    value

996

997

998

#[cfg(test)]

999

mod tests {

1000

    use std::ops::Range;

1001

1002

    use oxidd::BooleanFunction;

1003

    use oxidd::Edge;

1004

    use oxidd::Function;

1005

    use oxidd::Manager;

1006

    use oxidd::ManagerRef;

1007

    use oxidd::VarNo;

1008

    use oxidd::bdd::BDDFunction;

1009

    use oxidd::error::DuplicateVarName;

1010

    use oxidd::util::Borrowed;

1011

    use rand::RngExt;

1012

1013

    use merc_lts::LTS;

1014

    use merc_lts::LtsBuilderMem;

1015

    use merc_reduction::Equivalence;

1016

    use merc_reduction::compare_lts;

1017

    use merc_reduction::reduce_lts;

1018

    use merc_utilities::Timing;

1019

    use merc_utilities::random_test;

1020

1021

    use super::decode_block;

1022

    use super::encode_block;

1023

    use super::is_bdd_cube_edge;

1024

    use crate::SymbolicLtsBdd;

1025

    use crate::convert_symbolic_lts;

1026

    use crate::convert_symbolic_lts_bdd;

1027

    use crate::quotient_symbolic;

1028

    use crate::random_bdd;

1029

    use crate::random_symbolic_lts;

1030

    use crate::read_symbolic_lts;

1031

    use crate::required_bits_64;

1032

    use crate::sigref_symbolic;

1033

1034

    #[test]

1035

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1036

1

    fn test_random_encode_blocks() {

1037

100

        random_test(100, |rng| {

1038

100

            let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

1039

1040

100

            let block_number: u64 = rng.random();

1041

1042

100

            let num_of_bits = required_bits_64(block_number);

1043

6320

            let block_variable_names = (0..num_of_bits).map(|i| format!("b_{}", i)).collect::<Vec<String>>();

1044

1045

            // Create variables in the BDD manager

1046

100

            let block_variables = manager_ref

1047

100

                .with_manager_exclusive(|manager| -> Result<Range<VarNo>, DuplicateVarName> {

1048

100

                    manager.add_named_vars(block_variable_names)

1049

100

})

1050

100

                .unwrap();

1051

1052

100

            manager_ref.with_manager_shared(|manager| {

1053

100

                let block_variables_bdds = block_variables

1054

6320

                    .map(|var_no| BDDFunction::var(manager, var_no))

1055

100

                    .collect::<Result<Vec<BDDFunction>, oxidd::util::OutOfMemory>>()

1056

100

                    .unwrap();

1057

1058

100

                let encoded = encode_block(manager, &block_variables_bdds, block_number).unwrap();

1059

100

                let decoded = decode_block(manager, Borrowed::new(encoded));

1060

1061

100

                assert_eq!(

1062

                    block_number, decoded,

1063

                    "Decoding the block number did not yield the original"

1064

);

1065

100

});

1066

100

})

1067

1

1068

1069

    #[test]

1070

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1071

1

    fn test_random_sigref_split_signature() {

1072

100

        random_test(100, |rng| {

1073

100

            let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

1074

1075

100

            let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap();

1076

1077

100

            let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1);

1078

100

            let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &lts).unwrap();

1079

1080

100

            let (_, _, expected_num_blocks) =

1081

100

                sigref_symbolic(&bdd_manager, &lts_bdd, &Timing::new(), false, false, false, false).unwrap();

1082

1083

            // Create a separate manager since sigref_symbolic creates new block variables.

1084

100

            let bdd_manager_split = oxidd::bdd::new_manager(2028, 2028, 1);

1085

100

            let lts_bdd_split = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager_split, &lts).unwrap();

1086

100

            let (_, _, split_num_blocks) = sigref_symbolic(

1087

100

                &bdd_manager_split,

1088

100

                &lts_bdd_split,

1089

100

                &Timing::new(),

1090

100

                true,

1091

100

                false,

1092

100

                false,

1093

100

                false,

1094

100

1095

100

            .unwrap();

1096

1097

100

            assert_eq!(

1098

                expected_num_blocks, split_num_blocks,

1099

                "Split signature approach does not match actual signature refinement"

1100

);

1101

100

});

1102

1

1103

1104

    #[test]

1105

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1106

1

    fn test_szymanski_symbolic_refinement() {

1107

1

        let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

1108

1

        let lts_bdd = read_symbolic_lts(

1109

1

            &ldd_manager,

1110

1

            include_bytes!("../../../../examples/lts/Szymanski_3-bit_lin_wait_alt.sym") as &[u8],

1111

1112

1

        .unwrap();

1113

1114

1

        let bdd_manager = oxidd::bdd::new_manager(2048, 1024, 1);

1115

1

        let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &lts_bdd).unwrap();

1116

1117

1

        let (_, _, num_of_blocks) =

1118

1

            sigref_symbolic(&bdd_manager, &lts_bdd, &Timing::new(), false, false, false, false).unwrap();

1119

1

        assert_eq!(

1120

            num_of_blocks, 1791,

1121

            "The Szymanski example has 1791 bisimulation blocks"

1122

);

1123

1

1124

1125

    #[test]

1126

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1127

1

    fn test_symbolic_signature_refinement_abp() {

1128

1

        let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

1129

1

        let lts = read_symbolic_lts(

1130

1

            &ldd_manager,

1131

1

            include_bytes!("../../../../examples/lts/abp.sym") as &[u8],

1132

1133

1

        .unwrap();

1134

1135

1

        let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1);

1136

1

        let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &lts).unwrap();

1137

1138

1

        let (_, _, num_of_blocks) =

1139

1

            sigref_symbolic(&bdd_manager, &lts_bdd, &Timing::new(), false, false, false, false).unwrap();

1140

1

        assert_eq!(num_of_blocks, 68, "The ABP examples has 68 bisimulation blocks");

1141

1

1142

1143

    #[test]

1144

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1145

1

    fn test_random_is_cube() {

1146

100

        random_test(100, |rng| {

1147

100

            let ldd_manager = oxidd::bdd::new_manager(2048, 1024, 1);

1148

1149

            // Create variables in the BDD manager

1150

100

            let vars: Vec<VarNo> =

1151

100

                ldd_manager.with_manager_exclusive(|manager| manager.add_vars(8).collect::<Vec<VarNo>>());

1152

1153

100

            let bdd_vars = ldd_manager

1154

100

                .with_manager_exclusive(|manager| {

1155

100

                    vars.iter()

1156

800

                        .map(|v| BDDFunction::var(manager, *v))

1157

100

                        .collect::<Result<Vec<BDDFunction>, _>>()

1158

100

})

1159

100

                .unwrap();

1160

1161

100

            let bdd = random_bdd(&ldd_manager, rng, &bdd_vars, 1).unwrap();

1162

1163

100

            ldd_manager.with_manager_shared(|manager| {

1164

100

                assert!(

1165

100

                    !bdd.satisfiable() || is_bdd_cube_edge(manager, bdd.as_edge(manager).borrowed()).unwrap(),

1166

                    "The bdd was created as a cube, so it should be a cube"

1167

);

1168

100

})

1169

100

})

1170

1

1171

1172

    #[test]

1173

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

1174

1

    fn test_random_sigref() {

1175

100

        random_test(100, |rng| {

1176

100

            let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

1177

1178

100

            let lts = random_symbolic_lts(rng, &ldd_manager, 10, 5).unwrap();

1179

1180

100

            let bdd_manager = oxidd::bdd::new_manager(2028, 2028, 1);

1181

100

            let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&ldd_manager, &bdd_manager, &lts).unwrap();

1182

1183

100

            let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new());

1184

100

            let explicit_lts = convert_symbolic_lts(&ldd_manager, &mut builder, &lts).unwrap();

1185

100

            let explicit_lts_reduced =

1186

100

                reduce_lts(explicit_lts.clone(), Equivalence::StrongBisim, false, &Timing::new());

1187

1188

100

            let (partition, block_vars, _num_of_blocks) =

1189

100

                sigref_symbolic(&bdd_manager, &lts_bdd, &Timing::new(), false, false, false, false).unwrap();

1190

1191

100

            let quotient_lts = quotient_symbolic(&bdd_manager, &lts_bdd, &partition, &block_vars).unwrap();

1192

1193

100

            let mut builder = LtsBuilderMem::new(Vec::new(), Vec::new());

1194

100

            let symbolic_lts_reduced = convert_symbolic_lts_bdd(&bdd_manager, &mut builder, &quotient_lts).unwrap();

1195

1196

100

            println!(

1197

                "Explicit LTS has {} states and {} transitions",

1198

100

                explicit_lts.num_of_states(),

1199

100

                explicit_lts.num_of_transitions()

1200

);

1201

1202

100

            assert_eq!(

1203

100

                explicit_lts_reduced.num_of_states(),

1204

100

                symbolic_lts_reduced.num_of_states()

1205

);

1206

100

            assert_eq!(

1207

100

                explicit_lts_reduced.num_of_transitions(),

1208

100

                symbolic_lts_reduced.num_of_transitions()

1209

);

1210

1211

100

            assert!(

1212

100

                compare_lts(

1213

100

                    Equivalence::StrongBisim,

1214

100

                    explicit_lts_reduced,

1215

100

                    symbolic_lts_reduced,

1216

                    false,

1217

100

                    &Timing::new()

1218

),

1219

                "Both the explicit LTS and the one converted from the symbolic LTS should be bisimilar"

1220

);

1221

100

});

1222

1

1223