Dear Spot Developer,

My name is Jun, and I am reaching out to you regarding an issue I've encountered while working with the Spot package. I have successfully installed the Spot package on two different computers with Linux systems of different versions. The Spot package functions perfectly in Terminator, allowing me to execute all official website shell codes.

However, I am encountering an issue in Python. While I can import the Spot package without errors, attempting to run any functions like spot.formula or spot.translate results in “AttributeError: module 'spot' has no attribute 'formula'”. I have tried simply copying and pasting any example codes from the official website, but the problem persists. Could you tell me how to solve this problem?

If you need any further information, please don’t hesitate to ask. Many thanks in advance.

Best regards,

Jun Luo

The original codes from the example on official website and the output:

import sys

sys.path.append('/u/halle/luju/home_at/spot')

import spot

print(spot.formula('[]<>p0 || <>[]p1'))
f = spot.formula('& & G p0 p1 p2')
print(f.to_str('latex'))
print(f.to_str('lbt'))
print(f.to_str('spin', parenth=True))

custom_print(spot.automaton("tut21.hoa"))

Output:

/u/halle/luju/home_at/Desktop/a.py
Traceback (most recent call last):
  File "/u/halle/luju/home_at/Desktop/a.py", line 7, in <module>
    print(spot.formula('[]<>p0 || <>[]p1'))
AttributeError: module 'spot' has no attribute 'formula'

Process finished with exit code 1

Just input spot:

import sys

sys.path.append('/u/halle/luju/home_at/spot')

import spot

Output:

/u/halle/luju/home_at/Desktop/a.py

Process finished with exit code 0