Quick Start Guide: Using The TeSSLa Compiler and Interpreter

The CLI of TeSSLa follows a command based structure. The following commands are available:

Command   Description
interpreter   Evaluate a specification with a given trace (file or stdin)
compile-core   Compile TeSSLa to TeSSLa Core and print the result
doc   Generate documentation for TeSSLa code in JSON format
compile-scala   Generate a Scala monitor from a specification
compile-rust   Generate a Rust monitor from a specification
instrumenter   Instrument C code based on the provided annotations

For detailed usage information run java -jar tessla.jar --help

TeSSLa Interpreter

The TeSSLa interpreter takes a TeSSLa specification and an input trace, compiles the TeSSLa specification and generates an output trace by applying the compiled specification to the input trace.

As a starting point let's assume you have the following TeSSLa specification in a file specification.tessla:

in x: Events[Int]
in y: Events[Int]

def diff = sum(x) - sum(y)

def abs(x: Int) = if x < 0 then -x else x
def tooBig = abs(diff) >= 10

out diff
out tooBig

This specification takes two input streams x and y, sums up the values of all their events and compares these sums on every change. It produces the output streams diff and tooBig containing the difference between the two sums and indicating if the difference exceeds the limit of 10.

An input trace for this specification could be the following, stored e.g. in a file trace.input:

10: x = 2
17: x = 1
19: y = 4
37: x = 7
45: x = 6
78: y = 9
98: x = 2

Such a trace is a text file containing one event per line. Every line starts with a timestamp, followed by the name of the event and its values if there is a value attached to the event. The timestamps must be increasing in the entire trace and strictly increasing per input stream, i.e. multiple events with the same stream name and the same timestamp are not allowed.

To apply this TeSSLa specification to this trace you can run

java -jar tessla.jar interpreter specification.tessla trace.input

and get the following output

0: tooBig = false
0: diff = 0
10: tooBig = false
10: diff = 2
17: tooBig = false
17: diff = 3
19: tooBig = false
19: diff = -1
37: tooBig = false
37: diff = 6
45: tooBig = true
45: diff = 12
78: tooBig = false
78: diff = 3
98: tooBig = false
98: diff = 5

Note, that the output is not by accident in the same trace format as the input: TeSSLa can be seen as a stream transformation engine, which derives intermediate and output streams by applying the specification to the input streams.

For a detailed manual of the interpreter see here.

A software API for the interpreter is located here.

TeSSLa Scala/Rust Compiler

In alternative to interpreting a TeSSLa specification it can also be compiled to a Scala or Rust monitor. The compiled monitor has a higher performance than the interpreter and should especially be used for application where runtime matters. The Scala and Rust compiler can compile to a monitor handling I/O via stdio in the same way the interpreter does. Further they provide an API interfaces for direct incorporation on source code level.

Scala compiler

The compiler allows compilation to Scala code or a JAR file executable on the Java JVM.

java -jar tessla.jar compile-scala -j monitor.jar specification.tessla

creates an executeable Jar-File monitor.jar which receives inputs and produces outputs via stdio in the same format as the interpreter (see above).

For a detailed manual of the compiler see here.

Rust compiler

TeSSLa also supports compilation to Rust with even higher performance than the Scala compilation.

java -jar tessla.jar compile-rust -b monitor specification.tessla

creates an executable monitor which receives inputs and produces outputs via stdio in the same format as the interpreter (see above).

For a detailed manual of the compiler see here.

TeSSLa C Code Instrumenter

For runtime verification purposes the TeSSLa bundle contains an instrumenter for C code.

It uses the annotations from a TeSSLa specification to automatically include logging statements in a C file. The modified C code can then be compiled and directly attached to the TeSSLa monitor

More information can be found in the Runtime Verification tutorial.

Other features

The TeSSLa bundle can also be used to generate a TeSSLa Core specification which can be handed to custom backends (command compile-core). With this command it is also possible to extract a summary of annotations used in the specification which can then be handed to other backends.

It can also be used to extract json files containing the TeSSLa-Doc documentation from specifications (command doc). For more information about TeSSLa-Doc see here.