tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h

/* SPDX-License-Identifier: GPL-2.0 */

/*
 * C implementation of Buchi automaton, automatically generated by
 * tools/verification/rvgen from the linear temporal logic specification.
 * For further information, see kernel documentation:
 *   Documentation/trace/rv/linear_temporal_logic.rst
 */

#include <linux/rv.h>

#define MONITOR_NAME test_ltl

enum ltl_atom {
	LTL_EVENT_A,
	LTL_EVENT_B,
	LTL_NUM_ATOM
};
static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);

static const char *ltl_atom_str(enum ltl_atom atom)
{
	static const char *const names[] = {
		"ev_a",
		"ev_b",
	};

	return names[atom];
}

enum ltl_buchi_state {
	S0,
	S1,
	S2,
	S3,
	S4,
	RV_NUM_BA_STATES
};
static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);

static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
{
	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
	bool val1 = !event_a;

	if (val1)
		__set_bit(S0, mon->states);
	if (true)
		__set_bit(S1, mon->states);
	if (event_b)
		__set_bit(S4, mon->states);
}

static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
	bool val1 = !event_a;

	switch (state) {
	case S0:
		if (val1)
			__set_bit(S0, next);
		if (true)
			__set_bit(S1, next);
		if (event_b)
			__set_bit(S4, next);
		break;
	case S1:
		if (true)
			__set_bit(S1, next);
		if (true && val1)
			__set_bit(S2, next);
		if (event_b && val1)
			__set_bit(S3, next);
		if (event_b)
			__set_bit(S4, next);
		break;
	case S2:
		if (true)
			__set_bit(S1, next);
		if (true && val1)
			__set_bit(S2, next);
		if (event_b && val1)
			__set_bit(S3, next);
		if (event_b)
			__set_bit(S4, next);
		break;
	case S3:
		if (val1)
			__set_bit(S0, next);
		if (true)
			__set_bit(S1, next);
		if (event_b)
			__set_bit(S4, next);
		break;
	case S4:
		if (val1)
			__set_bit(S0, next);
		if (true)
			__set_bit(S1, next);
		if (event_b)
			__set_bit(S4, next);
		break;
	}
}