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

History

0.3.0 (2020-03-24)

• Refinement of all the grammars. Extensive improvement of the parsing.
• Integration with Pythomata >=0.3.0
• Simplified interfaces and refactoring of the class hierarchy for the logic modules.
• Introduced FiniteTraceWrapper. It allows evaluating any propositional over a finite trace.
• Several bug fixes and improved testing.
• Improvement of docs and metadata consistency.

0.2.3 (2019-10-10)

• Reverting some changes made on release 0.2.2.
• Updated live version: http://flloat.herokuapp.com/

0.2.2 (2019-10-09)

• Fix several issues in the computation of the delta function for LDLf.

0.2.1 (2019-10-09)

• Replace parsing library PLY with Lark.

0.2.0 (2019-10-06)

• Main refactoring of the package. No new features.

0.1.3 (2018-04-20)

• Support for LTLf formulas and conversion into NFA, DFA and DFA on-the-fly

0.1.1 (2018-04-15)

• Syntax, semantics and parsing support for the following formal languages:
  • Propositional Logic;
  • Linear Dynamic Logic on Finite Traces;
• Conversion from LDLf formula to NFA, DFA and DFA on-the-fly

0.1.0 (2018-04-11)

• First release on PyPI.