Skip to content
This repository has been archived by the owner on Oct 9, 2022. It is now read-only.

whitemech/flloat

Repository files navigation

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