- Spot - LRE

is_tt and is_ff in Python bindings
by František Blahoudek 18 Oct '17

18 Oct '17

Hi, I have found out that is_tt and is_ff does nt work as expected in Python. See the attached notebook for details. Best, Fanda Blahoudek

2 1

genaut - documentation
by František Blahoudek 07 Sep '17

07 Sep '17

Hi, there is a tiny inconsistency in man genaut. For the families from Löding's paper there is ... 4N states ... less than n! states. I guess the n and N should share their case. Best, Fanda

2 1

man autcross
by František Blahoudek 06 Sep '17

06 Sep '17

Hi, the manual says in the section DESCRIPTION: The list of automata to use should be supplied on standard input, or using the -f or -F options. However, the tool knows no -f option. Fanda

1 0

can't compile spot
by Pedro Marquez 19 Jul '17

19 Jul '17

I downloaded the spot tar package and tried to compile it using ./configure, make, sudo make install. However, make reports the error: make: *** No targets specified and no makefile found. Stop. and sudo make install reports: make: *** No rule to make target 'install'. Stop. What's happening, what can I do? Thank you in advance, -Pedro Marquez, Prof.

2 1

Swig is required, but isn't
by Clément Gillard 06 Apr '17

06 Apr '17

Hello, I was trying to build Spot on a fresh ArchLinux install, when I came across this issue: > $ ./configure ... > [...] > checking for swig3.0... no > checking for swig... no > [...] > $ make > [...] > swig -c++ -python -py3 -O -nofastproxy -MD -I../buddy/src -MF > .deps/buddy_wrap.TPcxx ./buddy.i > make[3]: swig: Command not found > [...] > make: *** [Makefile:1163: all] Error 2 If Spot requires Swig, shouldn't `configure` fail ? Or, if Swig is only required for users who want to build the Python library, shouldn't the latter not be included in the `all` rule ? If that's any help, I attached my config.log. Regards, -- Clément 'Cigix' Gillard "EAT SLEEP EAT REPEAT" @skrillbug_bot, 2016-06-23

2 1

Reference request: Converting UCW to k-safety automaton
by Ayrat Khalimov 20 Mar '17

20 Mar '17

Hi all, Do you know any tools that can convert universal co-buchi automata into universal safety automata via bounding the number of visits to the final states? (I.e., go to absorbing bad state if visit a final state k times) (Alternatively, convert NBW into nondet finite automaton: accept a word if it visits a final state k times) (I am just trying to avoid work that may have already be done:) Thanks, Ayrat

1 0

Enumerating accepting runs
by Ayrat Khalimov 12 Mar '17

12 Mar '17

hi, Is there a way to get more than one accepting run of the product automaton? Ideally would be to have all simple accepting runs, but some cheap heuristics would also do. I wanted to implement some heuristics [1], but got stuck with the following: how to map edges of the accepting run to the edges of the original product? (or: states of the accepting run to states of the product?) thanks!:) ayrat [1] An heuristics: - get an accepting run, - forbid one edge of that run in the original product (for example, by setting its label to bddfalse), - ask for another accepting run on the thus modified product, - restore that edge and change another edge, and so on.

2 3

underlying algorithm of monitor construction
by Marvin Stenger 03 Mar '17

03 Mar '17

Hello dear spot devs, I need to know which construction is used when I'm translating an LTL formula into a monitor automaton. By that I mean: /spot::formula some_ltl; spot::translator trans;/ /trans.set_type(spot::postprocessor::Monitor) spot::const_twa_graph_ptr aut = trans.run(some_ltl)/ I couldn't find documentation about this, besides some rather informal description. It would be great if you could point me to some more useful documentation about the algorithm or even better a paper on it. Best, Marvin Stenger

2 2

Re: [Spot] c++ help stepping through automaton
by Alexandre Duret-Lutz 06 Dec '16

06 Dec '16

Hi Marvin, > Hello dear spot devs, > > I have a question concerning stepping through an automaton based on the boolean formula assigned to the edge between two states, using c++. > What I want to achieve is the following: > I'm translating an LTL formula into a deterministic monitor automaton, so I have a spot::const_twa_graph_ptr. > Now I simply want to "run" the DFA, i.e., I have a trace and want to perform a state change based on the transition matching the current letter in my trace. > I don't get that step just from the examples or the doxygen documentation. maybe something like unsigned step(const const_twa_graph_ptr& aut, unsigned src, bdd label) { for (auto& edge: aut->out(src)) if (bdd_implies(label, edge.cond)) return edge.dst; throw std::runtime_error("unmatched label"); } > Furthermore it would also be great, if you could tell me how to output the bdd on the edge in an human readable way (boolean formula), as it is done in the online tool of yours (https://spot.lrde.epita.fr/trans.html) I believe this is shown in https://spot.lrde.epita.fr/tut21.html -- Alexandre Duret-Lutz

2 1

Re: [Spot] SPOT installation error
by Alexandre Duret-Lutz 10 Nov '16

10 Nov '16

On Thu, Nov 10, 2016 at 8:44 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: > 2016-11-10 13:01 GMT-06:00 Alexandre Duret-Lutz <adl(a)lrde.epita.fr>: >> On Thu, Nov 10, 2016 at 6:33 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: >> > can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or >> > directory >> > libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a >> > valid libtool archive >> >> Could you show the entire output you get when you type "make" ? > > Please see attached for the entire output. OK, so this error is due to the fact that the source code is in a directory called /home/saffie/LTLf synthesis/spot-2.1.2 with "LTLf synthesis" containing a space. Directory or file names with spaces cannot be supported in Makefiles. Just rename that directory to LTLf_synthesis (or something else), and be sure to run './configure && make clean' (to forget about the old path) before rebuilding with 'make'. -- Alexandre Duret-Lutz

1 0