Grcov report - weak_bisimulation.rs

1

//! Authors: Maurice Laveaux, Eduardo Costa Martins

2

//!

3

//! Implements the weak bisimulation algorithm by Eduardo Costa Martins.

4

#![forbid(unsafe_code)]

5

6

use bitvec::bitvec;

7

use bitvec::order::Lsb0;

8

9

use bitvec::vec::BitVec;

10

use log::info;

11

use log::trace;

12

use merc_collections::BlockIndex;

13

use merc_io::TimeProgress;

14

use merc_lts::IncomingTransitions;

15

use merc_lts::LTS;

16

use merc_lts::LabelIndex;

17

use merc_lts::LabelledTransitionSystem;

18

use merc_utilities::Timing;

19

20

use crate::Equivalence;

21

use crate::SimpleBlockPartition;

22

use crate::tau_loop_elimination_and_reorder;

23

use crate::reduce_lts;

24

25

/// Type alias because we use bitvec for marking states

26

type BitArray = BitVec<u64, Lsb0>;

27

28

/// Apply weak bisimulation reduction

29

///

30

/// # Details

31

///

32

/// The `preprocess` flag indicates whether to preprocess the LTS using

33

/// branching bisimulation.

34

100

pub fn weak_bisimulation<L: LTS>(

35

100

    lts: L,

36

100

    preprocess: bool,

37

100

    timing: &Timing,

38

100

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

39

    // Preprocess the LTS if desired.

40

100

    if preprocess {

41

        let lts = timing.measure("preprocess", || reduce_lts(lts, Equivalence::BranchingBisim, true, timing));

42

        weak_bisimulation_impl(lts, timing)

43

    } else {

44

100

        weak_bisimulation_impl(lts, timing)

45

46

100

47

48

/// Core weak bisimulation algorithm implementation.

49

100

fn weak_bisimulation_impl<L: LTS>(

50

100

    lts: L,

51

100

    timing: &Timing,

52

100

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

53

100

    let tau_loop_free_lts = timing.measure("preprocess", || tau_loop_elimination_and_reorder(lts));

54

55

100

    timing.measure("reduction", || {

56

100

        let mut blocks = SimpleBlockPartition::new(tau_loop_free_lts.num_of_states());

57

58

100

        let mut act_mark = bitvec![u64, Lsb0; 0; tau_loop_free_lts.num_of_states()];

59

100

        let mut tau_mark = bitvec![u64, Lsb0; 0; tau_loop_free_lts.num_of_states()];

60

61

100

        let incoming = IncomingTransitions::new(&tau_loop_free_lts);

62

63

100

        let progress = TimeProgress::new(

64

            |num_of_blocks: usize| {

65

                info!("Found {} blocks...", num_of_blocks);

66

},

67

1,

68

);

69

70

        loop {

71

260

            let mut stable = true;

72

441

            for block_index in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

73

441

                progress.print(blocks.num_of_blocks());

74

441

                if blocks.block(block_index).is_stable() {

75

191

                    continue;

76

250

77

78

250

                trace!("Stabilising block {:?}", block_index);

79

250

                stable = false;

80

250

                blocks.mark_block_stable(block_index);

81

82

                // tau is the first label.

83

2250

                for label in tau_loop_free_lts

84

250

                    .labels()

85

250

                    .iter()

86

250

                    .enumerate()

87

2250

                    .map(|(i, _)| LabelIndex::new(i))

88

89

2250

                    compute_weak_act(

90

2250

                        &mut act_mark,

91

2250

                        &mut tau_mark,

92

2250

                        &tau_loop_free_lts,

93

2250

                        &blocks,

94

2250

                        &incoming,

95

2250

                        block_index,

96

2250

                        label,

97

);

98

99

                    // Note that we cannot use the block references here, and instead uses indices, because stabilise

100

                    // also modifies the blocks structure.

101

5169

                    for block_prime in (0usize..blocks.num_of_blocks()).map(BlockIndex::new) {

102

5169

                        stabilise(block_prime, &mut act_mark, &mut blocks);

103

5169

104

105

106

107

260

            if stable {

108

                // Quit the outer loop.

109

100

                trace!("Partition is stable!");

110

100

                break;

111

160

112

113

114

100

        (tau_loop_free_lts, blocks)

115

100

})

116

100

117

118

/// Sets s.act_mark to true iff exists t: S. s =\not{a}=> t

119

/// If a = tau, then also updates s.tau_mark

120

2250

fn compute_weak_act(

121

2250

    act_mark: &mut BitArray,

122

2250

    tau_mark: &mut BitArray,

123

2250

    lts: &impl LTS,

124

2250

    blocks: &SimpleBlockPartition,

125

2250

    incoming: &IncomingTransitions,

126

2250

    block: BlockIndex,

127

2250

    label: LabelIndex,

128

2250

) {

129

6669

    for s in lts.iter_states() {

130

        // s.act_mark := true iff s in B && a == tau

131

6669

        act_mark.set(

132

6669

*s,

133

6669

            lts.is_hidden_label(label) && blocks.iter_block(block).any(|state| state == s),

134

);

135

136

13986

        for transition in lts.outgoing_transitions(s) {

137

13986

            if transition.label == label {

138

                // s.act_mark := true iff a != tau && tau_mark[t]

139

1554

                if !lts.is_hidden_label(transition.label) && tau_mark[*transition.to] {

140

769

                    act_mark.set(*s, true);

141

785

142

12432

143

144

145

146

6669

    for t in lts.iter_states() {

147

        // t.tau_mark := t.act_mark if a == tau

148

6669

        if lts.is_hidden_label(label) {

149

741

            tau_mark.set(*t, act_mark[*t]);

150

5928

151

152

6669

        if act_mark[*t] {

153

1208

            for transition in incoming.incoming_silent_transitions(t) {

154

212

                act_mark.set(*transition.to, true);

155

212

156

5461

157

158

2250

159

160

/// Splits the given block according to the given marking.

161

5169

fn stabilise(block: BlockIndex, act_mark: &mut BitArray, blocks: &mut SimpleBlockPartition) {

162

6669

    blocks.split_block(block, |state| act_mark[*state]);

163

5169

164

165

#[cfg(test)]

166

mod tests {

167

    use merc_io::DumpFiles;

168

    use merc_lts::LTS;

169

    use merc_lts::random_lts;

170

    use merc_lts::write_aut;

171

    use merc_utilities::Timing;

172

    use merc_utilities::random_test;

173

174

    use crate::Equivalence;

175

    use crate::compare_lts;

176

    use crate::reduce_lts;

177

178

    #[test]

179

    #[cfg_attr(miri, ignore)]

180

1

    fn test_weak_bisimulation() {

181

100

        random_test(100, |rng| {

182

100

            let mut files = DumpFiles::new("test_weak_bisimulation");

183

184

100

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

185

100

            let mut timing = Timing::new();

186

100

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

187

188

100

            let result = reduce_lts(lts.clone(), Equivalence::WeakBisim, false, &mut timing);

189

100

            let expected = reduce_lts(lts, Equivalence::WeakBisimSigref, false, &mut timing);

190

191

100

            assert_eq!(result.num_of_states(), expected.num_of_states());

192

100

            assert_eq!(result.num_of_transitions(), expected.num_of_transitions());

193

194

100

            files.dump("result.aut", |f| write_aut(f, &result)).unwrap();

195

100

            files.dump("expected.aut", |f| write_aut(f, &expected)).unwrap();

196

197

100

            assert!(compare_lts(Equivalence::StrongBisim, result, expected, false, &mut timing));

198

100

})

199

1

200