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

608

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

16

608

    match counter_example {

17

98

        CounterExample::Trace(trace) => {

18

98

            let mut expr = StateFrm::True;

19

20

            // We build the formula bottom up.

21

157

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

22

157

                expr = StateFrm::Modality {

23

157

                    operator: ModalityOperator::Diamond,

24

157

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

25

157

                    expr: Box::new(expr),

26

157

27

28

29

98

            expr

30

31

293

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

32

2

        CounterExample::Divergence(trace) => weaktrace_formula(

33

2

            trace,

34

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

35

2

            StateFrm::FixedPoint {

36

2

                operator: FixedPointOperator::Greatest,

37

2

                variable: StateVarDecl {

38

2

                    identifier: "X".to_string(),

39

2

                    arguments: Vec::new(),

40

2

                    span: Span::default(),

41

2

},

42

2

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

43

2

                    operator: ModalityOperator::Diamond,

44

2

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

45

2

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

46

2

}),

47

2

},

48

2

            ModalityOperator::Diamond,

49

),

50

140

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

51

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

52

140

            let inner = refusals

53

140

                .iter()

54

140

                .map(|l| StateFrm::Modality {

55

239

                    operator: ModalityOperator::Box,

56

239

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

57

239

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

58

239

})

59

140

                .fold(

60

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

61

140

                    StateFrm::Modality {

62

140

                        operator: ModalityOperator::Box,

63

140

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

64

140

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

65

140

},

66

                    |acc, expr| StateFrm::Binary {

67

239

                        op: StateFrmOp::Conjunction,

68

239

                        lhs: Box::new(acc),

69

239

                        rhs: Box::new(expr),

70

239

},

71

);

72

73

140

            weaktrace_formula(trace, inner, ModalityOperator::Diamond)

74

75

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

76

75

            let expressions = futures

77

75

                .iter()

78

106

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

79

75

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

80

81

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

82

75

            let expr = expressions

83

75

                .into_iter()

84

75

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

85

106

                    op: StateFrmOp::Conjunction,

86

106

                    lhs: Box::new(acc),

87

106

                    rhs: Box::new(expr),

88

106

});

89

90

75

            weaktrace_formula(trace, expr, ModalityOperator::Diamond)

91

92

93

608

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

616

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

101

    // Build the formula tau*

102

616

    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

616

    let mut result = StateFrm::Modality {

106

616

        operator: modality,

107

616

        formula: tau_star.clone(),

108

616

        expr: Box::new(expr),

109

616

};

110

111

934

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

112

722

        result = StateFrm::Modality {

113

722

            operator: modality,

114

722

            formula: tau_star.clone(),

115

722

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

116

722

                operator: modality,

117

722

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

118

722

                expr: Box::new(result),

119

722

}),

120

722

121

122

123

616

    result

124

616

125

126

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

127

1118

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

128

1118

    if label.is_tau_label() {

129

61

        MultiAction::tau()

130

    } else {

131

1057

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

132

133

1118