openETCS / modeling

WP3 Top Level Project: to cover all tasks related with modeling
31 stars 42 forks source link

Usage of REAL types within the SCADE model #522

Open MarcBehrens opened 9 years ago

MarcBehrens commented 9 years ago

Dear developers,

since there are currently some restrictions in the usage of REAL typed variables in the railway sector, I would like to invite you to list here the use cases of the variabel you want to have typed REAL in order to clarify what the rationale is behind it.

MarcBehrens commented 9 years ago

@BenjaminBeichler @T12z yould you please detail on your design decisions for REAL type variables listing all use cases.

T12z commented 9 years ago

Sorry for the delayed response Marc,

we do have the SDM_Types_Pkg that centrally defines the types we use within Supervision. The basic types that map to real are:

The basic decisions that led to this:

  1. Due to acceleration, all braking curves and related calculations are based on squaring functions and inverse on the square root. The square root function is only defined for float types in SCADE and C.
  2. There are quite a few math calculations to be done within the package. Often chained and intermediate results are to be reused at different places. To avoid confusions and errors with values being of different scale we agreed to have only one representation (the basic SI) per physical magnitude.
  3. Using fixed-point integer-based operations may introduce quite some obfuscation into the already quite complex formulars. This adheres to the aim of formalizing the SRS rather than having a thoroughly tuned implementation.

Having said that, I am also aware of:

  1. We really have concentrated on formalizing the SRS. None of us (at least not that I am aware of) has done any proof that the data types in use and their resolution actually suffice the requirements in that they do not saturate and accumulate all transitions.
    • e.g. at a location of 88123 km adding distance made at 5 km/h at 100ms intervals may just not work (totally constructed)
    • yes, using real is just a way to obfuscate this problem, but using different tuned fixed-point integers complicates things by dimensions
  2. Coming from µC background I know that there are powerful sqrt implementations for integers, but a lot of analysis is need to get fix-point resolution right.
  3. We could shift real operations to innermost calculation routines at the cost of formalization traceability and men-power.

On a last 50ct, with the Scade version we are using, no types are strongly typed. When I compiled for nanoETCS I had to keep in mind that int is only guaranteed to have 16bit by C standards.

T12z commented 8 years ago

(groooming "my" issues) Issue-alive-check / update: @MarcBehrens What is the goal of this issue? What needs to be done to finalize this? Who is assigned?

As an updated information on SDM, when possible, I have started to refactor / clean away floats where they do not make a difference. (e.g. SDM_Commands - the SDM decision / output module, relating to SRS 26 / 3.13.10) The lambda-brake model has been done without ints where possible. Unfortunately there are basic types that have needlessly been defined real. I already had discussions on that but there was no action feedback to clean it up. see: #719 #794 I may need to enforce some cleaning ...