Skip to main content

LTLf and PLTLf to Deterministic Finite-state Automata (DFA)

Project description

LTLf2DFA

LTLf2DFA CI pipeline codecov

LTLf2DFA is a tool that transforms an LTLf or a PLTLf formula into a minimal Deterministic Finite state Automaton (DFA) using MONA.

It is also available online at ltlf2dfa.diag.uniroma1.it.

Prerequisites

This tool uses MONA for the generation of the DFA. Hence, you should first install MONA with all its dependencies on your system following the instructions here.

This tool is also based on the following libraries:

They are automatically added while installing LTLf2DFA.

Install

pip install ltlf2dfa
  • or, from source (master branch):
pip install git+https://github.com/whitemech/LTLf2DFA.git
  • or, clone the repository and install:
git clone htts://github.com/whitemech/LTLf2DFA.git
cd ltlf2dfa
pip install .

How To Use

  • Parse an LTLf formula:
from ltlf2dfa.parser.ltlf import LTLfParser

parser = LTLfParser()
formula_str = "G(a -> X b)"
formula = parser(formula_str)       # returns an LTLfFormula

print(formula)                      # prints "G(a -> X (b))"
  • Or, parse a PLTLf formula:
from ltlf2dfa.parser.pltlf import PLTLfParser

parser = PLTLfParser()
formula_str = "H(a -> Y b)"
formula = parser(formula_str)       # returns a PLTLfFormula

print(formula)                      # prints "H(a -> Y (b))"
  • Translate a formula to the corresponding DFA automaton:
dfa = formula.to_dfa()
print(dfa)                          # prints the DFA in DOT format

Features

  • Syntax and parsing support for the following formal languages:

    • Propositional Logic;
    • Linear Temporal Logic on Finite Traces;
    • Pure-Past Linear Temporal Logic on Finite Traces.
  • Conversion from LTLf/PLTLf formula to MONA (First-order Logic)

NOTE: LTLf2DFA accepts either LTLf formulas or PLTLf formulas, i.e., formulas that have only past, only future or none operators.

Tests

To run tests: tox

To run only the code tests: tox -e py37

To run only the code style checks: tox -e flake8

Docs

To build the docs: mkdocs build

To view documentation in a browser: mkdocs serve and then go to http://localhost:8000

License

LTLf2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).

Copyright 2018-2020 WhiteMech

Author

Francesco Fuggitti

History

1.0.0.post0 (2020-06-05)

1.0.0 (2020-05-20)

  • Refinement of all the grammars. Extensive improvement of the parsing.
  • Introduce interfaces and class hierarchy for the logic modules.
  • Several bug fixes and introduce testing.
  • Introduce of docs.
  • Introduce Continuous Integration.
  • Refactor translation feature.
  • Replace parsing library PLY with Lark.

0.2.2 (2019-09-25)

0.2.0 (2019-09-03)

0.1.3 (2018-07-22)

0.1.0 (2018-07-18)

  • First release on PyPI.

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 1.0.0.post0
Filename, size File type Python version Upload date Hashes
Filename, size ltlf2dfa-1.0.0.post0-py2.py3-none-any.whl (27.5 kB) File type Wheel Python version py2.py3 Upload date Hashes View
Filename, size ltlf2dfa-1.0.0.post0.tar.gz (28.0 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page