FLLOAT

A Python implementation of the FLLOAT library.

Links

• GitHub: https://github.com/whitemech/flloat
• PyPI: https://pypi.org/project/flloat/
• Documentation: https://whitemech.github.io/flloat
• Changelog: https://whitemech.github.io/flloat/release-history/
• Issue Tracker:https://github.com/whitemech/flloat/issues
• Download: https://pypi.org/project/flloat/#files

Install

• from PyPI:

pip install flloat

• or, from source (master branch):

pip install git+https://github.com/whitemech/flloat.git

• or, clone the repository and install:

git clone htts://github.com/whitemech/flloat.git
cd flloat
pip install .

How to use

• Parse a LDLf formula:

from flloat.parser.ldlf import LDLfParser

parser = LDLfParser()
formula_string = "<true*; a & b>tt"
formula = parser(formula_string)        # returns a LDLfFormula

print(formula)                          # prints "<((true)* ; (a & b))>(tt)"
print(formula.find_labels())            # prints {a, b}

• Evaluate it over finite traces:

t1 = [
    {"a": False, "b": False},
    {"a": True, "b": False},
    {"a": True, "b": False},
    {"a": True, "b": True},
    {"a": False, "b": False},
]
formula.truth(t1, 0)  # True

• Transform it into an automaton (pythomata.SymbolicAutomaton object):

dfa = formula.to_automaton()
assert dfa.accepts(t1)

# print the automaton
graph = dfa.to_graphviz()
graph.render("./my-automaton")  # requires Graphviz installed on your system.

Notice: to_dot requires Graphviz. For info about how to use a pythomata.DFA please look at the Pythomata docs.

• The same for a LTLf formula:

from flloat.parser.ltlf import LTLfParser

# parse the formula
parser = LTLfParser()
formula = "F (a & !b)"
parsed_formula = parser(formula)

# evaluate over finite traces
t1 = [
    {"a": False, "b": False},
    {"a": True, "b": False},
    {"a": True, "b": False},
    {"a": True, "b": True},
    {"a": False, "b": False},
]
assert parsed_formula.truth(t1, 0)
t2 = [
    {"a": False, "b": False},
    {"a": True, "b": True},
    {"a": False, "b": True},
]
assert not parsed_formula.truth(t2, 0)

# from LTLf formula to DFA
dfa = parsed_formula.to_automaton()
assert dfa.accepts(t1)
assert not dfa.accepts(t2)

Features

• Syntax, semantics and parsing support for the following formal languages:

  • Propositional Logic;
  • Linear Temporal Logic on Finite Traces
  • Linear Dynamic Logic on Finite Traces;

• Conversion from LTLf/LDLf formula to DFA

Tests

To run the tests:

tox

To run only the code tests:

tox -e py37

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

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

Copyright 2018-2020 WhiteMech