Each node in the AST stores the verdict-timestamp tuples required by their parent node(s) in a shared connection queue (SCQ),
where the SCQ is a circular buffer that overwrites verdict-timestamp tuples in a circular manner.
This will produce the following assembly:
BZ b0 iload 0 0
BZ b1 store 0 0
BZ b2 iload 1 0
BZ b3 store 2 1
TL n0 load a0
TL n1 release False n0
TL n2 load a1
TL n3 until n1 n2
TL n4 return n3 0
CG TL SCQ q0 |1|
CG TL SCQ q1 |5|
CG TL TEMP q1 [0, 3]
CG TL SCQ q2 |4|
CG TL SCQ q3 |5|
CG TL TEMP q3 [2, 4]
CG TL SCQ q4 |1|
F SPEC0 0
In the outputted assembly, there are computation instructions and configuration instructions.
The computation instructions are saved in a table and sequentially iterated over at each timestamp. The computation
instructions are ordered such that R2U2 reasons over the AST by determining the evaluation of
each subformula node from the bottom-up and
propagating verdicts to the parent node(s). The configuration instructions are run once upon initialization to configure the AST in terms of
sizing and metadata (e.g., the lower and upper bounds of temporal operators).
## Computation Instructions
In the example above, the following are computation instructions:
BZ b0 iload 0 0
BZ b1 store 0 0
BZ b2 iload 1 0
BZ b3 store 2 1
TL n0 load a0
TL n1 release False n0
TL n2 load a1
TL n3 until n1 n2
TL n4 return n3 0
The BZ instructions are run in R2U2's Booleanizer. R2U2’s Booleanizer enables boolean
expressions over booleans, integers, and/or float input signals using arithmetic, bitwise, relational,
and set operators (e.g., “forexactlyn” or “foratmostn”). The output of R2U2's booleanizer are atomics that are
then read by R2U2's Temporal Logic engine.
The TL instructions are executed in R2U2's Temporal Logic engine, which reasons over MLTL and ptMLTL specifications.
## Configuration Instructions
In the example above, the following are configuration instructions:
CG TL SCQ q0 |1|
CG TL SCQ q1 |5|
CG TL TEMP q1 [0, 3]
CG TL SCQ q2 |4|
CG TL SCQ q3 |5|
CG TL TEMP q3 [2, 4]
CG TL SCQ q4 |1|
F SPEC0 0
The `CG TL SCQ ...` instructions give the minimal size required for each of the shared connection queues in order to store the applicable
verdict-timestamp tuples required by their parent node(s).
The `CG TL TEMP ...` instructions give the temporal bounds of the temporal operator nodes.
`F ...` and `C ...` instructions provide the auxilary string name for each formula and contract, respectively. In this example, the formula (G[0,3]a) U[2,4] b
was given the name `SPEC0`.
Each node of the AST directly corresponds to an assembly instruction (refer to the Assembly tab for more information).
Inside R2U2, there are two main engines: the **Booleanizer** and the **Temporal Logic Engine**. R2U2’s Booleanizer enables boolean
expressions over booleans, integers, and/or float input signals using arithmetic, bitwise, relational,
and set operators (e.g., “forexactlyn” or “foratmostn”). The output of R2U2's booleanizer are atomics that are
then read by R2U2's Temporal Logic engine. R2U2's Temporal Logic engine reasons over MLTL and ptMLTL specifications. The AST is
color-coded as follows:
-  grey nodes represent nodes within the Booleanizer.
-  red nodes represent nodes within the Temporal Logic Engine.
Each node in the AST stores the verdict-timestamp tuples required by their parent node(s) in a shared connection queue (SCQ),
where the SCQ is a circular buffer that overwrites verdict-timestamp tuples in a circular manner.