Hi,
With the Python API, is it possible to directly access the condition formulas on the automata edges? Statements like "aut.show_storage("v”)” will display them in a table. Yet if I cycle through my edges (for ed in aut.out(s):) and look at ed.cond I see it’s a buddy BDD. I can’t go any further than that. Looking at the Buddy SWIG file included with Spot shows many functions that appear to be able to view or manipulate the bdd but most of them appear to not be populated for Python - much like the state exposure noted in the example Python Jupyter notebooks. I wrote a really crude lex/yacc routine to parse the dot file and get the formulas but that seems a bit of ugly work duplication.
Any help or advice would be appreciated.
Thank-you for your time,
John Komp
Department of Computer Science
University of Colorado, Boulder
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
Dear all,
there seems to be a problem with the translation LTLf -> LTL,
as supported by the "ltlfilt --from-ltlf" command from the SPOT distribution.
It seems that subformulas of the type "X p" get translated into "X (!alive | p)"
instead of "X (alive & p)", as they should be according to the LTLf semantics,
as well as the translation outlined in the Memocode '14 paper by Dutta
and Vardi.
Do you agree or am I missing something?
By the way, we are planning to use SPOT as part
of a toolchain to check the satisfiability of a flavor of LTLf-modulo-theory.
Thanks,
Marco Faella
--
Associate professor
Electrical Engineering and Information Technologies
University of Naples Federico II, Italy
http://wpage.unina.it/m.faella
Hello,
Using the Spot C++ API I am having a strange issue testing whether a formula is safety or liveness. Specifically, many of the formulas I am testing are coming back as both safety and liveness, despite being non-trivial.
My code snippet for the testing is (with some extraneous steps omitted):
>>>
int simplification_level = 3;
spot::tl_simplifier_options tlopt(simplification_level);
spot::tl_simplifier simpl(tlopt);
spot::parsed_formula pf = spot::parse_infix_psl(ltl);
spot::formula f = simpl.simplify(pf.f);
spot::twa_graph_ptr aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
safe = f.is_syntactic_safety() || is_safety_automaton(aut);
live = is_liveness_automaton(aut);
<<<
Here `safe` and `live` are both booleans. It is based on similar code within `/bin/ltlfilt.cc <http://ltlfilt.cc/>` in the Spot codebase.
However, for many formulas this code resolves both `safe` and `live` to true. As a concrete example, when I test
```
G((!"(P_0 == 'p1')" & !"(P_0 == 'p2')" & !"(P_0 == 'p3')") | F"(P_0 == 'CS')")
```
(after simplification, and derived from the BEEM benchmarks) both resolve to true.
Am I using the testing API incorrectly? Is this a bug in Spot? Or is the formula malformed in some way that isn’t obvious to me?
Thanks in advance for any help you can give.
Samuel Judson
Bonjour,
J'ai installé spot sur macos(M2).
Pour les logiciels cela a l'air de marcher.
Par contre quand j'ai voulu uitiliser les
bindings Python, j'ai eu des problèmes qui
semblent dûs à l'architecture ARM.
Voici mon test Python et le résulat:
-----
import sys
import os
sys.path.insert(0, '/usr/local/lib/python3.10/site-packages') #
homonymie avec un autre spot.
import spot
f = spot.formula("FGa -> (GFb & GF(c & b & d & e))")
-----
résultat
-------
dali:~ filali$ cd /Users/filali ; /usr/bin/env
/opt/homebrew/bin/python3
/Users/filali/.vscode/extensions/ms-python.python-2023.19.12901009/pythonFiles/lib/python/debugpy/adapter/../../debugpy/launcher
57565 -- /Users/filali/test_spot.py
Traceback (most recent call last):
File "/Users/filali/test_spot.py", line 4, in <module>
import spot
File "/usr/local/lib/python3.10/site-packages/spot/__init__.py", line
49, in <module>
from spot.impl import *
File "/usr/local/lib/python3.10/site-packages/spot/impl.py", line 10,
in <module>
from . import _impl
ImportError:
dlopen(/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so,
0x0002): tried:
'/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so'
(mach-o file, but is an incompatible architecture (have 'x86_64', need
'arm64')),
'/System/Volumes/Preboot/Cryptexes/OS/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so'
(no such file),
'/usr/local/lib/python3.10/site-packages/spot/_impl.cpython-310-darwin.so'
(mach-o file, but is an incompatible architecture (have 'x86_64', need
'arm64'))
------
Merci pour votre aide.
Mamoun Filali
PS (je pense avoir installé la version de dev.)
Dear Spot development team,
I am currently working on a python project that uses Spot to process
omega-automata. We want to use tgba_powerset() and obtain a map from states
of the original automaton to the sets representing states of the
deterministic automaton. There is a struct power_map, which one can obtain
when passing it as an argument to tgba_powerset(). However, it returns
SwigPyObject (obtained form C++ method) that is not iterable and we cannot
convert the object to Python dictionary/list/set. One can use
power_map.states_of(const int), however it is also not iterable. Is there a
workaround for this problem? Could you add support for this in python or
make power_map.states_of(const int) iterable?
This fix would be a big help to our project from which we want to publish a
paper soon. Thank you very much for the possible collaboration.
Best regards,
Marek Jankola
Ioana Huștiu <ioana.hustiu(a)academic.tuiasi.ro> writes:
> Well, I am trying to install the 2.11.6 version (the latest that is
> available on the website).
> My computer has Windows, but I tried to install it on a virtual
> machine with Debian 11. I have attached all the commands and their
> outputs below.
I see that "make check" failed only the randltl.ipynb test,
but given than (1) all other Python tests passed, and (2)
what the error looks like, I believe that tests/python/randltl.ipynb
has been modified compared to was was in the tarball.
Probably you tried to open it, execute the first cell, and that
created an error message that was saved into the file.
> A minor curiosity of mine: can the tool be used by using Visual
> Studio Code and python after installation?
No idea. I'm not familiar with Visual Studio or Windows.
Dear authors,
I am a PhD student at Technical University of Iasi, Romania and I also work
with professor Cristian Mahulea from University of Zaragoza, Spain. During
my research I'm finding the Spot tool to be very useful.
I am writing to you as I encountered an error during the installation of
Spot during the "make check" step. The generated file is attached below and
it is not clear to me how I can solve this problem.
I tried multiple times to install the tool, even by skipping the "make
check" step, but in this case another error appeared when trying to install
the stable package "python3-spot" - the python version that I have (meaning
3.9.7) is not >=3 python 3.5, which is quite strange.
What would you recommend me to do?
Thank you,
Ioana Hustiu
+ cat
+ /usr/local/bin/python3.9 test.py
Traceback (most recent call last):
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py",
line 1490, in array_func
result = self.grouper._cython_operation(
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 959, in _cython_operation
return cy_op.cython_operation(
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 657, in cython_operation
return self._cython_op_ndim_compat(
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 482, in _cython_op_ndim_compat
res = self._call_cython_op(
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 541, in _call_cython_op
func = self._get_cython_function(self.kind, self.how, values.dtype,
is_numeric)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 173, in _get_cython_function
raise NotImplementedError(
NotImplementedError: function is not implemented for this dtype:
[how->mean,dtype->object]
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "/usr/local/lib/python3.9/site-packages/pandas/core/nanops.py",
line 1692, in _ensure_numeric
x = float(x)
ValueError: could not convert string to float: '(G(F(p0))) &
(G(F(p1)))!((G(F(p0))) & (G(F(p1))))(G(F(p0))) -> (G(F(p1)))!((G(F(p0)))
-> (G(F(p1))))'
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "/usr/local/lib/python3.9/site-packages/pandas/core/nanops.py",
line 1696, in _ensure_numeric
x = complex(x)
ValueError: complex() arg is a malformed string
The above exception was the direct cause of the following exception:
Traceback (most recent call last):
File
"/usr/ports/math/spot/work/spot-2.11.5/tests/core/ltlcross4.dir/test.py",
line 12, in <module>
print(x.filter(('formula', 'tool',
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py",
line 1269, in aggregate
result = op.agg()
File "/usr/local/lib/python3.9/site-packages/pandas/core/apply.py",
line 166, in agg
return self.agg_list_like()
File "/usr/local/lib/python3.9/site-packages/pandas/core/apply.py",
line 355, in agg_list_like
new_res = colg.aggregate(arg, *self.args, **self.kwargs)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py",
line 238, in aggregate
ret = self._aggregate_multiple_funcs(func, *args, **kwargs)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py",
line 316, in _aggregate_multiple_funcs
results[key] = self.aggregate(func, *args, **kwargs)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/generic.py",
line 250, in aggregate
return getattr(self, cyfunc)()
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py",
line 1855, in mean
result = self._cython_agg_general(
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py",
line 1507, in _cython_agg_general
new_mgr = data.grouped_reduce(array_func)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/internals/base.py",
line 197, in grouped_reduce
res = func(arr)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py",
line 1503, in array_func
result = self._agg_py_fallback(values, ndim=data.ndim, alt=alt)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/groupby.py",
line 1457, in _agg_py_fallback
res_values = self.grouper.agg_series(ser, alt, preserve_dtype=True)
File
"/usr/local/lib/python3.9/site-packages/pandas/core/groupby/ops.py",
line 994, in agg_series
result = self._aggregate_series_pure_python(obj, func)
Version: 2.11.5
FreeBSD 13.2
Yuri
Hi,
I ran into a couple of issues when using SPOT in a project. I'll be glad
for any assistance.
1) I am calling sat_minimize from a python script using the spot python
library. Is there any way to set a timeout on this function call? Or do I
have to use the CLI if I want a timeout?
2) I am manipulating an automaton generated from an LTL formula, and then
printing it in HOA format. Is there a way to guarantee that the initial
state is the state numbered 0? If not, is there any other way to control
the naming of states?
Thank you,
Yoav Ben Shimon
