A tool for generating a DFA from an LTLf formula
Project description
LTLf2DFA
LTLf2DFA is a simple tool that processes an LTLf formula (with all past or all 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 and on macOS 10.13.6.
Now it is also available online at ltlf2dfa.diag.uniroma1.it.
Getting Started
Requirements
This tool uses MONA for the generation of the DFA. Hence, you should first install MONA with all its dependencies on your OS following the instructions here.
This tool is also based on the following libraries:
They are automatically added while installing LTLf2DFA.
How To Install It
- From PyPI:
pip install ltlf2dfa
- From this repository:
pip install git+https://github.com/Francesco17/LTLf2DFA@master#egg=ltlf2dfa
How To Use It
- Simply parse an LTLf formula with past or future operators:
from ltlf2dfa.Parser import MyParser
formula = "G(a->Xb)"
parser = MyParser()
parsed_formula = parser(formula)
print(parsed_formula)
- Translate an LTLf formula to the corresponding DFA automaton:
from ltlf2dfa.Translator import Translator
from ltlf2dfa.DotHandler import DotHandler
formula = "G(a->Xb)"
declare_flag = False #True if you want to compute DECLARE assumption for the formula
translator = Translator(formula)
translator.formula_parser()
translator.translate()
translator.createMonafile(declare_flag) #it creates automa.mona file
translator.invoke_mona() #it returns an intermediate automa.dot file
dotHandler = DotHandler()
dotHandler.modify_dot()
dotHandler.output_dot() #it returns the final automa.dot file
Syntax
The syntax accepted by LTLf2DFA is the following:
OPERATOR | SYMBOL |
---|---|
TRUE | true |
FALSE | false |
AND | & |
OR | | |
NOT | ~ |
IMPLICATION | -> |
D-IMPLICATION | <-> |
NEXT | X |
UNTIL | U |
EVENTUALLY | F |
GLOBALLY | G |
WEAK NEXT | W |
RELEASE | R |
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.
Project details
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.
Source Distribution
Built Distribution
Hashes for ltlf2dfa-0.2.2.post0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 6f3bfed43e127d540f5c2a61f0b4cd9fd409fb4783243a3e0cea297b53ca5879 |
|
MD5 | 994881885c06638adb80b84893c9c9ca |
|
BLAKE2b-256 | dea2db7bfce47624d8ea4ef53399651fff1a2ef1d53e48f06f06662bbb19ff12 |