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::SummandGroupBdd;

37

use crate::SymbolicLtsBdd;

38

use crate::ValuesIter;

39

use crate::collect_children;

40

use crate::compute_vars_bdd;

41

use crate::reduce;

42

use crate::required_bits_64;

43

use crate::to_value;

44

use crate::variable_rename;

45

46

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

47

/// refinement.

48

///

49

/// # Details

50

///

51

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

52

///

53

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

54

/// > Minimization.

55

101

pub fn sigref_symbolic(

56

101

    manager_ref: &BDDManagerRef,

57

101

    lts: &SymbolicLtsBdd,

58

101

    timing: &Timing,

59

101

    split_signature: bool,

60

101

    extend_relation: bool,

61

101

    merge_transitions: bool,

62

101

    visualize: bool,

63

101

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

64

101

    if merge_transitions && !extend_relation {

65

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

66

101

67

68

101

    let use_extended_relations = extend_relation || merge_transitions;

69

101

    let use_split_signature = split_signature && !merge_transitions;

70

71

101

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

72

73

101

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

74

101

75

76

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

77

///

78

/// # Details

79

///

80

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

81

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

82

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

83

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

84

/// group covering the full state domain.

85

101

fn preprocess_lts(

86

101

    manager_ref: &BDDManagerRef,

87

101

    lts: &SymbolicLtsBdd,

88

101

    extend_relations: bool,

89

101

    merge_transitions: bool,

90

101

) -> Result<SymbolicLtsBdd, MercError> {

91

101

    if !extend_relations && !merge_transitions {

92

101

        let groups = lts

93

101

            .transition_groups()

94

101

            .iter()

95

510

            .map(|group| {

96

510

                SummandGroupBdd::new(

97

510

                    group.relation().clone(),

98

510

                    group.read_variables().to_vec(),

99

510

                    group.write_variables().to_vec(),

100

101

510

})

102

101

            .collect();

103

101

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

104

105

106

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

107

    let mut groups: Vec<SummandGroupBdd> = lts

108

        .transition_groups()

109

        .iter()

110

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

111

            let relation = extend_relation(

112

                manager_ref,

113

                group.relation(),

114

                lts.state_variables(),

115

                lts.next_state_variables(),

116

                group.write_variables(),

117

)?;

118

            Ok(SummandGroupBdd::new(

119

                relation,

120

                lts.state_variables().to_vec(),

121

                lts.next_state_variables().to_vec(),

122

))

123

})

124

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

125

126

    if merge_transitions && !groups.is_empty() {

127

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

128

        for group in &groups {

129

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

130

131

        groups = vec![SummandGroupBdd::new(

132

            merged_relation,

133

            lts.state_variables().to_vec(),

134

            lts.next_state_variables().to_vec(),

135

)];

136

137

138

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

139

101

140

141

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

142

101

fn sigref_symbolic_impl(

143

101

    manager_ref: &BDDManagerRef,

144

101

    lts: &SymbolicLtsBdd,

145

101

    timing: &Timing,

146

101

    split_signature: bool,

147

101

    visualize: bool,

148

101

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

149

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

150

    // represent all states.

151

101

    let number_of_states = lts

152

101

        .states()

153

101

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

154

101

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

155

156

101

    let split_partition_groups = if split_signature {

157

        combine_transition_groups(manager_ref, lts)?

158

    } else {

159

101

        Vec::new()

160

};

161

162

101

    let num_of_block_bits = required_bits_64(number_of_states);

163

101

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

164

165

101

    let block_variable_names = (0..num_of_block_bits)

166

380

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

167

101

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

168

169

    // Create variables in the BDD manager

170

101

    let block_variable_indices: Vec<VarNo> = manager_ref

171

101

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

172

101

            manager.add_named_vars(block_variable_names)

173

101

})

174

101

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

175

101

        .collect();

176

177

    // Create BDD functions for the block variables

178

101

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

179

180

101

    let mut signature_to_block = FxHashMap::default();

181

182

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

183

101

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

184

101

        .state_variables()

185

101

        .iter()

186

101

        .cloned()

187

101

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

188

101

        .collect();

189

190

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

191

101

    let signature_variables = lts

192

101

        .next_state_variables()

193

101

        .iter()

194

101

        .chain(lts.action_variables())

195

101

        .chain(block_variable_indices.iter())

196

101

        .cloned()

197

101

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

198

199

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

200

101

    let partition_variables = lts

201

101

        .next_state_variables()

202

101

        .iter()

203

101

        .chain(block_variable_indices.iter())

204

101

        .cloned()

205

101

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

206

207

    // Stores the partition of the states as BDD.

208

101

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

209

101

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

210

101

            Ok(BDDFunction::from_edge(

211

101

                manager,

212

101

                encode_block(manager, &block_variables_bdds, 0)?,

213

))

214

101

},

215

    )?)?;

216

217

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

218

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

219

101

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

220

221

    // Keep track of local information.

222

101

    let mut num_of_blocks = 0;

223

101

    let mut iteration = 0usize;

224

225

101

    let progress = TimeProgress::new(

226

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

227

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

228

},

229

1,

230

);

231

232

101

    if visualize {

233

        // Visualize the initial partition.

234

        manager_ref.with_manager_shared(|manager| {

235

            Visualizer::new()

236

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

237

                .serve()

238

        })?;

239

101

240

241

101

    trace!(

242

        "Initial partition: {}",

243

        PartitionDisplay::new(

244

            &partition,

245

            &partition_variables,

246

            lts.state_variable_num_of_bits(),

247

            num_of_block_bits

248

249

);

250

251

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

252

    // preprocessed) write variables of that group.

253

101

    let relation_quantified_next_state_vars: Vec<BDDFunction> = lts

254

101

        .transition_groups()

255

101

        .iter()

256

510

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

257

101

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

258

259

101

    let mut signature_index = 0;

260

    loop {

261

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

262

228

        let old_num_of_blocks = num_of_blocks;

263

228

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

264

265

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

266

228

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

267

228

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

268

269

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

270

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

271

228

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

272

228

                if split_signature && !split_partition_groups.is_empty() {

273

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

274

                } else {

275

228

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

276

};

277

278

1170

            for index in group_indices {

279

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

280

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

281

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

282

1170

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

283

1170

                    signature_strong(

284

1170

                        &partition,

285

1170

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

286

1170

                        &relation_quantified_next_state_vars[index],

287

288

1170

                })?;

289

290

1170

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

291

1170

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

292

293

294

228

            Ok(signature)

295

228

        })?;

296

297

228

        trace!(

298

            "Signature at iteration {}: {}",

299

            iteration,

300

            SignatureDisplay::new(

301

                &signature,

302

                &signature_variables,

303

                lts.state_variable_num_of_bits(),

304

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

305

                num_of_block_bits

306

307

);

308

309

228

        if visualize {

310

            // Visualize the computed signature.

311

            manager_ref.with_manager_shared(|manager| {

312

                Visualizer::new()

313

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

314

                    .serve()

315

            })?;

316

228

317

318

        // Build the new partition based on the signatures.

319

228

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

320

228

            refine(

321

228

                manager_ref,

322

228

                &mut signature_to_block,

323

228

                &block_variables_bdds,

324

228

                lts.next_state_variables(),

325

228

                &signature,

326

228

                &partition,

327

328

228

        })?;

329

330

228

        if visualize {

331

            // Visualize the current partition.

332

            manager_ref.with_manager_shared(|manager| {

333

                Visualizer::new()

334

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

335

                    .serve()

336

            })?;

337

228

338

339

228

        trace!(

340

            "Partition at iteration {}: {}",

341

            iteration,

342

            PartitionDisplay::new(

343

                &partition,

344

                &partition_variables,

345

                lts.state_variable_num_of_bits(),

346

                num_of_block_bits

347

348

);

349

350

228

        num_of_blocks = signature_to_block.len();

351

228

        progress.print((iteration, num_of_blocks));

352

228

        iteration += 1;

353

354

228

        if split_signature {

355

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

356

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

357

                break;

358

359

360

            signature_index += 1;

361

            if signature_index >= split_partition_groups.len() {

362

                // Start from the first transition group again.

363

                signature_index = 0;

364

365

228

        } else if num_of_blocks == old_num_of_blocks {

366

101

            break;

367

127

368

369

        // Clear the block assignment for the next iteration.

370

127

        signature_to_block.clear();

371

372

373

101

    info!(

374

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

375

        iteration, num_of_blocks

376

);

377

378

101

    Ok((partition, block_variable_indices, num_of_blocks))

379

101

380

381

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

382

///

383

/// # Details

384

///

385

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

386

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

387

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

388

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

389

    // transition groups that share action labels.

390

391

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

392

    // only the action labels.

393

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

394

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

395

396

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

397

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

398

            bdd = bdd.and(&var)?;

399

400

401

        Ok(bdd)

402

    })?;

403

404

    // Compute the action labels for all transition groups.

405

    let representatives = lts

406

        .transition_groups()

407

        .iter()

408

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

409

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

410

411

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

412

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

413

414

    for i in 0..lts.transition_groups().len() {

415

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

416

        // each group as representative.

417

        let mut placed = false;

418

        for group in result.iter_mut() {

419

            let Some(first) = group.first() else {

420

                continue;

421

};

422

            if representatives[*first].and(&representatives[i])?.satisfiable() {

423

                group.push(i);

424

                placed = true;

425

                break;

426

427

428

        if !placed {

429

            // Create new group, and add the representative

430

            result.push(vec![i]);

431

432

433

434

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

435

    Ok(result)

436

437

438

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

439

/// relation.

440

///

441

/// # Details

442

///

443

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

444

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

445

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

446

///

447

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

448

1170

fn signature_strong(

449

1170

    partition: &BDDFunction,

450

1170

    relation: &BDDFunction,

451

1170

    next_state_vars: &BDDFunction,

452

1170

) -> Result<BDDFunction, OutOfMemory> {

453

1170

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

454

1170

455

456

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

457

/// to signatures.

458

///

459

/// # Details

460

///

461

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

462

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

463

///

464

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

465

///

466

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

467

228

fn refine(

468

228

    manager_ref: &BDDManagerRef,

469

228

    signature_to_block: &mut FxHashMap<BDDFunction, u64>,

470

228

    block_variables_bdds: &[BDDFunction],

471

228

    next_state_variables: &[VarNo],

472

228

    signature: &BDDFunction,

473

228

    partition: &BDDFunction,

474

228

) -> Result<BDDFunction, MercError> {

475

228

    debug_assert!(

476

228

        check_partition_function(manager_ref, partition, next_state_variables)?,

477

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

478

);

479

480

228

    manager_ref.with_manager_shared(|manager| {

481

228

        let mut cache = FxHashMap::default();

482

483

228

        Ok(BDDFunction::from_edge(

484

228

            manager,

485

228

            refine_edge(

486

228

                manager,

487

228

                &mut cache,

488

228

                signature_to_block,

489

228

                block_variables_bdds,

490

228

                next_state_variables,

491

228

                signature.as_edge(manager).borrowed(),

492

228

                partition.as_edge(manager).borrowed(),

493

)?,

494

))

495

228

})

496

228

497

498

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

499

142230

fn refine_edge<'id>(

500

142230

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

501

142230

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

502

142230

    signature_to_block: &mut FxHashMap<BDDFunction, u64>,

503

142230

    block_variables_bdds: &[BDDFunction],

504

142230

    next_state_variables: &[VarNo],

505

142230

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

506

142230

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

507

142230

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

508

142230

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

509

60592

        Node::Terminal(terminal) => {

510

60592

            if terminal == BDDTerminal::False {

511

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

512

60592

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

513

514

515

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

516

517

81638

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

518

};

519

520

81638

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

521

81638

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

522

81638

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

523

81638

    )) {

524

9795

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

525

71843

526

527

    // topVar

528

71843

    let lowest_level = {

529

71843

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

530

1799

            Node::Terminal(_) => plevel,

531

70044

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

532

};

533

71843

        plevel.min(slevel)

534

};

535

536

71843

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

537

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

538

71001

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

539

69261

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

540

33646

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

541

};

542

71001

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

543

71001

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

544

187

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

545

};

546

547

71001

        let low = refine_edge(

548

71001

            manager,

549

71001

            cache,

550

71001

            signature_to_block,

551

71001

            block_variables_bdds,

552

71001

            next_state_variables,

553

71001

            s_low,

554

71001

            p_low,

555

)?;

556

71001

        let high = refine_edge(

557

71001

            manager,

558

71001

            cache,

559

71001

            signature_to_block,

560

71001

            block_variables_bdds,

561

71001

            next_state_variables,

562

71001

            s_high,

563

71001

            p_high,

564

)?;

565

566

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

567

71001

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

568

    } else {

569

        // 9. else:

570

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

571

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

572

573

        // 10. B := decode_block(partition)

574

842

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

575

842

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

576

842

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

577

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

578

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

579

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

580

            // 14.     return P

581

            if *block == block_index {

582

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

583

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

584

            } else {

585

                // New partition needed

586

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

587

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

588

589

        } else {

590

842

            let new_block_index = signature_to_block.len() as u64;

591

842

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

592

842

            signature_to_block.insert(signature, new_block_index);

593

842

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

594

595

}?;

596

597

71843

    cache.insert(

598

71843

599

71843

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

600

71843

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

601

71843

),

602

71843

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

603

);

604

605

71843

    Ok(result)

606

142230

607

608

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

609

///

610

/// # Details

611

///

612

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

613

/// variables.

614

228

fn check_partition_function(

615

228

    manager_ref: &BDDManagerRef,

616

228

    bdd: &BDDFunction,

617

228

    domain: &[VarNo],

618

228

) -> Result<bool, MercError> {

619

228

    manager_ref.with_manager_shared(|manager| {

620

228

        let mut cache = FxHashMap::default();

621

622

228

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

623

228

})

624

228

625

626

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

627

124219

fn check_partition_function_edge<'id>(

628

124219

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

629

124219

    cache: &mut FxHashMap<BDDFunction, bool>,

630

124219

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

631

124219

    domain: &[VarNo],

632

124219

) -> Result<bool, MercError> {

633

124219

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

634

8790

        return Ok(*result);

635

115429

636

637

115429

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

638

52639

        Node::Terminal(_terminal) => {

639

52639

            return Ok(true);

640

641

62790

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

642

};

643

644

62790

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

645

62116

        if bdd_level > *domain_var {

646

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

647

241

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

648

61875

        } else if bdd_level == *domain_var {

649

61875

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

650

651

61875

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

652

61875

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

653

61875

            Ok(high_result && low_result)

654

        } else {

655

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

656

            return Ok(false);

657

658

    } else {

659

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

660

        // exactly one assignment to the range variables.

661

674

        is_bdd_cube_edge(manager, bdd.borrowed())

662

}?;

663

664

62790

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

665

62790

    Ok(result)

666

124219

667

668

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

669

8110

fn is_bdd_cube_edge<'id>(

670

8110

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

671

8110

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

672

8110

) -> Result<bool, MercError> {

673

8110

    match manager.get_node(&bdd) {

674

4392

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

675

674

            BDDTerminal::True => Ok(true),

676

3718

            BDDTerminal::False => Ok(false),

677

},

678

3718

        Node::Inner(node) => {

679

3718

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

680

681

3718

            let high_is_cube = is_bdd_cube_edge(manager, high)?;

682

3718

            let low_is_cube = is_bdd_cube_edge(manager, low)?;

683

684

3718

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

685

686

687

8110

688

689

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

690

/// the irrelevant variables.

691

///

692

/// # Details

693

///

694

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

695

/// explicitly.

696

500

pub(crate) fn extend_relation(

697

500

    manager_ref: &BDDManagerRef,

698

500

    relation: &BDDFunction,

699

500

    state_variables: &[VarNo],

700

500

    next_state_variables: &[VarNo],

701

500

    write_variables: &[VarNo],

702

500

) -> Result<BDDFunction, OutOfMemory> {

703

500

    manager_ref.with_manager_shared(|manager| {

704

500

        Ok(BDDFunction::from_edge(

705

500

            manager,

706

500

            extend_relation_edge(

707

500

                manager,

708

500

                relation.as_edge(manager).borrowed(),

709

500

                state_variables,

710

500

                next_state_variables,

711

500

                write_variables,

712

)?,

713

))

714

500

})

715

500

716

717

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

718

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

719

500

fn extend_relation_edge<'id>(

720

500

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

721

500

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

722

500

    state_variables: &[VarNo],

723

500

    next_state_variables: &[VarNo],

724

500

    write_variables: &[VarNo],

725

500

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

726

500

    debug_assert_eq!(

727

500

        state_variables.len(),

728

500

        next_state_variables.len(),

729

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

730

);

731

732

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

733

500

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

734

500

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

735

736

14995

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

737

14995

        if write_variables.contains(next_state_var) {

738

6851

            continue;

739

8144

740

741

8144

        let low = EdgeDropGuard::new(

742

8144

            manager,

743

8144

            reduce(

744

8144

                manager,

745

8144

                *next_state_var,

746

8144

                manager.clone_edge(&eq),

747

8144

                manager.clone_edge(&f_edge),

748

)?,

749

);

750

8144

        let high = EdgeDropGuard::new(

751

8144

            manager,

752

8144

            reduce(

753

8144

                manager,

754

8144

                *next_state_var,

755

8144

                manager.clone_edge(&f_edge),

756

8144

                manager.clone_edge(&eq),

757

)?,

758

);

759

8144

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

760

761

762

500

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

763

500

764

765

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

766

///

767

/// # Details

768

///

769

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

770

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

771

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

772

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

773

/// nodes at the bottom layers.

774

1043

fn encode_block<'id>(

775

1043

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

776

1043

    variables: &[BDDFunction],

777

1043

    block_no: u64,

778

1043

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

779

1043

    debug_assert!(

780

1043

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

781

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

782

        block_no

783

);

784

785

1043

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

786

1043

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

787

788

11435

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

789

11435

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

790

            // bit is 1

791

4623

            result = EdgeDropGuard::new(

792

4623

                manager,

793

4623

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

794

);

795

        } else {

796

            // bit is 0

797

6812

            result = EdgeDropGuard::new(

798

6812

                manager,

799

6812

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

800

);

801

802

803

804

1043

    Ok(result.into_edge())

805

1043

806

807

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

808

///

809

/// # Details

810

///

811

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

812

942

fn decode_block<'id>(

813

942

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

814

942

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

815

942

) -> u64 {

816

942

    let mut result = 0u64;

817

942

    let mut mask = 1u64;

818

942

    let mut block = block.borrowed();

819

820

942

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

821

942

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

822

    loop {

823

11997

        match manager.get_node(&block) {

824

11055

            Node::Inner(node) => {

825

11055

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

826

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

827

11055

                if *b_low != *f_edge {

828

6624

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

829

6624

                    block = b_low;

830

                } else {

831

4431

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

832

4431

                    result |= mask;

833

4431

                    block = b_high;

834

835

11055

                mask <<= 1;

836

837

942

            Node::Terminal(_) => break,

838

839

840

841

942

    result

842

942

843

844

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

845

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

846

pub struct SignatureDisplay<'a> {

847

    signature: &'a BDDFunction,

848

849

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

850

    num_of_bits: &'a [u32],

851

    action_bits: u32,

852

    block_bits: u32,

853

854

    /// The variables that contribute to the signature.

855

    variables: &'a Vec<VarNo>,

856

857

858

impl<'a> SignatureDisplay<'a> {

859

    /// Creates a new partition display helper.

860

    fn new(

861

        signature: &'a BDDFunction,

862

        variables: &'a Vec<VarNo>,

863

        num_of_bits: &'a [u32],

864

        action_bits: u32,

865

        block_bits: u32,

866

    ) -> Self {

867

        Self {

868

            signature,

869

            num_of_bits,

870

            action_bits,

871

            block_bits,

872

            variables,

873

874

875

876

877

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

878

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

879

pub struct PartitionDisplay<'a> {

880

    signature: &'a BDDFunction,

881

882

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

883

    num_of_bits: &'a [u32],

884

    block_bits: u32,

885

886

    /// The variables that contribute to the signature.

887

    variables: &'a Vec<VarNo>,

888

889

890

impl<'a> PartitionDisplay<'a> {

891

    /// Creates a new partition display helper.

892

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

893

        Self {

894

            signature,

895

            num_of_bits,

896

            block_bits,

897

            variables,

898

899

900

901

902

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

903

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

904

        // Total number of bits for the state variables.

905

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

906

907

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

908

        let mut first = true;

909

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

910

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

911

912

            debug_assert_eq!(

913

                cube.len(),

914

                (total_num_of_bits + self.block_bits) as usize,

915

                "Unexpected number of bits found"

916

);

917

918

            if !first {

919

                writeln!(f)?;

920

921

            first = false;

922

923

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

924

            debug_assert_eq!(

925

                block_bits.len(),

926

                self.block_bits as usize,

927

                "Unexpected number of block bits found"

928

);

929

930

            write!(

931

f,

932

                "[{}] -> {}",

933

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

934

                to_block_index(block_bits)

935

)?;

936

937

938

        Ok(())

939

940

941

942

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

943

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

944

        // Total number of bits for the state variables.

945

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

946

947

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

948

        let mut first = true;

949

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

950

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

951

952

            debug_assert_eq!(

953

                cube.len(),

954

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

955

                "Unexpected number of bits found"

956

);

957

958

            if !first {

959

                writeln!(f)?;

960

961

            first = false;

962

963

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

964

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

965

            debug_assert_eq!(

966

                block_bits.len(),

967

                self.block_bits as usize,

968

                "Unexpected number of block bits found"

969

);

970

971

            write!(

972

f,

973

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

974

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

975

                to_value(action_bits),

976

                to_block_index(block_bits)

977

)?;

978

979

980

        Ok(())

981

982

983

984

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

985

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

986

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

987

    let mut value = 0u64;

988

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

989

        if *bit == OptBool::True {

990

            value |= 1 << i;

991

992

993

994

    value

995

996

997

#[cfg(test)]

998

mod tests {

999

    use std::ops::Range;

1000

1001

    use merc_ldd::Storage;

1002

    use merc_lts::LtsBuilderMem;

1003

    use merc_reduction::Equivalence;

1004

    use merc_reduction::compare_lts;

1005

    use merc_utilities::Timing;

1006

    use oxidd::BooleanFunction;

1007

    use oxidd::Edge;

1008

    use oxidd::Function;

1009

    use oxidd::Manager;

1010

    use oxidd::ManagerRef;

1011

    use oxidd::VarNo;

1012

    use oxidd::bdd::BDDFunction;

1013

    use oxidd::error::DuplicateVarName;

1014

    use oxidd::util::Borrowed;

1015

    use rand::RngExt;

1016

1017

    use merc_utilities::random_test;

1018

1019

    use crate::SymbolicLtsBdd;

1020

    use crate::convert_symbolic_lts;

1021

    use crate::convert_symbolic_lts_bdd;

1022

    use crate::quotient_symbolic;

1023

    use crate::random_bdd;

1024

    use crate::random_symbolic_lts;

1025

    use crate::read_symbolic_lts;

1026

    use crate::required_bits_64;

1027

    use crate::sigref::decode_block;

1028

    use crate::sigref::encode_block;

1029

    use crate::sigref::is_bdd_cube_edge;

1030

    use crate::sigref_symbolic;

1031

1032

    #[test]

1033

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

1034

1

    fn test_random_encode_blocks() {

1035

100

        random_test(100, |rng| {

1036

100

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

1037

1038

100

            let block_number: u64 = rng.random();

1039

1040

100

            let num_of_bits = required_bits_64(block_number);

1041

6332

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

1042

1043

            // Create variables in the BDD manager

1044

100

            let block_variables = manager_ref

1045

100

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

1046

100

                    manager.add_named_vars(block_variable_names)

1047

100

})

1048

100

                .unwrap();

1049

1050

100

            manager_ref.with_manager_shared(|manager| {

1051

100

                let block_variables_bdds = block_variables

1052

6332

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

1053

100

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

1054

100

                    .unwrap();

1055

1056

100

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

1057

100

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

1058

1059

100

                assert_eq!(

1060

                    block_number, decoded,

1061

                    "Decoding the block number did not yield the original"

1062

);

1063

100

});

1064

100

})

1065

1

1066

1067

    //     #[test]

1068

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

1069

    //     fn test_random_sigref_split_signature() {

1070

    //         random_test(100, |rng| {

1071

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

1072

1073

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

1074

1075

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

1076

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

1077

1078

    //             let (_, _, expected_num_blocks) =

1079

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

1080

1081

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

1082

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

1083

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

1084

    //             let (_, _, split_num_blocks) = sigref_symbolic(

1085

    //                 &manager_ref_split,

1086

    //                 &lts_bdd_split,

1087

    //                 &Timing::new(),

1088

    //                 true,

1089

    //                 false,

1090

    //                 false,

1091

    //                 false,

1092

    //             )

1093

    //             .unwrap();

1094

1095

    //             assert_eq!(

1096

    //                 expected_num_blocks, split_num_blocks,

1097

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

1098

    //             );

1099

    //         });

1100

    //     }

1101

1102

    //     #[test]

1103

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

1104

    //     fn test_szymanski_symbolic_refinement() {

1105

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

1106

    //         let lts_bdd = read_symbolic_lts(

1107

    //             &mut storage,

1108

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

1109

    //         )

1110

    //         .unwrap();

1111

1112

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

1113

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

1114

1115

    //         let (_, _, num_of_blocks) =

1116

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

1117

    //         assert_eq!(

1118

    //             num_of_blocks, 1791,

1119

    //             "The Szymanski example has 1791 bisimulation blocks"

1120

    //         );

1121

    //     }

1122

1123

    #[test]

1124

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

1125

1

    fn test_symbolic_signature_refinement_abp() {

1126

1

        let mut storage = Storage::new();

1127

1

        let lts = read_symbolic_lts(&mut storage, include_bytes!("../../../examples/lts/abp.sym") as &[u8]).unwrap();

1128

1129

1

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

1130

1

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

1131

1132

1

        let (_, _, num_of_blocks) =

1133

1

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

1134

1

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

1135

1

1136

1137

    #[test]

1138

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

1139

1

    fn test_random_is_cube() {

1140

100

        random_test(100, |rng| {

1141

100

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

1142

1143

            // Create variables in the BDD manager

1144

100

            let vars: Vec<VarNo> =

1145

100

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

1146

1147

100

            let bdd_vars = manager

1148

100

                .with_manager_exclusive(|manager| {

1149

100

                    vars.iter()

1150

800

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

1151

100

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

1152

100

})

1153

100

                .unwrap();

1154

1155

100

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

1156

1157

100

            manager.with_manager_shared(|manager| {

1158

100

                assert!(

1159

100

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

1160

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

1161

);

1162

100

})

1163

100

})

1164

1

1165

1166

    #[test]

1167

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

1168

1

    fn test_random_sigref() {

1169

100

        random_test(100, |rng| {

1170

100

            let mut storage = Storage::new();

1171

1172

100

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

1173

1174

100

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

1175

100

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

1176

1177

100

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

1178

100

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

1179

1180

100

            let (partition, block_vars, _num_of_blocks) =

1181

100

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

1182

1183

100

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

1184

1185

100

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

1186

100

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

1187

1188

100

            assert!(

1189

100

                compare_lts(

1190

100

                    Equivalence::StrongBisim,

1191

100

                    explicit_lts,

1192

100

                    symbolic_lts_reduced,

1193

                    false,

1194

100

                    &mut Timing::new()

1195

),

1196

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

1197

);

1198

100

});

1199

1

1200