Grcov report - counterexample

1

use merc_lts::TransitionLabel;

2

use merc_syntax::ActFrm;

3

use merc_syntax::Action;

4

use merc_syntax::ModalityOperator;

5

use merc_syntax::MultiAction;

6

use merc_syntax::RegFrm;

7

use merc_syntax::StateFrm;

8

use merc_syntax::StateFrmOp;

9

10

/// Represents a counter example.

11

pub enum CounterExample<L: TransitionLabel> {

12

    /// Represents a simple trace formula `<a0.a1. ... .a_n>true`.

13

    Trace(Vec<L>),

14

    /// Represents a weak trace formula `<tau*.a0.tau*.a1. ... .a_n.tau*>true`.

15

    WeakTrace(Vec<L>),

16

    /// Represents a stable failures formula `<tau*.a0.tau*.a1. ... .a_n.tau*>([refusal_0]false && ... [refusal_k]false)`.

17

    StableFailures(Vec<L>, Vec<L>),

18

    /// Represents an impossible futures formula `<tau*.a0.tau*.a1. ... .a_n.tau*>([future_0. ...]false && ... [future_k. ...]false)`.

19

    ImpossibleFutures(Vec<L>, Vec<Vec<L>>),

20

21

22

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

23

257

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

24

257

    match counter_example {

25

57

        CounterExample::Trace(trace) => {

26

57

            let mut expr = StateFrm::True;

27

28

            // We build the formula bottom up.

29

245

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

30

245

                expr = StateFrm::Modality {

31

245

                    operator: ModalityOperator::Diamond,

32

245

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

33

245

                    expr: Box::new(expr),

34

245

35

36

37

57

            expr

38

39

109

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

40

47

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

41

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

42

47

            let inner = refusals

43

47

                .iter()

44

167

                .map(|l| {

45

167

                    StateFrm::Modality {

46

167

                        operator: ModalityOperator::Box,

47

167

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

48

167

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

49

167

50

                    // Stable failures are only observed in stable states, so make this the base case.

51

167

})

52

47

                .fold(

53

47

                    StateFrm::Modality {

54

47

                        operator: ModalityOperator::Box,

55

47

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

56

47

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

57

47

},

58

                    |acc, expr| StateFrm::Binary {

59

167

                        op: StateFrmOp::Conjunction,

60

167

                        lhs: Box::new(acc),

61

167

                        rhs: Box::new(expr),

62

167

},

63

);

64

65

47

            weaktrace_formula(trace, inner, ModalityOperator::Diamond)

66

67

44

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

68

44

            let expressions = futures

69

44

                .iter()

70

55

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

71

44

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

72

73

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

74

44

            let expr = expressions

75

44

                .into_iter()

76

44

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

77

55

                    op: StateFrmOp::Conjunction,

78

55

                    lhs: Box::new(acc),

79

55

                    rhs: Box::new(expr),

80

55

});

81

82

44

            weaktrace_formula(trace, expr, ModalityOperator::Diamond)

83

84

85

257

86

87

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

88

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

89

///

90

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

91

/// it is a valid weaktrace formula.

92

255

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

93

    // Build the formula tau*

94

255

    let tau_star = RegFrm::Iteration(Box::new(RegFrm::Action(ActFrm::MultAct(MultiAction::new(vec![])))));

95

96

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

97

255

    let mut result = StateFrm::Modality {

98

255

        operator: modality,

99

255

        formula: tau_star.clone(),

100

255

        expr: Box::new(expr),

101

255

};

102

103

896

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

104

757

        result = StateFrm::Modality {

105

757

            operator: modality,

106

757

            formula: tau_star.clone(),

107

757

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

108

757

                operator: modality,

109

757

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

110

757

                expr: Box::new(result),

111

757

}),

112

757

113

114

115

255

    result

116

255

117

118

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

119

1169

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

120

1169

    if label.is_tau_label() {

121

53

        MultiAction::tau()

122

    } else {

123

1116

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

124

125

1169