Skip to main content

A Python implementation of the FLLOAT library.

Project description

FLLOAT

FLLOAT Continuous Integration pipeline. codecov

A Python implementation of the FLLOAT library.

Links

Install

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)

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.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for flloat, version 0.3.0
Filename, size File type Python version Upload date Hashes
Filename, size flloat-0.3.0-py2.py3-none-any.whl (39.8 kB) File type Wheel Python version py2.py3 Upload date Hashes View
Filename, size flloat-0.3.0.tar.gz (48.4 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page