Online Monitoring

SpecForge can be used as an online monitor for Lilo specifications. In contrast with offline monitoring, this means that the monitor will produce verdicts in a streaming manner as it ingests the trace, rather than in one shot after processing the entire trace.

To invoke the online monitor, use the streammon command in the specforge CLI. Run specforge streammon --help for the exact arguments necessary. Running the specforge streammon command will start the monitor, which will ingest a trace from STDIN and produce an output signal to STDOUT.

The monitor accepts traces in CSV or JSONL format. In the case of CSV, the monitor expects the first line fed in to be the headers, which can be used to identify the columns corresponding to each signal. In the case of JSONL, the monitor expects each line to be a JSON object with keys corresponding to signal names. The user can specify whether records are encoded in flat or nested format using the RECORD_ENCODING subcommand (see the chapter on Data).

The current implementation of the online monitor performs best when the intervals in temporal operators extend to a small window into the future or past. Intervals with unbounded windows, even if past-time, are not supported.

Future-time temporal operators are supported in the online monitor. Their verdicts are produced with a delay corresponding to the largest future window in the spec. For example, when monitoring the formula eventually [0, 5] f, the monitor will produce the verdict for the current time t, only after ingesting the part of the trace upto time t + 5.