Expand description
§Library for r2u2_core
R2U2: A stream-based runtime monitor written in #![no_std] that reasons over Mission-Time Linear
Temporal Logic (MLTL) specifications compiled with the Configuration Compiler for Property Organization (C2PO).
§Optional Features:
aux_string_specs: Enable Assume-Guarantee Contract status output and string auxiliary specification naming. This feature enables the following:- r2u2_contract type
- r2u2_output::spec_str member of the r2u2_output type
- get_contract_buffer function
- AGC_INACTIVE, AGC_INVALID, and AGC_VERIFIED constants
debug_print_std: Debug printing to terminal (i.e.,println!)debug_print_semihosting: Debug printing utilizing GDB debugger of microcontroller (i.e.,hprintln!)
§Usage:
- A monitor must be created utilizing get_monitor. The specification file from C2PO must be passed by reference as
&[u8]. The specifications can later be updated with update_binary_file; this will also reset the monitor to its intial state. - Signals must be loaded in according to the mapping specified when compiling the specification file through load_bool_signal, load_float_signal, load_int_signal, and load_string_signal.
- Run the monitor for a single timestep with monitor_step.
- Get output data through get_output_buffer and get_contract_buffer.
- Repeat steps 2-4. (Optionally check for overflow with the output of monitor_step or get_overflow_error.)
For details on compiling specifications with C2PO, refer to README.
Structs§
- Monitor
- Struct to contain monitor information
- r2u2_
contract - Struct to contain Assume-Guarantee Contract (AGC) verdicts (i.e., contract identification and status)
- r2u2_
output - Struct to contain output verdicts (i.e., specification identification and verdict)
- r2u2_
verdict - Struct to contain verdict-timestamp tuples
Constants§
- AGC_
INACTIVE - Assume-Guarantee Contract (AGC) inactive status
- AGC_
INVALID - Assume-Guarantee Contract (AGC) invalid status
- AGC_
VERIFIED - Assume-Guarantee Contract (AGC) verified status
- R2U2_
AUX_ MAX_ CONTRACTS - Number of assume-guarantee contract (AGC) auxilary information metadata blocks Represents maximum number of assume-guarantee contracts being monitored (only utilized when aux_string_specs feature is enabled)
- R2U2_
AUX_ MAX_ FORMULAS - Number of formula auxilary information metadata blocks Represents maximum number of formulas being monitored (only utilized when aux_string_specs feature is enabled)
- R2U2_
FLOAT_ EPSILON - R2U2_
MAX_ ATOMICS - Represents maximum number of Booleans passed from the front-end (booleanizer or directly loaded atomics) to the temporal logic engine
- R2U2_
MAX_ BZ_ INSTRUCTIONS - Represents maximum number of booleanizer instructions
- R2U2_
MAX_ OUTPUT_ CONTRACTS - Represents maximum number of output contract statuses that can be returned at a single timestamp (only utilized when aux_string_specs feature is enabled)
- R2U2_
MAX_ OUTPUT_ VERDICTS - Represents maximum number of output verdicts that can be returned at a single timestamp
- R2U2_
MAX_ QUEUE_ SLOTS - Represents total number of SCQ slots for both future-time and past-time reasoning
- R2U2_
MAX_ SIGNALS - Represents maximum number of input signals
- R2U2_
MAX_ TL_ INSTRUCTIONS - Represents maximum number of temporal logic instructions
Functions§
- get_
contract_ buffer - Get Assume-Guarantee Contract (AGC) buffer
- get_
monitor - Get runtime monitor
- get_
output_ buffer - Get output verdict buffer
- get_
overflow_ error - Get overflow error flag
- load_
bool_ signal - Load boolean signal
- load_
float_ signal - Load float signals
- load_
int_ signal - Load integer signal
- load_
string_ signal - Load signal as string (decoded as integer, float, or boolean)
- monitor_
step - Take a step with runtime monitor
- reset_
overflow_ error - Reset overflow flag
- update_
binary_ file - Update specification binary file (and reset monitor)