flloat 0.2.1

A Python implementation of the FLLOAT library.

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.