Spot May 2023

spot@lrde.epita.fr

3 participants
4 discussions

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

1 year, 8 months

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

1 year, 8 months

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

1 year, 9 months

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

1 year, 9 months

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot May 2023