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::bdd::BDDFunction;

12

use oxidd::bdd::BDDManagerRef;

13

use oxidd::error::DuplicateVarName;

14

use oxidd::util::OptBool;

15

use oxidd::util::OutOfMemory;

16

use oxidd::util::SatCountCache;

17

use oxidd::BooleanFunction;

18

use oxidd::BooleanFunctionQuant;

19

use oxidd::BooleanOperator;

20

use oxidd::Function;

21

use oxidd::FunctionSubst;

22

use oxidd::HasLevel;

23

use oxidd::Manager;

24

use oxidd::ManagerRef;

25

use oxidd::Subst;

26

use oxidd::VarNo;

27

use oxidd_dump::Visualizer;

28

use rustc_hash::FxBuildHasher;

29

use rustc_hash::FxHashMap;

30

31

use crate::compute_vars_bdd;

32

use crate::required_bits_64;

33

use crate::to_value;

34

use crate::CubeIterAll;

35

use crate::SymbolicLtsBdd;

36

use crate::ValuesIter;

37

38

/// Computes the signature refinement of the given symbolic LTS using strong bisimulation.

39

///

40

/// # Details

41

///

42

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

43

///

44

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

45

100

pub fn sigref_symbolic(

46

100

    manager_ref: &BDDManagerRef,

47

100

    lts: &SymbolicLtsBdd,

48

100

    timing: &Timing,

49

100

    visualize: bool,

50

100

) -> Result<(), MercError> {

51

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

52

    // represent all states.

53

100

    let number_of_states = lts

54

100

        .states()

55

100

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

56

100

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

57

58

100

    let num_of_block_bits = required_bits_64(number_of_states);

59

100

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

60

61

100

    let block_variable_names = (0..num_of_block_bits)

62

700

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

63

100

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

64

65

    // Create variables in the BDD manager

66

100

    let block_variable_indices: Vec<VarNo> = manager_ref

67

100

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

68

100

            manager.add_named_vars(block_variable_names)

69

100

})

70

100

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

71

100

        .collect();

72

73

    // Create BDD functions for the block variables

74

100

    let block_variables_bdds = block_variable_indices

75

100

        .iter()

76

700

        .map(|var_no| manager_ref.with_manager_shared(|manager| BDDFunction::var(manager, *var_no)))

77

100

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

78

79

100

    let mut signature_to_block = FxHashMap::default();

80

81

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

82

100

    let next_state_variables = compute_vars_bdd(manager_ref, lts.next_state_variables())?.0;

83

100

    let next_state_substitution = Subst::new(lts.state_variables(), next_state_variables);

84

85

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

86

100

    let signature_variables = lts

87

100

        .next_state_variables()

88

100

        .iter()

89

100

        .chain(lts.action_variables())

90

100

        .chain(block_variable_indices.iter())

91

100

        .cloned()

92

100

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

93

94

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

95

100

    let partition_variables = lts

96

100

        .next_state_variables()

97

100

        .iter()

98

100

        .chain(block_variable_indices.iter())

99

100

        .cloned()

100

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

101

102

    // Stores the partition of the states as BDD.

103

100

    let mut partition = lts

104

100

        .states()

105

100

        .and(&manager_ref.with_manager_shared(|manager| encode_block(manager, &block_variables_bdds, 0))?)?;

106

107

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

108

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

109

100

    partition = partition.substitute(&next_state_substitution)?;

110

111

    // Keep track of local information.

112

100

    let mut num_of_blocks = 0;

113

100

    let mut old_num_of_blocks = 1;

114

100

    let mut iteration = 0usize;

115

116

100

    let progress = TimeProgress::new(

117

26

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

118

26

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

119

26

},

120

1,

121

);

122

123

100

    if visualize {

124

        // Visualize the initial partition.

125

        manager_ref.with_manager_shared(|manager| {

126

            Visualizer::new()

127

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

128

                .serve()

129

        })?;

130

100

131

132

100

    trace!(

133

        "Initial partition: {}",

134

        PartitionDisplay::new(

135

            &partition,

136

            &partition_variables,

137

            lts.state_variable_num_of_bits(),

138

            num_of_block_bits

139

140

);

141

142

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

143

100

    let write_variable_bdd = lts

144

100

        .transition_groups()

145

100

        .iter()

146

500

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

147

100

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

148

149

262

    while num_of_blocks != old_num_of_blocks {

150

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

151

162

        old_num_of_blocks = num_of_blocks;

152

162

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

153

154

162

        iteration += 1;

155

156

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

157

162

        let signature = timing.measure("signature", || {

158

162

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

159

810

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

160

162

                .transition_groups()

161

162

                .iter()

162

                .zip(write_variable_bdd.iter())

163

162

                .enumerate()

164

165

                // Compute the signature for this transition group.

166

//

167

                // Observe that we explicitly do not quantify over state

168

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

169

                // Otherwise, these state variables would become unconstrained

170

                // and then after substituting next state variables with current

171

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

172

810

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

173

810

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

174

810

                })?;

175

810

                signature = signature.or(&group_signature)?;

176

177

178

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

179

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

180

162

            signature.substitute(&next_state_substitution)

181

162

        })?;

182

183

        // TODO: Why no intersection.

184

185

162

        trace!(

186

            "Signature at iteration {}: {}",

187

            iteration,

188

            SignatureDisplay::new(

189

                &signature,

190

                &signature_variables,

191

                lts.state_variable_num_of_bits(),

192

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

193

                num_of_block_bits

194

195

);

196

197

162

        if visualize {

198

            // Visualize the computed signature.

199

            manager_ref.with_manager_shared(|manager| {

200

                Visualizer::new()

201

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

202

                    .serve()

203

            })?;

204

162

205

206

        // Build the new partition based on the signatures.

207

162

        partition = manager_ref.with_manager_shared(|manager| {

208

162

            refine(

209

162

                manager,

210

162

                &mut signature_to_block,

211

162

                &block_variables_bdds,

212

162

                lts.next_state_variables(),

213

162

                &signature,

214

162

                &partition,

215

216

162

        })?;

217

218

162

        if visualize {

219

            // Visualize the current partition.

220

            manager_ref.with_manager_shared(|manager| {

221

                Visualizer::new()

222

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

223

                    .serve()

224

            })?;

225

162

226

227

162

        trace!(

228

            "Partition at iteration {}: {}",

229

            iteration,

230

            PartitionDisplay::new(

231

                &partition,

232

                &partition_variables,

233

                lts.state_variable_num_of_bits(),

234

                num_of_block_bits

235

236

);

237

238

162

        num_of_blocks = signature_to_block.len();

239

162

        progress.print((iteration, num_of_blocks));

240

241

        // Clear the block assignment for the next iteration.

242

162

        signature_to_block.clear();

243

244

245

100

    info!(

246

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

247

        iteration, num_of_blocks

248

);

249

250

100

    Ok(())

251

100

252

253

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

254

/// relation.

255

///

256

/// # Details

257

///

258

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

259

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

260

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

261

///

262

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

263

810

fn signature_strong(

264

810

    partition: &BDDFunction,

265

810

    relation: &BDDFunction,

266

810

    next_state_vars: &BDDFunction,

267

810

) -> Result<BDDFunction, OutOfMemory> {

268

810

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

269

810

270

271

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

272

/// to signatures.

273

///

274

/// # Details

275

///

276

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

277

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

278

///

279

/// TODO: Definition

280

206716

fn refine<'id>(

281

206716

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

282

206716

    signature_to_block: &mut FxHashMap<BDDFunction, u64>,

283

206716

    block_variables_bdds: &[BDDFunction],

284

206716

    state_variables: &[VarNo],

285

206716

    signature: &BDDFunction,

286

206716

    partition: &BDDFunction,

287

206716

) -> Result<BDDFunction, MercError> {

288

    // TODO: Handle the `true` case.

289

206716

    if !partition.satisfiable() || !signature.satisfiable() {

290

        // In this case the state is not part of the partition function, or (s,

291

        // a) not part of the actions. So return empty.

292

99075

        return Ok(partition.clone());

293

107641

294

295

    // topVar

296

107641

    let level = {

297

107641

        let fnode = manager.get_node(partition.as_edge(manager)).unwrap_inner();

298

107641

        let gnode = manager.get_node(signature.as_edge(manager)).unwrap_inner();

299

107641

        let flevel = fnode.level();

300

107641

        let glevel = gnode.level();

301

107641

        flevel.min(glevel)

302

};

303

304

107641

    if state_variables.contains(&level) {

305

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

306

103277

        let (s_high, s_low) = {

307

103277

            let gnode = manager.get_node(signature.as_edge(manager)).unwrap_inner();

308

103277

            if gnode.level() == level {

309

98170

                signature.cofactors().expect("Not a terminal node")

310

            } else {

311

5107

                (signature.clone(), signature.clone())

312

313

};

314

103277

        let (p_high, p_low) = {

315

103277

            let fnode = manager.get_node(partition.as_edge(manager)).unwrap_inner();

316

103277

            if fnode.level() == level {

317

103277

                partition.cofactors().expect("Not a terminal node")

318

            } else {

319

                (partition.clone(), partition.clone())

320

321

};

322

323

103277

        let low = refine(

324

103277

            manager,

325

103277

            signature_to_block,

326

103277

            block_variables_bdds,

327

103277

            state_variables,

328

103277

            &s_low,

329

103277

            &p_low,

330

)?;

331

103277

        let high = refine(

332

103277

            manager,

333

103277

            signature_to_block,

334

103277

            block_variables_bdds,

335

103277

            state_variables,

336

103277

            &s_high,

337

103277

            &p_high,

338

)?;

339

340

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

341

103277

        Ok(BDDFunction::var(manager, level)?.ite(&high, &low)?)

342

    } else {

343

        // 9. else:

344

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

345

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

346

347

        // 10. B := decode_block(partition)

348

4364

        let block_index = decode_block(manager, partition);

349

4364

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

350

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

351

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

352

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

353

            // 14.     return P

354

3992

            if *block == block_index {

355

3381

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

356

3381

                Ok(partition.clone()) // The partition just encodes the current block.

357

            } else {

358

                // New partition needed

359

611

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

360

611

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

361

362

        } else {

363

372

            let new_block_index = signature_to_block.len() as u64;

364

372

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

365

372

            signature_to_block.insert(signature.clone(), new_block_index);

366

372

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

367

368

369

206716

370

371

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

372

///

373

/// # Details

374

///

375

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

376

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

377

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

378

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

379

/// nodes at the bottom layers.

380

1183

fn encode_block<'id>(

381

1183

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

382

1183

    variables: &[BDDFunction],

383

1183

    block_no: u64,

384

1183

) -> Result<BDDFunction, MercError> {

385

1183

    debug_assert!(

386

1183

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

387

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

388

        block_no

389

);

390

391

1183

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

392

13864

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

393

13864

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

394

            // bit is 1

395

4254

            result = var.ite(&result, &BDDFunction::f(manager))?;

396

        } else {

397

            // bit is 0

398

9610

            result = var.ite(&BDDFunction::f(manager), &result)?;

399

400

401

402

1183

    Ok(result)

403

1183

404

405

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

406

///

407

/// # Details

408

///

409

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

410

4464

fn decode_block<'id>(_manager: &<BDDFunction as Function>::Manager<'id>, block: &BDDFunction) -> u64 {

411

4464

    let mut result = 0u64;

412

4464

    let mut mask = 1u64;

413

4464

    let mut block = block.clone();

414

415

41295

    while block.satisfiable() {

416

41295

        if let Some((b_high, b_low)) = block.cofactors() {

417

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

418

36831

            if b_low.satisfiable() {

419

32738

                block = b_low;

420

32738

            } else {

421

4093

                result |= mask;

422

4093

                block = b_high;

423

4093

424

36831

            mask <<= 1;

425

        } else {

426

4464

            break;

427

428

429

430

4464

    result

431

4464

432

433

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

434

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

435

pub struct SignatureDisplay<'a> {

436

    signature: &'a BDDFunction,

437

438

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

439

    num_of_bits: &'a [u32],

440

    action_bits: u32,

441

    block_bits: u32,

442

443

    /// The variables that contribute to the signature.

444

    variables: &'a Vec<VarNo>,

445

446

447

impl<'a> SignatureDisplay<'a> {

448

    /// Creates a new partition display helper.

449

    fn new(

450

        signature: &'a BDDFunction,

451

        variables: &'a Vec<VarNo>,

452

        num_of_bits: &'a [u32],

453

        action_bits: u32,

454

        block_bits: u32,

455

    ) -> Self {

456

        Self {

457

            signature,

458

            num_of_bits,

459

            action_bits,

460

            block_bits,

461

            variables,

462

463

464

465

466

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

467

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

468

pub struct PartitionDisplay<'a> {

469

    signature: &'a BDDFunction,

470

471

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

472

    num_of_bits: &'a [u32],

473

    block_bits: u32,

474

475

    /// The variables that contribute to the signature.

476

    variables: &'a Vec<VarNo>,

477

478

479

impl<'a> PartitionDisplay<'a> {

480

    /// Creates a new partition display helper.

481

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

482

        Self {

483

            signature,

484

            num_of_bits,

485

            block_bits,

486

            variables,

487

488

489

490

491

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

492

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

493

        // Total number of bits for the state variables.

494

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

495

496

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

497

        let mut first = true;

498

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

499

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

500

501

            debug_assert_eq!(

502

                cube.len(),

503

                (total_num_of_bits + self.block_bits) as usize,

504

                "Unexpected number of bits found"

505

);

506

507

            if !first {

508

                writeln!(f)?;

509

510

            first = false;

511

512

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

513

            debug_assert_eq!(

514

                block_bits.len(),

515

                self.block_bits as usize,

516

                "Unexpected number of block bits found"

517

);

518

519

            write!(

520

f,

521

                "[{}] -> {}",

522

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

523

                to_block_index(block_bits)

524

)?;

525

526

527

        Ok(())

528

529

530

531

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

532

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

533

        // Total number of bits for the state variables.

534

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

535

536

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

537

        let mut first = true;

538

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

539

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

540

541

            debug_assert_eq!(

542

                cube.len(),

543

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

544

                "Unexpected number of bits found"

545

);

546

547

            if !first {

548

                writeln!(f)?;

549

550

            first = false;

551

552

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

553

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

554

            debug_assert_eq!(

555

                block_bits.len(),

556

                self.block_bits as usize,

557

                "Unexpected number of block bits found"

558

);

559

560

            write!(

561

f,

562

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

563

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

564

                to_value(action_bits),

565

                to_block_index(block_bits)

566

)?;

567

568

569

        Ok(())

570

571

572

573

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

574

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

575

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

576

    let mut value = 0u64;

577

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

578

        if *bit == OptBool::True {

579

            value |= 1 << i;

580

581

582

583

    value

584

585

586

#[cfg(test)]

587

mod tests {

588

    use std::ops::Range;

589

590

    use merc_utilities::Timing;

591

    use oxidd::bdd::BDDFunction;

592

    use oxidd::error::DuplicateVarName;

593

    use oxidd::BooleanFunction;

594

    use oxidd::Manager;

595

    use oxidd::ManagerRef;

596

    use oxidd::VarNo;

597

    use rand::Rng;

598

599

    use merc_utilities::random_test;

600

601

    use crate::random_symbolic_lts;

602

    use crate::required_bits_64;

603

    use crate::sigref::decode_block;

604

    use crate::sigref::encode_block;

605

    use crate::sigref_symbolic;

606

    use crate::SymbolicLtsBdd;

607

608

    #[test]

609

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

610

1

    fn test_random_symbolic_sigref() {

611

100

        random_test(100, |rng| {

612

100

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

613

614

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

615

100

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

616

100

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

617

100

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

618

619

100

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

620

100

});

621

1

622

623

    #[test]

624

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

625

1

    fn test_random_encode_blocks() {

626

100

        random_test(100, |rng| {

627

100

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

628

629

100

            let block_number: u64 = rng.random();

630

631

100

            let num_of_bits = required_bits_64(block_number);

632

6283

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

633

634

            // Create variables in the BDD manager

635

100

            let block_variables = manager_ref

636

100

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

637

100

                    manager.add_named_vars(block_variable_names)

638

100

})

639

100

                .unwrap();

640

641

100

            manager_ref.with_manager_shared(|manager| {

642

100

                let block_variables_bdds = block_variables

643

6283

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

644

100

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

645

100

                    .unwrap();

646

647

100

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

648

100

                let decoded = decode_block(manager, &encoded);

649

650

100

                assert_eq!(

651

                    block_number, decoded,

652

                    "Decoding the block number did not yield the original"

653

);

654

100

});

655

100

})

656

1

657