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

2558668

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

30

2558668

        Signature(slice)

31

2558668

32

33

4051309

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

34

4051309

        self.0

35

4051309

36

37

38

impl Signature<'_> {

39

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

40

129882

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

41

129882

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

42

176448

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

43

44

129882

        let mut self_item = self_iter.next();

45

129882

        let mut other_item = other_iter.next();

46

47

216629

        while let Some(&o) = other_item {

48

68157

            match self_item {

49

110281

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

50

42124

                    // Match found, move both iterators forward

51

42124

                    self_item = self_iter.next();

52

42124

                    other_item = other_iter.next();

53

42124

54

68157

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

55

44623

                    // Move only self iterator forward

56

44623

                    self_item = self_iter.next();

57

44623

58

                _ => {

59

                    // No match found in self for o

60

59299

                    return false;

61

62

63

64

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

65

70583

        true

66

129882

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

66127

    fn default() -> Self {

73

66127

        Signature(&[])

74

66127

75

76

77

impl PartialEq for Signature<'_> {

78

800464

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

79

800464

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

80

800464

81

82

83

impl Hash for Signature<'_> {

84

1380128

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

85

1380128

        self.as_slice().hash(state)

86

1380128

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

1279343

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

97

1279343

    label == lts.num_of_labels()

98

1279343

99

100

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

101

133119

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

102

133119

    LabelIndex::new(lts.num_of_labels())

103

133119

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

409834

pub fn strong_bisim_signature<L: LTS, P: Partition>(

111

409834

    state_index: StateIndex,

112

409834

    lts: &L,

113

409834

    partition: &P,

114

409834

    builder: &mut SignatureBuilder,

115

409834

) {

116

409834

    builder.clear();

117

118

572099

    for transition in lts.outgoing_transitions(state_index) {

119

572099

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

120

572099

121

122

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

123

409834

    builder.sort_unstable();

124

409834

    builder.dedup();

125

409834

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

721702

pub fn branching_bisim_signature<L: LTS, P: Partition>(

133

721702

    state_index: StateIndex,

134

721702

    lts: &L,

135

721702

    partition: &P,

136

721702

    builder: &mut SignatureBuilder,

137

721702

    visited: &mut FxHashSet<StateIndex>,

138

721702

    stack: &mut Vec<StateIndex>,

139

721702

) {

140

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

141

721702

    builder.clear();

142

721702

    visited.clear();

143

144

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

145

721702

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

146

721702

    stack.push(state_index);

147

148

1601320

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

149

879618

        visited.insert(inner_state_index);

150

151

1119876

        for transition in lts.outgoing_transitions(inner_state_index) {

152

1119876

            if lts.is_hidden_label(transition.label) {

153

229735

                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

162284

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

156

157916

                        visited.insert(transition.to);

157

157916

                        stack.push(transition.to);

158

157916

159

67451

                } else {

160

67451

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

161

67451

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

162

67451

163

890141

            } else {

164

890141

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

165

890141

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

166

890141

167

168

169

170

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

171

721702

    builder.sort_unstable();

172

721702

    builder.dedup();

173

721702

174

175

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

176

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

177

22511

pub fn branching_bisim_signature_sorted<L: LTS, P: Partition>(

178

22511

    state_index: StateIndex,

179

22511

    lts: &L,

180

22511

    partition: &P,

181

22511

    state_to_signature: &[Signature],

182

22511

    builder: &mut SignatureBuilder,

183

22511

) {

184

22511

    builder.clear();

185

186

41661

    for transition in lts.outgoing_transitions(state_index) {

187

41661

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

188

189

41661

        if partition.block_number(state_index) == to_block {

190

24269

            if lts.is_hidden_label(transition.label) {

191

12868

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

192

12868

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

193

12868

            } else {

194

11401

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

195

11401

196

17392

        } else {

197

17392

            // Visible action, add to the signature.

198

17392

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

199

17392

200

201

202

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

203

22511

    builder.sort_unstable();

204

22511

    builder.dedup();

205

22511

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

699191

pub fn branching_bisim_signature_inductive<L: LTS>(

210

699191

    state_index: StateIndex,

211

699191

    lts: &L,

212

699191

    partition: &BlockPartition,

213

699191

    state_to_key: &[BlockIndex],

214

699191

    builder: &mut SignatureBuilder,

215

699191

) {

216

699191

    builder.clear();

217

218

877122

    for transition in lts.outgoing_transitions(state_index) {

219

877122

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

220

221

877122

        if partition.block_number(state_index) == to_block {

222

457974

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

223

112042

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

224

112042

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

225

345932

            } else {

226

345932

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

227

345932

228

419148

        } else {

229

419148

            // Visible action, add to the signature.

230

419148

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

231

419148

232

233

234

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

235

699191

    builder.sort_unstable();

236

699191

    builder.dedup();

237

699191

238

239

/// Computes the weak bisimulation presignature.

240

///

241

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

242

33811

pub fn weak_bisim_presignature_sorted<L: LTS, P: Partition>(

243

33811

    state_index: StateIndex,

244

33811

    lts: &L,

245

33811

    partition: &P,

246

33811

    state_to_taus: &[Signature],

247

33811

    state_to_key: &[Option<usize>],

248

33811

    builder: &mut SignatureBuilder,

249

33811

) {

250

33811

    builder.clear();

251

33811

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

252

76005

    for transition in lts.outgoing_transitions(state_index) {

253

76005

        if lts.is_hidden_label(transition.label) {

254

21077

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

255

21077

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

256

21077

        } else {

257

69097

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

258

69097

                if lts.is_hidden_label(*label_after) {

259

69097

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

260

69097

261

262

263

264

265

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

266

33811

    builder.sort_unstable();

267

33811

    builder.dedup();

268

33811

269

270

/// Computes the weak bisimulation signature.

271

///

272

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

273

24697

pub fn weak_bisim_signature_sorted_full<L: LTS, P: Partition>(

274

24697

    state_index: StateIndex,

275

24697

    lts: &L,

276

24697

    partition: &P,

277

24697

    state_to_taus: &[Signature],

278

24697

    state_to_signature: &[Option<usize>],

279

24697

    key_to_signature: &[Signature],

280

24697

    builder: &mut SignatureBuilder,

281

24697

) {

282

24697

    builder.clear();

283

24697

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

284

54437

    for transition in lts.outgoing_transitions(state_index) {

285

54437

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

286

287

54437

        if lts.is_hidden_label(transition.label) {

288

10395

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

289

10395

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

290

10395

        } else {

291

44042

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

292

56352

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

293

56352

                if lts.is_hidden_label(*label_after) {

294

56352

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

295

56352

296

297

298

299

300

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

301

24697

    builder.sort_unstable();

302

24697

    builder.dedup();

303

24697

304

305

/// Computes the weak bisimulation signature.

306

///

307

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

308

12554

pub fn weak_bisim_signature_sorted<L: LTS, P: Partition>(

309

12554

    state_index: StateIndex,

310

12554

    lts: &L,

311

12554

    partition: &P,

312

12554

    state_to_signature: &[Signature],

313

12554

    builder: &mut SignatureBuilder,

314

12554

) {

315

12554

    builder.clear();

316

12554

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

317

21125

    for transition in lts.outgoing_transitions(state_index) {

318

21125

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

319

320

21125

        if lts.is_hidden_label(transition.label) {

321

8626

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

322

8626

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

323

8626

        } else {

324

12499

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

325

19638

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

326

19638

                if lts.is_hidden_label(*label_after) {

327

14332

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

328

14332

329

330

331

332

333

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

334

12554

    builder.sort_unstable();

335

12554

    builder.dedup();

336

12554

337

338

/// This computes only tau signatures.

339

///

340

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

341

43301

pub fn weak_bisim_signature_sorted_taus<L: LTS, P: Partition>(

342

43301

    state_index: StateIndex,

343

43301

    lts: &L,

344

43301

    partition: &P,

345

43301

    state_to_taus: &[Signature],

346

43301

    builder: &mut SignatureBuilder,

347

43301

) {

348

43301

    builder.clear();

349

43301

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

350

92311

    for transition in lts.outgoing_transitions(state_index) {

351

92311

        if lts.is_hidden_label(transition.label) {

352

27785

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

353

27785

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

354

64526

355

356

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

357

43301

    builder.sort_unstable();

358

43301

    builder.dedup();

359

43301

360

361

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

362

/// sorted signature [branching_bisim_signature_sorted] and

363

/// [branching_bisim_signature_inductive].

364

///

365

/// # Details

366

///

367

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

368

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

369

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

370

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

371

///

372

/// Returns the state of the preprocessed LTS corresponding to the given state.

373

2500

pub fn tau_loop_elimination_and_reorder<L: LTS>(

374

2500

    lts: L,

375

2500

    state: StateIndex,

376

2500

) -> (LabelledTransitionSystem<L::Label>, StateIndex) {

377

2500

    let scc_partition = tau_scc_decomposition(&lts);

378

2500

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

379

2500

    let mapped_state = StateIndex::new(*scc_partition.block_number(state));

380

2500

    drop(lts);

381

2500

    drop(scc_partition);

382

383

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

384

2500

    let topological_permutation = sort_topological(

385

2500

        &tau_loop_free_lts,

386

922032

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

387

        true,

388

389

2500

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

390

391

392

893718

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

393

2500

        topological_permutation[mapped_state],

394

395

2500