Grcov report - failures

1

use std::collections::HashSet;

2

use std::collections::VecDeque;

3

4

use itertools::Itertools;

5

use log::trace;

6

7

use merc_collections::VecSet;

8

use merc_lts::LTS;

9

use merc_lts::LabelIndex;

10

use merc_lts::StateIndex;

11

use merc_reduction::diverges;

12

13

use crate::AC;

14

use crate::Antichain;

15

use crate::CounterExampleTree;

16

use crate::ExplorationStrategy;

17

use crate::RefinementType;

18

19

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

20

pub enum InnerCe {

21

    Refusal(Vec<LabelIndex>),

22

    Diverges,

23

24

25

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

26

///

27

/// These antichain-based algorithms cover trace, weak-trace, stable-failures and

28

/// failures-divergence inclusion, and are described in:

29

///

30

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

31

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

32

/// > Science 17(1) 2021

33

///

34

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

35

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

36

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

37

/// example.

38

698

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

39

698

    lts: &L,

40

698

    initial_spec: StateIndex,

41

698

    refinement: RefinementType,

42

698

    strategy: ExplorationStrategy,

43

698

    counter_example: &mut CE,

44

698

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

45

698

    let mut antichain = Antichain::new();

46

47

698

    match refinement {

48

175

        RefinementType::Trace => is_refinement_generic(

49

175

            strategy,

50

175

            lts,

51

175

            lts.initial_state_index(),

52

175

            initial_spec,

53

290

            |_, _| (None, true),

54

            |_, _| (),

55

            false,

56

175

            counter_example,

57

175

            &mut antichain,

58

),

59

181

        RefinementType::Weaktrace => is_refinement_generic(

60

181

            strategy,

61

181

            lts,

62

181

            lts.initial_state_index(),

63

181

            initial_spec,

64

473

            |_, _| (None, true),

65

            |_, _| (),

66

            true,

67

181

            counter_example,

68

181

            &mut antichain,

69

),

70

166

        RefinementType::StableFailures => is_refinement_generic(

71

166

            strategy,

72

166

            lts,

73

166

            lts.initial_state_index(),

74

166

            initial_spec,

75

331

            |impl_state, spec_states| {

76

331

77

331

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

78

331

                    true,

79

331

80

331

},

81

            |_, _| (),

82

            true,

83

166

            counter_example,

84

166

            &mut antichain,

85

),

86

176

        RefinementType::FailuresDivergences => is_refinement_generic(

87

176

            strategy,

88

176

            lts,

89

176

            lts.initial_state_index(),

90

176

            initial_spec,

91

352

            |impl_state, spec_states| {

92

602

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

93

349

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

94

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

95

349

                    if diverges(lts, impl_state) {

96

1

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

97

1

                        (Some(InnerCe::Diverges), true)

98

                    } else {

99

348

100

348

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

101

348

                            true,

102

348

103

104

                } else {

105

3

                    (None, false)

106

107

352

},

108

            |_, _| (),

109

            true,

110

176

            counter_example,

111

176

            &mut antichain,

112

),

113

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

114

115

698

116

117

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

118

///

119

/// # Details

120

///

121

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

122

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

123

/// LTSs.

124

///

125

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

126

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

127

/// transitions.

128

///

129

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

130

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

131

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

132

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

133

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

134

///

135

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

136

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

137

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

138

/// example information.

139

///

140

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

141

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

142

/// on the `antichain` property.

143

#[allow(clippy::too_many_arguments)]

144

1203

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

145

1203

    strategy: ExplorationStrategy,

146

1203

    merged_lts: &L,

147

1203

    initial_impl: StateIndex,

148

1203

    initial_spec: StateIndex,

149

1203

    mut check: F,

150

1203

    mut failing_trace: G,

151

1203

    weak_transition: bool,

152

1203

    counter_example: &mut CE,

153

1203

    antichain: &mut A,

154

1203

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

155

1203

where

156

1203

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

157

1203

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

158

159

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

160

1203

    let mut closure_cache = ClosureCache::new();

161

162

1203

    let mut working = VecDeque::from([(

163

1203

        initial_impl,

164

1203

        if weak_transition {

165

1028

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

166

        } else {

167

175

            VecSet::singleton(initial_spec)

168

},

169

1203

        counter_example.root_index(),

170

    )]);

171

172

    // pop (impl,spec) from working;

173

3383

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

174

2972

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

175

2972

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

176

2972

        if let Some(counter_example) = inner_counter_example {

177

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

178

206

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

179

2766

180

181

2766

        if !continue_exploration {

182

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

183

3

            continue;

184

2763

185

186

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

187

3324

        for impl_transition in merged_lts.outgoing_transitions(impl_state) {

188

3324

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

189

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

190

828

                spec.clone()

191

            } else {

192

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

193

2496

                let mut spec_prime = VecSet::new();

194

195

2496

                if weak_transition {

196

                    // For weak trace refinement we need to consider

197

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

198

                    // the states after the `e` transition.

199

2178

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

200

201

10752

                    for s in &closure {

202

19306

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

203

19306

                            if impl_transition.label == spec_transition.label {

204

7688

                                spec_prime.insert(spec_transition.to);

205

11618

206

207

208

209

2178

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

210

                } else {

211

                    // Otherwise, simply consider direct transitions.

212

350

                    for s in &spec {

213

485

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

214

485

                            if impl_transition.label == spec_transition.label {

215

265

                                spec_prime.insert(spec_transition.to);

216

265

217

218

219

220

221

2496

                spec_prime

222

};

223

224

3324

            trace!(

225

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

226

                merged_lts.labels()[impl_transition.label],

227

                impl_transition.to,

228

                spec_prime

229

);

230

3324

            if spec_prime.is_empty() {

231

                // if spec' = {} then

232

586

                failing_trace(impl_state, &spec);

233

586

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

234

586

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

235

2738

236

237

2738

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

238

                // if antichain_insert(impl,spec') then

239

2581

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

240

2581

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

241

2581

                match strategy {

242

2581

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

243

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

244

245

157

246

247

248

249

411

    (true, None, None)

250

1203

251

252

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

253

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

254

///

255

/// # Details

256

///

257

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

258

///

259

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

260

/// states:

261

///

262

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

263

///

264

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

265

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

266

/// more efficient to compute.

267

679

fn refusals_contained_in<L: LTS>(

268

679

    lts: &L,

269

679

    impl_state: StateIndex,

270

679

    spec_states: &VecSet<StateIndex>,

271

679

) -> Option<Vec<LabelIndex>> {

272

679

    if !is_stable(lts, impl_state) {

273

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

274

215

        return None;

275

464

276

277

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

278

580

    for s in spec_states.iter() {

279

580

        if !is_stable(lts, *s) {

280

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

281

92

            continue;

282

488

283

284

        // This is O(n^2), but it avoids allocating the refusal sets, which are

285

        // often small anyway.

286

488

        let mut is_witness = true;

287

488

        for transition_spec in lts.outgoing_transitions(*s) {

288

334

            if !lts

289

334

                .outgoing_transitions(impl_state)

290

334

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

291

292

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

293

144

                is_witness = false;

294

144

                break;

295

190

296

297

298

488

        if is_witness {

299

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

300

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

301

344

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

302

344

            return None;

303

144

304

305

306

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

307

120

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

308

120

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

309

679

310

311

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

312

464

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

313

464

    if !is_stable(lts, impl_state) {

314

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

315

        return true;

316

464

317

318

464

    let impl_refusals = refusals(lts, impl_state);

319

464

    let spec_refusals = refusals_set(lts, spec_states);

320

464

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

321

322

464

    impl_refusals.is_subset(&spec_refusals)

323

464

324

325

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

326

///

327

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

328

464

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

329

464

    let mut result = VecSet::new();

330

331

763

    for s in spec_states.iter() {

332

763

        if is_stable(lts, *s) {

333

563

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

334

563

335

336

337

464

    result

338

464

339

340

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

341

///

342

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

343

///

344

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

345

1147

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

346

1147

    if !is_stable(lts, state) {

347

        return VecSet::new();

348

1147

349

350

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

351

1147

    let enabled_labels: VecSet<LabelIndex> =

352

1147

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

353

354

    // The set of all visible actions.

355

1147

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

356

1147

        lts.labels()

357

1147

            .iter()

358

1147

            .enumerate()

359

            // We cannot refuse the tau action.

360

3453

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

361

2306

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

362

1147

            .collect(),

363

);

364

365

1147

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

366

1147

367

368

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

369

///

370

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

371

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

372

///

373

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

374

1027

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

375

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

376

1027

    let maximal_refusal = maximal_refusals(lts, state);

377

378

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

379

1027

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

380

1027

381

382

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

383

3933

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

384

3933

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

385

3933

386

387

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

388

pub struct ClosureCache {

389

    /// States that are still to be explored.

390

    working: Vec<StateIndex>,

391

392

    /// Set of already visited states.

393

    visited: HashSet<StateIndex>,

394

395

396

impl ClosureCache {

397

    /// Creates a new closure cache.

398

7073

    pub fn new() -> Self {

399

7073

        ClosureCache {

400

7073

            working: Vec::new(),

401

7073

            visited: HashSet::new(),

402

7073

403

7073

404

405

406

impl Default for ClosureCache {

407

    fn default() -> Self {

408

        Self::new()

409

410

411

412

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

413

///

414

/// # Details

415

///

416

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

417

/// tau-closure is to be computed; the original states are always included in the

418

/// returned closure. The `cache` parameter is used to avoid repeated allocations.

419

5384

pub fn tau_closure<L: LTS>(lts: &L, mut states: Vec<StateIndex>, cache: &mut ClosureCache) -> Vec<StateIndex> {

420

5384

    debug_assert!(

421

5384

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

422

        "Closure cache working not cleared before use."

423

);

424

425

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

426

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

427

5384

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

428

429

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

430

19017

    for s in &states {

431

19017

        cache.visited.insert(*s);

432

19017

433

434

28983

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

435

41165

        for t in lts.outgoing_transitions(s) {

436

41165

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

437

4582

                cache.working.push(t.to);

438

4582

                cache.visited.insert(t.to);

439

4582

                states.push(t.to);

440

36583

441

442

443

444

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

445

5384

    cache.visited.clear();

446

447

5384

    states

448

5384

449

450

#[cfg(test)]

451

mod tests {

452

    use merc_lts::read_aut;

453

    use merc_utilities::Timing;

454

    use merc_utilities::test_logger;

455

456

    use crate::ExplorationStrategy;

457

    use crate::RefinementType;

458

    use crate::refines;

459

460

    #[test]

461

1

    fn test_example_2_12() {

462

1

        test_logger();

463

464

1

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

465

1

            (0, "req", 1)

466

1

            (1, "i", 2)

467

1

            (2, "10", 3)

468

1

            (3, "10", 0)

469

1

            (1, "i", 5)

470

1

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

471

472

1

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

473

1

            (0, "req", 1)

474

1

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

475

476

1

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

477

1

            (0, "req", 1)

478

1

            (1, "i", 1)

479

1

            (1, "20", 2)

480

1

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

481

482

1

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

483

1

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

484

1

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

485

486

1

        let mut timing = Timing::new();

487

1

        assert!(

488

1

            refines(

489

1

                t0.clone(),

490

1

                s0.clone(),

491

1

                RefinementType::Weaktrace,

492

1

                ExplorationStrategy::BFS,

493

1

                false,

494

1

                false,

495

1

                &mut timing

496

1

497

1

.0

498

);

499

1

        assert!(

500

1

            !refines(

501

1

t0,

502

1

                s0.clone(),

503

1

                RefinementType::StableFailures,

504

1

                ExplorationStrategy::BFS,

505

1

                false,

506

1

                false,

507

1

                &mut timing

508

1

509

1

.0

510

);

511

1

        assert!(

512

1

            refines(

513

1

u0,

514

1

s0,

515

1

                RefinementType::StableFailures,

516

1

                ExplorationStrategy::BFS,

517

1

                false,

518

1

                false,

519

1

                &mut timing

520

1

521

1

.0

522

);

523

1

524