Skip to main content
Join the official 2019 Python Developers SurveyStart the survey!

A tool for generating a DFA from an LTLf formula

Project description

LTLf2DFA

ciaio

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

Francesco Fuggitti

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


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for ltlf2dfa, version 0.2.2.post0
Filename, size File type Python version Upload date Hashes
Filename, size ltlf2dfa-0.2.2.post0-py3-none-any.whl (173.6 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size ltlf2dfa-0.2.2.post0.tar.gz (174.3 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page