January 2022 - Spot

How to free the memory of an automaton in spot's Python API?
by Yechuan Xia 31 Jan '22

31 Jan '22

Hi, I'm building some automatons using spot's python interface. Simply, codes like: for i in n: temp_aut = spot.automaton(aut.to_str()) # copy an automaton ...something del temp_aut But I found that whenever it enters a new loop, the memory of the automaton assigned to temp_aut is not freed. And it leads to a memory overflow. I thought this might be solved with 'delete temp_aut' in the C++ version spot, but in the python interface 'del temp' doesn't seem to work. Is there any interface in Python or other operations to make it possible?

3 9

Question regarding SPOT's accepting_run behaviour
by Clément TAMINES 14 Jan '22

14 Jan '22

Hello, I am contacting this list because I have a question regarding the behaviour of SPOT’s accepting_run function. I created an example (see attached) where, if I am not mistaken, the accepting run that is yielded does not satisfy the acceptance formula. Could you confirm that this is a problem and not a mistake in my understanding of the function and/or acceptance formula ? In addition, the acceptance formula is somehow detected as being a gen. Streett condition, can this be prevented and does it have an influence on how the emptiness check/accepting run generation is handled ? Thank you for your help, Clément

2 1

ltlsynt and hoa input
by Ayrat Khalimov 06 Jan '22

06 Jan '22

hello, Is there a way to feed HOA file (as a nondet Buchi) instead of a formula to ltlsynt? I tried smth (see below), but I am getting 'unrealisable' for nondet Buchi automaton spec that is supposed to be realisable (see attached). Maybe I missing something? (like ltlsynt dualising the automaton, etc.) Here is what I tried. Into file synthesis.cc, add: #include "spot/parseaut/public.hh" Then in line 822, comment out: // auto aut = trans.run(f); and instead add: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); auto parsed_aut = parse_aut("/tmp/spec.hoa", dict); if (parsed_aut->aborted) abort(); auto aut = parsed_aut->aut; This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula. Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'): ./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no and provide the correct --ins and --outs arguments, and any formula with one of those propositions. The tool outputs expected implementations on toy examples, but on a larger example attached it outputs "unrealizable" instead of "realizable". That is why the question. best wishes, Ayrat

2 5

Spot Debian package not working due to expired certificate error for the LRDE website
by Young, David Clark 02 Jan '22

02 Jan '22

Hi, I am trying to install Spot using the Debian package at www.lrde.epita.fr/repo/debian/ but it looks as though the security certificate for www.lrde.epita.fr has expired. In fact, it looks like it expired yesterday (Dec. 29th). The reason I'm installing Spot is that it's a dependency of another project I would like to install, and that project's Dockerfile uses the Debian package. It is possible to compile Spot from the source, but it is more efficient to use a Debian package (and potentially eases reproducibility, which is nice when using Docker). Would it be possible for someone to update the certificate? Thanks! - David

2 1