- Spot - LRE

Bug in ltlcross manual
by František Blahoudek 28 Dec '17

28 Dec '17

Hi, I think there is a bug in the manual of ltlcross. There is the paragraph > If the translator produced a Streett or Rabin automaton, these columns > contains the size of a TGBA (or BA) produced by ltlcross from that > Streett or Rabin automaton. Check in_states, in_edges, in_transitions, and in_acc for statistics about the actual input automaton. which seems no longer to be valid as I have no such columns in the output files created by ltlcross v. 2.4.4. Best, Fanda Blahoudek

2 1

genaut --ks-nca error
by Florian Barta 18 Oct '17

18 Oct '17

Hi, when using genaut --ks-nca e.g. genaut --ks-nca=1..10 I get the following error: genaut: print_hoa(): automaton is complete but prop_complete()==false Is this a bug? What can I do to get the desired result? I am using spot version 2.4.1 on Ubuntu 16.04. Best regards, Florian Barta

2 1

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