A Python implementation of the FLLOAT library.
Project description
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.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
flloat-0.3.0.tar.gz
(48.4 kB
view hashes)
Built Distribution
flloat-0.3.0-py2.py3-none-any.whl
(39.8 kB
view hashes)
Close
Hashes for flloat-0.3.0-py2.py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4423ee6fe4df59669493101e1bcbfc1089ea4809fc48d1029923d363527c418c |
|
MD5 | 470b41f9fe040dc95ba3eefe966c9d06 |
|
BLAKE2b-256 | 62259e0f75576ce2a7d85e89eecf856938d144f5ed66edee41df74e3310b11b8 |