<h1 align="center">
<img src="http://ltlf2dfa.diag.uniroma1.it/static/images/logo-ltlf2dfa.svg">
</h1>
<p align="center">
<a href="https://pypi.org/project/ltlf2dfa">
<img alt="PyPI" src="https://img.shields.io/pypi/v/ltlf2dfa">
</a>
<a href="https://pypi.org/project/ltlf2dfa">
<img alt="PyPI - Python Version" src="https://img.shields.io/pypi/pyversions/ltlf2dfa" />
</a>
<a href="">
<img alt="PyPI - Implementation" src="https://img.shields.io/pypi/implementation/ltlf2dfa">
</a>
<a href="https://github.com/whitemech/ltlf2dfa/blob/master/LICENSE">
<img alt="GitHub" src="https://img.shields.io/badge/license-LGPLv3%2B-blue">
</a>
<a href="">
<img alt="PyPI - Wheel" src="https://img.shields.io/pypi/wheel/ltlf2dfa">
</a>
</p>
<p align="center">
<a href="">
<img alt="test" src="https://github.com/whitemech/ltlf2dfa/workflows/test/badge.svg">
</a>
<a href="">
<img alt="lint" src="https://github.com/whitemech/ltlf2dfa/workflows/lint/badge.svg">
</a>
<a href="">
<img alt="docs" src="https://github.com/whitemech/ltlf2dfa/workflows/docs/badge.svg">
</a>
<a href="https://codecov.io/gh/whitemech/pddl">
<img alt="codecov" src="https://codecov.io/gh/whitemech/ltlf2dfa/branch/master/graph/badge.svg">
</a>
<a href="">
<img alt="PyPI - Status" src="https://img.shields.io/pypi/status/ltlf2dfa" />
</a>
</p>
<p align="center">
<a href="https://img.shields.io/badge/flake8-checked-blueviolet">
<img alt="" src="https://img.shields.io/badge/flake8-checked-blueviolet">
</a>
<a href="https://img.shields.io/badge/mypy-checked-blue">
<img alt="" src="https://img.shields.io/badge/mypy-checked-blue">
</a>
<a href="https://img.shields.io/badge/isort-checked-yellow">
<img alt="isort" src="https://img.shields.io/badge/isort-checked-yellow" />
</a>
<a href="https://img.shields.io/badge/code%20style-black-black">
<img alt="black" src="https://img.shields.io/badge/code%20style-black-black" />
</a>
<a href="https://www.mkdocs.org/">
<img alt="" src="https://img.shields.io/badge/docs-mkdocs-9cf">
</p>
<p align="center">
</a>
<a href="https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg">
<img alt="" src="https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg">
</a>
</p>
---
LTL<sub>f</sub>2DFA is a tool that transforms an LTL<sub>f</sub> or a PLTL<sub>f</sub> formula into a minimal
Deterministic Finite state Automaton (DFA) using [MONA](http://www.brics.dk/mona/).
It is also available online at [http://ltlf2dfa.diag.uniroma1.it](http://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](http://www.brics.dk/mona/download.html).
This tool is also based on the following libraries:
- [lark-parser 0.9.0](https://pypi.org/project/lark-parser/)
- [sympy 1.6.1](https://pypi.org/project/sympy/)
They are automatically added while installing LTL<sub>f</sub>2DFA.
## Install
- from [PyPI](https://pypi.org/project/ltlf2dfa/):
```
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 .
```
## How To Use
- Parse an LTL<sub>f</sub> formula:
```python
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 PLTL<sub>f</sub> formula:
```python
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:
```python
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 LTL<sub>f</sub>/PLTL<sub>f</sub> formula to MONA (First-order Logic)
**NOTE**: LTL<sub>f</sub>2DFA accepts either LTL<sub>f</sub> formulas or PLTL<sub>f</sub> 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 py3.7`
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](http://localhost:8000)
## License
LTL<sub>f</sub>2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).
Copyright 2018-2022 WhiteMech @ Sapienza University
## Citing
If you are interested in this tool, and you use it in your own work, please consider citing it.
## Author
[Francesco Fuggitti](https://francescofuggitti.github.io/)
# History
## 1.0.2 (2022-02-25)
* Introduce `PLTLfWeakBefore` and `PLTLfPastRelease` support
* Hotfix problem on translation of the Once operator
* Increase code coverage
## 1.0.1 (2020-07-03)
* Introduce optional argument to `to_dfa()` method for DFA in MONA output
* Add parsing support for `LTLfLast()` and `PLTLfStart()` keywords
* Some fixes
* Increase code coverage
## 1.0.0.post0 (2020-06-05)
* Include *.lark files in the package build
* New online version: [http://ltlf2dfa.diag.uniroma1.it/](http://ltlf2dfa.diag.uniroma1.it).
## 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)
* Online version: [http://ltlf2dfa.diag.uniroma1.it/](http://ltlf2dfa.diag.uniroma1.it).
## 0.2.0 (2019-09-03)
## 0.1.3 (2018-07-22)
## 0.1.0 (2018-07-18)
* First release on PyPI.
Raw data
{
"_id": null,
"home_page": "https://github.com/whitemech/ltlf2dfa.git",
"name": "ltlf2dfa",
"maintainer": "",
"docs_url": null,
"requires_python": "",
"maintainer_email": "",
"keywords": "ltlf2dfa",
"author": "Francesco Fuggitti",
"author_email": "fuggitti@diag.uniroma1.it",
"download_url": "https://files.pythonhosted.org/packages/2e/b2/a659c37e6158c3742b2a427268fde1debaef54e2b3598d5758a0d872241d/ltlf2dfa-1.0.2.tar.gz",
"platform": "",
"description": "<h1 align=\"center\">\n <img src=\"http://ltlf2dfa.diag.uniroma1.it/static/images/logo-ltlf2dfa.svg\">\n</h1>\n\n<p align=\"center\">\n <a href=\"https://pypi.org/project/ltlf2dfa\">\n <img alt=\"PyPI\" src=\"https://img.shields.io/pypi/v/ltlf2dfa\">\n </a>\n <a href=\"https://pypi.org/project/ltlf2dfa\">\n <img alt=\"PyPI - Python Version\" src=\"https://img.shields.io/pypi/pyversions/ltlf2dfa\" />\n </a>\n <a href=\"\">\n <img alt=\"PyPI - Implementation\" src=\"https://img.shields.io/pypi/implementation/ltlf2dfa\">\n </a>\n <a href=\"https://github.com/whitemech/ltlf2dfa/blob/master/LICENSE\">\n <img alt=\"GitHub\" src=\"https://img.shields.io/badge/license-LGPLv3%2B-blue\">\n </a> \n <a href=\"\">\n <img alt=\"PyPI - Wheel\" src=\"https://img.shields.io/pypi/wheel/ltlf2dfa\">\n </a>\n</p>\n<p align=\"center\">\n <a href=\"\">\n <img alt=\"test\" src=\"https://github.com/whitemech/ltlf2dfa/workflows/test/badge.svg\">\n </a>\n <a href=\"\">\n <img alt=\"lint\" src=\"https://github.com/whitemech/ltlf2dfa/workflows/lint/badge.svg\">\n </a>\n <a href=\"\">\n <img alt=\"docs\" src=\"https://github.com/whitemech/ltlf2dfa/workflows/docs/badge.svg\">\n </a>\n <a href=\"https://codecov.io/gh/whitemech/pddl\">\n <img alt=\"codecov\" src=\"https://codecov.io/gh/whitemech/ltlf2dfa/branch/master/graph/badge.svg\">\n </a>\n <a href=\"\">\n <img alt=\"PyPI - Status\" src=\"https://img.shields.io/pypi/status/ltlf2dfa\" />\n </a>\n</p>\n<p align=\"center\">\n <a href=\"https://img.shields.io/badge/flake8-checked-blueviolet\">\n <img alt=\"\" src=\"https://img.shields.io/badge/flake8-checked-blueviolet\">\n </a>\n <a href=\"https://img.shields.io/badge/mypy-checked-blue\">\n <img alt=\"\" src=\"https://img.shields.io/badge/mypy-checked-blue\">\n </a>\n <a href=\"https://img.shields.io/badge/isort-checked-yellow\">\n <img alt=\"isort\" src=\"https://img.shields.io/badge/isort-checked-yellow\" />\n </a>\n <a href=\"https://img.shields.io/badge/code%20style-black-black\">\n <img alt=\"black\" src=\"https://img.shields.io/badge/code%20style-black-black\" />\n </a>\n <a href=\"https://www.mkdocs.org/\">\n <img alt=\"\" src=\"https://img.shields.io/badge/docs-mkdocs-9cf\">\n</p>\n<p align=\"center\">\n </a>\n <a href=\"https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg\">\n <img alt=\"\" src=\"https://zenodo.org/badge/DOI/10.5281/zenodo.3888410.svg\">\n </a>\n</p>\n\n---\n\nLTL<sub>f</sub>2DFA is a tool that transforms an LTL<sub>f</sub> or a PLTL<sub>f</sub> formula into a minimal \nDeterministic Finite state Automaton (DFA) using [MONA](http://www.brics.dk/mona/).\n\nIt is also available online at [http://ltlf2dfa.diag.uniroma1.it](http://ltlf2dfa.diag.uniroma1.it).\n\n## Prerequisites\n\nThis tool uses MONA for the generation of the DFA. Hence, you should first install MONA with all its dependencies on \nyour system following the instructions [here](http://www.brics.dk/mona/download.html).\n\nThis tool is also based on the following libraries:\n\n- [lark-parser 0.9.0](https://pypi.org/project/lark-parser/)\n- [sympy 1.6.1](https://pypi.org/project/sympy/)\n\nThey are automatically added while installing LTL<sub>f</sub>2DFA.\n\n## Install\n\n- from [PyPI](https://pypi.org/project/ltlf2dfa/):\n```\npip install ltlf2dfa\n```\n- or, from source (`master` branch):\n```\npip install git+https://github.com/whitemech/LTLf2DFA.git\n```\n\n- or, clone the repository and install:\n```\ngit clone https://github.com/whitemech/LTLf2DFA.git\ncd ltlf2dfa\npip install .\n```\n## How To Use\n\n- Parse an LTL<sub>f</sub> formula:\n```python\nfrom ltlf2dfa.parser.ltlf import LTLfParser\n\nparser = LTLfParser()\nformula_str = \"G(a -> X b)\"\nformula = parser(formula_str) # returns an LTLfFormula\n\nprint(formula) # prints \"G(a -> X (b))\"\n```\n- Or, parse a PLTL<sub>f</sub> formula:\n```python\nfrom ltlf2dfa.parser.pltlf import PLTLfParser\n\nparser = PLTLfParser()\nformula_str = \"H(a -> Y b)\"\nformula = parser(formula_str) # returns a PLTLfFormula\n\nprint(formula) # prints \"H(a -> Y (b))\"\n```\n- Translate a formula to the corresponding DFA automaton:\n```python\ndfa = formula.to_dfa()\nprint(dfa) # prints the DFA in DOT format\n```\n## Features\n\n* Syntax and parsing support for the following formal languages:\n * Propositional Logic;\n * Linear Temporal Logic on Finite Traces;\n * Pure-Past Linear Temporal Logic on Finite Traces.\n\n* Conversion from LTL<sub>f</sub>/PLTL<sub>f</sub> formula to MONA (First-order Logic)\n\n**NOTE**: LTL<sub>f</sub>2DFA accepts either LTL<sub>f</sub> formulas or PLTL<sub>f</sub> formulas, i.e., formulas that \nhave only past, only future or none operators.\n\n## Tests\n\nTo run tests: `tox`\n\nTo run only the code tests: `tox -e py3.7`\n\nTo run only the code style checks: `tox -e flake8`\n\n## Docs\n\nTo build the docs: `mkdocs build`\n\nTo view documentation in a browser: `mkdocs serve`\nand then go to [http://localhost:8000](http://localhost:8000)\n\n## License\n\nLTL<sub>f</sub>2DFA is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).\n\nCopyright 2018-2022 WhiteMech @ Sapienza University\n\n## Citing\nIf you are interested in this tool, and you use it in your own work, please consider citing it.\n\n## Author\n\n[Francesco Fuggitti](https://francescofuggitti.github.io/)\n\n\n# History\n\n## 1.0.2 (2022-02-25)\n* Introduce `PLTLfWeakBefore` and `PLTLfPastRelease` support\n* Hotfix problem on translation of the Once operator\n* Increase code coverage\n\n## 1.0.1 (2020-07-03)\n* Introduce optional argument to `to_dfa()` method for DFA in MONA output\n* Add parsing support for `LTLfLast()` and `PLTLfStart()` keywords\n* Some fixes\n* Increase code coverage\n\n## 1.0.0.post0 (2020-06-05)\n\n* Include *.lark files in the package build\n* New online version: [http://ltlf2dfa.diag.uniroma1.it/](http://ltlf2dfa.diag.uniroma1.it).\n\n## 1.0.0 (2020-05-20)\n\n* Refinement of all the grammars. Extensive improvement of the parsing.\n* Introduce interfaces and class hierarchy for the logic modules.\n* Several bug fixes and introduce testing.\n* Introduce of docs.\n* Introduce Continuous Integration.\n* Refactor translation feature.\n* Replace parsing library PLY with Lark.\n\n## 0.2.2 (2019-09-25)\n\n* Online version: [http://ltlf2dfa.diag.uniroma1.it/](http://ltlf2dfa.diag.uniroma1.it).\n\n## 0.2.0 (2019-09-03)\n\n## 0.1.3 (2018-07-22)\n\n## 0.1.0 (2018-07-18)\n\n* First release on PyPI.\n\n\n\n",
"bugtrack_url": null,
"license": "GNU Lesser General Public License v3 or later (LGPLv3+)",
"summary": "LTLf and PLTLf to Deterministic Finite-state Automata (DFA)",
"version": "1.0.2",
"project_urls": {
"Homepage": "https://github.com/whitemech/ltlf2dfa.git"
},
"split_keywords": [
"ltlf2dfa"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "f7723a89f5927f1abfbdb618b584849d52381db85d9654381d8e2299ccf5ee25",
"md5": "994fa3bbabc5e9c813f218d7cd3c0a42",
"sha256": "8218f9e16e74fbabed460772fe9d53525805d5d2f26aca64fba98f825137a684"
},
"downloads": -1,
"filename": "ltlf2dfa-1.0.2-py2.py3-none-any.whl",
"has_sig": false,
"md5_digest": "994fa3bbabc5e9c813f218d7cd3c0a42",
"packagetype": "bdist_wheel",
"python_version": "py2.py3",
"requires_python": null,
"size": 32275,
"upload_time": "2022-02-25T13:34:15",
"upload_time_iso_8601": "2022-02-25T13:34:15.039673Z",
"url": "https://files.pythonhosted.org/packages/f7/72/3a89f5927f1abfbdb618b584849d52381db85d9654381d8e2299ccf5ee25/ltlf2dfa-1.0.2-py2.py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "2eb2a659c37e6158c3742b2a427268fde1debaef54e2b3598d5758a0d872241d",
"md5": "3f8e919fbb9a823d7a086374ab6b13f1",
"sha256": "e2c9d7788bd319e753c2aae04dbb3b3bac8199438715104042308580911f8df3"
},
"downloads": -1,
"filename": "ltlf2dfa-1.0.2.tar.gz",
"has_sig": false,
"md5_digest": "3f8e919fbb9a823d7a086374ab6b13f1",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 30797,
"upload_time": "2022-02-25T13:34:17",
"upload_time_iso_8601": "2022-02-25T13:34:17.692406Z",
"url": "https://files.pythonhosted.org/packages/2e/b2/a659c37e6158c3742b2a427268fde1debaef54e2b3598d5758a0d872241d/ltlf2dfa-1.0.2.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2022-02-25 13:34:17",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "whitemech",
"github_project": "ltlf2dfa",
"travis_ci": false,
"coveralls": true,
"github_actions": true,
"tox": true,
"lcname": "ltlf2dfa"
}
JSON
