+
Point of view
All features
class AUTOMATON [E_]
Summary
top
Direct parents
Insert list: ANY
Class invariant
top
Overview
top
Creation features
Features
Simple one-shot execution
{ANY}
Step-by-step execution
{ANY}
{}
{STATE}
{ANY}
{}
{}
run (start_state: ABSTRACT_STRING, e: E_)
effective procedure
{ANY}
top
require
  • has(start_state)
has (state_name: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
top
require
  • state_name /= Void
start (start_state: ABSTRACT_STRING, e: E_): AUTOMATON_CONTEXT[E_]
effective function
{ANY}
top
require
  • has(start_state)
ensure
  • Result.is_valid
  • Result.current_state /= Void
next (context: AUTOMATON_CONTEXT[E_])
effective procedure
{ANY}
top
require
  • context.is_valid
next_transition (from_state: STATE[E_], state_name: ABSTRACT_STRING, e: E_): STATE[E_]
effective function
{}
top
last_transition (from_state: STATE[E_], e: E_)
effective procedure
{}
top
require
  • from_state /= Void
call_before_guards (e: E_, state: STATE[E_])
effective procedure
{STATE}
top
call_after_guards (e: E_, state: STATE[E_])
effective procedure
{STATE}
top
set_before_guards (p: PROCEDURE[TUPLE[TUPLE 2[E_, STATE[E_]]]])
effective procedure
{ANY}
top
ensure
set_after_guards (p: PROCEDURE[TUPLE[TUPLE 2[E_, STATE[E_]]]])
effective procedure
{ANY}
top
ensure
set_transition (p: PROCEDURE[TUPLE[TUPLE 3[E_, STATE[E_], STATE[E_]]]])
effective procedure
{ANY}
top
ensure
states: DICTIONARY[STATE[E_], FIXED_STRING]
writable attribute
{}
top
A dictionary of all the states
before_guards: PROCEDURE[TUPLE[TUPLE 2[E_, STATE[E_]]]]
writable attribute
{}
top
That agent is called before checking guards.
The given state is the current one.
after_guards: PROCEDURE[TUPLE[TUPLE 2[E_, STATE[E_]]]]
writable attribute
{}
top
That agent is called after checking guards, whether a guard was raised or not.
The given state the current one.
transition: PROCEDURE[TUPLE[TUPLE 3[E_, STATE[E_], STATE[E_]]]]
writable attribute
{}
top
That agent is called when the next state was found.
The given states are resp. the current one (Void if first transition) and the successor (Void is last transition).
default_before_guards
effective procedure
{}
top
default_after_guards
effective procedure
{}
top
default_transition
effective procedure
{}
top
manifest_make (needed_capacity: INTEGER_32)
effective procedure
{}
top
manifest_put (index: INTEGER_32, state_name: ABSTRACT_STRING, state: STATE[E_])
effective procedure
{}
top
require
  • index >= 0
  • not states.fast_has(state_name.intern)
ensure
  • states.fast_has(state_name.intern)
manifest_semicolon_check: INTEGER_32
is 2
constant attribute
{}
top