GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
libraries
>
AUTOMATON
+
Point of view
All features
ANY
STATE
All features
class AUTOMATON [E_]
Summary
top
Direct parents
Insert list:
ANY
Class invariant
top
states
/= Void
before_guards
/= Void
after_guards
/= Void
transition
/= Void
Overview
top
Creation features
Features
Simple one-shot execution
{
ANY
}
run
(start_state:
ABSTRACT_STRING
, e: E_)
has
(state_name:
ABSTRACT_STRING
):
BOOLEAN
Step-by-step execution
{
ANY
}
start
(start_state:
ABSTRACT_STRING
, e: E_): AUTOMATON_CONTEXT[E_]
next
(context: AUTOMATON_CONTEXT[E_])
{}
next_transition
(from_state: STATE[E_], state_name:
ABSTRACT_STRING
, e: E_): STATE[E_]
last_transition
(from_state: STATE[E_], e: E_)
{
STATE
}
call_before_guards
(e: E_, state: STATE[E_])
call_after_guards
(e: E_, state: STATE[E_])
{
ANY
}
set_before_guards
(p:
PROCEDURE
[
TUPLE
[TUPLE 2[E_, STATE[E_]]]])
set_after_guards
(p:
PROCEDURE
[
TUPLE
[TUPLE 2[E_, STATE[E_]]]])
set_transition
(p:
PROCEDURE
[
TUPLE
[TUPLE 3[E_, STATE[E_], STATE[E_]]]])
{}
states
: DICTIONARY[STATE[E_],
FIXED_STRING
]
A dictionary of all the states
before_guards
:
PROCEDURE
[
TUPLE
[TUPLE 2[E_, STATE[E_]]]]
That agent is called before checking guards.
after_guards
:
PROCEDURE
[
TUPLE
[TUPLE 2[E_, STATE[E_]]]]
That agent is called after checking guards, whether a guard was raised or not.
transition
:
PROCEDURE
[
TUPLE
[TUPLE 3[E_, STATE[E_], STATE[E_]]]]
That agent is called when the next state was found.
default_before_guards
default_after_guards
default_transition
{}
manifest_make
(needed_capacity:
INTEGER_32
)
manifest_put
(index:
INTEGER_32
, state_name:
ABSTRACT_STRING
, state: STATE[E_])
manifest_semicolon_check
:
INTEGER_32
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
before_guards
= p
set_after_guards
(p:
PROCEDURE
[
TUPLE
[TUPLE 2[E_, STATE[E_]]]])
effective procedure
{
ANY
}
top
ensure
after_guards
= p
set_transition
(p:
PROCEDURE
[
TUPLE
[TUPLE 3[E_, STATE[E_], STATE[E_]]]])
effective procedure
{
ANY
}
top
ensure
transition
= p
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