82 lines
2.1 KiB
C
82 lines
2.1 KiB
C
/* SPDX-License-Identifier: GPL-2.0 */
|
|
/*
|
|
* Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
|
|
*
|
|
* Deterministic automata helper functions, to be used with the automata
|
|
* models in C generated by the dot2k tool.
|
|
*/
|
|
|
|
#ifndef _RV_AUTOMATA_H
|
|
#define _RV_AUTOMATA_H
|
|
|
|
#ifndef MONITOR_NAME
|
|
#error "MONITOR_NAME macro is not defined. Did you include $(MODEL_NAME).h generated by rvgen?"
|
|
#endif
|
|
|
|
#define RV_AUTOMATON_NAME CONCATENATE(automaton_, MONITOR_NAME)
|
|
#define EVENT_MAX CONCATENATE(event_max_, MONITOR_NAME)
|
|
#define STATE_MAX CONCATENATE(state_max_, MONITOR_NAME)
|
|
#define events CONCATENATE(events_, MONITOR_NAME)
|
|
#define states CONCATENATE(states_, MONITOR_NAME)
|
|
|
|
/*
|
|
* model_get_state_name - return the (string) name of the given state
|
|
*/
|
|
static char *model_get_state_name(enum states state)
|
|
{
|
|
if ((state < 0) || (state >= STATE_MAX))
|
|
return "INVALID";
|
|
|
|
return RV_AUTOMATON_NAME.state_names[state];
|
|
}
|
|
|
|
/*
|
|
* model_get_event_name - return the (string) name of the given event
|
|
*/
|
|
static char *model_get_event_name(enum events event)
|
|
{
|
|
if ((event < 0) || (event >= EVENT_MAX))
|
|
return "INVALID";
|
|
|
|
return RV_AUTOMATON_NAME.event_names[event];
|
|
}
|
|
|
|
/*
|
|
* model_get_initial_state - return the automaton's initial state
|
|
*/
|
|
static inline enum states model_get_initial_state(void)
|
|
{
|
|
return RV_AUTOMATON_NAME.initial_state;
|
|
}
|
|
|
|
/*
|
|
* model_get_next_state - process an automaton event occurrence
|
|
*
|
|
* Given the current state (curr_state) and the event (event), returns
|
|
* the next state, or INVALID_STATE in case of error.
|
|
*/
|
|
static inline enum states model_get_next_state(enum states curr_state,
|
|
enum events event)
|
|
{
|
|
if ((curr_state < 0) || (curr_state >= STATE_MAX))
|
|
return INVALID_STATE;
|
|
|
|
if ((event < 0) || (event >= EVENT_MAX))
|
|
return INVALID_STATE;
|
|
|
|
return RV_AUTOMATON_NAME.function[curr_state][event];
|
|
}
|
|
|
|
/*
|
|
* model_is_final_state - check if the given state is a final state
|
|
*/
|
|
static inline bool model_is_final_state(enum states state)
|
|
{
|
|
if ((state < 0) || (state >= STATE_MAX))
|
|
return 0;
|
|
|
|
return RV_AUTOMATON_NAME.final_states[state];
|
|
}
|
|
|
|
#endif
|