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_lts::LTS;

8

use merc_lts::LabelIndex;

9

use merc_lts::LabelledTransitionSystem;

10

use merc_lts::StateIndex;

11

use rustc_hash::FxHashSet;

12

13

use crate::BlockIndex;

14

use crate::Partition;

15

use crate::quotient_lts_naive;

16

17

use super::BlockPartition;

18

use super::sort_topological;

19

use super::tau_scc_decomposition;

20

21

/// The builder used to construct the signature.

22

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

23

24

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

25

/// sets that might have unused values.

26

#[derive(Eq)]

27

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

28

29

impl<'a> Signature<'a> {

30

169659

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

31

169659

        Signature(slice)

32

169659

33

34

239687

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

35

239687

        self.0

36

239687

37

38

39

impl Signature<'_> {

40

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

41

1486

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

42

1486

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

43

2793

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

44

45

1486

        let mut self_item = self_iter.next();

46

1486

        let mut other_item = other_iter.next();

47

48

3007

        while let Some(&o) = other_item {

49

329

            match self_item {

50

1625

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

51

1296

                    // Match found, move both iterators forward

52

1296

                    self_item = self_iter.next();

53

1296

                    other_item = other_iter.next();

54

1296

55

329

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

56

225

                    // Move only self iterator forward

57

225

                    self_item = self_iter.next();

58

225

59

                _ => {

60

                    // No match found in self for o

61

174

                    return false;

62

63

64

65

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

66

1312

        true

67

1486

68

69

70

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

71

#[allow(clippy::derivable_impls)]

72

impl Default for Signature<'_> {

73

38389

    fn default() -> Self {

74

38389

        Signature(&[])

75

38389

76

77

78

impl PartialEq for Signature<'_> {

79

32994

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

80

32994

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

81

32994

82

83

84

impl Hash for Signature<'_> {

85

112671

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

86

112671

        self.as_slice().hash(state)

87

112671

88

89

90

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

91

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

92

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

93

94

95

96

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

97

3566

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

98

3566

    label == lts.num_of_labels()

99

3566

100

101

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

102

1982

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

103

1982

    LabelIndex::new(lts.num_of_labels())

104

1982

105

106

/// Returns the signature for strong bisimulation.

107

///

108

/// ```plain

109

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

110

/// ```

111

47159

pub fn strong_bisim_signature(

112

47159

    state_index: StateIndex,

113

47159

    lts: &impl LTS,

114

47159

    partition: &impl Partition,

115

47159

    builder: &mut SignatureBuilder,

116

47159

) {

117

47159

    builder.clear();

118

119

177845

    for transition in lts.outgoing_transitions(state_index) {

120

177845

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

121

177845

122

123

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

124

47159

    builder.sort_unstable();

125

47159

    builder.dedup();

126

47159

127

128

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

129

///

130

/// ```plain

131

///     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)) }

132

/// ```

133

16789

pub fn branching_bisim_signature(

134

16789

    state_index: StateIndex,

135

16789

    lts: &impl LTS,

136

16789

    partition: &impl Partition,

137

16789

    builder: &mut SignatureBuilder,

138

16789

    visited: &mut FxHashSet<StateIndex>,

139

16789

    stack: &mut Vec<StateIndex>,

140

16789

) {

141

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

142

16789

    builder.clear();

143

16789

    visited.clear();

144

145

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

146

16789

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

147

16789

    stack.push(state_index);

148

149

52072

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

150

35283

        visited.insert(inner_state_index);

151

152

73787

        for transition in lts.outgoing_transitions(inner_state_index) {

153

73787

            if lts.is_hidden_label(transition.label) {

154

27056

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

155

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

156

22937

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

157

18494

                        visited.insert(transition.to);

158

18494

                        stack.push(transition.to);

159

18494

160

4119

                } else {

161

4119

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

162

4119

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

163

4119

164

46731

            } else {

165

46731

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

166

46731

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

167

46731

168

169

170

171

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

172

16789

    builder.sort_unstable();

173

16789

    builder.dedup();

174

16789

175

176

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

177

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

178

14408

pub fn branching_bisim_signature_sorted(

179

14408

    state_index: StateIndex,

180

14408

    lts: &impl LTS,

181

14408

    partition: &impl Partition,

182

14408

    state_to_signature: &[Signature],

183

14408

    builder: &mut SignatureBuilder,

184

14408

) {

185

14408

    builder.clear();

186

187

30786

    for transition in lts.outgoing_transitions(state_index) {

188

30786

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

189

190

30786

        if partition.block_number(state_index) == to_block {

191

20448

            if lts.is_hidden_label(transition.label) {

192

10136

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

193

10136

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

194

10312

            } else {

195

10312

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

196

10312

197

10338

        } else {

198

10338

            // Visible action, add to the signature.

199

10338

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

200

10338

201

202

203

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

204

14408

    builder.sort_unstable();

205

14408

    builder.dedup();

206

14408

207

208

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

209

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

210

2381

pub fn branching_bisim_signature_inductive(

211

2381

    state_index: StateIndex,

212

2381

    lts: &impl LTS,

213

2381

    partition: &BlockPartition,

214

2381

    state_to_key: &[BlockIndex],

215

2381

    builder: &mut SignatureBuilder,

216

2381

) {

217

2381

    builder.clear();

218

219

5467

    for transition in lts.outgoing_transitions(state_index) {

220

5467

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

221

222

5467

        if partition.block_number(state_index) == to_block {

223

4094

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

224

1982

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

225

1982

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

226

2112

            } else {

227

2112

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

228

2112

229

1373

        } else {

230

1373

            // Visible action, add to the signature.

231

1373

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

232

1373

233

234

235

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

236

2381

    builder.sort_unstable();

237

2381

    builder.dedup();

238

2381

239

240

/// Computes the weak bisimulation signature.

241

///

242

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

243

5399

pub fn weak_bisim_signature_sorted(

244

5399

    state_index: StateIndex,

245

5399

    lts: &impl LTS,

246

5399

    partition: &impl Partition,

247

5399

    state_to_signature: &[Signature],

248

5399

    builder: &mut SignatureBuilder,

249

5399

) {

250

5399

    builder.clear();

251

5399

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

252

10682

    for transition in lts.outgoing_transitions(state_index) {

253

10682

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

254

255

10682

        if lts.is_hidden_label(transition.label) {

256

3311

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

257

3311

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

258

3311

        } else {

259

7371

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

260

13480

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

261

13480

                if lts.is_hidden_label(*label_after) {

262

8633

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

263

8633

264

265

266

267

268

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

269

5399

    builder.sort_unstable();

270

5399

    builder.dedup();

271

5399

272

273

/// This computes only tau signatures.

274

///

275

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

276

4224

pub fn weak_bisim_signature_sorted_taus(

277

4224

    state_index: StateIndex,

278

4224

    lts: &impl LTS,

279

4224

    partition: &impl Partition,

280

4224

    state_to_signature: &[Signature],

281

4224

    builder: &mut SignatureBuilder,

282

4224

) {

283

4224

    builder.clear();

284

4224

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

285

8476

    for transition in lts.outgoing_transitions(state_index) {

286

8476

        if lts.is_hidden_label(transition.label) {

287

2645

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

288

2645

289

2645

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

290

2645

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

291

2645

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

292

5831

293

294

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

295

4224

    builder.sort_unstable();

296

4224

    builder.dedup();

297

4224

298

299

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

300

/// sorted signature see [branching_bisim_signature_sorted].

301

600

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

302

600

    let scc_partition = tau_scc_decomposition(&lts);

303

600

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

304

600

    drop(lts);

305

306

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

307

600

    let topological_permutation = sort_topological(

308

600

        &tau_loop_free_lts,

309

22340

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

310

        true,

311

312

600

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

313

314

6138

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

315

600