A tool for generating a DFA from an LTLf formula
Project description
LTLf2DFA
LTLf2DFA is a simple tool that processes an LTLf formula (with past or future operators) and generates the corresponding minimized DFA (Deterministic Finite state Automaton) using MONA. This tool is written in Python 3.6.
It is tested on Linux Ubuntu 16.04.
Getting Started
Requirements
This tool uses MONA for the generation of the DFA. Hence, you should first install all MONA dependencies following the instructions here.
This tool is also based on the following libraries:
You should install them apart from pyparsing, which is automatically installed by pydot
How To Use It
- Download the LTLf2DFA.zip repository or clone it locally:
git clone https://github.com/Francesco17/LTLf2DFA.git
- Unzip it
- Enter the folder with the terminal and run the program
python3 main.py [-h] [-d] "formula"
Flags:
-h, --help Show help message and exit
-d, --declare Compute DECLARE assumption for the formula. -- OPTIONAL
- You will get the DFA automaton in .dot format within the current folder.
Syntax
The syntax accepted by LTLf2DFA is the following:
| OPERATOR | SYMBOL |
|---|---|
| TRUE | T |
| FALSE | F |
| AND | & |
| OR | | |
| NOT | ~ |
| IMPLICATION | -> |
| D-IMPLICATION | <-> |
| NEXT | X |
| UNTIL | U |
| EVENTUALLY | E |
| GLOBALLY | G |
| YESTERDAY (*) | Y |
| SINCE (*) | S |
| ONCE (*) | O |
| GLOBALLY (*) | H |
(*) are PAST operators.
Also parentheses ( and ) can be used.
NOTE: LTLf2DFA accepts ONLY separated formulas, i.e. formulas that have only past, only future or none operators.
Author
License
This project is licensed under the MIT License - see the LICENSE file for details
Contacts
If, for any reason, you are interested in feel free to contact me by email.
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
