Spot January 2022

spot@lrde.epita.fr

5 participants
4 discussions

How to free the memory of an automaton in spot's Python API?

by Yechuan Xia

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 years

Question regarding SPOT's accepting_run behaviour

by Clément TAMINES

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

3 years

ltlsynt and hoa input

by Ayrat Khalimov

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

3 years

Spot Debian package not working due to expired certificate error for the LRDE website

by Young, David Clark

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

3 years, 1 month

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot January 2022