Dev Guide

Key Dependencies

Server Side

The LTL tutor is implemented as a Flask web server, and uses:

• ANTLR 4, to generate the parser for various LTL syntaxes.
• SPOT to generate LTL formulae, translate them to automata, and check the relations between them.
• SQLAlchemy as an ORM. This is primarily used for logging.
• Flask-Login for user session management.

Client Side

• BootStrap 4 for styling / responsive layout, etc.
• Mermaid JS to draw both traces and LTL syntax trees.

See requirements.txt and conda-requirements.txt for a full list of dependencies.

ANTLR Use

To modify the parser, first:

• Make your ANTLR changes in src/ltl.g4.
• Regenerate the parser (in Python) by running antlr4 -Dlanguage=Python3 ltl.g4.

Testing

Tests currently consist only of Unit Tests. These are run using the unittest framework, and are in the test directory.

Test files must be of the form test_*.py