Grcov report - refinement.rs

1

use itertools::Itertools;

2

use log::debug;

3

use log::trace;

4

use log::warn;

5

use merc_lts::LTS;

6

use merc_lts::StateIndex;

7

use merc_reduction::Equivalence;

8

use merc_reduction::Partition;

9

use merc_reduction::branching_bisim_sigref;

10

use merc_reduction::quotient_lts_block;

11

use merc_reduction::quotient_lts_naive;

12

use merc_reduction::strong_bisim_sigref;

13

use merc_reduction::tau_scc_decomposition;

14

use merc_utilities::Timing;

15

16

use crate::CounterExample;

17

use crate::CounterExampleConstructor;

18

use crate::is_failures_refinement;

19

use crate::is_impossible_futures_refinement;

20

21

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

22

#[cfg_attr(feature = "clap", derive(clap::ValueEnum))]

23

pub enum RefinementType {

24

    /// Checks for (strong) trace inclusion, i.e., whether all traces of the implementation are also traces of the specification.

25

    Trace,

26

    /// Checks for weak trace inclusion, i.e., whether all weak traces of the implementation are also weak traces of the specification.

27

    Weaktrace,

28

    /// Checks for stable failures inclusion, i.e., whether all stable failures of the implementation are also stable failures of the specification.

29

    StableFailures,

30

    /// Checks for impossible futures inclusion, i.e., whether all impossible futures of the implementation are also impossible futures of the specification.

31

    ImpossibleFutures,

32

33

34

/// Determines the exploration strategy for the failures refinement algorithm.

35

///

36

/// Typically `BFS` is more suited for counter examples, but `DFS` can be more efficient

37

/// in practice when a counter example is not required.

38

#[derive(Clone, Copy)]

39

pub enum ExplorationStrategy {

40

    BFS,

41

    DFS,

42

43

44

/// Checks whether `impl_lts` refines `spec_lts` according to the given

45

/// `refinement` relation.

46

///

47

/// # Details

48

///

49

/// The `refinement_type` determines (weak) trace inclusions, failures inclusion

50

/// and divergence failures inclusion etc.

51

///

52

/// The `strategy` parameter determines whether a breadth-first search

53

/// or depth-first search is used to explore the state space. Breadth-first search

54

/// is often better suited for finding short counter examples, while depth-first

55

/// search often uses less memory.

56

///

57

/// The `preprocess` flag indicates whether preprocessing should be applied to

58

/// the LTSs. The refinement checks often involve product constructions, and

59

/// reducing the state space beforehand can lead to significant performance

60

/// improvements. However, for quick failing checks the preprocessing could cause

61

/// unnecessary overhead.

62

803

pub fn refines<L: LTS>(

63

803

    impl_lts: L,

64

803

    spec_lts: L,

65

803

    refinement: RefinementType,

66

803

    strategy: ExplorationStrategy,

67

803

    preprocess: bool,

68

803

    counter_example: bool,

69

803

    timing: &mut Timing,

70

803

) -> (bool, Option<CounterExample<L::Label>>) {

71

803

    let (reduction, divergence_preserving) = match refinement {

72

200

        RefinementType::Trace => (Equivalence::StrongBisim, false),

73

        // Note that for impossible futures we use branching bisimulation, which also removes tau loops.

74

401

        RefinementType::Weaktrace | RefinementType::ImpossibleFutures => (Equivalence::BranchingBisim, false),

75

202

        RefinementType::StableFailures => (Equivalence::BranchingBisim, true),

76

};

77

78

    // For the preprocessing/quotienting step it makes sense to merge both LTSs

79

    // together in case that some states are equivalent. So we do this in all branches.

80

803

    let (merged_lts, initial_spec) = if preprocess {

81

        // Reduce all states in the merged LTS.

82

400

        match reduction {

83

            Equivalence::StrongBisim => {

84

100

                let (merged_lts, initial_spec) = impl_lts.merge_disjoint(&spec_lts);

85

100

                let (preprocess_lts, partition) = strong_bisim_sigref(merged_lts, timing);

86

87

100

                let impl_block = partition.block_number(preprocess_lts.initial_state_index());

88

100

                let spec_block = partition.block_number(initial_spec);

89

90

100

                if impl_block == spec_block {

91

                    // The initial states are already in the same block, so we can skip the refinement check.

92

59

                    debug!(

93

                        "Initial states are in the same block after strong bisimulation reduction, skipping refinement check."

94

);

95

59

                    return (true, None);

96

41

97

98

                // After partitioning the block becomes the state in the reduced_lts.

99

41

                let reduced_lts = quotient_lts_block::<_, false>(&preprocess_lts, &partition);

100

41

                (reduced_lts, StateIndex::new(*spec_block))

101

102

            Equivalence::BranchingBisim => {

103

300

                if divergence_preserving {

104

100

                    warn!(

105

                        "Preprocessing for divergence preserving branching bisimulation has not been implemented yet."

106

);

107

100

                    impl_lts.merge_disjoint(&spec_lts)

108

                } else {

109

200

                    let (merged_lts, initial_spec) = impl_lts.merge_disjoint(&spec_lts);

110

200

                    let (preprocess_lts, initial_spec, partition) = branching_bisim_sigref(merged_lts, initial_spec, timing);

111

112

200

                    let impl_block = partition.block_number(preprocess_lts.initial_state_index());

113

200

                    let spec_block = partition.block_number(initial_spec);

114

115

200

                    if impl_block == spec_block {

116

                        // The initial states are already in the same block, so we can skip the refinement check.

117

127

                        debug!(

118

                            "Initial states are in the same block after branching bisimulation reduction, skipping refinement check."

119

);

120

127

                        return (true, None);

121

73

122

123

73

                    let reduced_lts = quotient_lts_block::<_, true>(&preprocess_lts, &partition);

124

73

                    (reduced_lts, StateIndex::new(*spec_block))

125

126

127

            _ => unimplemented!("Preprocessing for refinement type {refinement:?} has not been implemented yet."),

128

129

    } else {

130

403

        if refinement == RefinementType::ImpossibleFutures {

131

            // For impossible futures we need to remove tau loops from the implementation.

132

100

            let scc_partition = tau_scc_decomposition(&impl_lts);

133

100

            let tau_loop_free_lts = quotient_lts_naive(&impl_lts, &scc_partition, true);

134

135

100

            tau_loop_free_lts.merge_disjoint(&spec_lts)

136

        } else {

137

303

            impl_lts.merge_disjoint(&spec_lts)

138

139

};

140

141

    // Print the labels of the merged LTS for debugging purposes.

142

617

    trace!(

143

        "Merged LTS labels: {:?}",

144

        merged_lts.labels().iter().enumerate().format("\n")

145

);

146

147

617

    timing.measure("refinement", || {

148

617

        if counter_example {

149

            // Construct a counter example tree, and return a trace.

150

614

            let mut ce_constructor = CounterExampleConstructor::new();

151

614

            let result = match refinement {

152

                RefinementType::Trace | RefinementType::Weaktrace | RefinementType::StableFailures => {

153

481

                    let (result, ce_state, ce_inner) =

154

481

                        is_failures_refinement(&merged_lts, initial_spec, refinement, strategy, &mut ce_constructor);

155

156

481

                    if let Some(state) = ce_state {

157

                        // Reconstruct a trace from the counter example tree, relabelling the indices to their actual labels.

158

193

                        let trace = ce_constructor

159

193

                            .reconstruct_trace(state)

160

193

                            .iter()

161

866

                            .map(|l| merged_lts.labels()[*l].clone())

162

193

                            .collect();

163

164

193

                            result,

165

193

                            Some(match refinement {

166

57

                                RefinementType::Trace => CounterExample::Trace(trace),

167

51

                                RefinementType::Weaktrace => CounterExample::WeakTrace(trace),

168

                                RefinementType::StableFailures => {

169

85

                                    if let Some(inner) = ce_inner {

170

                                        CounterExample::StableFailures(

171

47

                                            trace,

172

167

                                            inner.iter().map(|l| merged_lts.labels()[*l].clone()).collect(),

173

174

                                    } else {

175

                                        // The stable failures failed because of a weak trace difference.

176

38

                                        CounterExample::WeakTrace(trace)

177

178

179

                                _ => unreachable!("Refinement {refinement:?} is not valid in this path"),

180

}),

181

182

                    } else {

183

288

                        (result, None)

184

185

186

                RefinementType::ImpossibleFutures => {

187

133

                    let (result, ce_state, ce_inner) =

188

133

                        is_impossible_futures_refinement(&merged_lts, initial_spec, strategy, &mut ce_constructor);

189

190

133

                    if let Some(state) = ce_state {

191

                        // Reconstruct a trace from the counter example tree, relabelling the indices to their actual labels.

192

64

                        let trace = ce_constructor

193

64

                            .reconstruct_trace(state)

194

64

                            .iter()

195

103

                            .map(|l| merged_lts.labels()[*l].clone())

196

64

                            .collect();

197

198

64

                            result,

199

64

                            Some(if let Some(inner) = ce_inner {

200

44

                                CounterExample::ImpossibleFutures(trace, inner)

201

                            } else {

202

                                // The impossible futures failed because of a weak trace.

203

20

                                CounterExample::WeakTrace(trace)

204

}),

205

206

                    } else {

207

69

                        (result, None)

208

209

210

};

211

212

614

            trace!("Counter example tree: {:?}", ce_constructor);

213

614

            result

214

        } else {

215

            // Run without constructing a counter example.

216

3

            match refinement {

217

                RefinementType::Trace | RefinementType::Weaktrace | RefinementType::StableFailures => {

218

3

                    let (result, _, _) =

219

3

                        is_failures_refinement(&merged_lts, initial_spec, refinement, strategy, &mut ());

220

3

                    (result, None)

221

222

                RefinementType::ImpossibleFutures => {

223

                    let (result, _, _) = is_impossible_futures_refinement(&merged_lts, initial_spec, strategy, &mut ());

224

                    (result, None)

225

226

227

228

617

})

229

803

230

231

#[cfg(test)]

232

mod tests {

233

    use std::io::Write;

234

235

    use merc_vpg::PG;

236

    use rand::rngs::StdRng;

237

238

    use merc_io::DumpFiles;

239

    use merc_lts::mutate_lts;

240

    use merc_lts::random_lts_monolithic;

241

    use merc_lts::write_aut;

242

    use merc_utilities::Timing;

243

    use merc_utilities::random_test;

244

    use merc_vpg::solve_zielonka;

245

    use merc_vpg::translate;

246

247

    use crate::ExplorationStrategy;

248

    use crate::RefinementType;

249

    use crate::generate_formula;

250

    use crate::refines;

251

252

    #[test]

253

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

254

1

    fn test_random_trace_refinement() {

255

100

        random_test(100, |rng| {

256

100

            is_refinement_test(

257

100

                "test_random_trace_refinement",

258

100

                rng,

259

100

                RefinementType::Trace,

260

100

                ExplorationStrategy::BFS,

261

                false,

262

);

263

100

});

264

1

265

266

    #[test]

267

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

268

1

    fn test_random_weak_trace_refinement() {

269

100

        random_test(100, |rng| {

270

100

            is_refinement_test(

271

100

                "test_random_weak_trace_refinement",

272

100

                rng,

273

100

                RefinementType::Weaktrace,

274

100

                ExplorationStrategy::BFS,

275

                false,

276

);

277

100

});

278

1

279

280

    #[test]

281

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

282

1

    fn test_random_stable_failures_refinement() {

283

100

        random_test(100, |rng| {

284

100

            is_refinement_test(

285

100

                "test_random_stable_failures_refinement",

286

100

                rng,

287

100

                RefinementType::StableFailures,

288

100

                ExplorationStrategy::BFS,

289

                false,

290

);

291

100

});

292

1

293

294

    #[test]

295

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

296

1

    fn test_random_impossible_futures_refinement() {

297

100

        random_test(100, |rng| {

298

100

            is_refinement_test(

299

100

                "test_random_impossible_futures_refinement",

300

100

                rng,

301

100

                RefinementType::ImpossibleFutures,

302

100

                ExplorationStrategy::BFS,

303

                false,

304

);

305

100

});

306

1

307

308

    #[test]

309

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

310

1

    fn test_random_trace_refinement_preprocessed() {

311

100

        random_test(100, |rng| {

312

100

            is_refinement_test(

313

100

                "test_random_trace_refinement",

314

100

                rng,

315

100

                RefinementType::Trace,

316

100

                ExplorationStrategy::BFS,

317

                true,

318

);

319

100

});

320

1

321

322

    #[test]

323

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

324

1

    fn test_random_weak_trace_refinement_preprocessed() {

325

100

        random_test(100, |rng| {

326

100

            is_refinement_test(

327

100

                "test_random_weak_trace_refinement",

328

100

                rng,

329

100

                RefinementType::Weaktrace,

330

100

                ExplorationStrategy::BFS,

331

                true,

332

);

333

100

});

334

1

335

336

    #[test]

337

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

338

1

    fn test_random_stable_failures_refinement_preprocessed() {

339

100

        random_test(100, |rng| {

340

100

            is_refinement_test(

341

100

                "test_random_stable_failures_refinement",

342

100

                rng,

343

100

                RefinementType::StableFailures,

344

100

                ExplorationStrategy::BFS,

345

                true,

346

);

347

100

});

348

1

349

350

    #[test]

351

    #[cfg_attr(miri, ignore)] // Tests are too slow under miri.

352

1

    fn test_random_impossible_futures_refinement_preprocessed() {

353

100

        random_test(100, |rng| {

354

100

            is_refinement_test(

355

100

                "test_random_impossible_futures_refinement",

356

100

                rng,

357

100

                RefinementType::ImpossibleFutures,

358

100

                ExplorationStrategy::BFS,

359

                true,

360

);

361

100

});

362

1

363

364

    /// Helper function to define a refinement test that can be instantiated for

365

    /// the various types.

366

///

367

    /// # Details

368

///

369

    /// Internally requests a counter example to be generated, and checks that

370

    /// the counter example is indeed a valid witness for the failure of the

371

    /// refinement check.

372

800

    fn is_refinement_test(

373

800

        dump_name: &str,

374

800

        rng: &mut StdRng,

375

800

        refinement: RefinementType,

376

800

        strategy: ExplorationStrategy,

377

800

        preprocess: bool,

378

800

) {

379

800

        let mut files = DumpFiles::new(dump_name);

380

381

800

        let spec_lts = random_lts_monolithic(rng, 1000, 5, 3);

382

800

        let impl_lts = mutate_lts(&spec_lts, rng, 100).unwrap();

383

384

800

        files.dump("spec.aut", |w| write_aut(w, &spec_lts)).unwrap();

385

800

        files.dump("impl.aut", |w| write_aut(w, &impl_lts)).unwrap();

386

387

800

        let mut timing = Timing::default();

388

800

        let (result, counter_example) = refines(

389

800

            impl_lts.clone(),

390

800

            spec_lts.clone(),

391

800

            refinement,

392

800

            strategy,

393

800

            preprocess,

394

800

            true,

395

800

            &mut timing,

396

800

);

397

398

800

        if !result {

399

257

            if let Some(ce) = counter_example {

400

257

                let formula = generate_formula(&ce);

401

257

                println!("Counter example formula: {}", formula);

402

403

257

                files

404

257

                    .dump("counter_example.mcf", |f| Ok(writeln!(f, "{}", formula)?))

405

257

                    .unwrap();

406

407

257

                let impl_pg = translate(&impl_lts, &formula).unwrap();

408

257

                let spec_pg = translate(&spec_lts, &formula).unwrap();

409

410

257

                let (impl_solution, _) = solve_zielonka(&impl_pg, false);

411

257

                let (spec_solution, _) = solve_zielonka(&spec_pg, false);

412

413

257

                assert!(

414

257

                    impl_solution[impl_pg.initial_vertex()] != spec_solution[spec_pg.initial_vertex()],

415

                    "Refinement returned false, but the counter example is not distinguishing."

416

);

417

            } else {

418

                panic!("Expected a counter example.");

419

420

543

421

800

422