Grcov report - reachability.rs

1

#![forbid(unsafe_code)]

2

3

use log::trace;

4

5

use crate::LTS;

6

use crate::LabelIndex;

7

use crate::LabelledTransitionSystem;

8

use crate::LtsBuilder;

9

use crate::LtsBuilderFast;

10

use crate::StateIndex;

11

use crate::TransitionLabel;

12

13

/// Performs a reachability analysis on the given LTS using a depth-first search

14

/// from the initial state.

15

///

16

/// Only follows transitions for which `filter` returns `true`.

17

/// Calls `visit` for every newly reached state, including the start state.

18

383313

pub fn reachability<P, F, L: LTS>(lts: &L, state: StateIndex, mut filter: F, mut visit: P)

19

383313

where

20

383313

    P: FnMut(StateIndex),

21

383313

    F: FnMut(LabelIndex) -> bool,

22

23

383313

    let mut reachable = vec![false; lts.num_of_states()];

24

383313

    visit(state);

25

383313

    reachable[state] = true;

26

27

383313

    let mut stack = vec![state];

28

29

1347533

    while let Some(state) = stack.pop() {

30

964220

        debug_assert!(reachable[state], "State {} must already be marked as reachable", state);

31

964220

        trace!("Visiting {}", state);

32

33

4324503

        for transition in lts.outgoing_transitions(state) {

34

4324503

            if filter(transition.label) && !reachable[transition.to] {

35

580907

                trace!("Transition -[{}]-> {}", transition.label, transition.to);

36

580907

                reachable[transition.to] = true;

37

580907

                visit(transition.to);

38

580907

                stack.push(transition.to);

39

3743596

40

41

42

43

383313

    trace!("Finished reachability");

44

383313

45

46

/// Returns the number of states reachable from the given state of the LTS.

47

400

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

48

400

    let mut count = 0;

49

400

    reachability(lts, state, |_| true, |_| count += 1);

50

400

    count

51

400

52

53

/// Returns a new LTS containing only the states and transitions reachable from

54

/// the initial state of `lts`.

55

pub fn reachable_lts<L: LTS>(lts: &L) -> LabelledTransitionSystem<L::Label>

56

where

57

    L::Label: TransitionLabel,

58

59

    let initial = lts.initial_state_index();

60

61

    // Collect reachable states in discovery order.

62

    let mut old_to_new: Vec<Option<StateIndex>> = vec![None; lts.num_of_states()];

63

    let mut new_to_old: Vec<StateIndex> = Vec::new();

64

65

    reachability(

66

        lts,

67

        initial,

68

        |_| true,

69

        |state| {

70

            let new_index = StateIndex::new(new_to_old.len());

71

            old_to_new[state] = Some(new_index);

72

            new_to_old.push(state);

73

},

74

);

75

76

    let num_reachable = new_to_old.len();

77

78

    // Use LtsBuilderFast to collect the reachable transitions with renumbered state indices.

79

    let labels = lts.labels().to_vec();

80

    let mut builder = LtsBuilderFast::new(labels, vec![]);

81

    builder.require_num_of_states(num_reachable);

82

83

    for &old_state in &new_to_old {

84

        let new_from = old_to_new[old_state].expect("reachable state must have a mapping");

85

        for t in lts.outgoing_transitions(old_state) {

86

            if let Some(new_to) = old_to_new[t.to] {

87

                let label = &lts.labels()[t.label.value()];

88

                builder

89

                    .add_transition(new_from, label, new_to)

90

                    .expect("transition should be valid");

91

92

93

94

95

    builder.finish(StateIndex::new(0), false)

96