Definition of initial and final state of session

[treiher]

Context and Problem Statement

The definition of the initial state requires the session aspect Initial and the definition of the final state requires the session aspect Final and a null state declaration. A minimal session specification looks as follows:

generic
session S with
   Initial => Foo,
   Final => Bar
is
begin
   state Foo is
   begin
   transition
      then Bar
   end Foo;

   state Bar is null state;
end S;

The current approach requires a lot of boilerplate just to be able to give individual names to the initial and final states. I have the impression that this is unnecessary.

Considered Options

O1 Remove null state

Having the Final aspect is sufficient, as the declaration of a null state doesn't add any information.

generic
session S with
   Initial => Foo,
   Final => Bar
is
begin
   state Foo is
   begin
   transition
      then Bar
   end Foo;
end S;

+ Less boilerplate
− Inconsistent to Initial aspect, as Final aspect doesn't refer to declared state

O2 Use keyword instead of null state and Final aspect

Similar to message specifications, null could be used to refer to the final state. Also, another keyword like Final would be possible, as it is very improbable that a user would like to use Final as a state name with another semantics.

generic
session S with
   Initial => Foo
is
begin
   state Foo is
   begin
   transition
      then null
   end Foo;
end S;

+ Less boilerplate
− No individual name for final state

O3 Define initial state by name instead of Initial aspect

The initial state must have a specific name (e.g., Initial).

In combination with O2:

generic
session S is
begin
   state Initial is
   begin
   transition
      then null
   end Initial;
end S;

+ Least boilerplate
− No individual name for initial state

O4 Define initial state by position instead of Initial aspect

The first declared state is considered as the initial state.

In combination with O2:

generic
session S is
begin
   state Foo is
   begin
   transition
      then null
   end Foo;
end S;

+ Least boilerplate

Decision Outcome

O2 and O4