Grcov report - io_symbolic

1

use std::io::Read;

2

3

use merc_aterm::ATerm;

4

use merc_aterm::ATermList;

5

use merc_aterm::ATermRead;

6

use merc_aterm::ATermStreamable;

7

use merc_aterm::BinaryATermReader;

8

use merc_aterm::Symbol;

9

use merc_data::DataSpecification;

10

use merc_io::BitStreamRead;

11

use merc_ldd::BinaryLddReader;

12

use merc_ldd::Storage;

13

use merc_utilities::MercError;

14

15

use crate::SummandGroup;

16

use crate::SymbolicLts;

17

18

/// Reads a symbolic LTS from a binary stream in the mCRL2 `.sym` format.

19

///

20

/// # Details

21

///

22

/// The stream contains

23

/// <marker>: ATerm

24

/// <data specification>

25

/// <process parameters>: ATermList<ATerm>

26

///

27

/// <initial state>: LDD

28

/// <states>: LDD

29

///

30

/// For each process parameter:

31

///   <number of entries>: u64

32

///   For each entry:

33

///     <value>: ATerm

34

///

35

/// <number of action labels>: u64

36

/// For each action label:

37

///   <action label>: ATerm

38

///

39

/// <number of summand groups>: u64

40

/// For each summand group:

41

///  <number of read parameters>: u64

42

///  For each read parameter:

43

///    <read parameter>: ATerm

44

///

45

/// <number of write parameters>: u64

46

/// For each write parameter:

47

///  <write parameter>: ATerm

48

1

pub fn read_symbolic_lts<R: Read>(reader: R, storage: &mut Storage) -> Result<SymbolicLts, MercError> {

49

1

    let aterm_stream = BinaryATermReader::new(reader)?;

50

1

    let mut stream = BinaryLddReader::new(aterm_stream)?;

51

52

1

    if ATermRead::read_aterm(&mut stream)? != Some(symbolic_labelled_transition_system_mark()) {

53

        return Err("Expected symbolic labelled transition system stream".into());

54

1

55

56

1

    let data_spec = DataSpecification::read(&mut stream)?;

57

1

    let process_parameters: ATermList<ATerm> = stream.read_aterm()?.ok_or("Expected process parameters")?.into();

58

59

1

    let initial_state = stream.read_ldd(storage)?;

60

1

    let states = stream.read_ldd(storage)?;

61

62

    // Read the values for the process parameters.

63

30

    for _parameter in process_parameters {

64

30

        let num_of_entries = stream.read_integer()?;

65

66

30

        for _ in 0..num_of_entries {

67

193

            let _value = stream.read_aterm()?;

68

69

70

71

    // Read the action labels.

72

1

    let num_of_action_labels = stream.read_integer()?;

73

1

    for _ in 0..num_of_action_labels {

74

203

        let _action_label = stream.read_aterm()?;

75

76

77

    // Read the summand groups.

78

1

    let mut summand_groups = Vec::new();

79

1

    let num_of_groups = stream.read_integer()?;

80

1

    for _ in 0..num_of_groups {

81

82

        // Note: this is not an ATermInt, as expected by `read_aterm_iter`, but a variable integer.

83

101

        let num_of_reads = stream.read_integer()?;

84

101

        let mut read_parameters: Vec<ATerm> = Vec::with_capacity(num_of_reads as usize);

85

101

        for _ in 0..num_of_reads {

86

277

            read_parameters.push(stream.read_aterm()?.ok_or("Unexpected end of stream")?);

87

88

89

101

        let num_of_writes = stream.read_integer()?;

90

101

        let mut write_parameters: Vec<ATerm> = Vec::with_capacity(num_of_reads as usize);

91

101

        for _ in 0..num_of_writes {

92

324

            write_parameters.push(stream.read_aterm()?.ok_or("Unexpected end of stream")?);

93

94

95

101

        let relation = stream.read_ldd(storage)?;

96

97

101

        summand_groups.push(SummandGroup::new(read_parameters, write_parameters, relation));

98

99

100

1

    Ok(SymbolicLts::new(data_spec, states, initial_state, summand_groups))

101

1

102

103

/// Returns the ATerm mark for symbolic labelled transition systems.

104

1

fn symbolic_labelled_transition_system_mark() -> ATerm {

105

1

    ATerm::constant(&Symbol::new("symbolic_labelled_transition_system", 0))

106

1

107

108

#[cfg(test)]

109

mod tests {

110

    use merc_utilities::test_logger;

111

112

    use super::*;

113

114

    #[test]

115

    #[cfg_attr(miri, ignore)]

116

1

    fn test_read_symbolic_lts_wms_sym() {

117

1

        test_logger();

118

1

        let input = include_bytes!("../../../examples/lts/WMS.sym");

119

120

1

        let mut storage = Storage::new();

121

1

        let _lts = read_symbolic_lts(&input[..], &mut storage).unwrap();

122

1

123