Dear Spot support team,
I am a researcher at Developair Technologies. I write you looking for help
with a formula that ltl2tgba cannot handle, possibly a bug.
Here at Developair we have been using Spot for the past few months with
great satisfaction. However, it seems that *ltl2tgba *cannot process the
formula in attached file gb_formula.ltl . We let it run for quite some time
(like hours) and it didn't terminate. On the other hand, Owl can process
the same formula in a matter of a few milliseconds. We don't have any
problem using ltl2tgba with other, similar formulas.
It seems strange to us that Spot gets stuck with such a relatively simple
formula, especially since in our experience Spot worked reliably well with
other, way more complex formulas. Is it maybe a bug or something that we
are doing wrong? Could you please help us?
Please find some more details (version and command) below.
Thank you. Best regards,
J.
Spot version:
ltl2tgba --version
> ltl2tgba (spot) 2.10.6
>
> Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita.
> License GPLv3+: GNU GPL version 3 or later <
> http://gnu.org/licenses/gpl.html>.
> This is free software: you are free to change and redistribute it.
> There is NO WARRANTY, to the extent permitted by law.
>
Command:
ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl
Using the "simplest" command "ltl2tgba -F gb_formula.ltl" produces the same
result (that is, no result).
For comparison, with Owl we used command:
owl ltl2ldgba --state-acceptance -i gb_formula.ltl -o owl_gb.txt
--
Jacopo Binchi
jbinchi(a)developair.es
Paseo de Miramón 170
20014 San Sebastián – Donostia
Gipuzkoa (Spain)
www.developair.es
Hi all,
I did not find how to get the number of states (reachable or not) of an automaton using autfilt
(in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only.
I did find a workaround with `--hoaf` which outputs the automaton in HOA format and
then getting the number from the `States:` header.
For the number of transitions (reachable or not) I don't have a workaround.
Since spot can compute these numbers easily, it seems handy (at least for me)
to have a direct access to them thru the `--stats` interface.
Thank you,
Pierre.
Hi all,
I am trying to install spot on Ubuntu 20.04 following instructions from:
https://spot.lrde.epita.fr/install.html
But apt update complains about the signature:
W: An error occurred during the signature verification. The repository
is not updated and the previous index files will be used. GPG error:
http://www.lrde.epita.fr/repo/debian stable/ InRelease: The following
signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository
<admin(a)lrde.epita.fr>
W: Failed to fetch
http://www.lrde.epita.fr/repo/debian/stable/InRelease The following
signatures were invalid: EXPKEYSIG 03D99E7444F2A84A LRDE Repository
<admin(a)lrde.epita.fr>
Could the signature be expired?
I can actually install spot from source but Debian packages are useful
for preparing artifact submissions.
Thanks,
Ocan
