logaut


Namelogaut JSON
Version 0.2.0 PyPI version JSON
download
home_pagehttps://marcofavorito.me/logaut
SummaryFrom logic to automata.
upload_time2023-06-06 11:41:43
maintainer
docs_urlNone
authorMarco Favorito
requires_python>=3.8,<4.0
licenseGPL-3.0-or-later
keywords
VCS
bugtrack_url
requirements No requirements were recorded.
Travis-CI No Travis.
coveralls test coverage No coveralls.
            <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"
}
        
Elapsed time: 0.08326s