December 2021 - Spot

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

SPOT: formula:is_literal shall be marked const?
by Ayrat Khalimov 02 Dec '21

02 Dec '21

hi Alexandre, Seems like the function formula::is_literal() should be marked const: /// \brief Whether the formula is an atomic proposition or its /// negation. bool is_literal() { return (is(op::ap) || // If f is in nenoform, Not can only occur in front of // an atomic proposition. So this way we do not have // to check the type of the child. (is(op::Not) && is_boolean() && is_in_nenoform())); } kind wishes, Ayrat

2 1