The CLI of TeSSLa follows a command based structure. The following commands are available:
|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||Generate a Scala 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
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
y, sums up the values of all their events and compares these sums on every change. It produces the output streams
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
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.
In alternative to interpreting a TeSSLa specification it can also be compiled to a Scala monitor. The compiled monitor has a higher performance than the interpreter and should especially be used for application where runtime matters.
java -jar tessla.jar compile specification.tessla -j monitor.jar
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.
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.