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),

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

81

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

99

81

        &self.transition_groups

100

81

101

102

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

103

        // A Sylvan LTS does not have action labels.

104

&[]

105

106

107

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

108

        // A Sylvan LTS does not have parameter values.

109

&[]

110

111

112

113

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

114

pub struct SylvanTransitionGroup {

115

    relation: Ldd,

116

    meta: Ldd,

117

    read_proj: Vec<u32>,

118

    write_proj: Vec<u32>,

119

120

121

impl SylvanTransitionGroup {

122

    /// Creates a new Sylvan transition group.

123

24

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

124

24

        Self {

125

24

            relation,

126

24

            meta,

127

24

            read_proj,

128

24

            write_proj,

129

24

130

24

131

132

133

impl TransitionGroup for SylvanTransitionGroup {

134

1944

    fn relation(&self) -> &Ldd {

135

1944

        &self.relation

136

1944

137

138

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

139

        &self.read_proj

140

141

142

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

143

        &self.write_proj

144

145

146

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

147

        None

148

149

150

1944

    fn meta(&self) -> &Ldd {

151

1944

        &self.meta

152

1944

153

154

155

impl fmt::Debug for SylvanTransitionGroup {

156

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

157

        f.debug_struct("SylvanTransitionGroup")

158

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

159

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

160

            .finish()

161

162

163

164

#[cfg(test)]

165

mod test {

166

    use crate::reachability;

167

168

    use super::*;

169

170

    #[test]

171

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

172

1

    fn test_load_anderson_4() {

173

1

        let mut storage = Storage::new();

174

1

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

175

1

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

176

1

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

177

1

178

179

    #[test]

180

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

181

    #[cfg(not(debug_assertions))]

182

    fn test_load_collision_4() {

183

        let mut storage = Storage::new();

184

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

185

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

186

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

187

188