Skip to content

Commit

Permalink
Add function for getting current state of session
Browse files Browse the repository at this point in the history 
Ref. #796
  • Loading branch information
@treiher
treiher committed Oct 7, 2021
1 parent 2bbf5b0 commit 73f35cf
Show file tree
Hide file tree
Showing 28 changed files with 356 additions and 267 deletions.
48 changes: 36 additions & 12 deletions rflx/generator/session.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ def execute(self) -> Sequence[Statement]:
), f'missing exception transition for state "{self.state.identifier}"'
return [
Assignment(
"State",
"Next_State",
Variable(f"S_{self.state.exception_transition.target}"),
),
*self.finalization,
Expand Down Expand Up @@ -470,6 +470,7 @@ def _create_state_machine(self) -> UnitPart:
)
unit += self._create_tick_procedure(self._session)
unit += self._create_run_procedure()
unit += self._create_state_function()
return (
self._create_declarations(self._session, evaluated_declarations.global_declarations)
+ unit
Expand All @@ -479,16 +480,20 @@ def _create_declarations(
self, session: model.Session, declarations: Sequence[Declaration]
) -> UnitPart:
return UnitPart(
[
EnumerationType(
"Session_State", {ID(f"S_{s.identifier}"): None for s in session.states}
),
],
private=[
*[
UseTypeClause(self._prefix * ID(t))
for t in self._session_context.used_types
if not model.is_builtin_type(t) and not model.is_internal_type(t)
],
EnumerationType(
"Session_State", {ID(f"S_{s.identifier}"): None for s in session.states}
ObjectDeclaration(
["Next_State"], "Session_State", Variable(f"S_{session.initial}")
),
ObjectDeclaration(["State"], "Session_State", Variable(f"S_{session.initial}")),
*declarations,
],
)
Expand Down Expand Up @@ -546,7 +551,7 @@ def _create_states(self, session: model.Session) -> UnitPart:
unit_body += [
SubprogramBody(
ProcedureSpecification(
ID(state.identifier), [OutParameter(["State"], "Session_State")]
ID(state.identifier), [OutParameter(["Next_State"], "Session_State")]
),
[
*evaluated_declarations.global_declarations,
Expand All @@ -563,13 +568,17 @@ def _create_states(self, session: model.Session) -> UnitPart:
t.condition.substituted(
self._substitution()
).ada_expr(),
[Assignment("State", Variable(f"S_{t.target}"))],
[
Assignment(
"Next_State", Variable(f"S_{t.target}")
)
],
)
for t in state.transitions[:-1]
],
[
Assignment(
"State",
"Next_State",
Variable(f"S_{state.transitions[-1].target}"),
)
],
Expand Down Expand Up @@ -640,7 +649,7 @@ def _create_active_function(session: model.Session) -> UnitPart:
private=[
ExpressionFunctionDeclaration(
specification,
NotEqual(Variable("State"), Variable(f"S_{session.final}")),
NotEqual(Variable("Next_State"), Variable(f"S_{session.final}")),
),
],
)
Expand Down Expand Up @@ -668,7 +677,7 @@ def _create_initialize_procedure(
declarations,
[
*initialization,
Assignment("State", Variable(f"S_{session.initial}")),
Assignment("Next_State", Variable(f"S_{session.initial}")),
],
),
],
Expand Down Expand Up @@ -697,7 +706,7 @@ def _create_finalize_procedure(
declarations,
[
*finalization,
Assignment("State", Variable(f"S_{session.final}")),
Assignment("Next_State", Variable(f"S_{session.final}")),
],
),
],
Expand All @@ -723,13 +732,13 @@ def _create_tick_procedure(
[],
[
CaseStatement(
Variable("State"),
Variable("Next_State"),
[
(
Variable(f"S_{s.identifier}"),
[
*self._debug_output(f"State: {s.identifier}"),
CallStatement(ID(s.identifier), [Variable("State")])
CallStatement(ID(s.identifier), [Variable("Next_State")])
if s.identifier != session.final
else NullStatement(),
],
Expand Down Expand Up @@ -776,6 +785,21 @@ def _create_run_procedure() -> UnitPart:
],
)

@staticmethod
def _create_state_function() -> UnitPart:
specification = FunctionSpecification("State", "Session_State")
return UnitPart(
[
SubprogramDeclaration(specification),
],
private=[
ExpressionFunctionDeclaration(
specification,
Variable("Next_State"),
)
],
)

def _evaluate_declarations(
self,
declarations: Iterable[decl.BasicDeclaration],
Expand Down
28 changes: 14 additions & 14 deletions tests/integration/parameterized_messages/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ package body RFLX.Test.Session with
SPARK_Mode
is

procedure Receive (State : out Session_State) with
procedure Receive (Next_State : out Session_State) with
Pre =>
Initialized,
Post =>
Expand All @@ -22,13 +22,13 @@ is
end;
Test.Message.Verify_Message (M_Ctx);
if Test.Message.Structural_Valid_Message (M_Ctx) then
State := S_Reply;
Next_State := S_Reply;
else
State := S_Terminated;
Next_State := S_Terminated;
end if;
end Receive;

procedure Reply (State : out Session_State) with
procedure Reply (Next_State : out Session_State) with
Pre =>
Initialized,
Post =>
Expand Down Expand Up @@ -89,28 +89,28 @@ is
RFLX_Types.Free (RFLX_Message_Buffer);
end;
if RFLX_Exception then
State := S_Error;
Next_State := S_Error;
return;
end if;
State := S_Terminated;
Next_State := S_Terminated;
end Reply;

procedure Error (State : out Session_State) with
procedure Error (Next_State : out Session_State) with
Pre =>
Initialized,
Post =>
Initialized
is
begin
State := S_Terminated;
Next_State := S_Terminated;
end Error;

procedure Initialize is
M_Buffer : RFLX_Types.Bytes_Ptr;
begin
M_Buffer := new RFLX_Types.Bytes'(RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
Test.Message.Initialize (M_Ctx, M_Buffer, Length => Test.Length'First, Extended => Boolean'First);
State := S_Receive;
Next_State := S_Receive;
end Initialize;

procedure Finalize is
Expand All @@ -122,18 +122,18 @@ is
pragma Warnings (On, """M_Ctx"" is set by ""Take_Buffer"" but not used after the call");
pragma Warnings (On, "unused assignment to ""M_Ctx""");
RFLX_Types.Free (M_Buffer);
State := S_Terminated;
Next_State := S_Terminated;
end Finalize;

procedure Tick is
begin
case State is
case Next_State is
when S_Receive =>
Receive (State);
Receive (Next_State);
when S_Reply =>
Reply (State);
Reply (Next_State);
when S_Error =>
Error (State);
Error (Next_State);
when S_Terminated =>
null;
end case;
Expand Down
13 changes: 9 additions & 4 deletions tests/integration/parameterized_messages/generated/rflx-test-session.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ is

pragma Unreferenced (C_Has_Data);

type Session_State is (S_Receive, S_Reply, S_Error, S_Terminated);

function Uninitialized return Boolean;

function Initialized return Boolean;
Expand Down Expand Up @@ -56,13 +58,13 @@ is

pragma Warnings (On, "subprogram ""Run"" has no effect");

function State return Session_State;

private

use type RFLX.RFLX_Types.Index;

type Session_State is (S_Receive, S_Reply, S_Error, S_Terminated);

State : Session_State := S_Receive;
Next_State : Session_State := S_Receive;

M_Ctx : Test.Message.Context;

Expand All @@ -75,6 +77,9 @@ private
and then M_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095);

function Active return Boolean is
(State /= S_Terminated);
(Next_State /= S_Terminated);

function State return Session_State is
(Next_State);

end RFLX.Test.Session;
30 changes: 15 additions & 15 deletions tests/integration/session_append_unconstrained/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ package body RFLX.Test.Session with
SPARK_Mode
is

procedure Start (State : out Session_State) with
procedure Start (Next_State : out Session_State) with
Pre =>
Initialized,
Post =>
Expand All @@ -25,7 +25,7 @@ is
not Universal.Options.Has_Element (Options_Ctx)
or Universal.Options.Available_Space (Options_Ctx) < 32
then
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -52,7 +52,7 @@ is
pragma Warnings (On, "unused assignment to ""RFLX_Element_Options_Ctx""");
end;
if RFLX_Exception then
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -65,7 +65,7 @@ is
not Universal.Options.Has_Element (Options_Ctx)
or Universal.Options.Available_Space (Options_Ctx) < 40
then
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -92,7 +92,7 @@ is
pragma Warnings (On, "unused assignment to ""RFLX_Element_Options_Ctx""");
end;
if RFLX_Exception then
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -105,7 +105,7 @@ is
not Universal.Options.Has_Element (Options_Ctx)
or Universal.Options.Available_Space (Options_Ctx) < 8
then
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand Down Expand Up @@ -135,7 +135,7 @@ is
if Universal.Message.Field_Size (Message_Ctx, Universal.Message.F_Options) = Universal.Options.Size (Options_Ctx) then
Universal.Message.Set_Options (Message_Ctx, Options_Ctx);
else
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -145,7 +145,7 @@ is
return;
end if;
else
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -155,7 +155,7 @@ is
return;
end if;
else
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -171,7 +171,7 @@ is
Universal_Message_Read (Message_Ctx);
end;
else
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -180,7 +180,7 @@ is
RFLX_Types.Free (Options_Buffer);
return;
end if;
State := S_Terminated;
Next_State := S_Terminated;
pragma Warnings (Off, "unused assignment to ""Options_Ctx""");
pragma Warnings (Off, """Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (Options_Ctx, Options_Buffer);
Expand All @@ -194,7 +194,7 @@ is
begin
Message_Buffer := new RFLX_Types.Bytes'(RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
Universal.Message.Initialize (Message_Ctx, Message_Buffer);
State := S_Start;
Next_State := S_Start;
end Initialize;

procedure Finalize is
Expand All @@ -206,14 +206,14 @@ is
pragma Warnings (On, """Message_Ctx"" is set by ""Take_Buffer"" but not used after the call");
pragma Warnings (On, "unused assignment to ""Message_Ctx""");
RFLX_Types.Free (Message_Buffer);
State := S_Terminated;
Next_State := S_Terminated;
end Finalize;

procedure Tick is
begin
case State is
case Next_State is
when S_Start =>
Start (State);
Start (Next_State);
when S_Terminated =>
null;
end case;
Expand Down
Loading

0 comments on commit 73f35cf

Please sign in to comment.