Parameterized specifications

treiher commented 2 years ago

Context and Problem Statement

In some cases, it would be beneficial to parameterize the code generation.

Use Cases

UC1 Enable different feature sets (i.e. remove parts of sessions or messages)
UC2 Reduce memory requirements for messages (i.e. restrict possible message length)

Considered Options

O1 Explicit annotations

Specification

These use cases could be realized by making a specification parameterizable. The parameters could be defined in a generic part of a package:

generic
   P : Boolean;
   Q : range 1 .. 42;
package Test is

The parameter type can be a scalar type: A built-in type like Boolean or an anonymous range type.

UC1 could be realized by marking all transitions, states and functions related to a feature with an aspect.

generic
   Feature_X : Boolean;
package Test is
  generic
      with function F1 return Boolean;
      with function F2 return Boolean with Required => Feature_X;
   session Session is

      state S1
      is
      begin
         Transport'Read (Request);
      transition
         goto S2
            with Required => Feature_X
            if Request'Valid and Request.Code = Foo
         goto S3
            if Request'Valid and Request.Code = Bar
         goto Error_Invalid_Request
      end S1;

      state S2 with
         Required => Feature_X
      is

Alternatively, a condition depending on a parameter could be added to all transitions related to a feature. In that case, conditions which get statically false due to a parameter value must be ignored during code generation (and must not be detected as invalid during model verification). It would be necessary, to detect which states and functions only get unreachable because of a parameter (Is that even possible in the general case?) or related states and functions would need to be marked explicitly again.

More complex verification of the state machine (e.g., model checking) would likely need to be performed for each possible variant.

UC2 could be realized by adding a field condition depending on a parameter:

generic
   Max_Length : range 1 .. 2**16 - 1;
package Test is
   type Length is mod 2 ** 16;

   type Message is
      message
         Length : Length;
         Value  : Opaque
            with Size => Length * 8
            if Length <= Max_Length;
      end message;

Code Generation

The concrete values for the parameters could be defined in the integration file, i.e., only one specific variant is generated.

+ − Using an aspect to define that some entity does not exist is unusual (naming the aspect Required is probably also not optimal) − Annotating transitions seem to be redundant (annotating states should be sufficient)

O2 Explicit annotation of transitions

Implicit removal of states or functions.

Specification

generic
   Feature_X : Boolean;
package Test is
  generic
      with function F1 return Boolean;
      with function F2 return Boolean;
   session Session is

      state S1
      is
      begin
         Transport'Read (Request);
      transition
         goto S2
            if Request'Valid and Request.Code = Foo and Feature_X
         goto S3
            if Request'Valid and Request.Code = Bar
         goto Error_Invalid_Request
      end S1;

      state S2
      is

− Implicit removal of unreachable states and unused function can be confusing − Potential difficulties in finding out if a state or function was implicitly removed due to a formal parameter or due to a mistake in the specification

O3 Explicit annotation of states and functions

Implicit removal of transitions. No implicit removal of states or functions.

Specification

O3.1

generic
   Feature_X : Boolean;
package Test is
  generic
      with function F1 return Boolean;
      with function F2 return Boolean is null if not Feature_X;
   session Session is

      state S1
      is
      begin
         Transport'Read (Request);
      transition
         goto S2
            if Request'Valid and Request.Code = Foo
         goto S3
            if Request'Valid and Request.Code = Bar
         goto Error_Invalid_Request
      end S1;

      state S2
      is null if not Feature_X else
         ...
      begin
         ...

− is null if syntax is rather strange

O3.2

generic
   Feature_X : Boolean;
package Test is
   generic
      with function F1 return Boolean;
      with function F2 return Boolean if Feature_X;
   session Session is
      state S1
      is
      begin
         Transport'Read (Request);
      transition
         goto S2
            if Request'Valid and Request.Code = Foo
         goto S3
            if Request'Valid and Request.Code = Bar
         goto Error_Invalid_Request
      end S1;

      state S2
         if Feature_X
      is
         ...
      begin
         ...
      end S2;

TODO: We should find another keyword than if (e.g., when, present if, only if, requires, for) to differentiate it from existing uses of if (e.g., make it possible to make message fields optional).

+ −

Decision Outcome

TBD

sttaft commented 2 years ago

It might make more sense to treat the generic formals directly as aspects, rather than adding the "Required =>" part. Hence, you could write "with Feature_X" for a Boolean formal, and for an enumeration you could write "with R => Bar".

Alternatively, use "when <bool-expr>" rather than "with Required => <bool-expr>".

In any case, the use of "Required =>" seems like unnecessary noise.

senier commented 1 year ago

How about given?

generic
   Feature_X : Boolean;
package Test is
   generic
      with function F1 return Boolean;
      with function F2 return Boolean given Feature_X;
   session Session is
      state S1
      is
      begin
         Transport'Read (Request);
      transition
         goto S2
            if Request'Valid and Request.Code = Foo
         goto S3
            if Request'Valid and Request.Code = Bar
         goto Error_Invalid_Request
      end S1;

      state S2
         given Feature_X
      is
         ...
      begin
         ...
      end S2;

sttaft commented 1 year ago

Not bad. It is unique! ;-)

I would suggest making several examples, using "when", "for", and "given" and share them with a somewhat wider circle, and see if you get any strong reactions either way.

-Tuck

On Thu, Dec 8, 2022 at 10:03 AM Alexander Senier @.***> wrote:

How about given?

generic Feature_X : Boolean;package Test is generic with function F1 return Boolean; with function F2 return Boolean given Feature_X; session Session is state S1 is begin Transport'Read (Request); transition goto S2 if Request'Valid and Request.Code = Foo goto S3 if Request'Valid and Request.Code = Bar goto Error_Invalid_Request end S1;
  state S2
     given Feature_X
  is
     ...
  begin
     ...
  end S2;
— Reply to this email directly, view it on GitHub https://github.com/Componolit/RecordFlux/issues/1035#issuecomment-1342868482, or unsubscribe https://github.com/notifications/unsubscribe-auth/AANZ4FJNNKC7DZHBPTS3IZDWMH2FTANCNFSM5WFQJDWA . You are receiving this because you commented.Message ID: @.***>

AdaCore / RecordFlux