Re: [PATCH v3 14/17] verification/rvgen: Add selftests for rvgen kunit

[Wen Yang <wen.yang@linux.dev>]

On 6/25/26 20:14, Gabriele Monaco wrote:
> The rvgen kunit command patches monitor files and adds necessary
> definitions for kunit tests.
> 
> Add a test case validating its behaviour on dummy generated files and
> comparing it against reference files, like it's done for rvgen monitor.
> 
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
>   .../rvgen/rvgen/templates/kunit.c             |   2 +-
>   .../rvgen/tests/golden/test_da_kunit/Kconfig  |   9 +
>   .../golden/test_da_kunit/test_da_kunit.c      | 111 ++++++++
>   .../golden/test_da_kunit/test_da_kunit.h      |  47 ++++
>   .../test_da_kunit/test_da_kunit_kunit.c       |  29 ++
>   .../test_da_kunit/test_da_kunit_kunit.h       |  23 ++
>   .../test_da_kunit/test_da_kunit_trace.h       |  15 +
>   .../rvgen/tests/golden/test_ha_kunit/Kconfig  |   9 +
>   .../golden/test_ha_kunit/test_ha_kunit.c      | 264 ++++++++++++++++++
>   .../golden/test_ha_kunit/test_ha_kunit.h      |  88 ++++++
>   .../test_ha_kunit/test_ha_kunit_kunit.c       |  29 ++
>   .../test_ha_kunit/test_ha_kunit_kunit.h       |  24 ++
>   .../test_ha_kunit/test_ha_kunit_trace.h       |  19 ++
>   .../rvgen/tests/golden/test_ltl_kunit/Kconfig |   9 +
>   .../golden/test_ltl_kunit/test_ltl_kunit.c    | 107 +++++++
>   .../golden/test_ltl_kunit/test_ltl_kunit.h    | 108 +++++++
>   .../test_ltl_kunit/test_ltl_kunit_kunit.c     |  29 ++
>   .../test_ltl_kunit/test_ltl_kunit_kunit.h     |  22 ++
>   .../test_ltl_kunit/test_ltl_kunit_trace.h     |  14 +
>   tools/verification/rvgen/tests/rvgen_kunit.t  |  32 +++
>   20 files changed, 989 insertions(+), 1 deletion(-)
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h
>   create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h
>   create mode 100644 tools/verification/rvgen/tests/rvgen_kunit.t
> 
> diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c
> index d29bbf2ea5..402b5c8575 100644
> --- a/tools/verification/rvgen/rvgen/templates/kunit.c
> +++ b/tools/verification/rvgen/rvgen/templates/kunit.c
> @@ -8,7 +8,7 @@
>    */
>   #include "%%MODEL_NAME%%_kunit.h"
>   
> -#if IS_ENABLED(CONFIG_RV_MON_%%MODEL_NAME_UP%%)
> +#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%)
>   
>   static void rv_test_%%MODEL_NAME%%(struct kunit *test)
>   {
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig
> new file mode 100644
> index 0000000000..6d664ba562
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig
> @@ -0,0 +1,9 @@
> +# SPDX-License-Identifier: GPL-2.0-only
> +#
> +config RV_MON_TEST_DA_KUNIT
> +	depends on RV
> +	# XXX: add dependencies if there
> +	select DA_MON_EVENTS_IMPLICIT
> +	bool "test_da_kunit monitor"
> +	help
> +	  auto-generated
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c
> new file mode 100644
> index 0000000000..c2916c3e86
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c
> @@ -0,0 +1,111 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/ftrace.h>
> +#include <linux/tracepoint.h>
> +#include <linux/kernel.h>
> +#include <linux/module.h>
> +#include <linux/init.h>
> +#include <linux/rv.h>
> +#include <rv/instrumentation.h>
> +
> +#define MODULE_NAME "test_da_kunit"
> +
> +/*
> + * XXX: include required tracepoint headers, e.g.,
> + * #include <trace/events/sched.h>
> + */
> +#include <rv_trace.h>
> +
> +/*
> + * This is the self-generated part of the monitor. Generally, there is no need
> + * to touch this section.
> + */
> +#define RV_MON_TYPE RV_MON_PER_CPU
> +#include "test_da_kunit.h"
> +#include <rv/da_monitor.h>
> +
> +/*
> + * This is the instrumentation part of the monitor.
> + *
> + * This is the section where manual work is required. Here the kernel events
> + * are translated into model's event.
> + *
> + */
> +static void handle_event_1(void *data, /* XXX: fill header */)
> +{
> +	da_handle_event(event_1_test_da_kunit);
> +}
> +
> +static void handle_event_2(void *data, /* XXX: fill header */)
> +{
> +	/* XXX: validate that this event always leads to the initial state */
> +	da_handle_start_event(event_2_test_da_kunit);
> +}
> +
> +static int enable_test_da_kunit(void)
> +{
> +	int retval;
> +
> +	retval = da_monitor_init();
> +	if (retval)
> +		return retval;
> +
> +	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
> +	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
> +
> +	return 0;
> +}
> +
> +static void disable_test_da_kunit(void)
> +{
> +	rv_this.enabled = 0;
> +
> +	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
> +	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
> +
> +	da_monitor_destroy();
> +}
> +
> +/*
> + * This is the monitor register section.
> + */
> +static struct rv_monitor rv_this = {
> +	.name = "test_da_kunit",
> +	.description = "auto-generated",
> +	.enable = enable_test_da_kunit,
> +	.disable = disable_test_da_kunit,
> +	.reset = da_monitor_reset_all,
> +	.enabled = 0,
> +};
> +
> +static int __init register_test_da_kunit(void)
> +{
> +	return rv_register_monitor(&rv_this, NULL);
> +}
> +
> +static void __exit unregister_test_da_kunit(void)
> +{
> +	rv_unregister_monitor(&rv_this);
> +}
> +
> +module_init(register_test_da_kunit);
> +module_exit(unregister_test_da_kunit);
> +
> +MODULE_LICENSE("GPL");
> +MODULE_AUTHOR("dot2k: auto-generated");
> +MODULE_DESCRIPTION("test_da_kunit: auto-generated");
> +
> +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
> +#include <kunit/visibility.h>
> +#include "test_da_kunit_kunit.h"
> +
> +const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = {
> +	.mon = {
> +		.rv_this = &rv_this,
> +		.monitor_init = da_monitor_init,
> +		.monitor_destroy = da_monitor_destroy,
> +	},
> +	.handle_event_1 = handle_event_1,
> +	.handle_event_2 = handle_event_2,
> +};
> +EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops);
> +#endif
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h
> new file mode 100644
> index 0000000000..290a9454ca
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h
> @@ -0,0 +1,47 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Automatically generated C representation of test_da_kunit automaton
> + * For further information about this format, see kernel documentation:
> + *   Documentation/trace/rv/deterministic_automata.rst
> + */
> +
> +#define MONITOR_NAME test_da_kunit
> +
> +enum states_test_da_kunit {
> +	state_a_test_da_kunit,
> +	state_b_test_da_kunit,
> +	state_max_test_da_kunit,
> +};
> +
> +#define INVALID_STATE state_max_test_da_kunit
> +
> +enum events_test_da_kunit {
> +	event_1_test_da_kunit,
> +	event_2_test_da_kunit,
> +	event_max_test_da_kunit,
> +};
> +
> +struct automaton_test_da_kunit {
> +	char *state_names[state_max_test_da_kunit];
> +	char *event_names[event_max_test_da_kunit];
> +	unsigned char function[state_max_test_da_kunit][event_max_test_da_kunit];
> +	unsigned char initial_state;
> +	bool final_states[state_max_test_da_kunit];
> +};
> +
> +static const struct automaton_test_da_kunit automaton_test_da_kunit = {
> +	.state_names = {
> +		"state_a",
> +		"state_b",
> +	},
> +	.event_names = {
> +		"event_1",
> +		"event_2",
> +	},
> +	.function = {
> +		{       state_b_test_da_kunit,       state_a_test_da_kunit },
> +		{               INVALID_STATE,       state_a_test_da_kunit },
> +	},
> +	.initial_state = state_a_test_da_kunit,
> +	.final_states = { 1, 0 },
> +};
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c
> new file mode 100644
> index 0000000000..06a280444b
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c
> @@ -0,0 +1,29 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/kernel.h>
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +/*
> + * XXX: include required headers, e.g.,
> + * #include <linux/sched.h>
> + */
> +#include "test_da_kunit_kunit.h"
> +
> +#if IS_REACHABLE(CONFIG_RV_MON_TEST_DA_KUNIT)
> +
> +static void rv_test_test_da_kunit(struct kunit *test)
> +{
> +	struct rv_kunit_ctx *ctx = test->priv;
> +
> +	prepare_test(test, &rv_test_da_kunit_ops.mon);
> +
> +	/*
> +	 * XXX: write the test here
> +	 * e.g.
> +	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
> +	 *	rv_test_da_kunit_ops.handle_event(args);
> +	 */
> +}
> +
> +#else
> +#define rv_test_test_da_kunit rv_test_stub
> +#endif
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h
> new file mode 100644
> index 0000000000..0094215ff4
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h
> @@ -0,0 +1,23 @@
> +/* SPDX-License-Identifier: GPL-2.0-only */
> +/*
> + * Automatically generated by rvgen kunit.
> + * May need manual intervention for function prototypes that couldn't be
> + * found (e.g. are in another file) or variables to be exported.
> + */
> +
> +#ifndef __TEST_DA_KUNIT_KUNIT_H
> +#define __TEST_DA_KUNIT_KUNIT_H
> +
> +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
> +
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +
> +extern const struct rv_test_da_kunit_ops {
> +	struct rv_kunit_mon mon;
> +	void (*handle_event_1)(void *data, /* XXX: fill header */);
> +	void (*handle_event_2)(void *data, /* XXX: fill header */);
> +} rv_test_da_kunit_ops;
> +#endif
> +
> +#endif /* __TEST_DA_KUNIT_KUNIT_H */
> diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h
> new file mode 100644
> index 0000000000..16804a79e8
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h
> @@ -0,0 +1,15 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +
> +/*
> + * Snippet to be included in rv_trace.h
> + */
> +
> +#ifdef CONFIG_RV_MON_TEST_DA_KUNIT
> +DEFINE_EVENT(event_da_monitor, event_test_da_kunit,
> +	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
> +	     TP_ARGS(state, event, next_state, final_state));
> +
> +DEFINE_EVENT(error_da_monitor, error_test_da_kunit,
> +	     TP_PROTO(char *state, char *event),
> +	     TP_ARGS(state, event));
> +#endif /* CONFIG_RV_MON_TEST_DA_KUNIT */
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig
> new file mode 100644
> index 0000000000..6c48770ace
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig
> @@ -0,0 +1,9 @@
> +# SPDX-License-Identifier: GPL-2.0-only
> +#
> +config RV_MON_TEST_HA_KUNIT
> +	depends on RV
> +	# XXX: add dependencies if there
> +	select HA_MON_EVENTS_ID
> +	bool "test_ha_kunit monitor"
> +	help
> +	  auto-generated
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c
> new file mode 100644
> index 0000000000..69ca870ac2
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c
> @@ -0,0 +1,264 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/ftrace.h>
> +#include <linux/tracepoint.h>
> +#include <linux/kernel.h>
> +#include <linux/module.h>
> +#include <linux/init.h>
> +#include <linux/rv.h>
> +#include <rv/instrumentation.h>
> +
> +#define MODULE_NAME "test_ha_kunit"
> +
> +/*
> + * XXX: include required tracepoint headers, e.g.,
> + * #include <trace/events/sched.h>
> + */
> +#include <rv_trace.h>
> +
> +/*
> + * This is the self-generated part of the monitor. Generally, there is no need
> + * to touch this section.
> + */
> +#define RV_MON_TYPE RV_MON_PER_TASK
> +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
> +#define HA_TIMER_TYPE HA_TIMER_HRTIMER
> +#include "test_ha_kunit.h"
> +#include <rv/ha_monitor.h>
> +
> +/*
> + * This is the instrumentation part of the monitor.
> + *
> + * This is the section where manual work is required. Here the kernel events
> + * are translated into model's event.
> + *
> + */
> +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
> +
> +#define FOO_NS /* XXX: what is FOO_NS? */
> +
> +static inline u64 bar_ns(struct ha_monitor *ha_mon)
> +{
> +	return /* XXX: what is bar_ns(ha_mon)? */;
> +}
> +
> +static u64 foo_ns = /* XXX: default value */;
> +module_param(foo_ns, ullong, 0644);
> +
> +/*
> + * These functions define how to read and reset the environment variable.
> + *
> + * Common environment variables like ns-based and jiffy-based clocks have
> + * pre-define getters and resetters you can use. The parser can infer the type
> + * of the environment variable if you supply a measure unit in the constraint.
> + * If you define your own functions, make sure to add appropriate memory
> + * barriers if required.
> + * Some environment variables don't require a storage as they read a system
> + * state (e.g. preemption count). Those variables are never reset, so we don't
> + * define a reset function on monitors only relying on this type of variables.
> + */
> +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
> +{
> +	if (env == clk_test_ha_kunit)
> +		return ha_get_clk_ns(ha_mon, env, time_ns);
> +	else if (env == env1_test_ha_kunit)
> +		return /* XXX: how do I read env1? */
> +	else if (env == env2_test_ha_kunit)
> +		return /* XXX: how do I read env2? */
> +	return ENV_INVALID_VALUE;
> +}
> +
> +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
> +{
> +	if (env == clk_test_ha_kunit)
> +		ha_reset_clk_ns(ha_mon, env, time_ns);
> +}
> +
> +/*
> + * These functions are used to validate state transitions.
> + *
> + * They are generated by parsing the model, there is usually no need to change them.
> + * If the monitor requires a timer, there are functions responsible to arm it when
> + * the next state has a constraint, cancel it in any other case and to check
> + * that it didn't expire before the callback run. Transitions to the same state
> + * without a reset never affect timers.
> + * Due to the different representations between invariants and guards, there is
> + * a function to convert it in case invariants or guards are reachable from
> + * another invariant without reset. Those are not present if not required in
> + * the model. This is all automatic but is worth checking because it may show
> + * errors in the model (e.g. missing resets).
> + */
> +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
> +					enum states curr_state, enum events event,
> +					enum states next_state, u64 time_ns)
> +{
> +	if (curr_state == S0_test_ha_kunit)
> +		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns);
> +	else if (curr_state == S2_test_ha_kunit)
> +		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns);
> +	return true;
> +}
> +
> +static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
> +					enum states curr_state, enum events event,
> +					enum states next_state, u64 time_ns)
> +{
> +	if (curr_state == next_state)
> +		return;
> +	if (curr_state == S2_test_ha_kunit)
> +		ha_inv_to_guard(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns);
> +}
> +
> +static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
> +				    enum states curr_state, enum events event,
> +				    enum states next_state, u64 time_ns)
> +{
> +	bool res = true;
> +
> +	if (curr_state == S0_test_ha_kunit && event == event0_test_ha_kunit)
> +		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
> +	else if (curr_state == S0_test_ha_kunit && event == event1_test_ha_kunit)
> +		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
> +	else if (curr_state == S1_test_ha_kunit && event == event0_test_ha_kunit)
> +		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
> +	else if (curr_state == S1_test_ha_kunit && event == event2_test_ha_kunit) {
> +		res = ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 0ull;
> +		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
> +	} else if (curr_state == S2_test_ha_kunit && event == event1_test_ha_kunit)
> +		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
> +		      ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < foo_ns;
> +	else if (curr_state == S3_test_ha_kunit && event == event0_test_ha_kunit)
> +		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
> +		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < FOO_NS &&
> +		      ha_get_env(ha_mon, env2_test_ha_kunit, time_ns) == 0ull);
> +	else if (curr_state == S3_test_ha_kunit && event == event1_test_ha_kunit) {
> +		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
> +		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < 5000ull &&
> +		      ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 1ull);
> +		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
> +	}
> +	return res;
> +}
> +
> +static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
> +				       enum states curr_state, enum events event,
> +				       enum states next_state, u64 time_ns)
> +{
> +	if (next_state == curr_state && event != event0_test_ha_kunit)
> +		return;
> +	if (next_state == S0_test_ha_kunit)
> +		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, bar_ns(ha_mon), time_ns);
> +	else if (next_state == S2_test_ha_kunit)
> +		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns);
> +	else if (curr_state == S0_test_ha_kunit)
> +		ha_cancel_timer(ha_mon);
> +	else if (curr_state == S2_test_ha_kunit)
> +		ha_cancel_timer(ha_mon);
> +}
> +
> +static bool ha_verify_constraint(struct ha_monitor *ha_mon,
> +				 enum states curr_state, enum events event,
> +				 enum states next_state, u64 time_ns)
> +{
> +	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
> +		return false;
> +
> +	ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
> +
> +	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
> +		return false;
> +
> +	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
> +
> +	return true;
> +}
> +
> +static void handle_event0(void *data, /* XXX: fill header */)
> +{
> +	/* XXX: validate that this event always leads to the initial state */
> +	struct task_struct *p = /* XXX: how do I get p? */;
> +	da_handle_start_event(p, event0_test_ha_kunit);
> +}
> +
> +static void handle_event1(void *data, /* XXX: fill header */)
> +{
> +	struct task_struct *p = /* XXX: how do I get p? */;
> +	da_handle_event(p, event1_test_ha_kunit);
> +}
> +
> +static void handle_event2(void *data, /* XXX: fill header */)
> +{
> +	struct task_struct *p = /* XXX: how do I get p? */;
> +	da_handle_event(p, event2_test_ha_kunit);
> +}
> +
> +static int enable_test_ha_kunit(void)
> +{
> +	int retval;
> +
> +	retval = ha_monitor_init();
> +	if (retval)
> +		return retval;
> +
> +	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
> +	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
> +	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
> +
> +	return 0;
> +}
> +
> +static void disable_test_ha_kunit(void)
> +{
> +	rv_this.enabled = 0;
> +
> +	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
> +	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
> +	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
> +
> +	ha_monitor_destroy();
> +}
> +
> +/*
> + * This is the monitor register section.
> + */
> +static struct rv_monitor rv_this = {
> +	.name = "test_ha_kunit",
> +	.description = "auto-generated",
> +	.enable = enable_test_ha_kunit,
> +	.disable = disable_test_ha_kunit,
> +	.reset = da_monitor_reset_all,
> +	.enabled = 0,
> +};
> +
> +static int __init register_test_ha_kunit(void)
> +{
> +	return rv_register_monitor(&rv_this, NULL);
> +}
> +
> +static void __exit unregister_test_ha_kunit(void)
> +{
> +	rv_unregister_monitor(&rv_this);
> +}
> +
> +module_init(register_test_ha_kunit);
> +module_exit(unregister_test_ha_kunit);
> +
> +MODULE_LICENSE("GPL");
> +MODULE_AUTHOR("dot2k: auto-generated");
> +MODULE_DESCRIPTION("test_ha_kunit: auto-generated");
> +
> +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
> +#include <kunit/visibility.h>
> +#include "test_ha_kunit_kunit.h"
> +
> +const struct rv_test_ha_kunit_ops rv_test_ha_kunit_ops = {
> +	.mon = {
> +		.rv_this = &rv_this,
> +		.monitor_init = ha_monitor_init,
> +		.monitor_destroy = ha_monitor_destroy,
> +	},
> +	.handle_event0 = handle_event0,
> +	.handle_event1 = handle_event1,
> +	.handle_event2 = handle_event2,
> +};
> +EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops);
> +#endif
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h
> new file mode 100644
> index 0000000000..5c428f818b
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h
> @@ -0,0 +1,88 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Automatically generated C representation of test_ha_kunit automaton
> + * For further information about this format, see kernel documentation:
> + *   Documentation/trace/rv/deterministic_automata.rst
> + */
> +
> +#define MONITOR_NAME test_ha_kunit
> +
> +enum states_test_ha_kunit {
> +	S0_test_ha_kunit,
> +	S1_test_ha_kunit,
> +	S2_test_ha_kunit,
> +	S3_test_ha_kunit,
> +	state_max_test_ha_kunit,
> +};
> +
> +#define INVALID_STATE state_max_test_ha_kunit
> +
> +enum events_test_ha_kunit {
> +	event0_test_ha_kunit,
> +	event1_test_ha_kunit,
> +	event2_test_ha_kunit,
> +	event_max_test_ha_kunit,
> +};
> +
> +enum envs_test_ha_kunit {
> +	clk_test_ha_kunit,
> +	env1_test_ha_kunit,
> +	env2_test_ha_kunit,
> +	env_max_test_ha_kunit,
> +	env_max_stored_test_ha_kunit = env1_test_ha_kunit,
> +};
> +
> +_Static_assert(env_max_stored_test_ha_kunit <= MAX_HA_ENV_LEN, "Not enough slots");
> +#define HA_CLK_NS
> +
> +struct automaton_test_ha_kunit {
> +	char *state_names[state_max_test_ha_kunit];
> +	char *event_names[event_max_test_ha_kunit];
> +	char *env_names[env_max_test_ha_kunit];
> +	unsigned char function[state_max_test_ha_kunit][event_max_test_ha_kunit];
> +	unsigned char initial_state;
> +	bool final_states[state_max_test_ha_kunit];
> +};
> +
> +static const struct automaton_test_ha_kunit automaton_test_ha_kunit = {
> +	.state_names = {
> +		"S0",
> +		"S1",
> +		"S2",
> +		"S3",
> +	},
> +	.event_names = {
> +		"event0",
> +		"event1",
> +		"event2",
> +	},
> +	.env_names = {
> +		"clk",
> +		"env1",
> +		"env2",
> +	},
> +	.function = {
> +		{
> +			S0_test_ha_kunit,
> +			S1_test_ha_kunit,
> +			INVALID_STATE,
> +		},
> +		{
> +			S0_test_ha_kunit,
> +			INVALID_STATE,
> +			S2_test_ha_kunit,
> +		},
> +		{
> +			INVALID_STATE,
> +			S2_test_ha_kunit,
> +			S3_test_ha_kunit,
> +		},
> +		{
> +			S0_test_ha_kunit,
> +			S1_test_ha_kunit,
> +			INVALID_STATE,
> +		},
> +	},
> +	.initial_state = S0_test_ha_kunit,
> +	.final_states = { 1, 0, 0, 0 },
> +};
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c
> new file mode 100644
> index 0000000000..730a9a26a0
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c
> @@ -0,0 +1,29 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/kernel.h>
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +/*
> + * XXX: include required headers, e.g.,
> + * #include <linux/sched.h>
> + */
> +#include "test_ha_kunit_kunit.h"
> +
> +#if IS_REACHABLE(CONFIG_RV_MON_TEST_HA_KUNIT)
> +
> +static void rv_test_test_ha_kunit(struct kunit *test)
> +{
> +	struct rv_kunit_ctx *ctx = test->priv;
> +
> +	prepare_test(test, &rv_test_ha_kunit_ops.mon);
> +
> +	/*
> +	 * XXX: write the test here
> +	 * e.g.
> +	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
> +	 *	rv_test_ha_kunit_ops.handle_event(args);
> +	 */
> +}
> +
> +#else
> +#define rv_test_test_ha_kunit rv_test_stub
> +#endif
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h
> new file mode 100644
> index 0000000000..0b2030cb64
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h
> @@ -0,0 +1,24 @@
> +/* SPDX-License-Identifier: GPL-2.0-only */
> +/*
> + * Automatically generated by rvgen kunit.
> + * May need manual intervention for function prototypes that couldn't be
> + * found (e.g. are in another file) or variables to be exported.
> + */
> +
> +#ifndef __TEST_HA_KUNIT_KUNIT_H
> +#define __TEST_HA_KUNIT_KUNIT_H
> +
> +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
> +
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +
> +extern const struct rv_test_ha_kunit_ops {
> +	struct rv_kunit_mon mon;
> +	void (*handle_event0)(void *data, /* XXX: fill header */);
> +	void (*handle_event1)(void *data, /* XXX: fill header */);
> +	void (*handle_event2)(void *data, /* XXX: fill header */);
> +} rv_test_ha_kunit_ops;
> +#endif
> +
> +#endif /* __TEST_HA_KUNIT_KUNIT_H */
> diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h
> new file mode 100644
> index 0000000000..6c13ee0068
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h
> @@ -0,0 +1,19 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +
> +/*
> + * Snippet to be included in rv_trace.h
> + */
> +
> +#ifdef CONFIG_RV_MON_TEST_HA_KUNIT
> +DEFINE_EVENT(event_da_monitor_id, event_test_ha_kunit,
> +	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
> +	     TP_ARGS(id, state, event, next_state, final_state));
> +
> +DEFINE_EVENT(error_da_monitor_id, error_test_ha_kunit,
> +	     TP_PROTO(int id, char *state, char *event),
> +	     TP_ARGS(id, state, event));
> +
> +DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha_kunit,
> +	     TP_PROTO(int id, char *state, char *event, char *env),
> +	     TP_ARGS(id, state, event, env));
> +#endif /* CONFIG_RV_MON_TEST_HA_KUNIT */
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig
> new file mode 100644
> index 0000000000..3e334c3442
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig
> @@ -0,0 +1,9 @@
> +# SPDX-License-Identifier: GPL-2.0-only
> +#
> +config RV_MON_TEST_LTL_KUNIT
> +	depends on RV
> +	# XXX: add dependencies if there
> +	select LTL_MON_EVENTS_ID
> +	bool "test_ltl_kunit monitor"
> +	help
> +	  auto-generated
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c
> new file mode 100644
> index 0000000000..5e95a0f462
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c
> @@ -0,0 +1,107 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/ftrace.h>
> +#include <linux/tracepoint.h>
> +#include <linux/kernel.h>
> +#include <linux/module.h>
> +#include <linux/init.h>
> +#include <linux/rv.h>
> +#include <rv/instrumentation.h>
> +
> +#define MODULE_NAME "test_ltl_kunit"
> +
> +/*
> + * XXX: include required tracepoint headers, e.g.,
> + * #include <trace/events/sched.h>
> + */
> +#include <rv_trace.h>
> +
> +
> +/*
> + * This is the self-generated part of the monitor. Generally, there is no need
> + * to touch this section.
> + */
> +#include "test_ltl_kunit.h"
> +#include <rv/ltl_monitor.h>
> +
> +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
> +{
> +	/*
> +	 * This is called everytime the Buchi automaton is triggered.
> +	 *
> +	 * This function could be used to fetch the atomic propositions which
> +	 * are expensive to trace. It is possible only if the atomic proposition
> +	 * does not need to be updated at precise time.
> +	 *
> +	 * It is recommended to use tracepoints and ltl_atom_update() instead.
> +	 */
> +}
> +
> +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
> +{
> +	/*
> +	 * This should initialize as many atomic propositions as possible.
> +	 *
> +	 * @task_creation indicates whether the task is being created. This is
> +	 * false if the task is already running before the monitor is enabled.
> +	 */
> +	ltl_atom_set(mon, LTL_EVENT_A, true/false);
> +	ltl_atom_set(mon, LTL_EVENT_B, true/false);
> +}
> +
> +/*
> + * This is the instrumentation part of the monitor.
> + *
> + * This is the section where manual work is required. Here the kernel events
> + * are translated into model's event.
> + */
> +static void handle_example_event(void *data, /* XXX: fill header */)
> +{
> +	ltl_atom_update(task, LTL_EVENT_A, true/false);
> +}
> +
> +static int enable_test_ltl_kunit(void)
> +{
> +	int retval;
> +
> +	retval = ltl_monitor_init();
> +	if (retval)
> +		return retval;
> +
> +	rv_attach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event);
> +
> +	return 0;
> +}
> +
> +static void disable_test_ltl_kunit(void)
> +{
> +	rv_detach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_sample_event);
> +

one typo:
        handle_sample_event should be handle_example_event.

--
Wen

> +	ltl_monitor_destroy();
> +}
> +
> +/*
> + * This is the monitor register section.
> + */
> +static struct rv_monitor rv_this = {
> +	.name = "test_ltl_kunit",
> +	.description = "auto-generated",
> +	.enable = enable_test_ltl_kunit,
> +	.disable = disable_test_ltl_kunit,
> +};
> +
> +static int __init register_test_ltl_kunit(void)
> +{
> +	return rv_register_monitor(&rv_this, NULL);
> +}
> +
> +static void __exit unregister_test_ltl_kunit(void)
> +{
> +	rv_unregister_monitor(&rv_this);
> +}
> +
> +module_init(register_test_ltl_kunit);
> +module_exit(unregister_test_ltl_kunit);
> +
> +MODULE_LICENSE("GPL");
> +MODULE_AUTHOR(/* TODO */);

Please use a valid string here.


--
Wen

> +MODULE_DESCRIPTION("test_ltl_kunit: auto-generated");
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h
> new file mode 100644
> index 0000000000..acc503b56e
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h
> @@ -0,0 +1,108 @@
> +/* 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_kunit
> +
> +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;
> +	}
> +}
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c
> new file mode 100644
> index 0000000000..f64faef1b0
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c
> @@ -0,0 +1,29 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/kernel.h>
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +/*
> + * XXX: include required headers, e.g.,
> + * #include <linux/sched.h>
> + */
> +#include "test_ltl_kunit_kunit.h"
> +
> +#if IS_REACHABLE(CONFIG_RV_MON_TEST_LTL_KUNIT)
> +
> +static void rv_test_test_ltl_kunit(struct kunit *test)
> +{
> +	struct rv_kunit_ctx *ctx = test->priv;
> +
> +	prepare_test(test, &rv_test_ltl_kunit_ops.mon);
> +
> +	/*
> +	 * XXX: write the test here
> +	 * e.g.
> +	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
> +	 *	rv_test_ltl_kunit_ops.handle_event(args);
> +	 */
> +}
> +
> +#else
> +#define rv_test_test_ltl_kunit rv_test_stub
> +#endif
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h
> new file mode 100644
> index 0000000000..b2ca34be32
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h
> @@ -0,0 +1,22 @@
> +/* SPDX-License-Identifier: GPL-2.0-only */
> +/*
> + * Automatically generated by rvgen kunit.
> + * May need manual intervention for function prototypes that couldn't be
> + * found (e.g. are in another file) or variables to be exported.
> + */
> +
> +#ifndef __TEST_LTL_KUNIT_KUNIT_H
> +#define __TEST_LTL_KUNIT_KUNIT_H
> +
> +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
> +
> +#include <linux/rv.h>
> +#include <rv/kunit.h>
> +
> +extern const struct rv_test_ltl_kunit_ops {
> +	struct rv_kunit_mon mon;
> +	void (*handle_example_event)(void *data, /* XXX: fill header */);
> +} rv_test_ltl_kunit_ops;
> +#endif
> +
> +#endif /* __TEST_LTL_KUNIT_KUNIT_H */
> diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h
> new file mode 100644
> index 0000000000..a054d5b2c0
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h
> @@ -0,0 +1,14 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +
> +/*
> + * Snippet to be included in rv_trace.h
> + */
> +
> +#ifdef CONFIG_RV_MON_TEST_LTL_KUNIT
> +DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl_kunit,
> +	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
> +	     TP_ARGS(task, states, atoms, next));
> +DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl_kunit,
> +	     TP_PROTO(struct task_struct *task),
> +	     TP_ARGS(task));
> +#endif /* CONFIG_RV_MON_TEST_LTL_KUNIT */
> diff --git a/tools/verification/rvgen/tests/rvgen_kunit.t b/tools/verification/rvgen/tests/rvgen_kunit.t
> new file mode 100644
> index 0000000000..174a6fac0b
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/rvgen_kunit.t
> @@ -0,0 +1,32 @@
> +#!/bin/bash
> +# SPDX-License-Identifier: GPL-2.0
> +source ../tests/engine.sh
> +test_begin
> +
> +set_timeout 30s
> +
> +# Help tests
> +check "verify kunit subcommand help" \
> +	"$RVGEN kunit -h" 0 "model_name" "spec"
> +
> +check_and_compare_folder "KUnit generation with local lookup and test_da_kunit" \
> +	"$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu -n test_da_kunit && $RVGEN kunit -a -l -n test_da_kunit" \
> +	"test_da_kunit" "Now complete the test and add it to rv_monitors_test.c" "monitor_init"
> +
> +check_and_compare_folder "KUnit generation with local lookup and test_ha_kunit" \
> +	"$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task -n test_ha_kunit && $RVGEN kunit -a -l -n test_ha_kunit" \
> +	"test_ha_kunit" "Successfully created KUnit" "Append the following to"
> +
> +check_and_compare_folder "KUnit generation with local lookup and test_ltl_kunit" \
> +	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_ltl_kunit && $RVGEN kunit -l -n test_ltl_kunit" \
> +	"test_ltl_kunit" "monitor_init = ltl_monitor_init"
> +
> +# Error handling tests
> +check "missing required model_name" \
> +	"$RVGEN kunit" 2 "the following arguments are required: -n/--model_name"
> +
> +check "non-existent model_name with auto_patch" \
> +	"$RVGEN kunit -a -n nonexistent" 1 \
> +	"Could not find monitor C file" "Traceback (most recent call last)"
> +
> +test_end