Grcov report - counterexample

1

use crate::ActFrm;

2

use crate::Action;

3

use crate::FixedPointOperator;

4

use crate::ModalityOperator;

5

use crate::MultiAction;

6

use crate::RegFrm;

7

use crate::Span;

8

use crate::StateFrm;

9

use crate::StateFrmOp;

10

use crate::StateVarDecl;

11

use merc_lts::TransitionLabel;

12

use merc_refinement::CounterExample;

13

14

/// Generates a formula that characterizes the counter example trace.

15

590

pub fn generate_formula<L: TransitionLabel>(counter_example: &CounterExample<L>) -> StateFrm {

16

590

    match counter_example {

17

107

        CounterExample::Trace(trace) => {

18

107

            let mut expr = StateFrm::True;

19

20

            // We build the formula bottom up.

21

162

            for label in trace.iter().rev() {

22

162

                expr = StateFrm::Modality {

23

162

                    operator: ModalityOperator::Diamond,

24

162

                    formula: RegFrm::Action(ActFrm::MultAct(label_to_multi_action(label))),

25

162

                    expr: Box::new(expr),

26

162

27

28

29

107

            expr

30

31

299

        CounterExample::WeakTrace(trace) => weaktrace_formula(trace, StateFrm::True, ModalityOperator::Diamond),

32

1

        CounterExample::Divergence(trace) => weaktrace_formula(

33

1

            trace,

34

            // For the divergence we use `nu X. <tau>X` to require an infinite tau path.

35

1

            StateFrm::FixedPoint {

36

1

                operator: FixedPointOperator::Greatest,

37

1

                variable: StateVarDecl {

38

1

                    identifier: "X".to_string(),

39

1

                    arguments: Vec::new(),

40

1

                    span: Span::default(),

41

1

},

42

1

                body: Box::new(StateFrm::Modality {

43

1

                    operator: ModalityOperator::Diamond,

44

1

                    formula: RegFrm::Action(ActFrm::MultAct(MultiAction::tau())),

45

1

                    expr: Box::new(StateFrm::Id("X".to_string(), Vec::new())),

46

1

}),

47

1

},

48

1

            ModalityOperator::Diamond,

49

),

50

119

        CounterExample::StableFailures(trace, refusals) => {

51

            // Refused actions are characterized by box-false modalities.

52

119

            let inner = refusals

53

119

                .iter()

54

119

                .map(|l| StateFrm::Modality {

55

207

                    operator: ModalityOperator::Box,

56

207

                    formula: RegFrm::Action(ActFrm::MultAct(label_to_multi_action(l))),

57

207

                    expr: Box::new(StateFrm::False),

58

207

})

59

119

                .fold(

60

                    // Stable failures are only observed in stable states, so tau is refused.

61

119

                    StateFrm::Modality {

62

119

                        operator: ModalityOperator::Box,

63

119

                        formula: RegFrm::Action(ActFrm::MultAct(MultiAction::tau())),

64

119

                        expr: Box::new(StateFrm::False),

65

119

},

66

                    |acc, expr| StateFrm::Binary {

67

207

                        op: StateFrmOp::Conjunction,

68

207

                        lhs: Box::new(acc),

69

207

                        rhs: Box::new(expr),

70

207

},

71

);

72

73

119

            weaktrace_formula(trace, inner, ModalityOperator::Diamond)

74

75

64

        CounterExample::ImpossibleFutures(trace, futures) => {

76

64

            let expressions = futures

77

64

                .iter()

78

85

                .map(|future| weaktrace_formula(future, StateFrm::False, ModalityOperator::Box))

79

64

                .collect::<Vec<_>>();

80

81

            // Generate a conjunction of the expressions for each future.

82

64

            let expr = expressions

83

64

                .into_iter()

84

64

                .fold(StateFrm::True, |acc, expr| StateFrm::Binary {

85

                    op: StateFrmOp::Conjunction,

86

85

                    lhs: Box::new(acc),

87

85

                    rhs: Box::new(expr),

88

85

});

89

90

64

            weaktrace_formula(trace, expr, ModalityOperator::Diamond)

91

92

93

590

94

95

/// Generates a formula `[tau* . label1 . tau* . label2. ... . tau*]expr`, or

96

/// diamond based on `modality`, that characterizes the weak trace.

97

///

98

/// Note that every hidden label in the given `trace` is ignored, to ensure that

99

/// it is a valid weaktrace formula.

100

568

fn weaktrace_formula<L: TransitionLabel>(trace: &[L], expr: StateFrm, modality: ModalityOperator) -> StateFrm {

101

    // Build the formula tau*

102

568

    let tau_star = RegFrm::Iteration(Box::new(RegFrm::Action(ActFrm::MultAct(MultiAction::tau()))));

103

104

    // We build the formula bottom up: tau* . label . ... . tau*

105

568

    let mut result = StateFrm::Modality {

106

568

        operator: modality,

107

568

        formula: tau_star.clone(),

108

568

        expr: Box::new(expr),

109

568

};

110

111

847

    for label in trace.iter().rev().filter(|l| !l.is_tau_label()) {

112

680

        result = StateFrm::Modality {

113

680

            operator: modality,

114

680

            formula: tau_star.clone(),

115

680

            expr: Box::new(StateFrm::Modality {

116

680

                operator: modality,

117

680

                formula: RegFrm::Action(ActFrm::MultAct(label_to_multi_action(label))),

118

680

                expr: Box::new(result),

119

680

}),

120

680

121

122

123

568

    result

124

568

125

126

/// Converts a label to a multi-action, where tau labels are converted to the empty multi-action.

127

1049

fn label_to_multi_action<L: TransitionLabel>(label: &L) -> MultiAction {

128

1049

    if label.is_tau_label() {

129

62

        MultiAction::tau()

130

    } else {

131

987

        MultiAction::new(vec![Action::new(label.to_string(), Vec::new())])

132

133

1049