Grcov report - io

1

use std::fmt;

2

use std::io::Read;

3

4

use log::info;

5

use merc_data::DataExpression;

6

use merc_ldd::Ldd;

7

use merc_ldd::Storage;

8

use merc_ldd::SylvanReader;

9

use merc_ldd::Value;

10

use merc_ldd::compute_meta;

11

use merc_ldd::read_u32;

12

use merc_utilities::MercError;

13

14

use crate::SymbolicLTS;

15

use crate::TransitionGroup;

16

17

/// Returns the (initial state, transitions) read from the file in Sylvan's format.

18

1

pub fn read_sylvan<R: Read>(storage: &mut Storage, stream: &mut R) -> Result<SylvanLts, MercError> {

19

1

    info!("Reading symbolic LTS in Sylvan format...");

20

1

    let mut reader = SylvanReader::new();

21

22

1

    let _vector_length = read_u32(stream)?;

23

24

1

    let _unused = read_u32(stream)?; // This is called 'k' in Sylvan's ldd2bdd.c, but unused.

25

1

    let initial_state = reader.read_ldd(storage, stream)?;

26

1

    let num_transitions: usize = read_u32(stream)? as usize;

27

1

    let mut groups: Vec<SylvanTransitionGroup> = Vec::new();

28

29

    // Read all the transition groups.

30

1

    for _ in 0..num_transitions {

31

24

        let (read_proj, write_proj) = read_projection(stream)?;

32

24

        groups.push(SylvanTransitionGroup::new(

33

24

            storage.empty_set().clone(),

34

24

            compute_meta(storage, &read_proj, &write_proj).0,

35

24

            read_proj,

36

24

            write_proj,

37

));

38

39

40

24

    for transition in groups.iter_mut().take(num_transitions) {

41

24

        transition.relation = reader.read_ldd(storage, stream)?;

42

43

44

1

    Ok(SylvanLts::new(storage.empty_set().clone(), initial_state, groups))

45

1

46

47

/// Reads the read and write projections from the given stream.

48

24

pub fn read_projection<R: Read>(file: &mut R) -> Result<(Vec<Value>, Vec<Value>), MercError> {

49

24

    let num_read = read_u32(file)?;

50

24

    let num_write = read_u32(file)?;

51

52

    // Read num_read integers for the read parameters.

53

24

    let mut read_proj: Vec<Value> = Vec::new();

54

24

    for _ in 0..num_read {

55

68

        let value = read_u32(file)?;

56

68

        read_proj.push(value as Value);

57

58

59

    // Read num_write integers for the write parameters.

60

24

    let mut write_proj: Vec<Value> = Vec::new();

61

24

    for _ in 0..num_write {

62

72

        let value = read_u32(file)?;

63

72

        write_proj.push(value as Value);

64

65

66

24

    Ok((read_proj, write_proj))

67

24

68

69

/// A symbolic labelled transition system read from a Sylvan file.

70

pub struct SylvanLts {

71

    initial_state: merc_ldd::Ldd,

72

73

    transition_groups: Vec<SylvanTransitionGroup>, // (relation, meta)

74

75

    empty_set: Ldd,

76

77

78

impl SylvanLts {

79

    /// Creates a new Sylvan LTS.

80

1

    pub fn new(empty_set: Ldd, initial_state: Ldd, transition_groups: Vec<SylvanTransitionGroup>) -> Self {

81

1

        Self {

82

1

            initial_state,

83

1

            transition_groups,

84

1

            empty_set,

85

1

86

1

87

88

89

impl SymbolicLTS for SylvanLts {

90

    fn states(&self) -> &Ldd {

91

        &self.empty_set

92

93

94

2

    fn initial_state(&self) -> &Ldd {

95

2

        &self.initial_state

96

2

97

98

    fn transition_groups(&self) -> &[impl TransitionGroup] {

99

        &self.transition_groups

100

101

102

81

    fn transition_groups_mut(&mut self) -> &mut [impl TransitionGroup] {

103

81

        &mut self.transition_groups

104

81

105

106

    fn action_labels(&self) -> &[String] {

107

        // A Sylvan LTS does not have action labels.

108

&[]

109

110

111

    fn parameter_values(&self) -> &[Vec<DataExpression>] {

112

        // A Sylvan LTS does not have parameter values.

113

&[]

114

115

116

117

/// A transition group read from a Sylvan file.

118

pub struct SylvanTransitionGroup {

119

    relation: Ldd,

120

    meta: Ldd,

121

    read_proj: Vec<u32>,

122

    write_proj: Vec<u32>,

123

124

125

impl SylvanTransitionGroup {

126

    /// Creates a new Sylvan transition group.

127

24

    pub fn new(relation: Ldd, meta: Ldd, read_proj: Vec<u32>, write_proj: Vec<u32>) -> Self {

128

24

        Self {

129

24

            relation,

130

24

            meta,

131

24

            read_proj,

132

24

            write_proj,

133

24

134

24

135

136

137

impl TransitionGroup for SylvanTransitionGroup {

138

1944

    fn relation(&self) -> &Ldd {

139

1944

        &self.relation

140

1944

141

142

    fn read_indices(&self) -> &[u32] {

143

        &self.read_proj

144

145

146

    fn write_indices(&self) -> &[u32] {

147

        &self.write_proj

148

149

150

    fn action_label_index(&self) -> Option<usize> {

151

        None

152

153

154

1944

    fn meta(&self) -> &Ldd {

155

1944

        &self.meta

156

1944

157

158

1944

    fn learn_successors(&mut self, _storage: &mut Storage, _todo: &Ldd) -> Result<(), MercError> {

159

        // All states are already explored.

160

1944

        Ok(())

161

1944

162

163

164

impl fmt::Debug for SylvanTransitionGroup {

165

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

166

        f.debug_struct("SylvanTransitionGroup")

167

            .field("read_proj", &self.read_proj)

168

            .field("write_proj", &self.write_proj)

169

            .finish()

170

171

172

173

#[cfg(test)]

174

mod test {

175

    use merc_utilities::Timing;

176

177

    use crate::reachability;

178

179

    use super::Storage;

180

    use super::read_sylvan;

181

182

    #[test]

183

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

184

1

    fn test_load_anderson_4() {

185

1

        let mut storage = Storage::new();

186

1

        let bytes = include_bytes!("../../../examples/ldd/anderson.4.ldd");

187

1

        let mut lts = read_sylvan(&mut storage, &mut &bytes[..]).expect("Loading should work correctly");

188

1

        reachability(&mut storage, &mut lts, &Timing::new()).expect("Reachability should work correctly");

189

1

190

191

    #[test]

192

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

193

    #[cfg(not(debug_assertions))]

194

    fn test_load_collision_4() {

195

        let mut storage = Storage::new();

196

        let bytes = include_bytes!("../../../examples/ldd/collision.4.ldd");

197

        let mut lts = read_sylvan(&mut storage, &mut &bytes[..]).expect("Loading should work correctly");

198

        reachability(&mut storage, &mut lts, &Timing::new()).expect("Reachability should work correctly");

199

200