- Spot - LRE

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 05 Oct '18

05 Oct '18

Dear SPoT developers, I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem. I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for. However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem. My questions are the followings: 1) Do they allow to express the same properties ? and 2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ? Kind regards, Martin.

2 1

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 03 Oct '18

03 Oct '18

Dear SPoT developers, I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem. I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for. However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem. My questions are the followings: 1) Do they allow to express the same properties ? and 2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ? Kind regards, Martin.

1 0

Potential Bug in Spot?
by Andreas Tollkötter 25 Sep '18

25 Sep '18

Hello, with the currently newest version of Spot 2.6.1, the following behavior occurred for me, which I would call a bug. I attached a DOT file of a deterministic parity automaton which was written by "autfilt --dot --highlight-languages". What is notable that (among other pairs), states 10 and 66 are marked as language-equivalent states. Their "a1"-successors, 30 and 62 are not equivalent however, so something must be wrong here. I assume a potential cause is that there are a total of 18 non-trivial equivalence classes but only 16 different colors defined to be used by Spot, so some are used for multiple classes? If that is the case, I feel like there should be at least a warning output by "autfilt" when this happens. Best regards, Andreas Tollkötter

2 1

ltlfilt does not exhaustively simplify when --remove-wm is enabled
by Simon Jantsch 23 Sep '18

23 Sep '18

Hello, I am confused by the fact that the following two commands do not produce the same result: ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --simplify=3 The first command gives the same formula as: ltlfilt --simplify=3 --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --remove-wm which makes me believe that simplification is done before removing the operators M and W. I would expect ltlfilt to first remove the operators and then simplify exhaustively. Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators? Best regards, Simon

2 1

spot-2.6.1 conflicts with libiconv-1.14: it installs the file lib/charset.alias
by Yuri 10 Aug '18

10 Aug '18

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

3 4

--disable-doxygen doesn't disable doxygen
by Yuri 10 Aug '18

10 Aug '18

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

2 2

Multiple accepting runs for Buchi Automaton
by Thakur Neupane 10 Aug '18

10 Aug '18

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

2 1

Return all accepting runs for emptiness checking
by Zhen Zhang 02 Aug '18

02 Aug '18

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

1 0

Cloning an automaton
by Ayrat Khalimov 17 Jun '18

17 Jun '18

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

2 3

bug spot online
by MATTEO LUCCHI 22 Mar '18

22 Mar '18

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

2 1