+
Point of view
All features
class STATE [E_]
Summary
top
Direct parents
Insert list: ANY
Class invariant
top
Overview
top
Creation features
Features
{ANY}
{AUTOMATON}
{}
  • guards: COLLECTION[FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]]]]]
    Each guard tests if the corresponding transition may be done.
  • transitions: COLLECTION[FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]], ]]]
    The transition gives the name of the successor state.
{}
writable attribute
{ANY}
top
set_name (a_name: FIXED_STRING)
effective procedure
{AUTOMATON}
top
require
  • a_name /= Void
  • set_once: name = Void
ensure
run (a: AUTOMATON[E_], e: E_): ABSTRACT_STRING
effective function
{AUTOMATON}
top
guards: COLLECTION[FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]]]]]
writable attribute
{}
top
Each guard tests if the corresponding transition may be done.
transitions: COLLECTION[FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]], ]]]
writable attribute
{}
top
The transition gives the name of the successor state.
manifest_make (needed_capacity: INTEGER_32)
effective procedure
{}
top
manifest_put (index: INTEGER_32, guard: FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]]]], transition: FUNCTION[TUPLE[TUPLE 2[E_, STATE[E_]], ]])
effective procedure
{}
top
require
  • index >= 0
manifest_semicolon_check: INTEGER_32
is 2
constant attribute
{}
top