RV_AUTOMATON_NAME
return RV_AUTOMATON_NAME.state_names[state];
return RV_AUTOMATON_NAME.event_names[event];
return RV_AUTOMATON_NAME.initial_state;
return RV_AUTOMATON_NAME.function[curr_state][event];
return RV_AUTOMATON_NAME.final_states[state];