A Python implementation of the FLLOAT library.
Project description
FLLOAT
A Python implementation of the FLLOAT library.
- Free software: Apache 2.0 license
- Documentation: https://marcofavorito.github.io/flloat/
Dependencies
The package depends on Pythomata. Please follow the install instruction to get all the needed dependencies.
Install
- from PyPI:
pip install flloat
- or, from source (
master
branch):
pip install git+https://github.com/marcofavorito/flloat.git
- or, clone the repository and install:
git clone htts://github.com/marcofavorito/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:
from flloat.semantics.traces import FiniteTrace
t1 = FiniteTrace.from_symbol_sets([
{},
{"A"},
{"A"},
{"A", "B"},
{}
])
formula.truth(t1, 0) # True
- Transform it into an automaton (
pythomata.DFA
object):
dfa = formula.to_automaton()
# print the automaton
dfa.to_dot("./automaton.DFA")
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
from flloat.semantics.traces import FiniteTrace
# parse the formula
parser = LTLfParser()
formula_string = "F (A & !B)"
formula = parser(formula_string)
# evaluate over finite traces
t1 = FiniteTrace.from_symbol_sets([
{},
{"A"},
{"A"},
{"A", "B"}
])
assert formula.truth(t1, 0)
# from LTLf formula to DFA
dfa = formula.to_automaton()
assert dfa.accepts(t1.trace)
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
Copyright 2018-2019 Marco Favorito
History
0.1.0 (2018-04-11)
- First release on PyPI.
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.3 (2018-04-20)
- Support for LTLf formulas and conversion into NFA, DFA and DFA on-the-fly
0.2.0 (2019-10-06)
- Main refactoring of the package. No new features.
0.2.1 (2019-10-09)
- Replace parsing library PLY with Lark.
0.2.2 (2019-10-09)
- Fix several issues in the computation of the delta function for LDLf.
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.2.2.tar.gz
(47.1 kB
view hashes)