Grcov report - parse

1

use mcrl2_syntax::parse_mcrl2_specification;

2

use mcrl2_syntax::Mcrl2Parser;

3

use mcrl2_syntax::Rule;

4

use pest::Parser;

5

use test_case::test_case;

6

7

// This command can be used to generate the tests cases, but duplicate names have to be removed

8

// find ./3rd-party/mCRL2/examples/ -name *.mcf -exec sh -c 'echo "#[test_case(include_str!(\"../../.{}\") ; \"$(basename "{}")\")]"' \;

9

169

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/mpsu/mpsu.mcrl2") ; "mpsu.mcrl2")]

10

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/abp_bw/abp_bw.mcrl2") ; "abp_bw.mcrl2")]

11

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/food_distribution/food_package.mcrl2") ; "food_package.mcrl2")]

12

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/onebit/onebit.mcrl2") ; "onebit.mcrl2")]

13

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Dijkstra/Dijkstra_spec.mcrl2") ; "Dijkstra_spec.mcrl2")]

14

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Dekker/Dekker_spec.mcrl2") ; "Dekker_spec.mcrl2")]

15

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Lamport_3bit_incorrect_z/Lamport_3bit_incorrect_z_spec.mcrl2") ; "Lamport_3bit_incorrect_z_spec.mcrl2")]

16

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Attiya-Welch/Attiya-Welch_spec.mcrl2") ; "Attiya-Welch_spec.mcrl2")]

17

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Knuth/Knuth_spec.mcrl2") ; "Knuth_spec.mcrl2")]

18

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Szymanski_3bitlw_sem/Szymanski_3bitlw_sem_spec.mcrl2") ; "Szymanski_3bitlw_sem_spec.mcrl2")]

19

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Szymanski_flag_with_bits/Szymanski_flag_with_bits_spec.mcrl2") ; "Szymanski_flag_with_bits_spec.mcrl2")]

20

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Aravind_BLRU/Aravind_BLRU_spec.mcrl2") ; "Aravind_BLRU_spec.mcrl2")]

21

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Szymanski_3bit_linear_wait/Szymanski_3bit_linear_wait_spec.mcrl2") ; "Szymanski_3bit_linear_wait_spec.mcrl2")]

22

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Register_model/Register_model_spec.mcrl2") ; "Register_model_spec.mcrl2")]

23

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Peterson/Peterson_spec.mcrl2") ; "Peterson_spec.mcrl2")]

24

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Szymanski_flag/Szymanski_flag_spec.mcrl2") ; "Szymanski_flag_spec.mcrl2")]

25

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Attiya-Welch_alternate/Attiya-Welch_alternate_spec.mcrl2") ; "Attiya-Welch_alternate_spec.mcrl2")]

26

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Szymanski_fwb_pe/Szymanski_fwb_pe_spec.mcrl2") ; "Szymanski_fwb_pe_spec.mcrl2")]

27

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/non-atomic_registers/Lamport_3bit/Lamport_3bit_spec.mcrl2") ; "Lamport_3bit_spec.mcrl2")]

28

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/swp/swp_lists.mcrl2") ; "swp_lists.mcrl2")]

29

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/swp/swp_func.mcrl2") ; "swp_func.mcrl2")]

30

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/swp/swp_fgpbp.mcrl2") ; "swp_fgpbp.mcrl2")]

31

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/swp/swp_with_tanenbaums_bug.mcrl2") ; "swp_with_tanenbaums_bug.mcrl2")]

32

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/scheduler/scheduler.mcrl2") ; "scheduler.mcrl2")]

33

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/tree/tree.mcrl2") ; "tree.mcrl2")]

34

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bakery/bakery.mcrl2") ; "bakery.mcrl2")]

35

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/commprot/commprot.mcrl2") ; "commprot.mcrl2")]

36

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/trains/trains.mcrl2") ; "trains.mcrl2")]

37

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/mutex_models/Mutex-naive/Mutex-naive_spec.mcrl2") ; "Mutex-naive_spec.mcrl2")]

38

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/mutex_models/Petersons/Petersons_spec.mcrl2") ; "Petersons_spec.mcrl2")]

39

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/mutex_models/Improved-mutex-naive/Improved-mutex-naive_spec.mcrl2") ; "Improved-mutex-naive_spec.mcrl2")]

40

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/mutex_models/Petersons-3/Petersons-3_spec.mcrl2") ; "Petersons-3_spec.mcrl2")]

41

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/leader/dolev_klawe_rodeh.mcrl2") ; "dolev_klawe_rodeh.mcrl2")]

42

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/leader/leader.mcrl2") ; "leader.mcrl2")]

43

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/parallel/parallel.mcrl2") ; "parallel.mcrl2")]

44

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/par/par.mcrl2") ; "par.mcrl2")]

45

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bke/bke.mcrl2") ; "bke.mcrl2")]

46

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/parallel_proc_with_global_var/parallel_counting.mcrl2") ; "parallel_counting.mcrl2")]

47

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/allow/allow.mcrl2") ; "allow.mcrl2")]

48

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/block/block.mcrl2") ; "block.mcrl2")]

49

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/goback/goback.mcrl2") ; "goback.mcrl2")]

50

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/cabp/cabp.mcrl2") ; "cabp.mcrl2")]

51

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/hopcroft/hopcroft.mcrl2") ; "hopcroft.mcrl2")]

52

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/peterson_justness/mutex.mcrl2") ; "mutex.mcrl2")]

53

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining_10.mcrl2") ; "dining_10.mcrl2")]

54

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_ns_seq.mcrl2") ; "dining3_ns_seq.mcrl2")]

55

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_cs.mcrl2") ; "dining3_cs.mcrl2")]

56

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_seq.mcrl2") ; "dining3_seq.mcrl2")]

57

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_schedule.mcrl2") ; "dining3_schedule.mcrl2")]

58

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3.mcrl2") ; "dining3.mcrl2")]

59

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_ns.mcrl2") ; "dining3_ns.mcrl2")]

60

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining8.mcrl2") ; "dining8.mcrl2")]

61

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_cs_seq.mcrl2") ; "dining3_cs_seq.mcrl2")]

62

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/dining/dining3_schedule_seq.mcrl2") ; "dining3_schedule_seq.mcrl2")]

63

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/cellular_automata/cellular_automata.mcrl2") ; "cellular_automata.mcrl2")]

64

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula6/mp_fts_prop6.mcrl2") ; "mp_fts_prop6.mcrl2")]

65

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula8/mp_fts_prop8.mcrl2") ; "mp_fts_prop8.mcrl2")]

66

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula11/mp_fts_prop11.mcrl2") ; "mp_fts_prop11.mcrl2")]

67

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula10/mp_fts_prop10.mcrl2") ; "mp_fts_prop10.mcrl2")]

68

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula3/mp_fts_prop3.mcrl2") ; "mp_fts_prop3.mcrl2")]

69

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula5/mp_fts_prop5.mcrl2") ; "mp_fts_prop5.mcrl2")]

70

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula9/mp_fts_prop9.mcrl2") ; "mp_fts_prop9.mcrl2")]

71

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula4/mp_fts_prop4.mcrl2") ; "mp_fts_prop4.mcrl2")]

72

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula12/mp_fts_prop12.mcrl2") ; "mp_fts_prop12.mcrl2")]

73

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula2/mp_fts_prop2.mcrl2") ; "mp_fts_prop2.mcrl2")]

74

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula1/mp_fts_prop1.mcrl2") ; "mp_fts_prop1.mcrl2")]

75

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/family_based_experiments/formula7/mp_fts_prop7.mcrl2") ; "mp_fts_prop7.mcrl2")]

76

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/minepump_product_line/minepump_fts.mcrl2") ; "minepump_fts.mcrl2")]

77

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bounded_ricart-agrawala/RA_original/RA_original_spec.mcrl2") ; "RA_original_spec.mcrl2")]

78

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bounded_ricart-agrawala/RA_fixed+broadcast/RA_fixed+broadcast_spec.mcrl2") ; "RA_fixed+broadcast_spec.mcrl2")]

79

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bounded_ricart-agrawala/RA_fixed+reduced/RA_fixed+reduced_spec.mcrl2") ; "RA_fixed+reduced_spec.mcrl2")]

80

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/bounded_ricart-agrawala/RA_fixed/RA_fixed_spec.mcrl2") ; "RA_fixed_spec.mcrl2")]

81

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/producer_consumer/producer_consumer.mcrl2") ; "producer_consumer.mcrl2")]

82

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/academic/abp/abp.mcrl2") ; "abp.mcrl2")]

83

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/ieee-11073/11073.mcrl2") ; "11073.mcrl2")]

84

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage-r1.mcrl2") ; "garage-r1.mcrl2")]

85

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage-r2-error.mcrl2") ; "garage-r2-error.mcrl2")]

86

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage-ver.mcrl2") ; "garage-ver.mcrl2")]

87

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage-r3.mcrl2") ; "garage-r3.mcrl2")]

88

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage.mcrl2") ; "garage.mcrl2")]

89

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/garage/garage-r2.mcrl2") ; "garage-r2.mcrl2")]

90

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/chatbox/chatbox.mcrl2") ; "chatbox.mcrl2")]

91

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/1394/1394-fin.mcrl2") ; "1394-fin.mcrl2")]

92

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/lift/lift3-final.mcrl2") ; "lift3-final.mcrl2")]

93

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/lift/lift3-init.mcrl2") ; "lift3-init.mcrl2")]

94

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/ERTMS/version1A/section_II/IU/ertms-hl3.announce.mcrl2") ; "ertms-hl3.announce.mcrl2")]

95

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/ERTMS/version1A/section_II/IU/ertms-hl3.mcrl2") ; "ertms-hl3.mcrl2")]

96

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/brp/brp.mcrl2") ; "brp.mcrl2")]

97

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/DIRAC/WMS.mcrl2") ; "WMS.mcrl2")]

98

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/DIRAC/SMS.mcrl2") ; "SMS.mcrl2")]

99

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/flexray/3_Ideal_trace.expanded.mcrl2") ; "3_Ideal_trace.expanded.mcrl2")]

100

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/flexray/3_Mute_follower.expanded.mcrl2") ; "3_Mute_follower.expanded.mcrl2")]

101

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/flexray/3_Mute_leader.expanded.mcrl2") ; "3_Mute_leader.expanded.mcrl2")]

102

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/flexray/3_Regular.expanded.mcrl2") ; "3_Regular.expanded.mcrl2")]

103

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/flexray/Big_Deaf_follower.expanded.mcrl2") ; "Big_Deaf_follower.expanded.mcrl2")]

104

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/industrial/alma/alma.mcrl2") ; "alma.mcrl2")]

105

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/coins_simulate_dice/dice.mcrl2") ; "dice.mcrl2")]

106

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/self_stabilisation/self_stabilisation.mcrl2") ; "self_stabilisation.mcrl2")]

107

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/shared_coin_protocol/shared_coin_protocol.mcrl2") ; "shared_coin_protocol.mcrl2")]

108

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/game_of_goose/game_of_goose_stochastic.mcrl2") ; "game_of_goose_stochastic.mcrl2")]

109

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/coin_tossing/coins.mcrl2") ; "coins.mcrl2")]

110

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/monty_hall_tv_show/monty_hall.mcrl2") ; "monty_hall.mcrl2")]

111

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/airplane_ticket/airplane_ticket.mcrl2") ; "airplane_ticket.mcrl2")]

112

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/ant_on_grid/ant_on_grid.mcrl2") ; "ant_on_grid.mcrl2")]

113

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/brp/brp.mcrl2") ; "brp.mcrl2 (probabilitistic)")]

114

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/probabilistic/sultan_of_persia/sultan_of_persia.mcrl2") ; "sultan_of_persia.mcrl2")]

115

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/visualisation/cube/cube.mcrl2") ; "cube.mcrl2")]

116

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/visualisation/carpet/carpet.mcrl2") ; "carpet.mcrl2")]

117

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/snake/snake.mcrl2") ; "snake.mcrl2")]

118

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/clobber/clobber.mcrl2") ; "clobber.mcrl2")]

119

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/hex/hex.mcrl2") ; "hex.mcrl2")]

120

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/open_field_tic_tac_toe/open_field_tictactoe.mcrl2") ; "open_field_tictactoe.mcrl2")]

121

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/game_of_goose/game_of_goose.mcrl2") ; "game_of_goose.mcrl2")]

122

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/sokoban/sokoban.mcrl2") ; "sokoban.mcrl2")]

123

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/sudoku/sudoku.mcrl2") ; "sudoku.mcrl2")]

124

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/bridge_crossing/bridge_crossing.mcrl2") ; "bridge_crossing.mcrl2")]

125

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/tictactoe/tictactoe_fast.mcrl2") ; "tictactoe_fast.mcrl2")]

126

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/tictactoe/tictactoe.mcrl2") ; "tictactoe.mcrl2")]

127

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/magic_square/magic_square.mcrl2") ; "magic_square.mcrl2")]

128

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/magic_square/magic_hexagon.mcrl2") ; "magic_hexagon.mcrl2")]

129

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/domineering/domineering.mcrl2") ; "domineering.mcrl2")]

130

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/peg_solitaire/peg_solitaire.mcrl2") ; "peg_solitaire.mcrl2")]

131

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/quoridor/quoridor.mcrl2") ; "quoridor.mcrl2")]

132

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/wolf_goat_cabbage/wolf_goat_cabbage.mcrl2") ; "wolf_goat_cabbage.mcrl2")]

133

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/rubiks_cube/rubiks_cube.mcrl2") ; "rubiks_cube.mcrl2")]

134

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/othello/othello.mcrl2") ; "othello.mcrl2")]

135

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/rubiks_cube_small/small_cube.mcrl2") ; "small_cube.mcrl2")]

136

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/four_in_a_row/four_in_a_row.mcrl2") ; "four_in_a_row.mcrl2")]

137

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/games/knights/knights.mcrl2") ; "knights.mcrl2")]

138

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/lambda.mcrl2") ; "lambda.mcrl2")]

139

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/funccomp.mcrl2") ; "funccomp.mcrl2")]

140

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/tau.mcrl2") ; "tau.mcrl2")]

141

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/time.mcrl2") ; "time.mcrl2")]

142

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/small2.mcrl2") ; "small2.mcrl2")]

143

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/struct.mcrl2") ; "struct.mcrl2")]

144

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/gpa_10_3.mcrl2") ; "gpa_10_3.mcrl2")]

145

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/divide2_10.mcrl2") ; "divide2_10.mcrl2")]

146

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/delta0.mcrl2") ; "delta0.mcrl2")]

147

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/upcast.mcrl2") ; "upcast.mcrl2")]

148

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/sets_bags.mcrl2") ; "sets_bags.mcrl2")]

149

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/rational.mcrl2") ; "rational.mcrl2")]

150

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/divide2_500.mcrl2") ; "divide2_500.mcrl2")]

151

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/exists.mcrl2") ; "exists.mcrl2")]

152

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/divide2_100.mcrl2") ; "divide2_100.mcrl2")]

153

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/delta.mcrl2") ; "delta.mcrl2")]

154

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/small3.mcrl2") ; "small3.mcrl2")]

155

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/numbers.mcrl2") ; "numbers.mcrl2")]

156

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/small1.mcrl2") ; "small1.mcrl2")]

157

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/list.mcrl2") ; "list.mcrl2")]

158

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/gpa_10_1.mcrl2") ; "gpa_10_1.mcrl2")]

159

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/forall.mcrl2") ; "forall.mcrl2")]

160

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/language/gpa_10_2.mcrl2") ; "gpa_10_2.mcrl2")]

161

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Lamport_queue/Lamport_queue_spec.mcrl2") ; "Lamport_queue_spec.mcrl2")]

162

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Petersons_mutex/Petersons_F_T/Petersons_F_T_spec.mcrl2") ; "Petersons_F_T_spec.mcrl2")]

163

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Petersons_mutex/Petersons_T_T/Petersons_T_T_spec.mcrl2") ; "Petersons_T_T_spec.mcrl2")]

164

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Petersons_mutex/Petersons_F_F/Petersons_F_F_spec.mcrl2") ; "Petersons_F_F_spec.mcrl2")]

165

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Knuths_dancing_links/Dancing_links/Dancing_links_spec.mcrl2") ; "Dancing_links_spec.mcrl2")]

166

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Knuths_dancing_links/Dancing_links_no_stack/Dancing_links_no_stack_spec.mcrl2") ; "Dancing_links_no_stack_spec.mcrl2")]

167

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Knuths_dancing_links/Dancing_links_remove_0/Dancing_links_remove_0_spec.mcrl2") ; "Dancing_links_remove_0_spec.mcrl2")]

168

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Treiber_stack/Treiber_DCAS/Treiber_DCAS_spec.mcrl2") ; "Treiber_DCAS_spec.mcrl2")]

169

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Treiber_stack/Treiber_CAS/Treiber_CAS_spec.mcrl2") ; "Treiber_CAS_spec.mcrl2")]

170

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/software_models/Treiber_stack/Treiber_no_CAS/Treiber_no_CAS_spec.mcrl2") ; "Treiber_no_CAS_spec.mcrl2")]

171

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/light/light.mcrl2") ; "light.mcrl2")]

172

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/ball_game/ball_game.mcrl2") ; "ball_game.mcrl2")]

173

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/fischer/fischer.mcrl2") ; "fischer.mcrl2")]

174

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/clock/clock_drift.mcrl2") ; "clock_drift.mcrl2")]

175

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/clock/clock_hasty.mcrl2") ; "clock_hasty.mcrl2")]

176

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/clock/clock_exact.mcrl2") ; "clock_exact.mcrl2")]

177

#[test_case(include_str!("../../../3rd-party/mCRL2/examples/timed/simple/simple.mcrl2") ; "simple.mcrl2")]

178

169

fn test_parse_mcrl2_spec(input: &str) {

179

169

    if let Err(y) = parse_mcrl2_specification(input) {

180

        panic!("{}", y);

181

169

182

169

183

184

109

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/infinitely_often_enabled_then_infinitely_often_taken.mcf") ; "infinitely_often_enabled_then_infinitely_often_taken.mcf")]

185

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/infinitely_often_lost.mcf") ; "infinitely_often_lost.mcf")]

186

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/infinitely_often_receive_d1.mcf") ; "infinitely_often_receive_d1.mcf")]

187

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/infinitely_often_receive_for_all_d.mcf") ; "infinitely_often_receive_for_all_d.mcf")]

188

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/nodeadlock.mcf") ; "nodeadlock.mcf")]

189

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/no_duplication_of_messages.mcf") ; "no_duplication_of_messages.mcf")]

190

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/no_generation_of_messages.mcf") ; "no_generation_of_messages.mcf")]

191

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/read_then_eventually_send.mcf") ; "read_then_eventually_send.mcf")]

192

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/abp/read_then_eventually_send_if_fair.mcf") ; "read_then_eventually_send_if_fair.mcf")]

193

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bakery/always_can_get_number.mcf") ; "always_can_get_number.mcf")]

194

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bakery/get_at_least_number_circulating.mcf") ; "get_at_least_number_circulating.mcf")]

195

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bakery/request_can_eventually_enter.mcf") ; "request_can_eventually_enter.mcf")]

196

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bakery/request_must_eventually_enter.mcf") ; "request_must_eventually_enter.mcf")]

197

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bke/secret_not_leaked.mcf") ; "secret_not_leaked.mcf")]

198

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bounded_ricart-agrawala/RA_fixed/properties/deadlock freedom.mcf") ; "deadlock freedom.mcf")]

199

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bounded_ricart-agrawala/RA_fixed/properties/no deadlock in model.mcf") ; "no deadlock in model.mcf")]

200

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/bounded_ricart-agrawala/RA_fixed/properties/starvation freedom.mcf") ; "starvation freedom.mcf")]

201

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/dining/nostarvation.mcf") ; "nostarvation.mcf")]

202

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/dining/nostuffing.mcf") ; "nostuffing.mcf")]

203

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/food_distribution/sustained_delivery.mcf") ; "sustained_delivery.mcf")]

204

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/leader/at_most_one_leader.mcf") ; "at_most_one_leader.mcf")]

205

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/leader/leader_always_elected.mcf") ; "leader_always_elected.mcf")]

206

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula1/prop1.mcf") ; "prop1.mcf")]

207

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula10/prop10.mcf") ; "prop10.mcf")]

208

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula11/prop11.mcf") ; "prop11.mcf")]

209

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula12/prop12.mcf") ; "prop12.mcf")]

210

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula2/prop2.mcf") ; "prop2.mcf")]

211

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula3/prop3.mcf") ; "prop3.mcf")]

212

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula4/prop4.mcf") ; "prop4.mcf")]

213

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula5/prop5.mcf") ; "prop5.mcf")]

214

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula6/prop6.mcf") ; "prop6.mcf")]

215

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula7/prop7.mcf") ; "prop7.mcf")]

216

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula8/prop8.mcf") ; "prop8.mcf")]

217

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/minepump_product_line/family_based_experiments/formula9/prop9.mcf") ; "prop9.mcf")]

218

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu1.mcf") ; "mpsu1.mcf")]

219

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu2.mcf") ; "mpsu2.mcf")]

220

//#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu3.mcf") ; "mpsu3.mcf")]

221

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu4.mcf") ; "mpsu4.mcf")]

222

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu5.mcf") ; "mpsu5.mcf")]

223

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mpsu/mpsu6.mcf") ; "mpsu6.mcf")]

224

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mutex_models/Dekker/properties/Always eventually request.mcf") ; "Always eventually request.mcf")]

225

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mutex_models/Dekker/properties/Eventual access if fair.mcf") ; "Eventual access if fair.mcf")]

226

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mutex_models/Dekker/properties/Eventual access.mcf") ; "Eventual access.mcf")]

227

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/mutex_models/Dekker/properties/Mutual exclusion.mcf") ; "Mutual exclusion.mcf")]

228

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/parallel_proc_with_global_var/parallel_counting.mcf") ; "parallel_counting.mcf")]

229

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/peterson_justness/justlive.mcf") ; "justlive.mcf")]

230

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/scheduler/infinitely_often_enabled_then_infinitely_often_taken_a.mcf") ; "infinitely_often_enabled_then_infinitely_often_taken_a.mcf")]

231

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/academic/trains/infinitely_often_enabled_then_infinitely_often_taken_enter.mcf") ; "infinitely_often_enabled_then_infinitely_often_taken_enter.mcf")]

232

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/domineering/eventually_player1_or_player2_wins.mcf") ; "eventually_player1_or_player2_wins.mcf")]

233

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/domineering/player1_can_win.mcf") ; "player1_can_win.mcf")]

234

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/domineering/player2_can_win.mcf") ; "player2_can_win.mcf")]

235

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/four_in_a_row/red_wins.mcf") ; "red_wins.mcf")]

236

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/open_field_tic_tac_toe/red_has_a_winning_strategy.mcf") ; "red_has_a_winning_strategy.mcf")]

237

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/open_field_tic_tac_toe/yellow_has_a_winning_strategy.mcf") ; "yellow_has_a_winning_strategy.mcf")]

238

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/othello/exists_draw.mcf") ; "exists_draw.mcf")]

239

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/othello/red_can_win.mcf") ; "red_can_win.mcf")]

240

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/othello/red_wins_always.mcf") ; "red_wins_always.mcf")]

241

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/othello/white_can_win.mcf") ; "white_can_win.mcf")]

242

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/othello/white_wins_always.mcf") ; "white_wins_always.mcf")]

243

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule1.mcf") ; "rule1.mcf")]

244

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule11.mcf") ; "rule11.mcf")]

245

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule12.mcf") ; "rule12.mcf")]

246

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule14.mcf") ; "rule14.mcf")]

247

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule15.mcf") ; "rule15.mcf")]

248

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule3.mcf") ; "rule3.mcf")]

249

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule4.mcf") ; "rule4.mcf")]

250

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule5.mcf") ; "rule5.mcf")]

251

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule6a.mcf") ; "rule6a.mcf")]

252

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule6b.mcf") ; "rule6b.mcf")]

253

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/rule789.mcf") ; "rule789.mcf")]

254

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/winning_strategy_player_1.mcf") ; "winning_strategy_player_1.mcf")]

255

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/quoridor/properties/winning_strategy_player_2.mcf") ; "winning_strategy_player_2.mcf")]

256

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/snake/black_has_winning_strategy.mcf") ; "black_has_winning_strategy.mcf")]

257

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/snake/eventually_white_or_black_wins.mcf") ; "eventually_white_or_black_wins.mcf")]

258

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/snake/white_has_winning_strategy.mcf") ; "white_has_winning_strategy.mcf")]

259

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/tictactoe/has_player_cross_a_winning_strategy.mcf") ; "has_player_cross_a_winning_strategy.mcf")]

260

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/games/tictactoe/one_wrong_move.mcf") ; "one_wrong_move.mcf")]

261

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/DIRAC/properties_SMS/eventuallyDeleted.mcf") ; "eventuallyDeleted.mcf")]

262

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/DIRAC/properties_SMS/noTransitFromDeleted.mcf") ; "noTransitFromDeleted.mcf")]

263

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/DIRAC/properties_WMS/jobFailedToDone.mcf") ; "jobFailedToDone.mcf")]

264

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/DIRAC/properties_WMS/noZombieJobs.mcf") ; "noZombieJobs.mcf")]

265

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ERTMS/version1A/section_I/IU/deterministic_stabilisation.mcf") ; "deterministic_stabilisation.mcf")]

266

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ERTMS/version1A/section_I/IU/no_collision.mcf") ; "no_collision.mcf")]

267

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ERTMS/version1A/section_I/IU/strong_determinacy.mcf") ; "strong_determinacy.mcf")]

268

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ERTMS/version1A/section_I/IU/termination.mcf") ; "termination.mcf")]

269

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/flexray/mucalc/eventually_comm.mcf") ; "eventually_comm.mcf")]

270

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/flexray/mucalc/eventually_startup.mcf") ; "eventually_startup.mcf")]

271

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ieee-11073/data_can_be_communicated.mcf") ; "data_can_be_communicated.mcf")]

272

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ieee-11073/infinite_data_communication_is_possible.mcf") ; "infinite_data_communication_is_possible.mcf")]

273

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ieee-11073/no_inconsistent_operating_states.mcf") ; "no_inconsistent_operating_states.mcf")]

274

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/industrial/ieee-11073/no_successful_transmission_in_inconsistent_operating_states.mcf") ; "no_successful_transmission_in_inconsistent_operating_states.mcf")]

275

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/probabilistic/coin_tossing/formula1.mcf") ; "formula1.mcf")]

276

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/probabilistic/coin_tossing/formula2.mcf") ; "formula2.mcf")]

277

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/probabilistic/sultan_of_persia/best_spouse.mcf") ; "best_spouse.mcf")]

278

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Knuths_dancing_links/Dancing_links/properties/Correctness.mcf") ; "Correctness.mcf")]

279

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Head get set value.mcf") ; "Head get set value.mcf")]

280

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Head not set out of bounds.mcf") ; "Head not set out of bounds.mcf")]

281

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/No out of bounds read.mcf") ; "No out of bounds read.mcf")]

282

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/No out of bounds write.mcf") ; "No out of bounds write.mcf")]

283

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Pop always terminates.mcf") ; "Pop always terminates.mcf")]

284

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Pop can terminate.mcf") ; "Pop can terminate.mcf")]

285

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Push always terminates.mcf") ; "Push always terminates.mcf")]

286

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Push can terminate.mcf") ; "Push can terminate.mcf")]

287

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Queue behaviour.mcf") ; "Queue behaviour.mcf")]

288

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Tail get set value.mcf") ; "Tail get set value.mcf")]

289

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Tail not read out of bounds.mcf") ; "Tail not read out of bounds.mcf")]

290

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Lamport_queue/properties/Tail not set out of bounds.mcf") ; "Tail not set out of bounds.mcf")]

291

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Petersons_mutex/Petersons_F_F/properties/Bounded overtaking.mcf") ; "Bounded overtaking.mcf")]

292

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Treiber_stack/Treiber_CAS/properties/Correct release implies correct retrieve.mcf") ; "Correct release implies correct retrieve.mcf")]

293

#[test_case(include_str!("../../../3rd-party/mCRL2/./examples/software_models/Treiber_stack/Treiber_CAS/properties/Inevitably retrieve when stacksize is 2.mcf") ; "Inevitably retrieve when stacksize is 2.mcf")]

294

109

fn test_parse_mcrl2_modal_formula(input: &str) {

295

109

    if let Err(y) = Mcrl2Parser::parse(Rule::StateFrmSpec, input) {

296

        panic!("{}", y);

297

109

298

109

299

300

33

#[test_case(include_str!("../../../examples/REC/mcrl2/add8.dataspec") ; "add8")]

301

#[test_case(include_str!("../../../examples/REC/mcrl2/benchexpr10.dataspec") ; "benchexpr10")]

302

#[test_case(include_str!("../../../examples/REC/mcrl2/benchsym10.dataspec") ; "benchsym10")]

303

#[test_case(include_str!("../../../examples/REC/mcrl2/benchtree10.dataspec") ; "benchtree10")]

304

#[test_case(include_str!("../../../examples/REC/mcrl2/binarysearch.dataspec") ; "binarysearch")]

305

#[test_case(include_str!("../../../examples/REC/mcrl2/bubblesort10.dataspec") ; "bubblesort10")]

306

#[test_case(include_str!("../../../examples/REC/mcrl2/calls.dataspec") ; "calls")]

307

#[test_case(include_str!("../../../examples/REC/mcrl2/check1.dataspec") ; "check1")]

308

#[test_case(include_str!("../../../examples/REC/mcrl2/check2.dataspec") ; "check2")]

309

#[test_case(include_str!("../../../examples/REC/mcrl2/closure.dataspec") ; "closure")]

310

#[test_case(include_str!("../../../examples/REC/mcrl2/confluence.dataspec") ; "confluence")]

311

#[test_case(include_str!("../../../examples/REC/mcrl2/dart.dataspec") ; "dart")]

312

#[test_case(include_str!("../../../examples/REC/mcrl2/empty.dataspec") ; "empty")]

313

#[test_case(include_str!("../../../examples/REC/mcrl2/evalexpr.dataspec") ; "evalexpr")]

314

#[test_case(include_str!("../../../examples/REC/mcrl2/evalsym.dataspec") ; "evalsym")]

315

#[test_case(include_str!("../../../examples/REC/mcrl2/evaltree.dataspec") ; "evaltree")]

316

#[test_case(include_str!("../../../examples/REC/mcrl2/factorial5.dataspec") ; "factorial5")]

317

#[test_case(include_str!("../../../examples/REC/mcrl2/fib32.dataspec") ; "fib32")]

318

#[test_case(include_str!("../../../examples/REC/mcrl2/fibfree.dataspec") ; "fibfree")]

319

#[test_case(include_str!("../../../examples/REC/mcrl2/fibonacci05.dataspec") ; "fibonacci05")]

320

#[test_case(include_str!("../../../examples/REC/mcrl2/garbagecollection.dataspec") ; "garbagecollection")]

321

#[test_case(include_str!("../../../examples/REC/mcrl2/hanoi4.dataspec") ; "hanoi4")]

322

#[test_case(include_str!("../../../examples/REC/mcrl2/intnat.dataspec") ; "intnat")]

323

#[test_case(include_str!("../../../examples/REC/mcrl2/langton6.dataspec") ; "langton6")]

324

#[test_case(include_str!("../../../examples/REC/mcrl2/logic3.dataspec") ; "logic3")]

325

#[test_case(include_str!("../../../examples/REC/mcrl2/maa.dataspec") ; "maa")]

326

#[test_case(include_str!("../../../examples/REC/mcrl2/merge.dataspec") ; "merge")]

327

#[test_case(include_str!("../../../examples/REC/mcrl2/mergesort10.dataspec") ; "mergesort10")]

328

#[test_case(include_str!("../../../examples/REC/mcrl2/missionaries2.dataspec") ; "missionaries2")]

329

#[test_case(include_str!("../../../examples/REC/mcrl2/mul8.dataspec") ; "mul8")]

330

#[test_case(include_str!("../../../examples/REC/mcrl2/natlist.dataspec") ; "natlist")]

331

#[test_case(include_str!("../../../examples/REC/mcrl2/oddeven.dataspec") ; "oddeven")]

332

#[test_case(include_str!("../../../examples/REC/mcrl2/omul8.dataspec") ; "omul8")]

333

33

fn test_parse_mcrl2_dataspec(input: &str) {

334

33

    if let Err(y) = Mcrl2Parser::parse(Rule::MCRL2Spec, input) {

335

        panic!("{}", y);

336

33

337

33