tsltools

Code - https://github.com/Barnard-PL-Labs/tsltools

Tutorial blog post - https://barnard-pl-labs.github.io/tsltools/tsl_intro_blogpost

Run synthesis online - https://barnard-pl-labs.github.io/tsl-api/

Basic usage

Write a .tsl specification. As an example, let’s write a file called NoteButton.tsl:

always assume {
    F ! buttonPressed(userActivity);
}

always guarantee {
    buttonPressed(userActivity) -> [play <- noteE];
    F [play <- noteE];
    F [play <- noteG];
}

Install the tool locally or run the online tool. Then, run ./tslsynth NoteButton.tsl --python. The following code will be generated

if (currentState ==  0 ):

    if ((buttonPressed userActivity)):
        play = noteE
        currentState = 0

    if (not((buttonPressed userActivity))):
        play = noteG
        currentState = 1

if (currentState ==  1 ):

    if (True):
        play = noteE
        currentState = 0

You can save this in a file called noteButton.py (e.g. by running ./tslsynth NoteButton.tsl --python > noteButton.py), and run it as you would hand-written python code (e.g. python noteButton.py).

To generate a visualization of this code as a state machine, run ./tslsynth NoteButton.tsl --xstate. You will get xstate code that can be visualized as follows:

This site is open source. Improve this page.