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