Grcov report - quotient.rs

1

#![forbid(unsafe_code)]

2

3

use merc_collections::BlockIndex;

4

use merc_lts::LTS;

5

use merc_lts::LabelledTransitionSystem;

6

use merc_lts::LtsBuilderFast;

7

use merc_lts::StateIndex;

8

9

use crate::BlockPartition;

10

use crate::Partition;

11

12

/// Returns a new LTS based on the given partition.

13

///

14

/// The naive version will add the transitions of all states in the block to the quotient LTS.

15

3700

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

16

3700

    lts: &L,

17

3700

    partition: &P,

18

3700

    eliminate_tau_loops: bool,

19

3700

) -> LabelledTransitionSystem<L::Label> {

20

    // Introduce the transitions based on the block numbers, the number of blocks is a decent approximation for the number of transitions.

21

3700

    let mut builder = LtsBuilderFast::with_capacity(

22

3700

        lts.labels().into(),

23

3700

        Vec::new(),

24

3700

        partition.num_of_blocks(), // We expect one transition per state.

25

);

26

27

549747

    for state_index in lts.iter_states() {

28

605322

        for transition in lts.outgoing_transitions(state_index) {

29

605322

            let block = partition.block_number(state_index);

30

605322

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

31

32

            // If we eliminate tau loops then check if the 'to' and 'from' end up in the same block

33

605322

            if !(eliminate_tau_loops && lts.is_hidden_label(transition.label) && block == to_block) {

34

598068

                debug_assert!(

35

598068

                    partition.block_number(state_index) < partition.num_of_blocks(),

36

                    "Quotienting assumes that the block numbers do not exceed the number of blocks"

37

);

38

39

598068

                builder.add_transition(

40

598068

                    StateIndex::new(block.value()),

41

598068

                    &lts.labels()[transition.label],

42

598068

                    StateIndex::new(to_block.value()),

43

);

44

7254

45

46

47

48

3700

    builder.require_num_of_states(partition.num_of_blocks());

49

3700

    builder.finish(

50

3700

        StateIndex::new(partition.block_number(lts.initial_state_index()).value()),

51

        true,

52

53

3700

54

55

/// Optimised implementation for block partitions.

56

///

57

/// Chooses a single state in the block as representative. If `BRANCHING` then the

58

/// chosen state is a bottom state. For `BRANCHING` it assumes that the input LTS

59

/// is non-divergent.

60

314

pub fn quotient_lts_block<L: LTS, const BRANCHING: bool>(

61

314

    lts: &L,

62

314

    partition: &BlockPartition,

63

314

) -> LabelledTransitionSystem<L::Label> {

64

314

    let mut builder = LtsBuilderFast::new(lts.labels().into(), Vec::new());

65

66

90851

    for block in (0..partition.num_of_blocks()).map(BlockIndex::new) {

67

        // Pick any state in the block

68

90851

        let mut candidate = if let Some(state) = partition.iter_block(block).next() {

69

90851

            state

70

        } else {

71

            panic!("Blocks in the partition should not be empty {}", block);

72

};

73

74

90851

        if BRANCHING {

75

            // traverse any outgoing transition to find a bottom state.

76

            'outer: loop {

77

56293

                if let Some(trans) = lts

78

56293

                    .outgoing_transitions(candidate)

79

94563

                    .find(|trans| lts.is_hidden_label(trans.label) && partition.block_number(trans.to) == block)

80

81

308

                    debug_assert!(

82

308

                        !diverges(lts, candidate),

83

                        "The states of the given LTS should be non-divergent."

84

);

85

308

                    candidate = trans.to;

86

308

                    continue 'outer;

87

55985

88

89

                // No outgoing tau transition to the same block, so we found a bottom state.

90

55985

                break;

91

92

34866

93

94

        // Add all transitions from the representative state (or the bottom state if BRANCHING) to the quotient LTS.

95

150720

        for transition in lts.outgoing_transitions(candidate) {

96

150720

            if BRANCHING {

97

94251

                debug_assert!(

98

94251

                    !(lts.is_hidden_label(transition.label) && partition.block_number(transition.to) == block),

99

                    "The representative {} is not bottom state",

100

                    candidate

101

);

102

56469

103

104

150720

            builder.add_transition(

105

150720

                StateIndex::new(*block),

106

150720

                &lts.labels()[transition.label],

107

150720

                StateIndex::new(*partition.block_number(transition.to)),

108

);

109

110

111

112

314

    builder.require_num_of_states(partition.num_of_blocks());

113

314

    builder.finish(

114

314

        StateIndex::new(partition.block_number(lts.initial_state_index()).value()),

115

        true,

116

117

314

118

119

/// Returns true iff the given state diverges, i.e., it can perform an infinite

120

/// sequence of tau transitions.

121

///

122

/// Uses iterative DFS with 3-color marking to correctly detect cycles in any LTS,

123

/// including graphs where the same state is reachable via multiple paths (diamonds).

124

401

pub fn diverges<L: LTS>(lts: &L, state: StateIndex) -> bool {

125

401

    let mut color = vec![DfsColor::White; lts.num_of_states()];

126

    // Each stack entry is (node, backtrack): when backtrack is true the node is being finalised.

127

401

    let mut stack = vec![(state, false)];

128

129

2368

    while let Some((current, backtrack)) = stack.pop() {

130

1967

        if backtrack {

131

            // All descendants have been processed; mark the node as fully done.

132

983

            color[current] = DfsColor::Black;

133

983

            continue;

134

984

135

136

984

        match color[current] {

137

            DfsColor::Gray => return true,  // Back-edge: current is still on the DFS path → cycle found.

138

1

            DfsColor::Black => continue,    // Already fully processed; no new information.

139

983

            DfsColor::White => {}

140

141

142

        // Mark gray (on the current DFS path) and schedule finalisation.

143

983

        color[current] = DfsColor::Gray;

144

983

        stack.push((current, true));

145

146

1250

        for transition in lts.outgoing_transitions(current) {

147

1250

            if lts.is_hidden_label(transition.label) {

148

583

                stack.push((transition.to, false));

149

667

150

151

152

153

    // All reachable tau-transitions explored without finding a back-edge.

154

401

    false

155

401

156

157

/// DFS node colour used by [`diverges`].

158

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

159

enum DfsColor {

160

    /// Not yet visited.

161

    #[default]

162

    White,

163

    /// On the current DFS path (in the recursion stack).

164

    Gray,

165

    /// All descendants fully processed.

166

    Black,

167

168

169

#[cfg(test)]

170

mod tests {

171

    use merc_io::DumpFiles;

172

    use merc_lts::random_lts;

173

    use merc_lts::write_aut;

174

    use merc_utilities::Timing;

175

    use merc_utilities::random_test;

176

    use rand::rngs::StdRng;

177

178

    use crate::Equivalence;

179

    use crate::compare_lts;

180

    use crate::reduce_lts;

181

182

    /// Generates a random LTS, reduces it under `equivalence`, and asserts

183

    /// that the original and reduced LTS are equivalent.

184

800

    fn check_quotient_equivalence(rng: &mut StdRng, equivalence: Equivalence, test_name: &str) {

185

800

        let mut timing = Timing::new();

186

800

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

187

188

800

        let lts = random_lts(rng, 20, 10, 2);

189

190

800

        files.dump("input.aut", |w| write_aut(w, &lts)).unwrap();

191

192

800

        let reduced = reduce_lts(lts.clone(), equivalence, false, &mut timing);

193

800

        files.dump("quotient.aut", |w| write_aut(w, &reduced)).unwrap();

194

195

800

        assert!(

196

800

            compare_lts(equivalence, lts, reduced, false, &mut timing),

197

            "Quotient is not equivalent under {equivalence:?}",

198

);

199

800

200

201

    #[test]

202

1

    fn test_random_strong_bisim_quotient() {

203

100

        random_test(100, |rng| {

204

100

            check_quotient_equivalence(rng, Equivalence::StrongBisim, "test_random_strong_bisim_quotient");

205

100

});

206

1

207

208

    #[test]

209

1

    fn test_random_strong_bisim_naive_quotient() {

210

100

        random_test(100, |rng| {

211

100

            check_quotient_equivalence(

212

100

                rng,

213

100

                Equivalence::StrongBisimNaive,

214

100

                "test_random_strong_bisim_naive_quotient",

215

);

216

100

});

217

1

218

219

    #[test]

220

1

    fn test_random_branching_bisim_quotient() {

221

100

        random_test(100, |rng| {

222

100

            check_quotient_equivalence(rng, Equivalence::BranchingBisim, "test_random_branching_bisim_quotient");

223

100

});

224

1

225

226

    #[test]

227

1

    fn test_random_branching_bisim_naive_quotient() {

228

100

        random_test(100, |rng| {

229

100

            check_quotient_equivalence(

230

100

                rng,

231

100

                Equivalence::BranchingBisimNaive,

232

100

                "test_random_branching_bisim_naive_quotient",

233

);

234

100

});

235

1

236

237

    #[test]

238

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

239

1

    fn test_random_weak_bisim_quotient() {

240

100

        random_test(100, |rng| {

241

100

            check_quotient_equivalence(rng, Equivalence::WeakBisim, "test_random_weak_bisim_quotient");

242

100

});

243

1

244

245

    #[test]

246

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

247

1

    fn test_random_weak_bisim_parallel_quotient() {

248

100

        random_test(100, |rng| {

249

100

            check_quotient_equivalence(

250

100

                rng,

251

100

                Equivalence::WeakBisimParallel,

252

100

                "test_random_weak_bisim_parallel_quotient",

253

);

254

100

});

255

1

256

257

    #[test]

258

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

259

1

    fn test_random_weak_bisim_sigref_quotient() {

260

100

        random_test(100, |rng| {

261

100

            check_quotient_equivalence(

262

100

                rng,

263

100

                Equivalence::WeakBisimSigref,

264

100

                "test_random_weak_bisim_sigref_quotient",

265

);

266

100

});

267

1

268

269

    #[test]

270

1

    fn test_random_weak_bisim_sigref_naive_quotient() {

271

100

        random_test(100, |rng| {

272

100

            check_quotient_equivalence(

273

100

                rng,

274

100

                Equivalence::WeakBisimSigrefNaive,

275

100

                "test_random_weak_bisim_sigref_naive_quotient",

276

);

277

100

});

278

1

279