Tobias Reiher

When this runtime is used, the whole project is rebuilt every time. That is at least the case for RecordFlux. With the original runtime only changed files are rebuilt.

### Context and Problem Statement There are cases where a scalar value (usually an integer) is represented by a complex structure. One example would be variable-length integers (#8). While some...

The VCs for each action in a session state is generated. The VCs are used in the code generator to add checks to ensure that the needed properties are fulfilled....

Replace bindings by declare blocks

1

### Context and Problem Statement In #701 the introduction of declare blocks is proposed. Declare blocks provide a similar functionality as the already existing bindings. It could be beneficial to...

### Context and Problem Statement Declaring an integer type which covers the entire value range can be quite cumbersome: ```ada type T is range 0 .. 2 ** 16 -...

### Context and Problem Statement Integer overflows can occur in various scenarios: - Additions/multiplications using global variable in multiple states (e.g., incrementing sequence number for each message) - Additions/multiplications between...

Ensuring object properties in protocol session states

3

### Context and Problem Statement In many cases, certain properties of an object must be fulfilled before the object can be used for specific actions. #### Examples ##### E1 ```Ada...

Ideally, simplification should not change the order of expressions. ```python >>> str(Mul(Number(8), Variable("L")).simplified()) 'L * 8' ```

When parsing or generating a message, the message must be processed sequentially, i.e. before a field can be parsed or set, all predecessor fields must have been successfully verified. In...

```Ada generic Length_Type : ; Value_Type : ; type Length_Value is message Length : Length_Type then Value with Length => Length; Value : Value_Type; end message; ``` Instantiation of generic...