Configuration

While the R2U2 static monitor supports runtime configuration of specifications, two types of compile-time configuration also exists for tuning monitor behavior and performance, Bounds and Feature Flags.

---

Bounds

Bounds are numeric limits set as C pre-processor macros which are used primarily to set array and memory arena sizes. Using fixed memory bounds allows for fast, consistent operation without memory allocation (e.g., if it loads, it won’t OOM) at the cost of requiring manual tuning for optimal performance.

If these numbers must be adjusted, it is most consistent to do so in the internals/bounds.h file where they are defined to ensure the same value is set in all locations. It is recommend to run with debug output after changing bounds to enable extra memory size checks.

Array Extents

R2U2_AUX_MAX_FORMULAS

Number of formula auxilary information metadata blocks; only utilized when R2U2_AUX_SPEC_STRINGS feature is enabled.

Default: 128

R2U2_AUX_MAX_CONTRACTS

Number of assume-guarantee contract (AGC) auxilary information metadata blocks; only utilized when R2U2_AUX_SPEC_STRINGS feature is enabled.

Default: 64

R2U2_MAX_SIGNALS

Size of incoming signal vector, i.e., maximum number of signals.

Default: 256

R2U2_MAX_ATOMICS

Size of atomic vector, i.e., maximum number of Booleans passed from the front-end (BZ) to the temporal logic engine

Default: 256

R2U2_MAX_TL_INSTRUCTIONS

Size of temporal logic instruction table and number of SCQ metadata blocks; used as working memory by TL front end.

Default: 256

R2U2_MAX_BZ_INSTRUCTIONS

Size of booleanizer instruction table and value buffer; used as working memory by BZ front end.

Default: 256

Memory Arena Sizing

R2U2_MAX_AUX_BYTES

Total characters (and nulls) of string arena used by auxiliary output (e.g., formula names, contract names, etc.) ; only utilized when R2U2_AUX_SPEC_STRINGS feature is enabled.

Default: 1024

R2U2_MAX_SCQ_SLOTS

Total number of SCQ slots for both future-time and past-time reasoning

Default: 1024

Numeric Parameters

R2U2_FLOAT_EPSILON

Sets the error value used for float comparisons (i.e., how close is considered “equal”).

Default: 0.00001

---

Feature Flags

Feature flags are C pre-processor macros that are used to conditionally compile features in or out of the static monitor. Flags are used when the feature drastically alters the behavior of the monitor, such as altering the input format, or significantly impacts monitor performance, such as code size or evaluation speed.

Feature flags are declared in and controlled by the internals/config.h file. This headerfile ensures all flags are declared and performs a consistency check to prevent incompatible feature or platform combinations.

Flags can be set anywhere in the translation unit before R2U2 is included, or set environment wide though compiler define flags. See building the monitor for details.

Logging Output

R2U2_DEBUG

Enables debug printing to stderr. Also enable extra memory checks at runtime

R2U2_TRACE

Enables very verbose memory trace printing to stderr

Temporal Logic Features

R2U2_AUX_STRING_SPECS

Enables printing of named formula verdicts and tri-state reports of assume-guarantee contracts