TeSSLa
  • About
  • TeSSLa Examples
  • RV Examples
  • Settings
  • Trace
  • C Code
  • Specification
  • Status and Compiler Output
  • TeSSLa Output
  • TeSSLa Visualization
Welcome to the TeSSLa web IDE

Examples for plain TeSSLa and the TeSSLa runtime verification (RV) tool suite can be loaded using the links in the upper right corner.

  • Press the green Run button in the title bar to execute a loaded example.
  • The Trace editor in the upper left contains the input trace. Switch to the C Code editor to enter a C program which will be used as trace source.
  • The Specification editor in the upper right contains the specification.
  • The Status and Compiler Output view in the lower left contains compilation and runtime errors if any occurred.
  • The TeSSLa Output log in the lower right shows the output trace. Try clicking on TeSSLa Visualization to get a visual representation of the output trace instead.

An introduction to the TeSSLa language can be found on the official TeSSLa website.

Settings

General Options

Stop the interpreter when the output stream with the given name generates its first event. Leave blank to disable this feature.
Stop the interpreter after a given amount of events. Leave blank to disable this feature.

Trace Options

Use the given time constant (including a unit) as the reference time for time literals.

C Code Options

Command line arguments for the compiler.
Command line options for the linker.