On Thu, Feb 27, 2020 at 10:33 AM Ranjana N <ranjana.nallamalli(a)gmail.com> wrote:
>
> The following website:
>
> spot.lrde.epita.fr
Thanks. Our sysadmin said he banned all non-french IPs two days ago
because of a DDOS attack that would fill the ram of our shared web
server in just 1sec. Unfortunately he had no time yesterday to work
on this.
He tried to lift the ban a few minutes ago, and the server went down
in a couple of seconds again. He is currently trying to look for a
smaller range of IPs to block.
--
Alexandre Duret-Lutz
Dear all,
I was wondering if there exists an option to disable the generation of
the documentation.
Thank you in advance,
Best,
Jaime
--
--------------------------------------------------------------
Jaime Arias https://lipn.univ-paris13.fr/~arias
CNRS Research Engineer (LoVe Team)
LIPN, CNRS UMR 7030
Institut Galilée - Université Paris 13
99 Avenue Jean-Baptiste Clément, F-93430 Villetaneuse, France
tel:[+33] 01 49 40 40 67
--------------------------------------------------------------
Have been trying to access the resources at your website but not getting
through. Is the site down?
Kindly throw some light.
Thanks & Regards
Ranjana
New Delhi
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.
