r2u2_cli 4.1.0

R2U2 CLI: A stream-based runtime monitor command-line interface
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

# R2U2 Command Line Interface

The Realizable, Reconfigurable, Unobtrusive Unit (R2U2) is a stream-based runtime verification
framework based on Mission-time Linear Temporal Logic (MLTL) designed to monitor safety- or
mission-critical systems with constrained computational resources.

Given a specification and input stream, R2U2 will output a stream of verdicts computing whether the
specification with respect to the input stream. Specifications can be written and compiled using the
Configuration Compiler for Property Organization (C2PO).

This crate allows specifications to be compiled with C2PO and monitored with R2U2. For detailed usage try:

    r2u2_cli --help

# Requirements

Requires a Python 3.x interpreter as required by [PyO3](https://github.com/PyO3/pyo3).

To enable satisfiability checking, install [Z3](https://github.com/Z3Prover/z3). On debian-based
systems, this can be done via `sudo apt-get install z3`.

# Example Usage

Given the following example.c2po file:
   
    INPUT
        a,b: bool;

    FTSPEC
        F[1,2] (a && b);

and the following example.csv file:

    # a,b
    0,0
    1,0
    0,1
    1,1
    0,0
    1,0
    0,1
    1,1

the following command will create a spec.bin file in the current directory:

    r2u2_cli compile example.c2po example.csv

and the following command:

    r2u2_cli run spec.bin example.csv

will output the following to the console:

    0:0,F
    0:2,T
    0:3,F
    0:4,F
    0:6,T

The single following command will also provide the same output:
    
    r2u2_cli run example.c2po example.csv

For all available options, try `r2u2_cli compile --help` and `r2u2_cli run --help`.

## 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
```

# Examples, Specifications, and Traces

Example specifications and traces can be found on our [github page](https://github.com/R2U2/r2u2/tree/rust-develop).

# Documentation

The documentation for R2U2 can be found [here](https://r2u2.github.io/r2u2/). The documentation includes user and developer guides for both R2U2 and C2PO.

## License

Licensed under either of

* Apache License, Version 2.0, ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
* MIT license ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)

at your option.

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the
work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any
additional terms or conditions.