whitemech / flloat

From LTLf/LDLf To Automata
https://flloat.herokuapp.com/
GNU General Public License v3.0
21 stars 4 forks source link

'Or' object has no attribute 'simplify' #32

Open bittdy opened 2 years ago

bittdy commented 2 years ago

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.

marcofavorito commented 2 years ago

Thank you for your interest in the package.

Unfortunately FLLOAT is not super well maintained, as we switched to other projects.

May I suggest you to have a look at the following projects?

https://github.com/whitemech/pylogics https://github.com/whitemech/logaut

They do the same thing of FLLOAT, but in a more modular way. Logaut takes in input a Pylogics LTLf formula and gives in output a pythomata.DFA; please follow the instructions in the README (in particular, the installation of lydia)

marcofavorito commented 2 years ago

I will keep the issue open, as we will address it sometime in the future (I mean, sometime before the end of the universe)

bittdy commented 2 years ago

Thanks a lot for the recommendation and I will check them for my project. Meanwhile, hope your new projects go well!