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
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)
liftable
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.
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.
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.
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.
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.
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.