<h1 align="center">
<b>logaut</b>
</h1>
<p align="center">
<a href="https://pypi.org/project/logaut">
<img alt="PyPI" src="https://img.shields.io/pypi/v/logaut">
</a>
<a href="https://pypi.org/project/logaut">
<img alt="PyPI - Python Version" src="https://img.shields.io/pypi/pyversions/logaut" />
</a>
<a href="">
<img alt="PyPI - Status" src="https://img.shields.io/pypi/status/logaut" />
</a>
<a href="">
<img alt="PyPI - Implementation" src="https://img.shields.io/pypi/implementation/logaut">
</a>
<a href="">
<img alt="PyPI - Wheel" src="https://img.shields.io/pypi/wheel/logaut">
</a>
<a href="https://github.com/whitemech/logaut/blob/master/LICENSE">
<img alt="GitHub" src="https://img.shields.io/github/license/marcofavorito/logaut">
</a>
</p>
<p align="center">
<a href="">
<img alt="test" src="https://github.com/whitemech/logaut/workflows/test/badge.svg">
</a>
<a href="">
<img alt="lint" src="https://github.com/whitemech/logaut/workflows/lint/badge.svg">
</a>
<a href="">
<img alt="docs" src="https://github.com/whitemech/logaut/workflows/docs/badge.svg">
</a>
<a href="https://codecov.io/gh/marcofavorito/logaut">
<img alt="codecov" src="https://codecov.io/gh/marcofavorito/logaut/branch/master/graph/badge.svg?token=FG3ATGP5P5">
</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/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">
</a>
</p>
LOGics formalisms to AUTomata
## What is `logaut`
Logaut is to the logics-to-DFA problem
what Keras is for Deep Learning:
a wrapper to performant back-ends,
but with human-friendly APIs.
## Install
To install the package from PyPI:
```
pip install logaut
```
Make sure to have [Lydia](https://github.com/whitemech/lydia)
installed on your machine.
We suggest the following setup:
- [Install Docker](https://www.docker.com/get-started)
- Download the Lydia Docker image:
```
docker pull whitemech/lydia:latest
```
- Make the Docker image executable under the name `lydia`.
On Linux and MacOS machines, the following commands should work:
```
echo '#!/usr/bin/env sh' > lydia
echo 'docker run -v$(pwd):/home/default whitemech/lydia lydia "$@"' >> lydia
sudo chmod u+x lydia
sudo mv lydia /usr/local/bin/
```
This will install an alias to the inline Docker image execution
in your system PATH. Instead of `/usr/local/bin/`
you may use another path which is still in the `PATH` variable.
On Windows, make a `.bat` file:
```
docker run --name lydia -v"%cd%":/home/default whitemech/lydia lydia %*
```
And add it to your PATH variable.
## Quickstart
Now you are ready to go:
```python
from logaut import ltl2dfa
from pylogics.parsers import parse_ltl
formula = parse_ltl("F(a)")
dfa = ltl2dfa(formula, backend="lydia")
```
The function `ltl2dfa` takes in input a
[pylogics](https://github.com/whitemech/pylogics)
`formula` and gives in output
a [pythomata](https://github.com/whitemech/pythomata) DFA.
Then, you can manipulate the DFA as done with Pythomata,
e.g. to print:
```
dfa.to_graphviz().render("eventually.dfa")
```
Currently, the `lydia` backend only supports
the `ltl` and `ldl` logics.
The `ltlf2dfa`, based on
[LTLf2DFA](https://github.com/whitemech/LTLf2DFA/),
supports `ltl` and `pltl`.
First, install it at version `1.0.1`:
```
pip install git+https://github.com/whitemech/LTLf2DFA.git@develop#egg=ltlf2dfa
```
Then, you can use:
```python
from logaut import pltl2dfa
from pylogics.parsers import parse_pltl
formula = parse_pltl("a S b")
dfa = pltl2dfa(formula, backend="ltlf2dfa")
```
## Write your own backend
You can write your back-end by implementing
the `Backend` interface:
```python
from logaut.backends.base import Backend
class MyBackend(Backend):
def ltl2dfa(self, formula: Formula) -> DFA:
"""From LTL to DFA."""
def ldl2dfa(self, formula: Formula) -> DFA:
"""From LDL to DFA."""
def pltl2dfa(self, formula: Formula) -> DFA:
"""From PLTL to DFA."""
def pldl2dfa(self, formula: Formula) -> DFA:
"""From PLDL to DFA."""
def fol2dfa(self, formula: Formula) -> DFA:
"""From FOL to DFA."""
def mso2dfa(self, formula: Formula) -> DFA:
"""From MSO to DFA."""
```
Then, you can register the custom backend
class in the library:
```python
from logaut.backends import register
register(id_="my_backend", entry_point="dotted.path.to.MyBackend")
```
And then, use it through the main entry point:
```python
dfa = ltl2dfa(formula, backend="my_backend")
```
## Tests
To run tests: `tox`
To run only the code tests: `tox -e py3.7`
To run only the linters:
- `tox -e flake8`
- `tox -e mypy`
- `tox -e black-check`
- `tox -e isort-check`
Please look at the `tox.ini` file for the full list of supported commands.
## 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
logaut is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).
Copyright 2021 WhiteMech
## Authors
- [Marco Favorito](https://marcofavorito.me/)
Raw data
{
"_id": null,
"home_page": "https://marcofavorito.me/logaut",
"name": "logaut",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.8,<4.0",
"maintainer_email": "",
"keywords": "",
"author": "Marco Favorito",
"author_email": "marco.favorito@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/75/b9/03d0cf21bfcdec1d4981e6e89547410a6a115ec9d0d54e150ef158348d51/logaut-0.2.0.tar.gz",
"platform": null,
"description": "<h1 align=\"center\">\n <b>logaut</b>\n</h1>\n\n<p align=\"center\">\n <a href=\"https://pypi.org/project/logaut\">\n <img alt=\"PyPI\" src=\"https://img.shields.io/pypi/v/logaut\">\n </a>\n <a href=\"https://pypi.org/project/logaut\">\n <img alt=\"PyPI - Python Version\" src=\"https://img.shields.io/pypi/pyversions/logaut\" />\n </a>\n <a href=\"\">\n <img alt=\"PyPI - Status\" src=\"https://img.shields.io/pypi/status/logaut\" />\n </a>\n <a href=\"\">\n <img alt=\"PyPI - Implementation\" src=\"https://img.shields.io/pypi/implementation/logaut\">\n </a>\n <a href=\"\">\n <img alt=\"PyPI - Wheel\" src=\"https://img.shields.io/pypi/wheel/logaut\">\n </a>\n <a href=\"https://github.com/whitemech/logaut/blob/master/LICENSE\">\n <img alt=\"GitHub\" src=\"https://img.shields.io/github/license/marcofavorito/logaut\">\n </a>\n</p>\n<p align=\"center\">\n <a href=\"\">\n <img alt=\"test\" src=\"https://github.com/whitemech/logaut/workflows/test/badge.svg\">\n </a>\n <a href=\"\">\n <img alt=\"lint\" src=\"https://github.com/whitemech/logaut/workflows/lint/badge.svg\">\n </a>\n <a href=\"\">\n <img alt=\"docs\" src=\"https://github.com/whitemech/logaut/workflows/docs/badge.svg\">\n </a>\n <a href=\"https://codecov.io/gh/marcofavorito/logaut\">\n <img alt=\"codecov\" src=\"https://codecov.io/gh/marcofavorito/logaut/branch/master/graph/badge.svg?token=FG3ATGP5P5\">\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/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 </a>\n</p>\n\n\nLOGics formalisms to AUTomata\n\n## What is `logaut`\n\nLogaut is to the logics-to-DFA problem\nwhat Keras is for Deep Learning:\na wrapper to performant back-ends,\nbut with human-friendly APIs.\n\n## Install\n\nTo install the package from PyPI:\n```\npip install logaut\n```\n\nMake sure to have [Lydia](https://github.com/whitemech/lydia) \ninstalled on your machine.\nWe suggest the following setup:\n\n- [Install Docker](https://www.docker.com/get-started)\n- Download the Lydia Docker image:\n```\ndocker pull whitemech/lydia:latest\n```\n- Make the Docker image executable under the name `lydia`.\n On Linux and MacOS machines, the following commands should work:\n```\necho '#!/usr/bin/env sh' > lydia\necho 'docker run -v$(pwd):/home/default whitemech/lydia lydia \"$@\"' >> lydia\nsudo chmod u+x lydia\nsudo mv lydia /usr/local/bin/\n```\n\n\nThis will install an alias to the inline Docker image execution\nin your system PATH. Instead of `/usr/local/bin/`\nyou may use another path which is still in the `PATH` variable.\n\nOn Windows, make a `.bat` file:\n```\ndocker run --name lydia -v\"%cd%\":/home/default whitemech/lydia lydia %*\n```\nAnd add it to your PATH variable.\n\n\n## Quickstart\n\nNow you are ready to go:\n```python\nfrom logaut import ltl2dfa\nfrom pylogics.parsers import parse_ltl\nformula = parse_ltl(\"F(a)\")\ndfa = ltl2dfa(formula, backend=\"lydia\")\n```\n\nThe function `ltl2dfa` takes in input a \n[pylogics](https://github.com/whitemech/pylogics) \n`formula` and gives in output\na [pythomata](https://github.com/whitemech/pythomata) DFA.\n\nThen, you can manipulate the DFA as done with Pythomata,\ne.g. to print:\n```\ndfa.to_graphviz().render(\"eventually.dfa\")\n```\n\nCurrently, the `lydia` backend only supports\nthe `ltl` and `ldl` logics.\n\nThe `ltlf2dfa`, based on \n[LTLf2DFA](https://github.com/whitemech/LTLf2DFA/),\nsupports `ltl` and `pltl`.\nFirst, install it at version `1.0.1`:\n```\npip install git+https://github.com/whitemech/LTLf2DFA.git@develop#egg=ltlf2dfa\n```\n\nThen, you can use:\n```python\nfrom logaut import pltl2dfa\nfrom pylogics.parsers import parse_pltl\nformula = parse_pltl(\"a S b\")\ndfa = pltl2dfa(formula, backend=\"ltlf2dfa\")\n```\n\n## Write your own backend\n\nYou can write your back-end by implementing\nthe `Backend` interface:\n\n```python\nfrom logaut.backends.base import Backend\n\nclass MyBackend(Backend):\n\n def ltl2dfa(self, formula: Formula) -> DFA:\n \"\"\"From LTL to DFA.\"\"\"\n\n def ldl2dfa(self, formula: Formula) -> DFA:\n \"\"\"From LDL to DFA.\"\"\"\n\n def pltl2dfa(self, formula: Formula) -> DFA:\n \"\"\"From PLTL to DFA.\"\"\"\n\n def pldl2dfa(self, formula: Formula) -> DFA:\n \"\"\"From PLDL to DFA.\"\"\"\n \n def fol2dfa(self, formula: Formula) -> DFA:\n \"\"\"From FOL to DFA.\"\"\"\n\n def mso2dfa(self, formula: Formula) -> DFA:\n \"\"\"From MSO to DFA.\"\"\"\n```\n\nThen, you can register the custom backend\nclass in the library:\n\n```python\nfrom logaut.backends import register\nregister(id_=\"my_backend\", entry_point=\"dotted.path.to.MyBackend\")\n```\n\nAnd then, use it through the main entry point:\n```python\ndfa = ltl2dfa(formula, backend=\"my_backend\")\n```\n\n## Tests\n\nTo run tests: `tox`\n\nTo run only the code tests: `tox -e py3.7`\n\nTo run only the linters: \n- `tox -e flake8`\n- `tox -e mypy`\n- `tox -e black-check`\n- `tox -e isort-check`\n\nPlease look at the `tox.ini` file for the full list of supported commands. \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\nlogaut is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).\n\nCopyright 2021 WhiteMech\n\n## Authors\n\n- [Marco Favorito](https://marcofavorito.me/)\n\n",
"bugtrack_url": null,
"license": "GPL-3.0-or-later",
"summary": "From logic to automata.",
"version": "0.2.0",
"project_urls": {
"Bug Tracker": "https://github.com/whitemech/logaut/issues",
"Documentation": "https://marcofavorito.me/logaut",
"Homepage": "https://marcofavorito.me/logaut",
"Pull Requests": "https://github.com/whitemech/logaut/pulls",
"Repository": "https://github.com/whitemech/logaut.git"
},
"split_keywords": [],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "604d73eb7d67d279cf858ec61a7c2d738eee4c01c1c331e6385ecf492331a3ff",
"md5": "3a7854dec962f6a9493274d7157a86e9",
"sha256": "5ebcda45a5a83ea4c60baed5ce8c90783c61763dfbab971b84d109939e9e6225"
},
"downloads": -1,
"filename": "logaut-0.2.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "3a7854dec962f6a9493274d7157a86e9",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8,<4.0",
"size": 32884,
"upload_time": "2023-06-06T11:41:41",
"upload_time_iso_8601": "2023-06-06T11:41:41.384733Z",
"url": "https://files.pythonhosted.org/packages/60/4d/73eb7d67d279cf858ec61a7c2d738eee4c01c1c331e6385ecf492331a3ff/logaut-0.2.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "75b903d0cf21bfcdec1d4981e6e89547410a6a115ec9d0d54e150ef158348d51",
"md5": "01cc4fdb4820a5bda70353677634ec39",
"sha256": "35f82c7726dd53f6201fb6e440133e8d93b8a826810f7d3d8c46477afd6865bd"
},
"downloads": -1,
"filename": "logaut-0.2.0.tar.gz",
"has_sig": false,
"md5_digest": "01cc4fdb4820a5bda70353677634ec39",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8,<4.0",
"size": 19271,
"upload_time": "2023-06-06T11:41:43",
"upload_time_iso_8601": "2023-06-06T11:41:43.016587Z",
"url": "https://files.pythonhosted.org/packages/75/b9/03d0cf21bfcdec1d4981e6e89547410a6a115ec9d0d54e150ef158348d51/logaut-0.2.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-06-06 11:41:43",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "whitemech",
"github_project": "logaut",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"tox": true,
"lcname": "logaut"
}
JSON
