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

24

use crate::Antichain;

25

use crate::CounterExampleTree;

26

use crate::ExplorationStrategy;

27

use crate::RefinementType;

28

29

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

30

484

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

31

484

    lts: &L,

32

484

    initial_spec: StateIndex,

33

484

    refinement: RefinementType,

34

484

    strategy: ExplorationStrategy,

35

484

    counter_example: &mut CE,

36

484

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

37

484

    match refinement {

38

141

        RefinementType::Trace => is_refinement_generic(

39

141

            strategy,

40

141

            lts,

41

141

            lts.initial_state_index(),

42

141

            initial_spec,

43

            |_, _| None,

44

            false,

45

141

            counter_example,

46

),

47

141

        RefinementType::Weaktrace => is_refinement_generic(

48

141

            strategy,

49

141

            lts,

50

141

            lts.initial_state_index(),

51

141

            initial_spec,

52

            |_, _| None,

53

            true,

54

141

            counter_example,

55

),

56

202

        RefinementType::StableFailures => is_refinement_generic(

57

202

            strategy,

58

202

            lts,

59

202

            lts.initial_state_index(),

60

202

            initial_spec,

61

1073

            |impl_state, spec_states| refusals_contained_in(lts, impl_state, spec_states),

62

            true,

63

202

            counter_example,

64

),

65

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

66

67

484

68

69

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

70

///

71

/// # Details

72

///

73

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

74

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

75

/// LTSs.

76

///

77

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

78

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

79

/// transitions.

80

///

81

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

82

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

83

/// `Some(counter_example)` if the pair is invalid.

84

///

85

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

86

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

87

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

88

/// example information.

89

1103

pub fn is_refinement_generic<L: LTS, CE: CounterExampleTree, F, CC>(

90

1103

    strategy: ExplorationStrategy,

91

1103

    merged_lts: &L,

92

1103

    initial_impl: StateIndex,

93

1103

    initial_spec: StateIndex,

94

1103

    mut check: F,

95

1103

    weak_transition: bool,

96

1103

    counter_example: &mut CE,

97

1103

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

98

1103

where

99

1103

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

100

101

    // The antichain data structure is used for storing explored states. However, as opposed to a discovered set it

102

    // allows for pruning additional pairs based on the `antichain` property.

103

1103

    let mut antichain = Antichain::new();

104

105

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

106

1103

    let mut closure_cache = ClosureCache::new();

107

108

1103

    let mut working = VecDeque::from([(

109

1103

        initial_impl,

110

1103

        if weak_transition {

111

962

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

112

        } else {

113

141

            VecSet::singleton(initial_spec)

114

},

115

1103

        counter_example.root_index(),

116

    )]);

117

118

    // pop (impl,spec) from working;

119

6632

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

120

5926

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

121

5926

        if let Some(counter_example) = check(impl_state, &spec) {

122

            // if not check(impl,spec) then

123

92

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

124

5834

125

126

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

127

6218

        for impl_transition in merged_lts.outgoing_transitions(impl_state) {

128

6218

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

129

130

6218

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

131

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

132

904

                spec.clone()

133

            } else {

134

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

135

5314

                let mut spec_prime = VecSet::new();

136

137

5314

                if weak_transition {

138

                    // For weak trace refinement we need to consider

139

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

140

                    // the states after the `e` transition.

141

4379

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

142

143

6603

                    for s in &closure {

144

9679

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

145

9679

                            if impl_transition.label == spec_transition.label {

146

5072

                                spec_prime.insert(spec_transition.to);

147

5072

148

149

150

151

4379

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

152

                } else {

153

                    // Otherwise, simply consider direct transitions.

154

1017

                    for s in &spec {

155

1586

                        for spec_transition in merged_lts.outgoing_transitions(*s) {

156

1586

                            if impl_transition.label == spec_transition.label {

157

984

                                spec_prime.insert(spec_transition.to);

158

984

159

160

161

162

163

5314

                spec_prime

164

};

165

166

6218

            trace!(" -[{}]-> ({}, {:?})", merged_lts.labels()[impl_transition.label], impl_transition.to, spec_prime);

167

6218

            if spec_prime.is_empty() {

168

                // if spec' = {} then

169

305

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

170

5913

171

172

5913

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

173

                // if antichain_insert(impl,spec') then

174

5461

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

175

5461

                match strategy {

176

5461

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

177

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

178

179

452

180

181

182

183

706

    (true, None, None)

184

1103

185

186

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

187

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

188

///

189

/// # Details

190

///

191

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

192

///

193

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

194

/// states:

195

///

196

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

197

///

198

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

199

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

200

/// more efficient to compute.

201

1073

fn refusals_contained_in<L: LTS>(

202

1073

    lts: &L,

203

1073

    impl_state: StateIndex,

204

1073

    spec_states: &VecSet<StateIndex>,

205

1073

) -> Option<Vec<LabelIndex>> {

206

1073

    if !is_stable(lts, impl_state) {

207

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

208

188

        return None;

209

885

210

211

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

212

1018

    for s in spec_states.iter() {

213

1018

        if !is_stable(lts, *s) {

214

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

215

93

            continue;

216

925

217

218

925

        let mut is_witness = true;

219

925

        for transition_spec in lts.outgoing_transitions(*s) {

220

816

            if !lts

221

816

                .outgoing_transitions(impl_state)

222

977

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

223

224

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

225

88

                is_witness = false;

226

88

                break;

227

728

228

229

230

925

        if is_witness {

231

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

232

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

233

837

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

234

837

            return None;

235

88

236

237

238

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

239

48

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

240

48

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

241

1073

242

243

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

244

885

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

245

885

    if !is_stable(lts, impl_state) {

246

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

247

        return true;

248

885

249

250

885

    let impl_refusals = refusals(lts, impl_state);

251

885

    let spec_refusals = refusals_set(lts, spec_states);

252

885

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

253

254

885

    impl_refusals.is_subset(&spec_refusals)

255

885

256

257

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

258

///

259

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

260

885

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

261

885

    let mut result = VecSet::new();

262

263

1228

    for s in spec_states.iter() {

264

1228

        if is_stable(lts, *s) {

265

1038

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

266

1038

267

268

269

885

    result

270

885

271

272

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

273

///

274

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

275

///

276

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

277

1971

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

278

1971

    if !is_stable(lts, state) {

279

        return VecSet::new();

280

1971

281

282

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

283

1971

    let enabled_labels: VecSet<LabelIndex> =

284

1971

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

285

286

    // The set of all visible actions.

287

1971

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

288

1971

        lts.labels()

289

1971

            .iter()

290

1971

            .enumerate()

291

            // We cannot refuse the tau action.

292

9843

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

293

7872

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

294

1971

            .collect(),

295

);

296

297

1971

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

298

1971

299

300

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

301

///

302

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

303

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

304

///

305

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

306

1923

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

307

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

308

1923

    let maximal_refusal = maximal_refusals(lts, state);

309

310

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

311

1923

    VecSet::from_iter(

312

1923

        maximal_refusal

313

1923

            .iter()

314

1923

            .cloned()

315

1923

            .powerset()

316

1923

            .map(VecSet::from_iter),

317

318

1923

319

320

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

321

6659

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

322

6659

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

323

6659

324

325

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

326

pub struct ClosureCache {

327

    /// States that are still to be explored.

328

    working: Vec<StateIndex>,

329

330

    /// Set of already visited states.

331

    visited: HashSet<StateIndex>,

332

333

334

impl ClosureCache {

335

    /// Creates a new closure cache.

336

1103

    pub fn new() -> Self {

337

1103

        ClosureCache {

338

1103

            working: Vec::new(),

339

1103

            visited: HashSet::new(),

340

1103

341

1103

342

343

344

impl Default for ClosureCache {

345

    fn default() -> Self {

346

        Self::new()

347

348

349

350

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

351

///

352

/// # Details

353

///

354

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

355

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

356

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

357

/// used to avoid repeated allocations.

358

///

359

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

360

/// otherwise they are not.

361

9720

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

362

9720

    debug_assert!(cache.working.is_empty(), "Closure cache working not cleared before use.");

363

9720

    debug_assert!(cache.visited.is_empty(), "Closure cache visited not cleared before use.");

364

365

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

366

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

367

9720

    if extend {

368

9720

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

369

9720

    } else {

370

        // Clear the original states.

371

        cache.working.append(&mut states);

372

373

374

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

375

12621

    for s in &states {

376

12621

        cache.visited.insert(*s);

377

12621

378

379

23633

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

380

17076

        for t in lts.outgoing_transitions(s) {

381

17076

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

382

1292

                cache.working.push(t.to);

383

1292

                cache.visited.insert(t.to);

384

1292

                states.push(t.to);

385

15784

386

387

388

389

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

390

9720

    cache.visited.clear();

391

392

9720

    states

393

9720

394

395

#[cfg(test)]

396

mod tests {

397

    use merc_lts::read_aut;

398

    use merc_utilities::Timing;

399

    use merc_utilities::test_logger;

400

401

    use crate::ExplorationStrategy;

402

    use crate::RefinementType;

403

    use crate::refines;

404

405

    #[test]

406

1

    fn test_example_2_12() {

407

1

        let _ = test_logger();

408

409

1

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

410

1

            (0, "req", 1)

411

1

            (1, "i", 2)

412

1

            (2, "10", 3)

413

1

            (3, "10", 0)

414

1

            (1, "i", 5)

415

1

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

416

417

1

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

418

1

            (0, "req", 1)

419

1

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

420

421

1

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

422

1

            (0, "req", 1)

423

1

            (1, "i", 1)

424

1

            (1, "20", 2)

425

1

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

426

427

1

        let s0 = read_aut(s0.as_bytes(), Vec::new()).unwrap();

428

1

        let t0 = read_aut(t0.as_bytes(), Vec::new()).unwrap();

429

1

        let u0 = read_aut(u0.as_bytes(), Vec::new()).unwrap();

430

431

1

        let mut timing = Timing::new();

432

1

        assert!(

433

1

            refines(

434

1

                t0.clone(),

435

1

                s0.clone(),

436

1

                RefinementType::Weaktrace,

437

1

                ExplorationStrategy::BFS,

438

1

                false,

439

1

                false,

440

1

                &mut timing

441

1

442

1

.0

443

);

444

1

        assert!(

445

1

            !refines(

446

1

t0,

447

1

                s0.clone(),

448

1

                RefinementType::StableFailures,

449

1

                ExplorationStrategy::BFS,

450

1

                false,

451

1

                false,

452

1

                &mut timing

453

1

454

1

.0

455

);

456

1

        assert!(

457

1

            refines(

458

1

u0,

459

1

s0,

460

1

                RefinementType::StableFailures,

461

1

                ExplorationStrategy::BFS,

462

1

                false,

463

1

                false,

464

1

                &mut timing

465

1

466

1

.0

467

);

468

1

469