Grcov report - reachability.rs

1

use log::debug;

2

use log::info;

3

use log::trace;

4

use oxidd::ManagerRef;

5

use oxidd::ldd::LDDFunction;

6

use oxidd::ldd::LDDManagerRef;

7

8

use merc_data::DataExpression;

9

use merc_io::TimeProgress;

10

use merc_utilities::MercError;

11

use merc_utilities::Timing;

12

13

use crate::LddDisplay;

14

use crate::SymbolicLPS;

15

use crate::TransitionGroup;

16

17

/// A symbolic LTS — extends [SymbolicLPS] with LTS-specific metadata.

18

pub trait SymbolicLTS: SymbolicLPS {

19

    /// Returns the LDD representing the set of states.

20

    fn states(&self) -> &LDDFunction;

21

22

    /// Returns the action labels for the LTS.

23

    fn action_labels(&self) -> &[String];

24

25

    /// Returns the possible values for each process parameter.

26

    fn parameter_values(&self) -> &[Vec<DataExpression>];

27

28

29

/// The order in which transition groups are applied during reachability.

30

///

31

/// Mirrors the `saturation` × `chaining` matrix of the mCRL2 `lpsreach` tool. Saturation and chaining

32

/// do not change the resulting reachable set, only how quickly the symbolic representation converges.

33

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

34

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

35

pub enum ExplorationStrategy {

36

    /// Plain breadth-first: every group computes successors of the original frontier.

37

    #[default]

38

    BreadthFirst,

39

    /// Successors found by earlier groups feed into later groups within the same iteration.

40

    Chaining,

41

    /// Each group is applied to a fixpoint before moving on to the next one.

42

    Saturation,

43

    /// Like [Self::Saturation], but after each group all earlier groups are re-applied to a fixpoint.

44

    SaturationChaining,

45

46

47

/// Options controlling [reachability_with_options].

48

#[derive(Clone, Copy, Debug, Default)]

49

pub struct ReachabilityOptions {

50

    /// The strategy used to apply the transition groups.

51

    pub strategy: ExplorationStrategy,

52

53

    /// Whether to detect and report deadlock states (states without outgoing transitions).

54

    pub detect_deadlocks: bool,

55

56

57

/// The result of a reachability run.

58

pub struct ReachabilityResult {

59

    /// The set of reachable states.

60

    pub states: LDDFunction,

61

62

    /// The deadlock states (reachable states with no outgoing transition), or `None` when

63

    /// [ReachabilityOptions::detect_deadlocks] was not requested.

64

    pub deadlocks: Option<LDDFunction>,

65

66

67

/// Performs reachability analysis using the given initial state and transitions.

68

///

69

/// Uses the default [ReachabilityOptions]; see [reachability_with_options] for strategies and

70

/// deadlock detection. Returns only the reachable states.

71

501

pub fn reachability<L: SymbolicLPS>(

72

501

    storage: &LDDManagerRef,

73

501

    lts: &mut L,

74

501

    timing: &Timing,

75

501

) -> Result<LDDFunction, MercError> {

76

501

    Ok(reachability_with_options(storage, lts, &ReachabilityOptions::default(), timing)?.states)

77

501

78

79

/// Performs reachability analysis using the given initial state, transitions and [ReachabilityOptions].

80

509

pub fn reachability_with_options<L: SymbolicLPS>(

81

509

    storage: &LDDManagerRef,

82

509

    lts: &mut L,

83

509

    options: &ReachabilityOptions,

84

509

    timing: &Timing,

85

509

) -> Result<ReachabilityResult, MercError> {

86

    // Created once: the learning context (and any value interning it holds) must persist across

87

    // iterations so successors learned in later iterations stay consistent with earlier ones.

88

509

    let mut context = lts.create_context();

89

509

    let mut todo = lts.initial_state().clone();

90

509

    let mut states = lts.initial_state().clone();

91

509

    let mut deadlocks: Option<LDDFunction> = if options.detect_deadlocks {

92

4

        Some(storage.with_manager_shared(|m| LDDFunction::empty_set(m))?)

93

    } else {

94

505

        None

95

};

96

509

    let mut iteration = 0;

97

98

509

    trace!("states = {}", LddDisplay::new(&states));

99

509

    let progress = TimeProgress::new(

100

23

        |(iteration, num_of_states)| {

101

23

            info!("explored {} state(s) after {} iteration(s)", num_of_states, iteration);

102

23

},

103

1,

104

);

105

106

509

    timing.measure("reachability", || {

107

2511

        while !todo.is_empty() {

108

2002

            debug!("Iteration {}: todo size = {}", iteration, todo.len());

109

110

2002

            let (todo1, step_deadlocks) = step(

111

2002

                storage,

112

2002

                lts,

113

2002

                &mut context,

114

2002

                &todo,

115

2002

                options.strategy,

116

2002

                options.detect_deadlocks,

117

2002

                timing,

118

)?;

119

120

2002

            trace!("todo1 = {}", LddDisplay::new(&todo1));

121

122

2002

            todo = todo1.minus(&states)?;

123

2002

            states = states.union(&todo)?;

124

2002

            if let Some(accumulated) = &mut deadlocks {

125

10

                *accumulated = accumulated.union(&step_deadlocks)?;

126

1992

127

2002

            if progress.is_due() {

128

23

                progress.print((iteration, states.len()));

129

1979

130

2002

            iteration += 1;

131

132

133

509

        Ok(ReachabilityResult { states, deadlocks })

134

509

})

135

509

136

137

/// Performs a single exploration step from the frontier `todo`.

138

///

139

/// Returns `(todo1, deadlocks)`: the states reachable this step (the caller subtracts the already

140

/// visited states) and, when `detect_deadlocks` is set, the subset of `todo` with no outgoing

141

/// transition in any group. The transition relations are learned on the fly.

142

2002

fn step<L: SymbolicLPS>(

143

2002

    storage: &LDDManagerRef,

144

2002

    lts: &mut L,

145

2002

    context: &mut <L::Group as TransitionGroup>::Context,

146

2002

    todo: &LDDFunction,

147

2002

    strategy: ExplorationStrategy,

148

2002

    detect_deadlocks: bool,

149

2002

    timing: &Timing,

150

2002

) -> Result<(LDDFunction, LDDFunction), MercError> {

151

2002

    let chaining = matches!(

152

2002

        strategy,

153

        ExplorationStrategy::Chaining | ExplorationStrategy::SaturationChaining

154

);

155

2002

    let saturation = matches!(

156

2002

        strategy,

157

        ExplorationStrategy::Saturation | ExplorationStrategy::SaturationChaining

158

);

159

160

2002

    let groups = lts.transition_groups_mut();

161

162

    // Potential deadlocks start as the whole frontier; a state is removed as soon as a group is found

163

    // that takes it to a successor. Only tracked when requested.

164

2002

    let mut deadlocks = if detect_deadlocks {

165

10

        todo.clone()

166

    } else {

167

1992

        storage.with_manager_shared(|m| LDDFunction::empty_set(m))?

168

};

169

170

2002

    if !saturation {

171

        // Regular breadth-first, or chaining where successors found by earlier groups feed later groups.

172

1963

        let mut todo1 = if chaining {

173

36

            todo.clone()

174

        } else {

175

1927

            storage.with_manager_shared(|m| LDDFunction::empty_set(m))?

176

};

177

178

13496

        for (i, transition) in groups.iter_mut().enumerate() {

179

13496

            trace!("Learning successors for transition group {}:", i);

180

13496

            let source = if chaining { todo1.clone() } else { todo.clone() };

181

13496

            timing.measure(&format!("learn_successors_{}", i), || {

182

13496

                transition.learn_successors(context, storage, &source)

183

13496

            })?;

184

185

13496

            let result = source.relational_product(transition.relation(), transition.meta())?;

186

13496

            todo1 = todo1.union(&result)?;

187

188

13496

            if detect_deadlocks {

189

6

                deadlocks = remove_states_with_successor(&todo1, transition, &deadlocks)?;

190

13490

191

192

193

1963

        Ok((todo1, deadlocks))

194

    } else {

195

        // Saturation: apply each group to a fixpoint before the next, optionally re-saturating earlier

196

        // groups (chaining) after every group.

197

39

        let mut todo1 = todo.clone();

198

199

844

        for i in 0..groups.len() {

200

844

            trace!("Learning successors for transition group {}:", i);

201

844

            timing.measure(&format!("learn_successors_{}", i), || {

202

844

                groups[i].learn_successors(context, storage, &todo1)

203

844

            })?;

204

205

            // Apply group i repeatedly until it no longer adds new states.

206

            loop {

207

1507

                let old = todo1.clone();

208

1507

                let result = todo1.relational_product(groups[i].relation(), groups[i].meta())?;

209

1507

                todo1 = todo1.union(&result)?;

210

1507

                if todo1 == old {

211

844

                    break;

212

663

213

214

215

844

            if detect_deadlocks {

216

4

                deadlocks = remove_states_with_successor(&todo1, &groups[i], &deadlocks)?;

217

840

218

219

            // Apply all previously learned groups repeatedly until a fixpoint.

220

844

            if chaining {

221

                loop {

222

125

                    let old = todo1.clone();

223

1742

                    for group in groups.iter().take(i + 1) {

224

1742

                        let result = todo1.relational_product(group.relation(), group.meta())?;

225

1742

                        todo1 = todo1.union(&result)?;

226

227

125

                    if todo1 == old {

228

50

                        break;

229

75

230

231

794

232

233

234

39

        Ok((todo1, deadlocks))

235

236

2002

237

238

/// Removes from `deadlocks` every state that has a `group` transition into `todo1`, i.e. every state

239

/// that is not actually a deadlock with respect to `group`. Uses the relational predecessor (the

240

/// inverse of the relational product) restricted to the current deadlock candidates.

241

10

fn remove_states_with_successor(

242

10

    todo1: &LDDFunction,

243

10

    group: &impl TransitionGroup,

244

10

    deadlocks: &LDDFunction,

245

10

) -> Result<LDDFunction, MercError> {

246

10

    let with_successor = todo1.relational_predecessor(group.relation(), group.meta(), deadlocks)?;

247

10

    Ok(deadlocks.minus(&with_successor)?)

248

10

249

250

#[cfg(test)]

251

mod test {

252

    use merc_utilities::Timing;

253

    use oxidd::ManagerRef;

254

    use oxidd::ldd::LDDFunction;

255

    use oxidd::ldd::RelationProductMeta;

256

    use oxidd::ldd::Value;

257

258

    use crate::ExplorationStrategy;

259

    use crate::ReachabilityOptions;

260

    use crate::SylvanTransitionGroup;

261

    use crate::SymbolicLPS;

262

    use crate::from_iter;

263

    use crate::reachability_with_options;

264

    use crate::read_sylvan;

265

266

    /// Explores the `anderson.4` fixture with the given strategy and returns the reachable state count.

267

4

    fn explored_count(strategy: ExplorationStrategy) -> usize {

268

4

        let ldd_manager = oxidd::ldd::new_manager(2048, 1024, 1);

269

4

        let bytes = include_bytes!("../../../../examples/ldd/anderson.4.ldd");

270

4

        let mut lts = read_sylvan(&ldd_manager, &mut &bytes[..]).expect("Loading should work correctly");

271

272

4

        let options = ReachabilityOptions {

273

4

            strategy,

274

4

            detect_deadlocks: false,

275

4

};

276

4

        reachability_with_options(&ldd_manager, &mut lts, &options, &Timing::new())

277

4

            .expect("Reachability should work correctly")

278

4

            .states

279

4

            .len()

280

4

281

282

    #[test]

283

    #[cfg_attr(miri, ignore)] // Miri is too slow

284

1

    fn test_reachability_strategies_agree() {

285

        // All strategies must compute the same reachable set, only the convergence speed differs.

286

1

        let expected = explored_count(ExplorationStrategy::BreadthFirst);

287

1

        assert_eq!(expected, explored_count(ExplorationStrategy::Chaining));

288

1

        assert_eq!(expected, explored_count(ExplorationStrategy::Saturation));

289

1

        assert_eq!(expected, explored_count(ExplorationStrategy::SaturationChaining));

290

1

291

292

    /// Minimal hand-built LTS over a single parameter with transitions `0 -> 1 -> 2`, so the only

293

    /// reachable deadlock is state `2`.

294

    struct LineLts {

295

        initial: LDDFunction,

296

        groups: Vec<SylvanTransitionGroup>,

297

298

299

    impl SymbolicLPS for LineLts {

300

        type Group = SylvanTransitionGroup;

301

302

8

        fn initial_state(&self) -> &LDDFunction {

303

8

            &self.initial

304

8

305

306

        fn transition_groups(&self) -> &[Self::Group] {

307

            &self.groups

308

309

310

10

        fn transition_groups_mut(&mut self) -> &mut [Self::Group] {

311

10

            &mut self.groups

312

10

313

314

4

        fn create_context(&self) {}

315

316

317

4

    fn line_lts(manager: &oxidd::ldd::LDDManagerRef) -> LineLts {

318

        // One read+write of parameter 0; relation short vectors place the read/write values at the

319

        // positions reported by `relation_product_meta`.

320

        let RelationProductMeta {

321

4

            meta,

322

4

            read_positions,

323

4

            write_positions,

324

4

        } = manager

325

4

            .with_manager_shared(|m| LDDFunction::relation_product_meta(m, &[0], &[0]))

326

4

            .expect("meta");

327

8

        let transition = |from: Value, to: Value| {

328

8

            let mut vector: Vec<Value> = vec![0; read_positions.len() + write_positions.len()];

329

8

            vector[read_positions[0]] = from;

330

8

            vector[write_positions[0]] = to;

331

8

            vector

332

8

};

333

334

4

        let relation = from_iter(manager, [transition(0, 1), transition(1, 2)].iter());

335

4

        let group = SylvanTransitionGroup::new(relation, meta, vec![0], vec![0]);

336

337

4

        LineLts {

338

4

            initial: from_iter(manager, std::iter::once(&vec![0])),

339

4

            groups: vec![group],

340

4

341

4

342

343

    #[test]

344

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

345

1

    fn test_reachability_detect_deadlocks() {

346

4

        for strategy in [

347

1

            ExplorationStrategy::BreadthFirst,

348

1

            ExplorationStrategy::Chaining,

349

1

            ExplorationStrategy::Saturation,

350

1

            ExplorationStrategy::SaturationChaining,

351

1

] {

352

4

            let manager = oxidd::ldd::new_manager(2048, 1024, 1);

353

4

            let mut lts = line_lts(&manager);

354

355

4

            let options = ReachabilityOptions {

356

4

                strategy,

357

4

                detect_deadlocks: true,

358

4

};

359

4

            let result = reachability_with_options(&manager, &mut lts, &options, &Timing::new())

360

4

                .expect("Reachability should work correctly");

361

362

            // States 0, 1, 2 are reachable and only state 2 has no outgoing transition.

363

4

            assert_eq!(result.states.len(), 3, "{strategy:?}");

364

4

            let deadlocks = result.deadlocks.expect("detect_deadlocks was requested");

365

4

            assert_eq!(deadlocks.len(), 1, "{strategy:?}");

366

367

1

368