# FLLOAT
[](https://pypi.python.org/pypi/flloat)
[](https://pypi.python.org/pypi/flloat)
[](
https://github.com/whitemech/flloat/actions?query=workflow%3A%22FLLOAT+Continuous+Integration+pipeline.%22)
[](https://codecov.io/gh/whitemech/flloat)
[](https://www.mkdocs.org/)
[](https://img.shields.io/badge/flake8-checked-blueviolet)
[](https://img.shields.io/badge/mypy-checked-blue)
[](https://img.shields.io/badge/license-LGPLv3%2B-blue)
[](https://doi.org/10.5281/zenodo.2577006)
A Python implementation of the [FLLOAT](https://github.com/RiccardoDeMasellis/FLLOAT.git) library.
## Links
- GitHub: [https://github.com/whitemech/flloat](https://github.com/whitemech/flloat)
- PyPI: [https://pypi.org/project/flloat/](https://pypi.org/project/flloat/)
- Documentation: [https://whitemech.github.io/flloat](https://whitemech.github.io/flloat)
- Changelog: [https://whitemech.github.io/flloat/release-history/](https://whitemech.github.io/flloat/release-history/)
- Issue Tracker:[https://github.com/whitemech/flloat/issues](https://github.com/whitemech/flloat/issues)
- Download: [https://pypi.org/project/flloat/#files](https://pypi.org/project/flloat/#files)
## Install
- from [PyPI](https://pypi.org/project/flloat/):
```
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:
```python
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:
```python
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):
```python
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](https://graphviz.gitlab.io/download/).
For info about how to use a `pythomata.DFA` please look at the [Pythomata docs](https://github.com/whitemech/pythomata).
* The same for a LTLf formula:
```python
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](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/](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](https://github.com/lark-parser/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.