RecordFlux
RecordFlux copied to clipboard
AdaCore
Parameterized specifications
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
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.
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;
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: @.***>