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
ltl_atom_str(enum ltl_atom atom)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
ltl_start(struct task_struct * task,struct ltl_monitor * mon)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
ltl_possible_next_states(struct ltl_monitor * mon,unsigned int state,unsigned long * next)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