/* 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 pagefault

enum ltl_atom {
        LTL_PAGEFAULT,
        LTL_RT,
        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[] = {
                "pa",
                "rt",
        };

        return names[atom];
}

enum ltl_buchi_state {
        S0,
        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 pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
        bool val3 = !pagefault;
        bool rt = test_bit(LTL_RT, mon->atoms);
        bool val1 = !rt;
        bool val4 = val1 || val3;

        if (val4)
                __set_bit(S0, mon->states);
}

static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
        bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
        bool val3 = !pagefault;
        bool rt = test_bit(LTL_RT, mon->atoms);
        bool val1 = !rt;
        bool val4 = val1 || val3;

        switch (state) {
        case S0:
                if (val4)
                        __set_bit(S0, next);
                break;
        }
}