Spot

spot@lrde.epita.fr

212 discussions

by Ioana Huștiu

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

1 year, 10 months

The test ltlcross4.test fails

by Yuri

+ 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

2 years

SPOT questions

by Yoav Ben Shimon

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

2 years

Spot Compilation on Windows

by Jonah Romero

Hello, I was just curious if there were any plans to support building Spot on windows? Or maybe any plans to use CMake in the future? If not, are there any suggestions for building on windows? Thanks, Jonah

2 years

APT install of python3-spot requires python version <<3.10

by mgerber59＠gmail.com

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: ``` The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. ``` Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

2 years, 1 month

Possible to allow for product_or without completing left/right automata

by Marcel Gerber

Hello, I notice that `product_or` necessarily runs `complete` on both input automata [see this line in spot/twaalgos/product.cc <https://gitlab.lre.epita.fr/spot/spot/-/blob/b487ff4190cdec4094154486bb8c04…>]. In contrast, this is not the case for the "normal" `product`. If my thinking is correct, this would not be necessary if both input automata are Büchi automata, correct? Because the union of two incomplete Büchi automata is an incomplete Büchi automaton again, and the product automaton construction applies as normal as far as I can tell. Would it be possible to allow for this, potentially by introducing another method or exposing the `product_aux` function (incl. from Python)? Right now, running `product_or`, even on small input automata, produces absolutely unwieldy automata that are impossible to interpret. This is mostly due to my use case, where I'm using letters of an alphabet more akin to a standard DFA model, and encoding a symbol of `a` into the preposition formula `a & !b & !c` etc. This works well with single automata and with intersections, but not with unions sadly. Your help would be very much appreciated, Marcel

2 years, 1 month

APT install of python3-spot requires python version <<3.10

by Marcel Gerber

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

2 years, 2 months

Spot bus error

by Beutner, Raven

Dear spot team, I think I found a bug in spot. When I run % cat foo.hoa HOA: v1 States: 1 Start: 0 AP: 3 "l0" "l1" "l2" acc-name: generalized-Buchi 0 Acceptance: 0 t --BODY-- State: 0 [(0&1)] 0 [(2)] 0 [(!2)] 0 —-END-- %autfilt --small -S foo.hoa I get a bus error. It seems that options —small and -S are both necessary to reproduce the bug. Similarly, none of the transitions in the automaton can be removed. I am running spot version 2.11.4 on an MacBook Pro with M1 Pro CPU compiled with --disable-python. Given that this seems to be a “low-level” system error, it could very well be that it is an issue with my machine setup. In this case: Do you have any idea how to fix this? Thanks already for your help! All the best, Raven PS: The current download link for the most recent version of spot (https://spot.lre.epita.fr/install.html) claims to download version 2.11.4 but actually still points to version 2.11.3.

2 years, 2 months

Test suite for spot installation

by Fraca Santamaria, Estibaliz

Hi, I'm trying to install spot in my machine. I run make check and I got two errors (Fail : 2). I am just reporting it as it is asked. Please find test-suite.log attached. The installation did fail. I would like to ask if you know why did it fail and what could I do to install it. Thank you

2 years, 3 months

Mac OS Spot Library Installation

by Samuel Hongang Lam

Hello All, I am a PhD student that has been working on a project recently with a code base using the Spot library. The code was written on a Linux machine, but I have a MacBook running macOS. There seem to be some dependencies in the Spot library on glibc functions, such as strverscmp. I am inexperienced with setting up the libraries and such properly. Is there anywhere I can get help with setting up Spot to be able to access the features I need on a Mac? Any assistance would be greatly appreciated. Thank you! Sincerely, Samuel Lam

2 years, 3 months

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot