Quick-Start Guide

Dependencies

• Posix environment (Linux, MacOS, Etc.)

• Python3 (version 3.8 or greater)

• C99 std compiler (gcc or clang)

• Make

Building

To build R2U2, run make from r2u2/monitors/c/:

cd monitors/c/
make

Running

Running R2U2 requires a specification and an input stream.

1. Write the following specification to a file named simple.c2po:

    INPUT
        request, grant: bool;
   
    FTSPEC
        -- If a request is made, it shall be granted within 5 time steps.
        request -> F[0,5] grant;
   

2. Provide a mapping for variables to signal indices in a file named simple.map:

    request:0
    grant:1
   

3. Compile the specification using C2PO:

    python3 compiler/c2po.py --output spec.bin --map simple.map simple.c2po 
   

4. Write a simulated trace to monitor in a file named simple.csv, where the first column are the values of request and the second are the values of grant:

    1,0
    0,0
    0,1
    0,0
    1,0
    0,0
    0,0
    0,0
    0,0
    0,0
   

5. Run R2U2 using the compiled specification and the input stream:

    ./monitors/c/build/r2u2 spec.bin < simple.csv
   

Output

The output of R2U2 is a verdict stream with one verdict per line. A verdict includes a formula ID, timestamp, and truth value. Formula IDs are determined by the order in which they are defined in the specification file. Verdicts are aggregated so that if R2U2 can determine a range of values with the same truth at once, only the last time is output.

The following is a stream where formula 0 is true from 0-7 and false from 8-11 and formula 1 is false from times 0-4:

    0:7,T
    1:4,F
    0:11,F