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::util::SatCountCache;

28

use oxidd_core::function::EdgeOfFunc;

29

use oxidd_core::util::EdgeDropGuard;

30

use oxidd_dump::Visualizer;

31

use oxidd_rules_bdd::simple::BDDTerminal;

32

use rustc_hash::FxBuildHasher;

33

use rustc_hash::FxHashMap;

34

35

use crate::CubeIterAll;

36

use crate::SymbolicLtsBdd;

37

use crate::ValuesIter;

38

use crate::collect_children;

39

use crate::compute_vars_bdd;

40

use crate::reduce;

41

use crate::required_bits_64;

42

use crate::to_value;

43

use crate::variable_rename;

44

45

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

46

/// refinement.

47

///

48

/// # Details

49

///

50

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

51

///

52

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

53

/// > Minimization.

54

300

pub fn sigref_symbolic(

55

300

    manager_ref: &BDDManagerRef,

56

300

    lts: &SymbolicLtsBdd,

57

300

    timing: &Timing,

58

300

    split_signature: bool,

59

300

    visualize: bool,

60

300

) -> Result<BDDFunction, MercError> {

61

    // There can only be one block per state, so we need as many bits as required to

62

    // represent all states.

63

300

    let number_of_states = lts

64

300

        .states()

65

300

        .sat_count::<u64, FxBuildHasher>(lts.state_variables().len() as u32, &mut SatCountCache::default());

66

300

    debug!("Number of states: {}", number_of_states);

67

68

300

    let split_partition_groups = if split_signature {

69

        combine_transition_groups(manager_ref, lts)?

70

    } else {

71

        // We do not use the grouping

72

300

        Vec::new()

73

};

74

75

300

    let num_of_block_bits = required_bits_64(number_of_states);

76

300

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

77

78

300

    let block_variable_names = (0..num_of_block_bits)

79

2100

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

80

300

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

81

82

    // Create variables in the BDD manager

83

300

    let block_variable_indices: Vec<VarNo> = manager_ref

84

300

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

85

300

            manager.add_named_vars(block_variable_names)

86

300

})

87

300

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

88

300

        .collect();

89

90

    // Create BDD functions for the block variables

91

300

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

92

93

300

    let mut signature_to_block = FxHashMap::default();

94

95

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

96

300

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

97

300

        .state_variables()

98

300

        .iter()

99

300

        .cloned()

100

300

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

101

300

        .collect();

102

103

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

104

300

    let signature_variables = lts

105

300

        .next_state_variables()

106

300

        .iter()

107

300

        .chain(lts.action_variables())

108

300

        .chain(block_variable_indices.iter())

109

300

        .cloned()

110

300

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

111

112

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

113

300

    let partition_variables = lts

114

300

        .next_state_variables()

115

300

        .iter()

116

300

        .chain(block_variable_indices.iter())

117

300

        .cloned()

118

300

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

119

120

    // Stores the partition of the states as BDD.

121

300

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

122

300

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

123

300

            Ok(BDDFunction::from_edge(

124

300

                manager,

125

300

                encode_block(manager, &block_variables_bdds, 0)?,

126

))

127

300

},

128

    )?)?;

129

130

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

131

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

132

300

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

133

134

    // Keep track of local information.

135

300

    let mut num_of_blocks = 0;

136

300

    let mut iteration = 0usize;

137

138

300

    let progress = TimeProgress::new(

139

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

140

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

141

},

142

1,

143

);

144

145

300

    if visualize {

146

        // Visualize the initial partition.

147

        manager_ref.with_manager_shared(|manager| {

148

            Visualizer::new()

149

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

150

                .serve()

151

        })?;

152

300

153

154

300

    trace!(

155

        "Initial partition: {}",

156

        PartitionDisplay::new(

157

            &partition,

158

            &partition_variables,

159

            lts.state_variable_num_of_bits(),

160

            num_of_block_bits

161

162

);

163

164

    // Determine the write variables BDDs for all transition groups.

165

300

    let write_variable_bdd = lts

166

300

        .transition_groups()

167

300

        .iter()

168

1500

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

169

1500

            let variables = group.write_variables().to_vec();

170

171

1500

            Ok(compute_vars_bdd(manager_ref, &variables)?.1)

172

1500

})

173

300

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

174

175

300

    let mut signature_index = 0;

176

    loop {

177

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

178

600

        let old_num_of_blocks = num_of_blocks;

179

600

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

180

181

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

182

600

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

183

600

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

184

185

600

            if split_signature && !split_partition_groups.is_empty() {

186

                // Only compute the signature w.r.t. all transition groups that share actions.

187

                for index in &split_partition_groups[signature_index] {

188

                    let group_signature = signature_strong(

189

                        &partition,

190

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

191

                        &write_variable_bdd[*index],

192

)?;

193

194

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

195

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

196

197

            } else {

198

                // Compute the full signature by combining all transition groups.

199

3000

                for (index, (group, write_vars)) in lts

200

600

                    .transition_groups()

201

600

                    .iter()

202

600

                    .zip(write_variable_bdd.iter())

203

600

                    .enumerate()

204

205

                    // Compute the signature for this transition group.

206

//

207

                    // Observe that we explicitly do not quantify over state

208

                    // variables that are not written by the transition group.

209

                    // Otherwise, these state variables would become unconstrained

210

                    // and then after substituting next state variables with current

211

                    // state variables, they would lead to spurious states.

212

3000

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

213

3000

                        signature_strong(&partition, group.relation(), write_vars)

214

3000

                    })?;

215

216

                    // Substitute next state variables with current state variables to align

217

                    // with the partition representation, required for `refine`.

218

3000

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

219

3000

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

220

221

222

223

600

            Ok(signature)

224

600

        })?;

225

226

600

        trace!(

227

            "Signature at iteration {}: {}",

228

            iteration,

229

            SignatureDisplay::new(

230

                &signature,

231

                &signature_variables,

232

                lts.state_variable_num_of_bits(),

233

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

234

                num_of_block_bits

235

236

);

237

238

600

        if visualize {

239

            // Visualize the computed signature.

240

            manager_ref.with_manager_shared(|manager| {

241

                Visualizer::new()

242

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

243

                    .serve()

244

            })?;

245

600

246

247

        // Build the new partition based on the signatures.

248

600

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

249

600

            refine(

250

600

                manager_ref,

251

600

                &mut signature_to_block,

252

600

                &block_variables_bdds,

253

600

                lts.next_state_variables(),

254

600

                &signature,

255

600

                &partition,

256

257

600

        })?;

258

259

600

        if visualize {

260

            // Visualize the current partition.

261

            manager_ref.with_manager_shared(|manager| {

262

                Visualizer::new()

263

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

264

                    .serve()

265

            })?;

266

600

267

268

600

        trace!(

269

            "Partition at iteration {}: {}",

270

            iteration,

271

            PartitionDisplay::new(

272

                &partition,

273

                &partition_variables,

274

                lts.state_variable_num_of_bits(),

275

                num_of_block_bits

276

277

);

278

279

600

        num_of_blocks = signature_to_block.len();

280

600

        progress.print((iteration, num_of_blocks));

281

600

        iteration += 1;

282

283

600

        if split_signature {

284

            if signature_index == 0 && num_of_blocks == old_num_of_blocks {

285

                // We only reached a fixed point if after a full cycle no changes occurred.

286

                break;

287

288

289

            signature_index += 1;

290

            if signature_index >= split_partition_groups.len() {

291

                // Start from the first transition group again.

292

                signature_index = 0;

293

294

600

        } else if num_of_blocks == old_num_of_blocks {

295

300

            break;

296

300

297

298

        // Clear the block assignment for the next iteration.

299

300

        signature_to_block.clear();

300

301

302

300

    info!(

303

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

304

        iteration, num_of_blocks

305

);

306

307

300

    Ok(partition)

308

300

309

310

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

311

///

312

/// # Details

313

///

314

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

315

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

316

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

317

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

318

    // transition groups that share action labels.

319

320

    // Computes the BDD representing all action labels.

321

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

322

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

323

324

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

325

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

326

            bdd = bdd.and(&var)?;

327

328

329

        Ok(bdd)

330

    })?;

331

332

    // Compute the action labels for all transition groups.

333

    let representatives = lts

334

        .transition_groups()

335

        .iter()

336

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

337

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

338

339

    // For the split signature we must ensure that all action labels are disjoint.

340

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

341

342

    for (i, _transition_group) in lts.transition_groups().iter().enumerate() {

343

        // See if the element can be added to an existing group, by taking the first element of

344

        // each group as representative.

345

        if let Some(group) = result.iter_mut().find(|g: &&mut Vec<usize>| {

346

            if let Some(first) = g.first() {

347

                representatives[*first]

348

                    .and(&representatives[i])

349

                    .expect("Out of memory oxidd") // TODO: faillable try_find.

350

                    .satisfiable()

351

            } else {

352

                false

353

354

        }) {

355

            // Add to existing group

356

            group.push(i);

357

        } else {

358

            // Create new group, and add the representative

359

            result.push(vec![i]);

360

361

362

363

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

364

    Ok(result)

365

366

367

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

368

/// relation.

369

///

370

/// # Details

371

///

372

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

373

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

374

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

375

///

376

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

377

3000

fn signature_strong(

378

3000

    partition: &BDDFunction,

379

3000

    relation: &BDDFunction,

380

3000

    next_state_vars: &BDDFunction,

381

3000

) -> Result<BDDFunction, OutOfMemory> {

382

3000

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

383

3000

384

385

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

386

/// to signatures.

387

///

388

/// # Details

389

///

390

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

391

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

392

///

393

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

394

///

395

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

396

600

fn refine(

397

600

    manager_ref: &BDDManagerRef,

398

600

    signature_to_block: &mut FxHashMap<BDDFunction, u64>,

399

600

    block_variables_bdds: &[BDDFunction],

400

600

    state_variables: &[VarNo],

401

600

    signature: &BDDFunction,

402

600

    partition: &BDDFunction,

403

600

) -> Result<BDDFunction, MercError> {

404

600

    manager_ref.with_manager_shared(|manager| {

405

600

        let mut cache = FxHashMap::default();

406

407

600

        Ok(BDDFunction::from_edge(

408

600

            manager,

409

600

            refine_edge(

410

600

                manager,

411

600

                &mut cache,

412

600

                signature_to_block,

413

600

                block_variables_bdds,

414

600

                state_variables,

415

600

                signature.as_edge(manager).borrowed(),

416

600

                partition.as_edge(manager).borrowed(),

417

)?,

418

))

419

600

})

420

600

421

422

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

423

1811168

fn refine_edge<'id>(

424

1811168

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

425

1811168

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

426

1811168

    signature_to_block: &mut FxHashMap<BDDFunction, u64>,

427

1811168

    block_variables_bdds: &[BDDFunction],

428

1811168

    state_variables: &[VarNo],

429

1811168

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

430

1811168

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

431

1811168

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

432

1811168

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

433

845884

        Node::Terminal(terminal) => {

434

845884

            if terminal == BDDTerminal::False {

435

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

436

845884

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

437

438

439

            unreachable!();

440

441

965284

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

442

};

443

444

965284

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

445

965284

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

446

965284

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

447

965284

    )) {

448

58242

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

449

907042

450

451

    // topVar

452

907042

    let lowest_level = {

453

907042

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

454

713968

            Node::Terminal(_terminal) => {

455

713968

                VarNo::MAX // Terminal node, so no variable.

456

457

193074

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

458

};

459

907042

        plevel.min(slevel)

460

};

461

462

907042

    let result = if state_variables.contains(&lowest_level) {

463

        // Match paths on the level s_i, for irrelevant variables we take both paths.

464

905284

        let (s_high, s_low) = {

465

905284

            match manager.get_node(&signature) {

466

191868

                Node::Inner(node) => {

467

191868

                    if node.level() == lowest_level {

468

175880

                        collect_children(node)

469

                    } else {

470

15988

                        (signature.borrowed(), signature.borrowed())

471

472

473

713416

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

474

475

};

476

905284

        let (p_high, p_low) = {

477

905284

            match manager.get_node(&partition) {

478

905284

                Node::Inner(node) => {

479

905284

                    if node.level() == lowest_level {

480

905284

                        collect_children(node)

481

                    } else {

482

                        (partition.borrowed(), partition.borrowed())

483

484

485

                _ => unreachable!("Not a terminal node"),

486

487

};

488

489

905284

        let low = refine_edge(

490

905284

            manager,

491

905284

            cache,

492

905284

            signature_to_block,

493

905284

            block_variables_bdds,

494

905284

            state_variables,

495

905284

            s_low,

496

905284

            p_low,

497

)?;

498

905284

        let high = refine_edge(

499

905284

            manager,

500

905284

            cache,

501

905284

            signature_to_block,

502

905284

            block_variables_bdds,

503

905284

            state_variables,

504

905284

            s_high,

505

905284

            p_high,

506

)?;

507

508

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

509

905284

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

510

    } else {

511

        // 9. else:

512

        // \sigma (the signature function) now encodes the state signature (a, B)

513

        // P (the partition function) encodes the current block assignment

514

515

        // 10. B := decode_block(partition)

516

1758

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

517

1758

        let signature = BDDFunction::from_edge(manager, manager.clone_edge(&signature));

518

1758

        if let Some(block) = signature_to_block.get(&signature) {

519

            // 11. If blocks[B].signature == \bottom then

520

            // 12.     blocks[B].signature := signature

521

            // 13. if blocks[B].signature == signature then

522

            // 14.     return P

523

            if *block == block_index {

524

                trace!("Found existing signature for {block_index}");

525

                Ok(manager.clone_edge(&partition)) // The partition just encodes the current block.

526

            } else {

527

                // New partition needed

528

                trace!("Return existing block {block}");

529

                Ok(encode_block(manager, block_variables_bdds, *block)?)

530

531

        } else {

532

1758

            let new_block_index = signature_to_block.len() as u64;

533

1758

            trace!("Creating new block {new_block_index}");

534

1758

            signature_to_block.insert(signature, new_block_index);

535

1758

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

536

537

}?;

538

539

907042

    cache.insert(

540

907042

541

907042

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

542

907042

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

543

907042

),

544

907042

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

545

);

546

547

907042

    Ok(result)

548

1811168

549

550

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

551

///

552

/// # Details

553

///

554

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

555

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

556

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

557

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

558

/// nodes at the bottom layers.

559

2158

fn encode_block<'id>(

560

2158

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

561

2158

    variables: &[BDDFunction],

562

2158

    block_no: u64,

563

2158

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

564

2158

    debug_assert!(

565

2158

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

566

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

567

        block_no

568

);

569

570

2158

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

571

2158

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

572

573

20701

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

574

20701

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

575

            // bit is 1

576

4859

            result = EdgeDropGuard::new(

577

4859

                manager,

578

4859

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

579

);

580

        } else {

581

            // bit is 0

582

15842

            result = EdgeDropGuard::new(

583

15842

                manager,

584

15842

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

585

);

586

587

588

589

2158

    Ok(result.into_edge())

590

2158

591

592

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

593

///

594

/// # Details

595

///

596

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

597

1858

fn decode_block<'id>(

598

1858

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

599

1858

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

600

1858

) -> u64 {

601

1858

    let mut result = 0u64;

602

1858

    let mut mask = 1u64;

603

1858

    let mut block = block.borrowed();

604

605

1858

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

606

20459

    while *block != *f_edge {

607

20459

        match manager.get_node(&block) {

608

18601

            Node::Inner(node) => {

609

18601

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

610

                // For a cube: low satisfiable => bit 0, else => bit 1

611

18601

                if *b_low != *f_edge {

612

14556

                    block = b_low;

613

14556

                } else {

614

4045

                    result |= mask;

615

4045

                    block = b_high;

616

4045

617

18601

                mask <<= 1;

618

619

1858

            Node::Terminal(_) => break,

620

621

622

623

1858

    result

624

1858

625

626

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

627

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

628

pub struct SignatureDisplay<'a> {

629

    signature: &'a BDDFunction,

630

631

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

632

    num_of_bits: &'a [u32],

633

    action_bits: u32,

634

    block_bits: u32,

635

636

    /// The variables that contribute to the signature.

637

    variables: &'a Vec<VarNo>,

638

639

640

impl<'a> SignatureDisplay<'a> {

641

    /// Creates a new partition display helper.

642

    fn new(

643

        signature: &'a BDDFunction,

644

        variables: &'a Vec<VarNo>,

645

        num_of_bits: &'a [u32],

646

        action_bits: u32,

647

        block_bits: u32,

648

    ) -> Self {

649

        Self {

650

            signature,

651

            num_of_bits,

652

            action_bits,

653

            block_bits,

654

            variables,

655

656

657

658

659

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

660

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

661

pub struct PartitionDisplay<'a> {

662

    signature: &'a BDDFunction,

663

664

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

665

    num_of_bits: &'a [u32],

666

    block_bits: u32,

667

668

    /// The variables that contribute to the signature.

669

    variables: &'a Vec<VarNo>,

670

671

672

impl<'a> PartitionDisplay<'a> {

673

    /// Creates a new partition display helper.

674

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

675

        Self {

676

            signature,

677

            num_of_bits,

678

            block_bits,

679

            variables,

680

681

682

683

684

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

685

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

686

        // Total number of bits for the state variables.

687

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

688

689

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

690

        let mut first = true;

691

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

692

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

693

694

            debug_assert_eq!(

695

                cube.len(),

696

                (total_num_of_bits + self.block_bits) as usize,

697

                "Unexpected number of bits found"

698

);

699

700

            if !first {

701

                writeln!(f)?;

702

703

            first = false;

704

705

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

706

            debug_assert_eq!(

707

                block_bits.len(),

708

                self.block_bits as usize,

709

                "Unexpected number of block bits found"

710

);

711

712

            write!(

713

f,

714

                "[{}] -> {}",

715

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

716

                to_block_index(block_bits)

717

)?;

718

719

720

        Ok(())

721

722

723

724

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

725

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

726

        // Total number of bits for the state variables.

727

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

728

729

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

730

        let mut first = true;

731

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

732

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

733

734

            debug_assert_eq!(

735

                cube.len(),

736

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

737

                "Unexpected number of bits found"

738

);

739

740

            if !first {

741

                writeln!(f)?;

742

743

            first = false;

744

745

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

746

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

747

            debug_assert_eq!(

748

                block_bits.len(),

749

                self.block_bits as usize,

750

                "Unexpected number of block bits found"

751

);

752

753

            write!(

754

f,

755

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

756

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

757

                to_value(action_bits),

758

                to_block_index(block_bits)

759

)?;

760

761

762

        Ok(())

763

764

765

766

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

767

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

768

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

769

    let mut value = 0u64;

770

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

771

        if *bit == OptBool::True {

772

            value |= 1 << i;

773

774

775

776

    value

777

778

779

#[cfg(test)]

780

mod tests {

781

    use std::ops::Range;

782

783

    use merc_utilities::Timing;

784

    use oxidd::BooleanFunction;

785

    use oxidd::Manager;

786

    use oxidd::ManagerRef;

787

    use oxidd::VarNo;

788

    use oxidd::bdd::BDDFunction;

789

    use oxidd::error::DuplicateVarName;

790

    use oxidd::util::Borrowed;

791

    use rand::RngExt;

792

793

    use merc_utilities::random_test;

794

795

    use crate::SymbolicLtsBdd;

796

    use crate::random_symbolic_lts;

797

    use crate::required_bits_64;

798

    use crate::sigref::decode_block;

799

    use crate::sigref::encode_block;

800

    use crate::sigref_symbolic;

801

802

    #[test]

803

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

804

1

    fn test_random_symbolic_sigref() {

805

100

        random_test(100, |rng| {

806

100

            let mut storage = merc_ldd::Storage::new();

807

808

            // We don't really check anything here, just ensure that reachability runs without errors.

809

100

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

810

100

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

811

100

            let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &lts).unwrap();

812

813

100

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

814

100

});

815

1

816

817

    #[test]

818

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

819

1

    fn test_random_encode_blocks() {

820

100

        random_test(100, |rng| {

821

100

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

822

823

100

            let block_number: u64 = rng.random();

824

825

100

            let num_of_bits = required_bits_64(block_number);

826

6295

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

827

828

            // Create variables in the BDD manager

829

100

            let block_variables = manager_ref

830

100

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

831

100

                    manager.add_named_vars(block_variable_names)

832

100

})

833

100

                .unwrap();

834

835

100

            manager_ref.with_manager_shared(|manager| {

836

100

                let block_variables_bdds = block_variables

837

6295

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

838

100

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

839

100

                    .unwrap();

840

841

100

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

842

100

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

843

844

100

                assert_eq!(

845

                    block_number, decoded,

846

                    "Decoding the block number did not yield the original"

847

);

848

100

});

849

100

})

850

1

851

852

    #[test]

853

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

854

1

    fn test_random_sigref() {

855

100

        random_test(100, |rng| {

856

100

            let mut storage = merc_ldd::Storage::new();

857

858

            // We don't really check anything here, just ensure that reachability runs without errors.

859

100

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

860

861

100

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

862

100

            let lts_bdd = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &lts).unwrap();

863

864

100

            let _expected_partition = sigref_symbolic(&manager_ref, &lts_bdd, &mut Timing::new(), false, false).unwrap();

865

866

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

867

100

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

868

100

            let lts_bdd_split = SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref_split, &lts).unwrap();

869

100

            let _split_partition =

870

100

                sigref_symbolic(&manager_ref_split, &lts_bdd_split, &mut Timing::new(), false, false).unwrap();

871

872

            // Apparently this works even when the BDDs are created in different managers.

873

            // assert!(

874

            //     split_partition == expected_partition,

875

            //     "Split signature approach does not match actual signature refinement"

876

            // );

877

100

});

878

1

879