include/rv/automata.h

Source file repositories/reference/linux-study-clean/include/rv/automata.h

File Facts

System
Linux kernel
Corpus path
include/rv/automata.h
Extension
.h
Size
2115 bytes
Lines
82
Domain
Repository Root And Misc
Bucket
include
Inferred role
Repository Root And Misc: implementation source
Status
source implementation candidate

Why This File Exists

Top-level or miscellaneous repository surface. Use this as map coverage unless a later manual pass promotes the file into a deeper subsystem dossier.

Dependency Surface

Detected Declarations

Annotated Snippet

#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

Annotation

Implementation Notes