• spot
• EAHyper (recommended): Provide as executable named eahyper in working directory when executing RVHyper.

The given Makefile provides the functionality to build RVHyper. A singe make command should do the job. The binary rvhyper gets placed into build/release/.

$ make
$ ls -lgoh --time-style=+ build/release/rvhyper
-rwxr-xr-x 1 170K  build/release/rvhyper

We also provide a short demo to check if the build was successful.

$ make demo

The specification to monitor for has to be a valid HyperLTL formula only containing forall-quantifiers. The specification can be given to RVHyper either as a string parameter or contained in a file:

$ ./rvhyper -s 'forall x. forall y. (o_x <-> o_y) W ~(i_x <-> i_y)'
$ ./rvhyper -S observational_determinism.hltl

The typical way one wants to use RVHyper is with the option --stdin, which is suited for online monitoring. This reads commands as well as IO-events directly from the standard input.

• print commands:
  • print help: list the available commands
  • print specification: print the specification
  • print aps: list the atomic propositions of the specification formula
  • print stats: print statistics of the running RVHyper instance
• session commands:
  • session start: start new monitoring session
  • session end: end active monitoring session
• exit / quit: exit RVHyper

In order to provide one IO-event for the current monitoring session, one has to list the fulfilled input and output atomic propositions for the event. The format has to match the pattern

	[input (',' input)*] ';' [output (',' output)*]

This of course can only be used in an active session.

$ ./rvhyper -s 'forall x. forall y. (out_x <-> out_y) W !(in_x <-> in_y)' --stdin
Specification:
forall x.forall y. (out_x <-> out_y) W ~(in_x <-> in_y)
reflexive: true
symmetric: true
transitive: false

$ session start
$ in;out
$ in;
$ session end
$ session start
$ in;out
$ in;
$ in;
$ session end
$ print stats
seen traces: 2
trie size: 3
created instances: 1
done transitions: 2
$ session start
$ in;out
$ in;
$ in;out
 --> Monitor(2,3) detected violation at position 3
Counter Example:
Trace 2 | Trace 3
in;out | in;out
in | in
in | in;out

RVHyper can also be used to monitor offline, where it has to be given recorded IO-event traces.

RVHyper currently knows two different modes of operation, which differ in how the IO-event traces (see below) get processed for monitoring.

• --parallel: all traces get monitored in parallel
• --sequential: traces get monitored one after another
• --sequential-debug: Online Monitoring (see 2.2.) with given IO-event traces

IO-event traces have to be stored in files, where one file corresponds to one session and one line in the file corresponds to one IO-event. The lines have to match the pattern listed in 2.2.2., where only the fulfilled propositions must be listed. Filesnames have to be listed as the last parameters for RVHyper:

$ ./rvhyper -S demo.hltl -- demo_a.tr demo_b.tr demo_c.tr

By default RVHyper outputs information about the formula and found violations to the specification. Additionally there are options for even more verbose output, to suppress it or print extra statistics:

• --verbose: output extra information about the monitoring automaton, progress, IO-events, transitions, trace analysis
• --quiet: suppress most of the output
• --stats: output extra statistics such as computation time, traces seen, instances created, transistions taken