To whom it may concern,
I am having Ubuntu 16.04 and my python3 version is 3.5.2 (default version
from Ubuntu 16.04). After installing with the default configuration setting
(installing from a tarball), I am able to import spot in python3 but
"print(spot.version())" gives me this error: "AttributeError: module 'spot'
has no attribute 'version'".
Also, when trying "sudo apt-get install python3-spot", I am getting this
error: "The following packages have unmet dependencies:
python3-spot : Depends: python3 (>= 3.7~) but 3.5.1-3 is to be installed
E: Unable to correct problems, you have held broken packages."
I was wondering if you could help me with this issue. Thank you!
Best,
Yoon
--
*Yoonchang Sung*
Postdoctoral Associate
Massachusetts Institute of Technology
Computer Science and Artificial Intelligence Laboratory
32 Vassar St. / Room 32-335
Cambridge, MA 02139
USA
Hi Spot Team,
I am trying to compile Cyclist (cyclist-prover.org) against the latest
version (2.8.6) of Spot, and I am getting an error.
Cyclist is including spot/twa/twa.hh, and when compiling I get the
following error:
In file included from
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/acc.hh:28:0,
from
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/twa/twa.hh:27,
from src/soundness/proof_aut.hpp:4,
from src/soundness/proof_aut.c:1:
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh:
In constructor ‘spot::bitset<N>::bitset(spot::bitset<N>::word_t)’:
/home/cim/staff/uhac003/Academic/Resources/Spot/spot-2.8.6/install/include/spot/misc/bitset.hh:57:5:
error: constexpr constructor does not have empty body
}
^
In fact, I also get this error when trying to compile again versions
2.6.3 and 2.7.5 too.
When I try to compile against version 2.5.3, I get the error that there
is no such file spot/twa/twa.hh.
Is this a bug, or has the API changed? If the latter, how should I
update my code to use the newer versions?
Thanks,
Reuben
--
Lecturer, Dept of Computer Science
Royal Holloway, University of London
Egham
Surrey
TW20 0EX
Tel: +44 (0)1784 276827
Dear Team,
I am conducting an experiment to determine the performance/capacity of
atomic propositions that SPOT can handle when an intersecting run is
requested from a Buchi automaton and an LTL formula.
The experiment uses standard SPOT functionality: The command line utility
'Randaut' and 'RandLtl'.
Finally, I have been able to obtain the desired output and have no
obstacles anymore.
However, during the setup of the experiment, I observed that at least two
random generated formulas resulted in an error:
1. a C++ program I made, eventually resulted in error: " terminate
called after throwing an instance of 'std::bad_alloc' what():
std::bad_alloc"
2. The online translator at https://spot.lrde.epita.fr/app/ presented a
timeout with the same formula.
3. The spot-sandbox automata notebook at
https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/autom…
Presented the error: Kernel Restarting. The kernel appears to have
died. It will restart automatically.
There is no specific use for the specific formulas, so I removed those from
the experiment. I successfully ran the remaining batches.
The annoying part: It was not immediately obvious that my program
actually froze due to a 'questionable' formula instead of doing some
heavy lifiting on huge automatons. resulting in some useless waiting time.
I am not aware if there is a way to determine upfront whether there such a
formula will exist in a set.
I did not investigate if the likelihood can be reduced by manipulating a
specific operator priority (option of randltl). There are too few formulas
that exbibit this behavior.
Question:
Are such formulas a natural aspect of LTL of is this maybe a bug?
Is it an option to avoid or reduce the likelihood of occurrence of such
formulas in RandLTL? (making it less random :-) )
The affected formulas were:
1. G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <->
(G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6))))
2. (((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U
(p1))) M ((X(p5)) & (F(p4)))
Kind regards
Carlo Sengers
Master Student Software Engineering
Dear Spot Fans,
It is frustrating that I encountered some problems when using ltlcross. I have implemented a tool to get BA from LTL formula. Then I want to use ltlcross to compare spot with my tools. When I ran the ltlcross, I got the following result：//failed to create lcr-o0-fdbDS4
Besides, I tried the following and still failed：//failed to create lcr-o0-kSl51L
I sincerely hope you can help to see my question I would appreciate it if I could get some guidance on the use of ltlcross from you. Looking forward to your reply!
Best Regards!
Shengping Shaw, ECNU
Hello,
We are using the Python bindings in Spot to translate LTL to monitors, as
described at https://spot.lrde.epita.fr/tut11.html.
We have a question: Is it possible to set an option that will preserve all
the atomic propositions, even when they cannot affect the automaton? For
example, with the formula "Ga & Fb", the resulting monitor would not
include "b".
Is there a way to do this?
Thanks,
Dominick
Hi Alexandre,
Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be possible to print a warning with diagnostics, like the online tool does? Something like:
Warning: The property is stutter-sensitive - the following words are a proof, as they differ only by some stuttering:
Accepted word: a & b; a & b; cycle{!a & !b}
Rejected word: a & b; cycle{!a & !b}
Motivation:
* by passing the option --check=stutter-invariant the user tells the tool that stutter-invariance is important for them, hence a warning/diagnostics is desirable if the check fails (this warning does not have to be printed if this option is not passed)
* it's not easy to get these traces from the final automaton - my understanding is that some potentially costly operations are required, which are performed during the check anyway
* the current way of getting this diagnostics (python + libraries; maybe there is a better way I don't know about?) creates many dependencies, thus making it difficult to integrate this functionality into toolchains - ideally one would want just a single executable ltl2tgba
* my (perhaps naive) understanding is that this is not difficult to implement and does not incur much extra run-time as the check has to be performed anyway
Best regards,
Victor.
> > Could you add a command-line option for ltl2tgba to invert the input
> formula before computing the automaton?
>
> Done.
> https://gitlab.lrde.epita.fr/spot/spot/commit/7f21d3ff29ad3a513f261025c5
> 75e4676a14cc50
Great - many thanks!
> Any opinion on what passing --negate twice should do?
A really good and nerdy one - twice the smiley face! :-) :-)
Cheers,
Victor.
Hi,
Could you add a command-line option for ltl2tgba to invert the input formula before computing the automaton?
Yes, it's trivial to do externally, but there are good reasons to have this option:
* this would remove an extra step from model checking toolchains (where the automaton is built for the negation of a formula)
* if the formula goes through a toolchain, it's better to keep equivalence all the way through to the automata, so that the user can easily see that the property has not been broken by transformations, and also comprehend any formula-related diagnostics logged by the tools.
Thanks,
Victor.
Dear Spot developers,
I am Yong Li from Chinese Academy of Sciences and I am writing to you to
ask a question about parsing LTLf (LTL over finite traces) formulas.
Spot supports LTL with finite semantics (LTLf) but I found out that Spot
eagerly simplifies the input formulas with LTL semantics.
For instance, if I use command line ltlfilt --from-ltlf -f "a U !(X
True)", Spot immediately gives me 0.
This is not correct since the input formula should be satisfiable in
LTLf semantics.
I wonder whether there is a way to get around it?
Is there a an option I can use to make Spot parse the formula without
simplying it?
Regards,
Yong
I'm trying to use SPOT to build an automaton for an LTLf formula, but I
think there is a bug. I'm using this code (based on
https://spot.lrde.epita.fr/tut12.html):
#include <iostream>
#include <spot/tl/ltlf.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/translate.hh>
int main() {
spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))");
if (pf.format_errors(std::cerr))
return 1;
spot::translator trans;
trans.set_type(spot::postprocessor::BA);
trans.set_pref(spot::postprocessor::Small);
spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));
spot::remove_ap rem;
rem.add_ap("alive");
aut = rem.strip(aut);
spot::postprocessor post;
post.set_type(spot::postprocessor::BA);
post.set_pref(spot::postprocessor::Small); // or ::Deterministic
aut = post.run(aut);
print_hoa(std::cout, aut) << '\n';
return 0;
}
In LTL, this would be a contradiction, but in LTLf it is not as the next
operator cannot be true at the last timestep. There seems to be an issue
with SPOT where it simplifies the automaton as though the formula is in
LTL, yielding an incorrect automaton. Am I using this correctly? I'd be
willing to write a patch if this is indeed a bug.
Thanks,
Andrew Wells
