First thanks to all the authors for your time to develop this useful tool.
Recently I am trying to use the flloat to do model checking on my laptop with Windows 10, Python 3.6.
And the test code is as follows

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)

graph = dfa.to_graphviz()
graph.render("./my-automaton")

Then Python raises an error:

Traceback (most recent call last):
  File "d:/ownCode/Attension-Based-RL-for-STL-main/ppo-mujoco-rnnrewardnet-attention-last/algorithm/test.py", line 25, in <module>
    dfa = parsed_formula.to_automaton()
  File "D:\code\anaconda3\lib\site-packages\flloat\ltlf.py", line 74, in to_automaton
    return to_automaton(self)
  File "D:\code\anaconda3\lib\site-packages\flloat\flloat.py", line 215, in to_automaton
    minimized = determinized.minimize()
  File "D:\code\anaconda3\lib\site-packages\pythomata\impl\symbolic.py", line 319, in minimize
    new_guard = (guard | old_guard).simplify()
AttributeError: 'Or' object has no attribute 'simplify'

I find this error is related to 'Sympy' but I have no idea how to fix it. I appreciate it if you can give me any suggestions.

Subject of the issue

Atomic symbols in LDLf don't fully respect the interface LDLfFormula. In fact, conversion fails, due to the missing _delta() function.

I think i can quickly address this before merging #24 .
I'll try to check and use LDLfPropositionalAtom instead of FiniteTraceWrapper.

Your environment

• Python version: 3.7.3
• Package Version: commit 91549be (release candidate 0.3.0)

Steps to reproduce

from flloat.parser.ldlf import LDLfParser

f = LDLfParser()("A & B")
a = f.to_automaton()

Expected behaviour

Conversion to the correct automaton.

Actual behaviour

TypeError: PLAtomic has ho _delta function.

Is your feature request related to a problem? Please describe.
Currently, it is still legal to create an LDLf formula whose atoms have upper-cased characters, differently from LTLf.

from flloat.parser.ltlf import LTLfParser
LTLfParser()("F(a)") # this is OK
LTLfParser()("F(A)") # this raises error

from flloat.parser.ldlf import LDLfParser
LTLfParser()("a") # this is OK
LTLfParser()("A") # this is OK although should raise exception

Describe the solution you'd like
Update LDLf module to forbid uppercased propositions.

Describe alternatives you've considered

Additional context

Is your feature request related to a problem? Please describe.

Describe the solution you'd like

Consider restricting the set of possible strings for atomic symbols, similar to what is done by
SPOT, Section 2.2.

Describe alternatives you've considered

Additional context

Subject of the issue

Last, End are special symbols that should have a special meaning. After #18 , these are no longer ignored, but they are parsed correctly. However, the feature is still not supported. There is no LTLfLast class, and LTLfEnd must be tested. Writing last or end inside a LTLf parsed formula causes a NotImplementedError.

Your environment

• OS: any
• Python version: using Python 3.7.3, should apply to any.
• Package Version: no branch support this feature up to now (4/3/20)

• FLLOAT version: 0.1.4.post1
• Python version: 3.6.0
• Operating System: Ubuntu

Description

I want to create object of FunctionSymbol but I think the class definition is wrong so I can't initialize it.

What I Did

from flloat.base.Symbol import FunctionSymbol
>>> symbol = FunctionSymbol('A', 2)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: str() argument 2 must be str, not int

Now matter what argument you pass, object of this class won't be created. The same is true for PredicateSymbol.

Subject of the issue

It seems the truth evaluation of *Implies formulas does not work correctly (see here for an example).

Your environment

• OS: N/A
• Python version: N/A
• Package Version: N/A (the issue is on develop).

Steps to reproduce

Expected behaviour

Actual behaviour

Subject of the issue

I just copied this code from documentation. But it throws the error

`
from flloat.parser.ltlf import LTLfParser

parser = LTLfParser()
formula = "F (A & !B)"
parsed_formula = parser(formula)
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)
dfa = parsed_formula.to_automaton()
assert dfa.accepts(t1)
assert not dfa.accepts(t2)
`

Your environment

• OS: Ubuntu
• Python version: 3.6
• Package Version 0.3.0