logaut

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 installed on your machine. We suggest the following setup:

• Install Docker
• 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:

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 formula and gives in output a 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, 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:

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:

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:

from logaut.backends import register
register(id_="my_backend", entry_point="dotted.path.to.MyBackend")

And then, use it through the main entry point:

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

License

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

Copyright 2021 WhiteMech

Authors

• Marco Favorito