A Python implementation of the FLLOAT library.
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 .
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}
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
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.
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)
Syntax, semantics and parsing support for the following formal languages:
Conversion from LTLf/LDLf formula to DFA
To run the tests:
tox
To run only the code tests:
tox -e py37
To run only the code style checks:
tox -e flake8
To build the docs:
mkdocs build
To view documentation in a browser
mkdocs serve
and then go to http://localhost:8000
FLLOAT is released under the GNU Lesser General Public License v3.0 or later (LGPLv3+).
Copyright 2018-2020 WhiteMech