xref: /linux/tools/verification/rvgen/tests/golden/test_ha/test_ha.h (revision 55ee4b931a7ffedc886175d265dd6e6d08fd4151)
1 /* SPDX-License-Identifier: GPL-2.0 */
2 /*
3  * Automatically generated C representation of test_ha automaton
4  * For further information about this format, see kernel documentation:
5  *   Documentation/trace/rv/deterministic_automata.rst
6  */
7 
8 #define MONITOR_NAME test_ha
9 
10 enum states_test_ha {
11 	S0_test_ha,
12 	S1_test_ha,
13 	S2_test_ha,
14 	S3_test_ha,
15 	state_max_test_ha,
16 };
17 
18 #define INVALID_STATE state_max_test_ha
19 
20 enum events_test_ha {
21 	event0_test_ha,
22 	event1_test_ha,
23 	event2_test_ha,
24 	event_max_test_ha,
25 };
26 
27 enum envs_test_ha {
28 	clk_test_ha,
29 	env1_test_ha,
30 	env2_test_ha,
31 	env_max_test_ha,
32 	env_max_stored_test_ha = env1_test_ha,
33 };
34 
35 _Static_assert(env_max_stored_test_ha <= MAX_HA_ENV_LEN, "Not enough slots");
36 #define HA_CLK_NS
37 
38 struct automaton_test_ha {
39 	char *state_names[state_max_test_ha];
40 	char *event_names[event_max_test_ha];
41 	char *env_names[env_max_test_ha];
42 	unsigned char function[state_max_test_ha][event_max_test_ha];
43 	unsigned char initial_state;
44 	bool final_states[state_max_test_ha];
45 };
46 
47 static const struct automaton_test_ha automaton_test_ha = {
48 	.state_names = {
49 		"S0",
50 		"S1",
51 		"S2",
52 		"S3",
53 	},
54 	.event_names = {
55 		"event0",
56 		"event1",
57 		"event2",
58 	},
59 	.env_names = {
60 		"clk",
61 		"env1",
62 		"env2",
63 	},
64 	.function = {
65 		{            S0_test_ha,            S1_test_ha,         INVALID_STATE },
66 		{            S0_test_ha,         INVALID_STATE,            S2_test_ha },
67 		{         INVALID_STATE,            S2_test_ha,            S3_test_ha },
68 		{            S0_test_ha,            S1_test_ha,         INVALID_STATE },
69 	},
70 	.initial_state = S0_test_ha,
71 	.final_states = { 1, 0, 0, 0 },
72 };
73