Skip to content

Latest commit

 

History

History
167 lines (127 loc) · 4.69 KB

README.md

File metadata and controls

167 lines (127 loc) · 4.69 KB
Raw

PyPI PyPI - Python Version GitHub

test lint docs codecov

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

It is also available online at http://ltlf2dfa.diag.uniroma1.it.

Prerequisites

MONA Installation

LTLf2DFA relies on the MONA tool for the generation of the DFA. Please, make sure you have the MONA tool installed on your system before running LTLf2DFA. You can follow the instructions here to get MONA.

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 https://github.com/whitemech/LTLf2DFA.git
cd ltlf2dfa
pip install .

Quickstart

You can use the LTLf2DFA package in two ways: as a library, and as a CLI tool.

As a Library

  • 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 PPLTL formula:
from ltlf2dfa.parser.ppltl import PPLTLParser

parser = PPLTLParser()
formula_str = "H(a -> Y b)"
formula = parser(formula_str)       # returns a PPLTLFormula

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

As a CLI Interface

ltlf2dfa -l {ltlf | ppltl} -f <path/to/formula>

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/PPLTL formula to MONA (First-order Logic)

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

Development

If you want to contribute, set up your development environment as follows:

  • Intall Poetry
  • Clone the repository: git clone https://github.com/whitemech/LTLf2DFA.git && cd LTLf2DFA
  • Install the dependencies: poetry shell && poetry install

Tests

To run tests: tox

To run only the code tests: tox -e py38

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-2023 WhiteMech

Citing

If you use LTLf2DFA in your research, please consider citing it with the following bibtex:

@software{fuggitti-ltlf2dfa,
  author       = {Francesco Fuggitti},
  title        = {LTLf2DFA},
  month        = {March},
  year         = {2019},
  publisher    = {Zenodo},
  version      = {1.0.3},
  doi          = {10.5281/zenodo.3888410},
  url_code    = {https://github.com/whitemech/LTLf2DFA},
  url_website = {http://ltlf2dfa.diag.uniroma1.it},
}

Author

Francesco Fuggitti