Grcov report - failures

1

//! Authors: Jan Friso Groote, Maurice Laveaux, Wieger Wesselink and Tim A.C.

2

//! Willemse

3

//!

4

//! > M. Laveaux, J.F. Groote and T.A.C. Willemse. Correct and Efficient

5

//! > Antichain Algorithms for Refinement Checking. Logical Methods in Computer

6

//! > Science 17(1) 2021

7

//!

8

//! There are six algorithms. One for trace inclusion, one for failures

9

//! inclusion and one for failures-divergence inclusion. All algorithms come in

10

//! a variant with and without internal steps. It is possible to generate a

11

//! counter transition system in case the inclusion is answered by no.

12

13

use std::collections::HashSet;

14

use std::collections::VecDeque;

15

16

use itertools::Itertools;

17

use log::trace;

18

19

use merc_collections::VecSet;

20

use merc_lts::LTS;

21

use merc_lts::LabelIndex;

22

use merc_lts::StateIndex;

23

use merc_reduction::diverges;

24

25

use crate::AC;

26

use crate::Antichain;

27

use crate::CounterExampleTree;

28

use crate::ExplorationStrategy;

29

use crate::RefinementType;

30

31

/// The result of the inner check in the refinement algorithm.

32

pub enum InnerCe {

33

    Refusal(Vec<LabelIndex>),

34

    Diverges,

35

36

37

/// Checks for the various stable failures refinement relations.

38

///

39

/// Returns the result, and the state in the counter example tree that witnesses

40

/// the failure if the result is false. Finally, the result of the inner

41

/// (impl,spec) check is returned as well, this is used to construct the counter

42

/// example.

43

712

pub fn is_failures_refinement<L: LTS, CE: CounterExampleTree>(

44

712

    lts: &L,

45

712

    initial_spec: StateIndex,

46

712

    refinement: RefinementType,

47

712

    strategy: ExplorationStrategy,

48

712

    counter_example: &mut CE,

49

712

) -> (bool, Option<CE::Index>, Option<InnerCe>) {

50

712

    let mut antichain = Antichain::new();

51

52

712

    match refinement {

53

176

        RefinementType::Trace => is_refinement_generic(

54

176

            strategy,

55

176

            lts,

56

176

            lts.initial_state_index(),

57

176

            initial_spec,

58

315

            |_, _| (None, true),

59

            |_, _| (),

60

            false,

61

176

            counter_example,

62

176

            &mut antichain,

63

),

64

183

        RefinementType::Weaktrace => is_refinement_generic(

65

183

            strategy,

66

183

            lts,

67

183

            lts.initial_state_index(),

68

183

            initial_spec,

69

503

            |_, _| (None, true),

70

            |_, _| (),

71

            true,

72

183

            counter_example,

73

183

            &mut antichain,

74

),

75

175

        RefinementType::StableFailures => is_refinement_generic(

76

175

            strategy,

77

175

            lts,

78

175

            lts.initial_state_index(),

79

175

            initial_spec,

80

392

            |impl_state, spec_states| {

81

392

82

392

                    refusals_contained_in(lts, impl_state, spec_states).map(InnerCe::Refusal),

83

392

                    true,

84

392

85

392

},

86

            |_, _| (),

87

            true,

88

175

            counter_example,

89

175

            &mut antichain,

90

),

91

178

        RefinementType::FailuresDivergences => is_refinement_generic(

92

178

            strategy,

93

178

            lts,

94

178

            lts.initial_state_index(),

95

178

            initial_spec,

96

383

            |impl_state, spec_states| {

97

701

                if !spec_states.iter().any(|s| diverges(lts, *s)) {

98

381

                    trace!("spec {:?} is convergent!", spec_states);

99

                    // If the implementation state diverges, then it can refuse any set of actions.

100

381

                    if diverges(lts, impl_state) {

101

2

                        trace!("impl {:?} diverges, return false", impl_state);

102

2

                        (Some(InnerCe::Diverges), true)

103

                    } else {

104

379

105

379

                            refusals_contained_in(lts, impl_state, spec_states).map(InnerCe::Refusal),

106

379

                            true,

107

379

108

109

                } else {

110

2

                    (None, false)

111

112

383

},

113

            |_, _| (),

114

            true,

115

178

            counter_example,

116

178

            &mut antichain,

117

),

118

        _ => unreachable!("This refinement variant {refinement:?} can not be checked by is_failures_refinement"),

119

120

712

121

122

/// A generic implementation for antichain based refinement algorithm.

123

///

124

/// # Details

125

///

126

/// Given the (initial_impl, initial_spec) pair the algorithm explores the

127

/// product state space of the implementation and the normalised specification

128

/// LTSs.

129

///

130

/// If `weak_transition` is true then the algorithm considers weak transitions

131

/// for the specification LTS, otherwise it only considers the immediate

132

/// transitions.

133

///

134

/// The `check` function is applied to every pair (impl, spec) that is explored

135

/// during the algorithm, it should return `None` if the pair is valid, and

136

/// `Some(counter_example)` if the pair is invalid. Furthermore, a boolean is

137

/// returned to indicate that exploration should continue (true) for this pair.

138

/// This only applies when no counter example is returned.

139

///

140

/// The `CE` type parameter indicates the type of counter example tree that is

141

/// used to construct counter examples. If no counter examples are required,

142

/// this can be set to `()`. Avoiding the cost for keeping track of counter

143

/// example information.

144

///

145

/// The antichain data structure is used for storing explored states. However,

146

/// as opposed to a discovered set it allows for pruning additional pairs based

147

/// on the `antichain` property.

148

1290

pub fn is_refinement_generic<L: LTS, A: AC<StateIndex, StateIndex>, CE: CounterExampleTree, F, G, CC>(

149

1290

    strategy: ExplorationStrategy,

150

1290

    merged_lts: &L,

151

1290

    initial_impl: StateIndex,

152

1290

    initial_spec: StateIndex,

153

1290

    mut check: F,

154

1290

    mut failing_trace: G,

155

1290

    weak_transition: bool,

156

1290

    counter_example: &mut CE,

157

1290

    antichain: &mut A,

158

1290

) -> (bool, Option<CE::Index>, Option<CC>)

159

1290

where

160

1290

    F: FnMut(StateIndex, &VecSet<StateIndex>) -> (Option<CC>, bool),

161

1290

    G: FnMut(StateIndex, &VecSet<StateIndex>),

162

163

    // A local cache used for the tau closure computations.

164

1290

    let mut closure_cache = ClosureCache::new();

165

166

1290

    let mut working = VecDeque::from([(

167

1290

        initial_impl,

168

1290

        if weak_transition {

169

1114

            VecSet::from_vec(tau_closure(merged_lts, vec![initial_spec], &mut closure_cache, true))

170

        } else {

171

176

            VecSet::singleton(initial_spec)

172

},

173

1290

        counter_example.root_index(),

174

    )]);

175

176

    // pop (impl,spec) from working;

177

3668

    while let Some((impl_state, spec, ce)) = working.pop_front() {

178

3230

        trace!("Checking ({:?}, {:?})", impl_state, spec);

179

3230

        let (inner_counter_example, continue_exploration) = check(impl_state, &spec);

180

3230

        if let Some(counter_example) = inner_counter_example {

181

            // if not check(impl,spec) then return false.

182

244

            return (false, Some(ce), Some(counter_example));

183

2986

184

185

2986

        if !continue_exploration {

186

            // If the check indicates that we should not continue exploration, then we can skip exploring the outgoing edges.

187

2

            continue;

188

2984

189

190

        // for every impl -[e]-> impl' do

191

3696

        for impl_transition in merged_lts.outgoing_transitions(impl_state) {

192

3696

            let new_edge = counter_example.add_edge(impl_transition.label, ce);

193

194

3696

            let spec_prime = if weak_transition && merged_lts.is_hidden_label(impl_transition.label) {

195

                // spec' := spec if e == tau

196

1014

                spec.clone()

197

            } else {

198

                // spec' := {s' | exists s in spec. s -[e]-> s'};

199

2682

                let mut spec_prime = VecSet::new();

200

201

2682

                if weak_transition {

202

                    // For weak trace refinement we need to consider

203

                    // tau-closures `s => s1 -[e]-> s2 => s'`, but only include

204

                    // the states after the `e` transition.

205

2361

                    let closure = tau_closure(merged_lts, spec.clone().to_vec(), &mut closure_cache, true);

206

207

8046

                    for s in &closure {

208

13554

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

209

13554

                            if impl_transition.label == spec_transition.label {

210

5214

                                spec_prime.insert(spec_transition.to);

211

8340

212

213

214

215

2361

                    spec_prime =

216

2361

                        VecSet::from_vec(tau_closure(merged_lts, spec_prime.to_vec(), &mut closure_cache, true));

217

                } else {

218

                    // Otherwise, simply consider direct transitions.

219

337

                    for s in &spec {

220

454

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

221

454

                            if impl_transition.label == spec_transition.label {

222

265

                                spec_prime.insert(spec_transition.to);

223

265

224

225

226

227

228

2682

                spec_prime

229

};

230

231

3696

            trace!(

232

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

233

                merged_lts.labels()[impl_transition.label],

234

                impl_transition.to,

235

                spec_prime

236

);

237

3696

            if spec_prime.is_empty() {

238

                // if spec' = {} then

239

608

                failing_trace(impl_state, &spec);

240

608

                return (false, Some(new_edge), None);

241

3088

242

243

3088

            if antichain.insert(impl_transition.to, spec_prime.clone()) {

244

                // if antichain_insert(impl,spec') then

245

2876

                trace!("Added ({:?}, {:?}) to working", impl_transition.to, spec_prime);

246

2876

                match strategy {

247

2876

                    ExplorationStrategy::BFS => working.push_back((impl_transition.to, spec_prime, new_edge)),

248

                    ExplorationStrategy::DFS => working.push_front((impl_transition.to, spec_prime, new_edge)),

249

250

212

251

252

253

254

438

    (true, None, None)

255

1290

256

257

/// This function checks that the refusals(impl) are contained in the refusals

258

/// of spec, it returns Some(refusal) iff the inclusion fails for the maximal refusal set.

259

///

260

/// # Details

261

///

262

/// See [refusals_contained_in_naive] for the definition of refusals.

263

///

264

/// In practice it can be more efficient to look at the enabled set of

265

/// states:

266

///

267

/// > enabled(s) = { a | exists s'. s -a-> s' } if stable(s)

268

///

269

/// then we have that refusals(impl) ⊆ refusals(spec) iff there exists a stable

270

/// s in spec such that enabled(s) ⊆ enabled(impl), and the enabled sets are

271

/// more efficient to compute.

272

771

fn refusals_contained_in<L: LTS>(

273

771

    lts: &L,

274

771

    impl_state: StateIndex,

275

771

    spec_states: &VecSet<StateIndex>,

276

771

) -> Option<Vec<LabelIndex>> {

277

771

    if !is_stable(lts, impl_state) {

278

        // If the implementation state is not stable, then it cannot have any refusals (or is maximally accepting).

279

239

        return None;

280

532

281

282

    // refusals(impl) ⊆ refusals(spec) iff there exists a stable spec state s with enabled(s) ⊆ enabled(impl).

283

664

    for s in spec_states.iter() {

284

664

        if !is_stable(lts, *s) {

285

            // Unstable spec states do not contribute to the refusals of the specification, so we can ignore them.

286

108

            continue;

287

556

288

289

556

        let mut is_witness = true;

290

556

        for transition_spec in lts.outgoing_transitions(*s) {

291

427

            if !lts

292

427

                .outgoing_transitions(impl_state)

293

427

                .any(|transition_impl| transition_impl.label == transition_spec.label)

294

295

                // s has an action impl cannot do, so s is not a witness (enabled(s) ⊄ enabled(impl)).

296

165

                is_witness = false;

297

165

                break;

298

262

299

300

301

556

        if is_witness {

302

            // All of s's enabled actions are also enabled in impl: s is a witness.

303

            // Therefore refusals(impl) ⊆ refusals(s) ⊆ refusals_set(spec).

304

391

            debug_assert!(refusals_contained_in_naive(lts, impl_state, spec_states));

305

391

            return None;

306

165

307

308

309

    // No stable spec state can witness enabled(s) ⊆ enabled(impl), so refusal inclusion fails.

310

141

    debug_assert!(!refusals_contained_in_naive(lts, impl_state, spec_states));

311

141

    Some(maximal_refusals(lts, impl_state).to_vec())

312

771

313

314

/// A naive implementation for checking that the refusals of an implementation state are contained in the refusals of a set of specification states.

315

532

fn refusals_contained_in_naive<L: LTS>(lts: &L, impl_state: StateIndex, spec_states: &VecSet<StateIndex>) -> bool {

316

532

    if !is_stable(lts, impl_state) {

317

        // If the implementation state is not stable, then it cannot have any refusals.

318

        return true;

319

532

320

321

532

    let impl_refusals = refusals(lts, impl_state);

322

532

    let spec_refusals = refusals_set(lts, spec_states);

323

532

    trace!("impl refusals: {:?}, spec refusals: {:?}", impl_refusals, spec_refusals);

324

325

532

    impl_refusals.is_subset(&spec_refusals)

326

532

327

328

/// Naive implementation for the refusals of a set of states spec:

329

///

330

/// > refusals(spec) = { r | exists s in spec. r in refusals(s) and stable(s) }

331

532

fn refusals_set<L: LTS>(lts: &L, spec_states: &VecSet<StateIndex>) -> VecSet<VecSet<LabelIndex>> {

332

532

    let mut result = VecSet::new();

333

334

860

    for s in spec_states.iter() {

335

860

        if is_stable(lts, *s) {

336

645

            result.extend(refusals(lts, *s).iter());

337

645

338

339

340

532

    result

341

532

342

343

/// Returns the maximal refusal set of a state s:

344

///

345

/// > maximal_refusals(s) = (Act \setminus enabled(s))

346

///

347

/// for stable states s. For unstable states this set is empty.

348

1318

fn maximal_refusals<L: LTS>(lts: &L, state: StateIndex) -> VecSet<LabelIndex> {

349

1318

    if !is_stable(lts, state) {

350

        return VecSet::new();

351

1318

352

353

    // The set of actions enabled in the given state.

354

1318

    let enabled_labels: VecSet<LabelIndex> =

355

1318

        VecSet::from_vec(lts.outgoing_transitions(state).map(|t| t.label).collect());

356

357

    // The set of all visible actions.

358

1318

    let all_labels: VecSet<LabelIndex> = VecSet::from_vec(

359

1318

        lts.labels()

360

1318

            .iter()

361

1318

            .enumerate()

362

            // We cannot refuse the tau action.

363

3966

            .filter(|(i, _)| !lts.is_hidden_label(LabelIndex::new(*i)))

364

2648

            .map(|(i, _)| LabelIndex::new(i))

365

1318

            .collect(),

366

);

367

368

1318

    VecSet::from_iter(all_labels.difference(&enabled_labels).cloned())

369

1318

370

371

/// Naive implementation of refusals of a state s:

372

///

373

/// A state s is stable, denoted by stable(s) iff `tau \not\in enabled(s)`, and

374

/// refusals are defined for stable states s by:

375

///

376

/// > refusals(s) = { r | r \subseteq (Act \setminus enabled(s)) }.

377

1177

fn refusals<L: LTS>(lts: &L, state: StateIndex) -> VecSet<VecSet<LabelIndex>> {

378

    // The refusal set of a stable state includes all subsets of its maximal refusal set.

379

1177

    let maximal_refusal = maximal_refusals(lts, state);

380

381

    // Take the powerset of `Act \setminus enabled(s)` to get all refusals.

382

1177

    VecSet::from_iter(maximal_refusal.iter().cloned().powerset().map(VecSet::from_iter))

383

1177

384

385

/// Returns true iff the given state is stable, i.e., it has no outgoing tau transitions.

386

4495

pub fn is_stable<L: LTS>(lts: &L, state: StateIndex) -> bool {

387

4495

    lts.outgoing_transitions(state).all(|t| !lts.is_hidden_label(t.label))

388

4495

389

390

/// A cache that is used to reuse allocations during tau-closure computations.

391

pub struct ClosureCache {

392

    /// States that are still to be explored.

393

    working: Vec<StateIndex>,

394

395

    /// Set of already visited states.

396

    visited: HashSet<StateIndex>,

397

398

399

impl ClosureCache {

400

    /// Creates a new closure cache.

401

3812

    pub fn new() -> Self {

402

3812

        ClosureCache {

403

3812

            working: Vec::new(),

404

3812

            visited: HashSet::new(),

405

3812

406

3812

407

408

409

impl Default for ClosureCache {

410

    fn default() -> Self {

411

        Self::new()

412

413

414

415

/// Returns the tau closure for a set of states in the given LTS.

416

///

417

/// # Details

418

///

419

/// The `states` parameter indicates the initial set of states for which the

420

/// tau-closure is to be computed. The `extend` parameter indicates whether the

421

/// closure should include the original states as well. The `cache` parameter is

422

/// used to avoid repeated allocations.

423

///

424

/// If `extend` is true then the original states are included in the closure,

425

/// otherwise they are not.

426

5836

pub fn tau_closure<L: LTS>(

427

5836

    lts: &L,

428

5836

    mut states: Vec<StateIndex>,

429

5836

    cache: &mut ClosureCache,

430

5836

    extend: bool,

431

5836

) -> Vec<StateIndex> {

432

5836

    debug_assert!(

433

5836

        cache.working.is_empty() && cache.visited.is_empty(),

434

        "Closure cache working not cleared before use."

435

);

436

437

    // Initialize the working set with the initial states, note that states is

438

    // kept in tact. As such the original states are also returned.

439

5836

    if extend {

440

5836

        cache.working.extend(states.iter().cloned());

441

5836

    } else {

442

        // Clear the original states.

443

        cache.working.append(&mut states);

444

445

446

    // Keep track of states that are already in the closure.

447

13991

    for s in &states {

448

13991

        cache.visited.insert(*s);

449

13991

450

451

23436

    while let Some(s) = cache.working.pop() {

452

28706

        for t in lts.outgoing_transitions(s) {

453

28706

            if lts.is_hidden_label(t.label) && !cache.visited.contains(&t.to) {

454

3609

                cache.working.push(t.to);

455

3609

                cache.visited.insert(t.to);

456

3609

                states.push(t.to);

457

25097

458

459

460

461

    // Clear the cache for the next use, the working set is empty by now.

462

5836

    cache.visited.clear();

463

464

5836

    states

465

5836

466

467

#[cfg(test)]

468

mod tests {

469

    use merc_lts::read_aut;

470

    use merc_utilities::Timing;

471

    use merc_utilities::test_logger;

472

473

    use crate::ExplorationStrategy;

474

    use crate::RefinementType;

475

    use crate::refines;

476

477

    #[test]

478

1

    fn test_example_2_12() {

479

1

        let _ = test_logger();

480

481

1

        let s0 = r#"des(0, 6, 5)

482

1

            (0, "req", 1)

483

1

            (1, "i", 2)

484

1

            (2, "10", 3)

485

1

            (3, "10", 0)

486

1

            (1, "i", 5)

487

1

            (5, "20", 0)"#;

488

489

1

        let t0 = r#"des(0, 3, 2)

490

1

            (0, "req", 1)

491

1

            (1, "20", 2)"#;

492

493

1

        let u0 = r#"des(0, 4, 3)

494

1

            (0, "req", 1)

495

1

            (1, "i", 1)

496

1

            (1, "20", 2)

497

1

            (2, "i", 0)"#;

498

499

1

        let s0 = read_aut(s0.as_bytes()).unwrap();

500

1

        let t0 = read_aut(t0.as_bytes()).unwrap();

501

1

        let u0 = read_aut(u0.as_bytes()).unwrap();

502

503

1

        let mut timing = Timing::new();

504

1

        assert!(

505

1

            refines(

506

1

                t0.clone(),

507

1

                s0.clone(),

508

1

                RefinementType::Weaktrace,

509

1

                ExplorationStrategy::BFS,

510

1

                false,

511

1

                false,

512

1

                &mut timing

513

1

514

1

.0

515

);

516

1

        assert!(

517

1

            !refines(

518

1

t0,

519

1

                s0.clone(),

520

1

                RefinementType::StableFailures,

521

1

                ExplorationStrategy::BFS,

522

1

                false,

523

1

                false,

524

1

                &mut timing

525

1

526

1

.0

527

);

528

1

        assert!(

529

1

            refines(

530

1

u0,

531

1

s0,

532

1

                RefinementType::StableFailures,

533

1

                ExplorationStrategy::BFS,

534

1

                false,

535

1

                false,

536

1

                &mut timing

537

1

538

1

.0

539

);

540

1

541