Spot

spot@lrde.epita.fr

209 discussions

spot-2.6.1 conflicts with libiconv-1.14: it installs the file lib/charset.alias

by Yuri

Installing spot-2.6.1... pkg-static: spot-2.6.1 conflicts with libiconv-1.14_11 (installs files into the same place). Problematic file: /usr/local/lib/charset.alias *** Error code 70 Please remove this file. Thanks! Yuri

6 years, 5 months

--disable-doxygen doesn't disable doxygen

by Yuri

gmake[5]: Leaving directory '/wrkdirs/usr/ports/math/spot/work/spot-2.6.1/doc' rm -rf spot.html spot.latex doxygen gmake[4]: doxygen: Command not found Version 2.6.1 on FreeBSD. Thanks, Yuri

6 years, 5 months

Multiple accepting runs for Buchi Automaton

by Thakur Neupane

Hello, I am using SPOT to work with Buchi Automaton. Does SPOT supports finding all the accepting runs instead of only one? Sincerely, Thakur Neupane

6 years, 5 months

Return all accepting runs for emptiness checking

by Zhen Zhang

Hello, We would like to know if the emptiness checking algorithms for Buchi automata can return all accepting runs, instead of a single one as the tool has implemented. Thanks, Zhen Zhang

6 years, 6 months

Cloning an automaton

by Ayrat Khalimov

Hello! Given a co-Buchi automaton and some number K, my function [1] creates another automaton ("co-Reachability") that bounds by K the maximal number of visits to co-Buchi accepting states. I currently create the new automaton like this: auto new_aut = make_twa_graph(aut->get_dict()) but this BDD-dictionary sharing between the new and the original automaton looks suspicious: once the original automaton dies and kills its dictionary (?), the new automaton will no longer be able to use it. Right? I guess the correct way is to create a new dictionary for the new automaton: auto new_d = spot::make_bdd_dict(); But then: what will be the natural way to copy edges of the original automaton into the new automaton? I currently simply iterate over edges of `aut` and do smth like: for (auto &t: aut->out(state)) k_aut->new_edge(src_state, dst_state, t.cond); where `t.cond` refers to a BDD of `aut`. So, I will need to create `cond` that uses new BDD dict, right? Which functions will be useful for doing that? Thanks! A minor point: If you use CUDD library and SPOT in the same project, then you will get compilation errors, because: CUDD does not use namespaces and has type `BDD`, and and Buddy in SPOT does not use namespaces and has `BDD`. To overcome the clash, the simple trick below works, but... maybe put Buddy into separate namespace? (minor feature request:) (I apologize for not providing the patch!) My current workaround is: whenever including SPOT headers, include them like this: #define BDD spotBDD #include <spot/twa/twagraph.hh> #include <spot/twaalgos/sccinfo.hh> #undef BDD best wishes, Ayrat Khalimov [1] https://github.com/5nizza/sdf-hoa/blob/master/src/k_reduce.cpp#L69

6 years, 7 months

bug spot online

by MATTEO LUCCHI

Good afternoon, You are probably already aware of that, but the spot online translator is not working anymore. I am trying to translate a LTL formula into a Buchi Automaton. It was working until 2 days ago, but now i get this: Traceback (most recent call last): File "/var/www/html/cgi-bin/spotcgi.py", line 732, in <module> render_automaton(degen, dont_run_dot) File "/var/www/html/cgi-bin/spotcgi.py", line 318, in render_automaton render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 305, in render_dot_maybe render_dot(autprefix, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 237, in render_dot run_dot(basename, 'svg') File "/var/www/html/cgi-bin/spotcgi.py", line 230, in run_dot os.link(outname, tmpdir + "/" + ext) FileNotFoundError: [Errno 2] No such file or directory: '../spotimg/960f234ef7d2cd7d8fbab23c49603c6a66fc284d.svg' -> '../spotimg/0f33f8af71a0356e3d63971bc8a4a7e39e64b7d9-154/svg' Any fix to the problem? Thank you! Kind Regards, Matteo Lucchi

6 years, 10 months

A bug in determinization procedure of Spot?

by Anton Pirogov

Hello, first I just want to say, thanks for creating Spot, it is immensely useful! And I think that I might have found a bug (or two). My inputs are classic state-based NBAs. I rely on Spot to compare and verify my determinized automata, i.e. I compare the automaton that my tool produces with the one I get from Spot using autfilt -D -S -p (to get a deterministic parity automaton). I use autfilt --equivalent-to=... for the equivalence test. Yesterday I noticed something strange. When I compare the original NBA and my DPA, it reports that they are equivalent. Same for the original NBA and the DPA I get from Spot. But when I compare my automaton with the one from Spot, it says that the languages are different! So the first thought was - something must be broken in the equivalence test. Apparently, at least one of the three answers I got is wrong. So I used a little Python script using the Spot API to get a word where two of the automata do not agree on. Let's call the original NBA A, my DPA B and the one from Spot C. There were no words found in A×¬B, ¬A×B, A×¬C, ¬A×C and also B×¬C. But there IS a word in ¬B×C. I used this word with autfilt --accept-word=... to check A, B and C. And it turned out that in fact A and B do not accept the word, but C does, i.e. C is incorrect. So, to conclude, there seems to be a bug in the determinization and the problem is not detected by the equivalence test between A and C. I don't know about Spot internals, but if the equivalence test is using the same determinization procedure to complement A for the required products, then the bug in the equivalence test is a consequence of the problem in the determinization (i.e., the equiv. test compares the wrong DPA with basically itself), so the issues might be related. It might be useful to know that I found the problem using Spot 2.4.4 and it is still present in the current version 2.5.1. I also attach the smallest automata A, B and C that illustrate the issue and the script I used to search for the counterexample. You can check that: cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0 and autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 1. I hope this helps. Thanks and best regards, Anton Pirogov

6 years, 10 months

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335478点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2229572857咨询

by 傅瑶

6 years, 11 months

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【336248点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2300040163咨询

by 高俏秀

6 years, 11 months

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335418点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2813339771咨询

by 孟荔娜

6 years, 11 months

← Newer
1
...
12
13
14
15
16
17
18
...
21
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot