Franck Pommereau / tlw

Go to a project
Toggle navigation Toggle navigation pinning
T

tlw

The Temporal Logic Wizard

Star
0
HTTPS
e65603ba initial import · by Franck Pommereau

The Temporal Logic Wizard

The TLW is a dynamic web page that allow to interactively build complex temporal logic formulas from a list of patterns. For instance, instead of writing EF(X & EF(Y)), users may select the pattern presented as "Y is reachable and is possibly preceded at some time by X" and then fill what they expect to be X and Y. Of course, patterns may be arbitrarily nested. So far, only CTL is supported, other temporal logics may be added in the future.

The syntax for temporal logic formulas is that of pytl as used in the ecco toolkit.

Installation

The TLW consists of three files:

  • wiz.css the CSS style sheet
  • wiz.py the PyScript to animate the wizard (the Python interpreter is loaded at runtime from PyScript homepage)
  • wiz.html the HTML page to be displayed to end-users

These three files should be copied on some web server, wiz.html may be renamed to something else. Renaming the other files will require to edit wiz.html in order to have them correctly loaded.

Licence

The Temporal Logic Wizard is (C) 2023 Franck Pommereau franck.pommereau@univ-evry.fr and released under the terms of the MIT Licence (see LICENCE.md).