Spot

spot@lrde.epita.fr

212 discussions

by Maxime Bouton

Dear spot maintainers, I am trying to compile spot v2.9.7 from source but my build errors due to latexmk not being available in the environment. From what I understand from the log, it is used in making the doc, is there a way to skip this step in the build? I built it on ubuntu (gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0) and it did not complain about latexmk, this only happened when changing to a new platform (the end goal is to cross compile it). Any help would be appreciated, Maxime I am using a linux platform with gcc: x86_64-linux-gnu-g++ (GCC) 9.1.0 Here is what I run: ./configure --prefix=${prefix}/spot-build --build=${MACHTYPE} --host=${target} --disable-python make -j${nproc} && make install Here is the partial log: ``` [15:46:03] Making all in doc [15:46:03] make[2]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] Making all in tl [15:46:03] make[3]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] BIBINPUTS='./..' latexmk -pdf -ps- -dvi- -pvc- -e '$bibtex_use=2' -e '$pdflatex="pdflatex %O \"\\def\\SpotVersion{2.9.7}\\input{%S}\""' ./tl.tex [15:46:03] /bin/sh: latexmk: not found [15:46:03] make[3]: *** [Makefile:1399: tl.pdf] Error 127 [15:46:03] make[3]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] make[2]: *** [Makefile:1319: all-recursive] Error 1 [15:46:03] make[2]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] make[1]: *** [Makefile:1341: all-recursive] Error 1 [15:46:03] make[1]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7' ````

4 years, 1 month

[Not-really-Spot] BDD libraries

by Michaël Cadilhac

Hi there ADL & all, Apologies for the not-really-spot question, but the expertise on this list is quite unique! I'm about to embark on a new project that relies on BDD. My only experience with BDD libraries was through using Spot, so I'm familiar with BuDDy, but that's it. Starting something fresh, I'm pondering what's the best C++ BDD library available nowadays. I axed through BuDDy and refactored it so that it's template-only and encapsulated the global variables in a class (hoping for some performance boost from inlining). While I'm fairly happy with the result, I now realize that there's been some progress in the BDD landscape since 1997—crazy! This paper: https://www.tvandijk.nl/pdf/2015setta.pdf by the author of Sylvan seems to indicate that Sylvan offers good performances on a single core, and great perf on multicore. It also comes with a nice C++ interface. I guess my question is: If you had to go from scratch today, which BDD library would you use? Cheers, M.

4 years, 1 month

Walking through BDD formula in python

by Ayrat Khalimov

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

4 years, 1 month

fail to install spot

by Jueming Hu

Good afternoon, I am Jueming, a Ph. D. student at Arizona State University. I would like to use spot for my research, such as getting the graph of an LTL formula. I downloaded 'linux-64/spot-2.9.6-py38_2.tar.bz2' and ran 'conda install -c adl spot' within the extracted folder. 'spot 2.5.2' is shown in conda list and also in python packages. However, 'import spot' doesn't work. The error says, 'No module named 'spot''. I have also tried 'linux-64/spot-2.9.4-py38_2.tar.bz2', 'conda install -c adl/label/adl spot', 'conda install -c adl/label/dev spot', append system path before import spot, and export LD_LIBRARY_PATH. But spot still doesn't work on my pc. Could you please help me install spot? Thanks in advance and looking forward to hearing from you. Best, Jueming

4 years, 2 months

Question about Transfoming from Non-deterministic Automata to Deterministic Automata

by Meng Ruijie

Dear Spot Team, Thanks for providing a wonderful tool. During constructing Buchi automata for LTL, Spot always shows non-determinism automata although I select the "deterministic" item. Would you mind telling me how to construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13 & (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U ousr2_ai3_ce8)))))). The following is its automata but non-determinism. [cid:83ad2cd0-bc60-443c-b387-4bc7953c05d2] Looking forward to your response. Kind Regards, Ruijie

4 years, 3 months

Translations to DPA

by Tobias Meggendorfer

Hi, I'm using / comparing Spot and other tools in the Rabin to Parity translation. I have two questions (to ensure my comparison is fair): 1) I want to minimize the input automata using Spot to remove the effects of preprocessing done by each tool as much as possible. However, I require that the acceptance condition remains a Rabin condition. Right now, I am using the call autfilt --remove-dead-states --cleanup-acceptance --remove-unused-ap --simplify-exclusive-ap --simplify-acc --partial-degeneralize --generalized-rabin --deterministic The last two are an effort to ensure that simplify-acc doesn't change the acceptance condition. 2) What are the ways to tell spot to translate DRA to DPA? Right now, I am using autfilt --hoa --deterministic --parity. This seems to be a sort of black box (which is fine with me). Just to make sure: Are there other DRA-to-DPA translations included in Spot which are worthwhile to be investigated? Cheers, Tobias

4 years, 3 months

ltlfilt filtering duplicates

by David Müller

Hi Alexandre, I hope you are not affected too badly by COVID and you and your family can deal with it in a good way. Simon and I stumbled over some slight problems with ltlfilt in combination with the flags -u and --relabel-bool=pnn. We expected to remove the duplicates, and thus being idempotent. However, we came across a set of LTL formulas, where two applications of ltlfilt -u --relabel-bool=pnn delivered a different result from applying it once. I attach the set of LTL formulas (ltlfilt-duplicates/ base.ltl in the archive) and a short script to evaluate the problem (ltlfilt- duplicates/reproduce.sh). I also tried to input a sorted list, it changed the numbers, but not the problem of being not idempotent. Could you tell us, whether we misunderstood something? Best regards, David

4 years, 3 months

Re: [Spot] set property "original-states" in function "purge_dead_states()

by Alexandre Duret-Lutz

Tobias John <tobias.john(a)tu-dresden.de> writes: > thanks for your quick response. Your suggestion solves my problem. > > I think a function like "set_default_original_states()" would be > helpful but it is not necessary. In my opinion, it is more important > to mention somewhere in the documentation, e.g. at > > https://spot.lrde.epita.fr/concepts.html#named-properties > > that one needs to set the property somewhen before transforming the > automaton. Yes. The usage is however not very uniform. Some functions, like degeneralize() have to maintain the equivalent of "original-states" in order to work. This function will always define "original-states" if it wasn't present, because that comes for free. However if "original-states" was defined previously, the two mappings will be composed at an extra-cost.

4 years, 3 months

set property "original-states" in function "purge_dead_states()

by Tobias John

Hello, I am using Spot for my Master Thesis. I try to simplify omega-automata by removing unnecessary states, e.g. states that are unreachable. The function "purge_dead_states()" does the job but there is an issue: for my application, I need to know the original state numbers of the states in the resulting (smaller) automaton, i.e. I need to map the states of the resulting automaton to the states of the original automaton. Is there some way to get the original state numbers from the reduced automaton? My intuition is that the property "original-states" would be suitable to store the original state numbers but the function "purge_dead_states()" does not set this property. In my opinion, the function "purge_dead_states()" setting the property "original-states" would be a useful feature to be included in future releases of Spot. Best regards, Tobias

4 years, 3 months

Encode input formula into URL

by John Lång

Hello, I'd like to thank the developers for the awesome Spot's online LTL toolset! It's helping me a lot with my model checking project with Spin. This is exactly how formal methods should look like in the 2020'ies... If I may be so bold to request a feature, would it be possible to encode the input formula into URL, so that I could share a link with my fellow students? Best regards, John Lång

4 years, 4 months

← Newer
1
...
4
5
6
7
8
9
10
...
22
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot