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 pagefault 13 14 enum ltl_atom { 15 LTL_PAGEFAULT, 16 LTL_RT, 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 "pa", 25 "rt", 26 }; 27 28 return names[atom]; 29 } 30 31 enum ltl_buchi_state { 32 S0, 33 RV_NUM_BA_STATES 34 }; 35 static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); 36 37 static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) 38 { 39 bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); 40 bool val3 = !pagefault; 41 bool rt = test_bit(LTL_RT, mon->atoms); 42 bool val1 = !rt; 43 bool val4 = val1 || val3; 44 45 if (val4) 46 __set_bit(S0, mon->states); 47 } 48 49 static void 50 ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) 51 { 52 bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); 53 bool val3 = !pagefault; 54 bool rt = test_bit(LTL_RT, mon->atoms); 55 bool val1 = !rt; 56 bool val4 = val1 || val3; 57 58 switch (state) { 59 case S0: 60 if (val4) 61 __set_bit(S0, next); 62 break; 63 } 64 } 65