1 /* SPDX-License-Identifier: GPL-2.0 */ 2 3 /* 4 * C implementation of Buchi automaton, automatically generated by 5 * tools/verification/rvgen from the linear temporal logic specification. 6 * For further information, see kernel documentation: 7 * Documentation/trace/rv/linear_temporal_logic.rst 8 */ 9 10 #include <linux/rv.h> 11 12 #define MONITOR_NAME test_bak_kunit 13 14 enum ltl_atom { 15 LTL_EVENT_A, 16 LTL_EVENT_B, 17 LTL_NUM_ATOM 18 }; 19 static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); 20 21 static const char *ltl_atom_str(enum ltl_atom atom) 22 { 23 static const char *const names[] = { 24 "ev_a", 25 "ev_b", 26 }; 27 28 return names[atom]; 29 } 30 31 enum ltl_buchi_state { 32 S0, 33 S1, 34 S2, 35 S3, 36 S4, 37 RV_NUM_BA_STATES 38 }; 39 static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); 40 41 static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) 42 { 43 bool event_b = test_bit(LTL_EVENT_B, mon->atoms); 44 bool event_a = test_bit(LTL_EVENT_A, mon->atoms); 45 bool val1 = !event_a; 46 47 if (val1) 48 __set_bit(S0, mon->states); 49 if (true) 50 __set_bit(S1, mon->states); 51 if (event_b) 52 __set_bit(S4, mon->states); 53 } 54 55 static void 56 ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) 57 { 58 bool event_b = test_bit(LTL_EVENT_B, mon->atoms); 59 bool event_a = test_bit(LTL_EVENT_A, mon->atoms); 60 bool val1 = !event_a; 61 62 switch (state) { 63 case S0: 64 if (val1) 65 __set_bit(S0, next); 66 if (true) 67 __set_bit(S1, next); 68 if (event_b) 69 __set_bit(S4, next); 70 break; 71 case S1: 72 if (true) 73 __set_bit(S1, next); 74 if (true && val1) 75 __set_bit(S2, next); 76 if (event_b && val1) 77 __set_bit(S3, next); 78 if (event_b) 79 __set_bit(S4, next); 80 break; 81 case S2: 82 if (true) 83 __set_bit(S1, next); 84 if (true && val1) 85 __set_bit(S2, next); 86 if (event_b && val1) 87 __set_bit(S3, next); 88 if (event_b) 89 __set_bit(S4, next); 90 break; 91 case S3: 92 if (val1) 93 __set_bit(S0, next); 94 if (true) 95 __set_bit(S1, next); 96 if (event_b) 97 __set_bit(S4, next); 98 break; 99 case S4: 100 if (val1) 101 __set_bit(S0, next); 102 if (true) 103 __set_bit(S1, next); 104 if (event_b) 105 __set_bit(S4, next); 106 break; 107 } 108 } 109