More flexible session trace output #1052
Labels
architectural decision
Discussion of design decision
generator
Related to generator package (SPARK code generation)
Context and Problem Statement
Debugging and validating a protocol session requires some insight into the transitions that the state machine performs. We currently have two mechanisms to achieve that: When the
--debug
flag is passed on therflx generate
command line, the state transitions and error output is printed to the console usingAda.Text_IO
. We use this for our own tests when running on Linux. The other option is to use theNext_State
function to return the next state in the main loop and print its value using the'Image
function.Both approaches are not ideal.
Ada.Text_IO
may not be available for on-target debugging in embedded systems when using a limited runtime. Printing the state names from the session context only reveals those states that follow an IO state - what happens in between cannot be observed. Furthermore, using'Image
may require runtime support which may not available or desirable.Use Cases
Ada.Text_IO
Considered Options
O1
Replace the current
Ada.Text_IO
andPut_Line
calls by a custom packageRFLX_Debug
with a procedureRFLX_Debug.Print (Text : String)
. The inclusion of the package and calls to thePrint
functions is governed by the presence of the--debug
flag.+ Little implementation effort
+ Simple, unified interface
+ Simple command line
−
RFLX_Debug
must be provided externally− No out-of-the box use of debug functionality
− No well-defined / checked API for
RFLX_Debug
O1a
Like O2, but a specification file for
RFLX_Debug
is generated.+ Moderate implementation effort
+ Simple, unified interface
+ Simple command line
−
RFLX_Debug
body must be provided externally− No out-of-the box use of debug functionality
O1b
Like O1, but the
RFLX_Debug
package with a default implementation mapping toAda.Text_IO
is generated. An optional parameterspec
can be passed to the--debug
switch in which case the default body would not be generated.+ Default behavior as convenient as current behavior
+ Compatible with current solution
− More complex to implement
− May result in conflicts between custom and generated trace packages
O2
Include
Ada.Text_IO
and generate calls toPut_Line
as before if the--debug
flag is used. A new optional parameterexternal
can be passed to--debug
which includesRFLX_Debug
and generates calls toPrint
. The spec and code forRFLX_Debug
must be provided by the user.+ Default behavior as convenient as current behavior
+ Compatible with current solution
− Slightly more complex to implement than O1
− No well-defined / checked API for
RFLX_Debug
O2b
Like O2, but a specification is generated for
RFLX_Debug
.+ Default behavior as convenient as current behavior
+ Compatible with current solution
− Slightly more complex to implement than O1
Decision Outcome
O2b
The text was updated successfully, but these errors were encountered: