Grcov report - signatures.rs

1

#![forbid(unsafe_code)]

2

3

use std::fmt;

4

use std::hash::Hash;

5

use std::hash::Hasher;

6

7

use merc_collections::BlockIndex;

8

use merc_lts::LTS;

9

use merc_lts::LabelIndex;

10

use merc_lts::LabelledTransitionSystem;

11

use merc_lts::StateIndex;

12

use rustc_hash::FxHashSet;

13

14

use super::BlockPartition;

15

use super::sort_topological;

16

use super::tau_scc_decomposition;

17

use crate::Partition;

18

use crate::quotient_lts_naive;

19

20

/// The builder used to construct the signature.

21

pub type SignatureBuilder = Vec<(LabelIndex, BlockIndex)>;

22

23

/// The type of a signature. We use sorted vectors to avoid the overhead of hash

24

/// sets that might have unused values.

25

#[derive(Eq)]

26

pub struct Signature<'a>(&'a [(LabelIndex, BlockIndex)]);

27

28

impl<'a> Signature<'a> {

29

129284

    pub fn new(slice: &'a [(LabelIndex, BlockIndex)]) -> Signature<'a> {

30

129284

        Signature(slice)

31

129284

32

33

213470

    pub fn as_slice(&self) -> &[(LabelIndex, BlockIndex)] {

34

213470

        self.0

35

213470

36

37

38

impl Signature<'_> {

39

    // Check if other is a subset of self, excluding a specific element

40

4800

    pub fn is_subset_of(&self, other: &[(LabelIndex, BlockIndex)], exclude: (LabelIndex, BlockIndex)) -> bool {

41

4800

        let mut self_iter = self.as_slice().iter();

42

11166

        let mut other_iter = other.iter().filter(|&&x| x != exclude);

43

44

4800

        let mut self_item = self_iter.next();

45

4800

        let mut other_item = other_iter.next();

46

47

14990

        while let Some(&o) = other_item {

48

4977

            match self_item {

49

11226

                Some(&s) if s == o => {

50

6249

                    // Match found, move both iterators forward

51

6249

                    self_item = self_iter.next();

52

6249

                    other_item = other_iter.next();

53

6249

54

4977

                Some(&s) if s < o => {

55

3941

                    // Move only self iterator forward

56

3941

                    self_item = self_iter.next();

57

3941

58

                _ => {

59

                    // No match found in self for o

60

1892

                    return false;

61

62

63

64

        // If we finished self_iter without returning false, self is a subset

65

2908

        true

66

4800

67

68

69

// This default implementation is actually different from the one generated by derive(Default).

70

#[allow(clippy::derivable_impls)]

71

impl Default for Signature<'_> {

72

37227

    fn default() -> Self {

73

37227

        Signature(&[])

74

37227

75

76

77

impl PartialEq for Signature<'_> {

78

24213

    fn eq(&self, other: &Self) -> bool {

79

24213

        self.as_slice() == other.as_slice()

80

24213

81

82

83

impl Hash for Signature<'_> {

84

62478

    fn hash<H: Hasher>(&self, state: &mut H) {

85

62478

        self.as_slice().hash(state)

86

62478

87

88

89

impl fmt::Debug for Signature<'_> {

90

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

91

        f.debug_list().entries(self.as_slice().iter()).finish()

92

93

94

95

/// Returns true if the label is the special tau_hat label for the given LTS.

96

18806

pub fn is_tau_hat(label: LabelIndex, lts: &impl LTS) -> bool {

97

18806

    label == lts.num_of_labels()

98

18806

99

100

/// Returns a special label that is not in the set of labels.

101

5949

fn tau_hat(lts: &impl LTS) -> LabelIndex {

102

5949

    LabelIndex::new(lts.num_of_labels())

103

5949

104

105

/// Returns the signature for strong bisimulation.

106

///

107

/// ```plain

108

///     sig(s, pi) = { (a, pi(t)) | s -a-> t in T }

109

/// ```

110

14987

pub fn strong_bisim_signature(

111

14987

    state_index: StateIndex,

112

14987

    lts: &impl LTS,

113

14987

    partition: &impl Partition,

114

14987

    builder: &mut SignatureBuilder,

115

14987

) {

116

14987

    builder.clear();

117

118

31488

    for transition in lts.outgoing_transitions(state_index) {

119

31488

        builder.push((transition.label, partition.block_number(transition.to)));

120

31488

121

122

    // Compute the flat signature, which has Hash and is more compact.

123

14987

    builder.sort_unstable();

124

14987

    builder.dedup();

125

14987

126

127

/// Returns the branching bisimulation signature for branching bisimulation.

128

///

129

/// ```plain

130

///     sig(s, pi) = { (a, pi(t)) | s -tau-> s1 -> ... s_n -a-> t in T && pi(s) = pi(s_i) && ((a != tau) || pi(s) != pi(t)) }

131

/// ```

132

18251

pub fn branching_bisim_signature(

133

18251

    state_index: StateIndex,

134

18251

    lts: &impl LTS,

135

18251

    partition: &impl Partition,

136

18251

    builder: &mut SignatureBuilder,

137

18251

    visited: &mut FxHashSet<StateIndex>,

138

18251

    stack: &mut Vec<StateIndex>,

139

18251

) {

140

    // Clear the builders and the list of visited states.

141

18251

    builder.clear();

142

18251

    visited.clear();

143

144

    // A stack used for depth first search of tau paths.

145

18251

    debug_assert!(stack.is_empty(), "The stack should be empty");

146

18251

    stack.push(state_index);

147

148

58686

    while let Some(inner_state_index) = stack.pop() {

149

40435

        visited.insert(inner_state_index);

150

151

74968

        for transition in lts.outgoing_transitions(inner_state_index) {

152

74968

            if lts.is_hidden_label(transition.label) {

153

35488

                if partition.block_number(state_index) == partition.block_number(transition.to) {

154

                    // Explore the outgoing state as well, still tau path in same block

155

28052

                    if !visited.contains(&transition.to) {

156

22184

                        visited.insert(transition.to);

157

22184

                        stack.push(transition.to);

158

22184

159

7436

                } else {

160

7436

                    //  pi(s) != pi(t)

161

7436

                    builder.push((transition.label, partition.block_number(transition.to)));

162

7436

163

39480

            } else {

164

39480

                // (a != tau) This is a visible action only reachable from tau paths with equal signatures.

165

39480

                builder.push((transition.label, partition.block_number(transition.to)));

166

39480

167

168

169

170

    // Compute the flat signature, which has Hash and is more compact.

171

18251

    builder.sort_unstable();

172

18251

    builder.dedup();

173

18251

174

175

/// The same as [branching_bisim_signature], but assuming that the input LTS is

176

/// topological sorted, and contains no tau-cycles.

177

16204

pub fn branching_bisim_signature_sorted(

178

16204

    state_index: StateIndex,

179

16204

    lts: &impl LTS,

180

16204

    partition: &impl Partition,

181

16204

    state_to_signature: &[Signature],

182

16204

    builder: &mut SignatureBuilder,

183

16204

) {

184

16204

    builder.clear();

185

186

31314

    for transition in lts.outgoing_transitions(state_index) {

187

31314

        let to_block = partition.block_number(transition.to);

188

189

31314

        if partition.block_number(state_index) == to_block {

190

18887

            if lts.is_hidden_label(transition.label) {

191

11257

                // Inert tau transition, take signature from the outgoing tau-transition.

192

11257

                builder.extend(state_to_signature[transition.to].as_slice());

193

11257

            } else {

194

7630

                builder.push((transition.label, to_block));

195

7630

196

12427

        } else {

197

12427

            // Visible action, add to the signature.

198

12427

            builder.push((transition.label, to_block));

199

12427

200

201

202

    // Compute the flat signature, which has Hash and is more compact.

203

16204

    builder.sort_unstable();

204

16204

    builder.dedup();

205

16204

206

207

/// The inductive version of [branching_bisim_signature_sorted]. Assumes that

208

/// the input LTS has no tau-cycles, and is topologically sorted.

209

2047

pub fn branching_bisim_signature_inductive(

210

2047

    state_index: StateIndex,

211

2047

    lts: &impl LTS,

212

2047

    partition: &BlockPartition,

213

2047

    state_to_key: &[BlockIndex],

214

2047

    builder: &mut SignatureBuilder,

215

2047

) {

216

2047

    builder.clear();

217

218

4366

    for transition in lts.outgoing_transitions(state_index) {

219

4366

        let to_block = partition.block_number(transition.to);

220

221

4366

        if partition.block_number(state_index) == to_block {

222

3280

            if lts.is_hidden_label(transition.label) && partition.is_element_marked(transition.to) {

223

1719

                // Inert tau transition, take signature from the outgoing tau-transition.

224

1719

                builder.push((tau_hat(lts), state_to_key[transition.to]));

225

1719

            } else {

226

1561

                builder.push((transition.label, to_block));

227

1561

228

1086

        } else {

229

1086

            // Visible action, add to the signature.

230

1086

            builder.push((transition.label, to_block));

231

1086

232

233

234

    // Compute the flat signature, which has Hash and is more compact.

235

2047

    builder.sort_unstable();

236

2047

    builder.dedup();

237

2047

238

239

240

/// Computes the weak bisimulation presignature.

241

///

242

/// The input lts must contain no tau-cycles.

243

5034

pub fn weak_bisim_presignature_sorted(

244

5034

    state_index: StateIndex,

245

5034

    lts: &impl LTS,

246

5034

    partition: &impl Partition,

247

5034

    state_to_taus: &[Signature],

248

5034

    state_to_key: &[Option<usize>],

249

5034

    builder: &mut SignatureBuilder,

250

5034

) {

251

5034

    builder.clear();

252

5034

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

253

10940

    for transition in lts.outgoing_transitions(state_index) {

254

10940

        if lts.is_hidden_label(transition.label) {

255

4230

            // Inert tau transition, take signature from the outgoing tau-transition.

256

4230

            builder.push((tau_hat(lts), BlockIndex::new(state_to_key[transition.to].unwrap())));

257

4230

        } else {

258

9103

            for (label_after, color) in state_to_taus[transition.to].as_slice() {

259

9103

                if lts.is_hidden_label(*label_after) {

260

9103

                    builder.push((transition.label, *color));

261

9103

262

263

264

265

266

    // Compute the flat signature, which has Hash and is more compact.

267

5034

    builder.sort_unstable();

268

5034

    builder.dedup();

269

5034

270

271

/// Computes the weak bisimulation signature.

272

///

273

/// The input lts must contain no tau-cycles.

274

3132

pub fn weak_bisim_signature_sorted_full(

275

3132

    state_index: StateIndex,

276

3132

    lts: &impl LTS,

277

3132

    partition: &impl Partition,

278

3132

    state_to_taus: &[Signature],

279

3132

    state_to_signature: &[Option<usize>],

280

3132

    key_to_signature: &[Signature],

281

3132

    builder: &mut SignatureBuilder,

282

3132

) {

283

3132

    builder.clear();

284

3132

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

285

6554

    for transition in lts.outgoing_transitions(state_index) {

286

6554

        let to_block = partition.block_number(transition.to);

287

288

6554

        if lts.is_hidden_label(transition.label) {

289

1795

            // Inert tau transition, take signature from the outgoing tau-transition.

290

1795

            builder.extend(key_to_signature[state_to_signature[transition.to].unwrap()].as_slice());

291

1795

        } else {

292

4759

            builder.push((transition.label, to_block));

293

6776

            for (label_after, color) in state_to_taus[transition.to].as_slice() {

294

6776

                if lts.is_hidden_label(*label_after) {

295

6776

                    builder.push((transition.label, *color));

296

6776

297

298

299

300

301

    // Compute the flat signature, which has Hash and is more compact.

302

3132

    builder.sort_unstable();

303

3132

    builder.dedup();

304

3132

305

306

307

/// Computes the weak bisimulation signature.

308

///

309

/// The input lts must contain no tau-cycles.

310

10182

pub fn weak_bisim_signature_sorted(

311

10182

    state_index: StateIndex,

312

10182

    lts: &impl LTS,

313

10182

    partition: &impl Partition,

314

10182

    state_to_signature: &[Signature],

315

10182

    builder: &mut SignatureBuilder,

316

10182

) {

317

10182

    builder.clear();

318

10182

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

319

21144

    for transition in lts.outgoing_transitions(state_index) {

320

21144

        let to_block = partition.block_number(transition.to);

321

322

21144

        if lts.is_hidden_label(transition.label) {

323

9162

            // Inert tau transition, take signature from the outgoing tau-transition.

324

9162

            builder.extend(state_to_signature[transition.to].as_slice());

325

9162

        } else {

326

11982

            builder.push((transition.label, to_block));

327

25566

            for (label_after, color) in state_to_signature[transition.to].as_slice() {

328

25566

                if lts.is_hidden_label(*label_after) {

329

16376

                    builder.push((transition.label, *color));

330

16376

331

332

333

334

335

    // Compute the flat signature, which has Hash and is more compact.

336

10182

    builder.sort_unstable();

337

10182

    builder.dedup();

338

10182

339

340

/// This computes only tau signatures.

341

///

342

/// The input lts must contain no tau-cycles.

343

13142

pub fn weak_bisim_signature_sorted_taus(

344

13142

    state_index: StateIndex,

345

13142

    lts: &impl LTS,

346

13142

    partition: &impl Partition,

347

13142

    state_to_taus: &[Signature],

348

13142

    builder: &mut SignatureBuilder,

349

13142

) {

350

13142

    builder.clear();

351

13142

    builder.push((LabelIndex::new(0), partition.block_number(state_index))); // Add the inert tau transition to itself.

352

28077

    for transition in lts.outgoing_transitions(state_index) {

353

28077

        if lts.is_hidden_label(transition.label) {

354

11623

            // Inert tau transition, take signature from the outgoing tau-transition.

355

11623

            builder.extend(state_to_taus[transition.to].as_slice());

356

16454

357

358

    // Compute the flat signature, which has Hash and is more compact.

359

13142

    builder.sort_unstable();

360

13142

    builder.dedup();

361

13142

362

363

/// Perform the preprocessing necessary for branching bisimulation with the

364

/// sorted signature [branching_bisim_signature_sorted] and

365

/// [branching_bisim_signature_inductive].

366

///

367

/// # Details

368

///

369

/// Computes the tau-SCC decomposition of the LTS, quotients the LTS modulo the

370

/// tau-SCCs, and then sorts the states according to a reverse topological order

371

/// of the tau transitions, i.e., if there is a tau-transition from state s to

372

/// state t, then t appears before s in the ordering.

373

900

pub fn tau_loop_elimination_and_reorder<L: LTS>(lts: L) -> LabelledTransitionSystem<L::Label> {

374

900

    let scc_partition = tau_scc_decomposition(&lts);

375

900

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

376

900

    drop(lts);

377

378

    // Sort the states according to the topological order of the tau transitions.

379

900

    let topological_permutation = sort_topological(

380

900

        &tau_loop_free_lts,

381

30216

        |label_index, _| tau_loop_free_lts.is_hidden_label(label_index),

382

        true,

383

384

900

    .expect("After quotienting, the LTS should not contain cycles");

385

386

8907

    LabelledTransitionSystem::new_from_permutation(tau_loop_free_lts, |i| topological_permutation[i])

387

900