- Spot - LRE

accepting_run() returning words containing false
by Jens Kreber 10 Apr '20

10 Apr '20

Hello, I am using spot to check randomly generated LTL formulas for satisfiability and extract traces / words fulfilling the formula if satisfiable. I have come across behavior which I do not understand and am therefore asking on this list about it. I would be very happy if you could help me with the issue. I'm using the python interface and call some_formula.translate().accepting_run() which usually either returns None if unsatisfiable or a valid trace, which I then convert using spot.twa_word() and inspect afterwards. Most of the time, this works as expected, but I've experienced several cases now where the produced trace contains a False (0) literal. Here, two cases must be distinguished: 1. The formula is satisfiable There exist formulas like "!b & e U (a & b & c)" which are quite obviously satisfiable, but still accepting_run() returns a trace with 0 in it, although there are other valid traces without False in them. 2. The formula is unsatisfiable There also exist formulas like "X!c & X(b & c & d & a U e)" which are unsatisfiable, and accepting_run() returns a trace with 0 in it. Normally, for unsatisfiable formulas (like "a & !a") it just returns None. I'd find point 2 alone totally okay, but I think point 1 is actually problematic since the trace I'm looking for exists, but isn't returned. So my question is whether I'm using spot incorrectly somehow or if this is actually a bug. I also attached a small list of formulas and traces with the described behavior. BTW I'm on Linux, Ubuntu 16.04, using spot 2.8.7 compiled from the tar.gz. I'm looking forward to your responses! Regards, Jens Kreber

2 2

Re: [Spot] Site is not responding
by Alexandre Duret-Lutz 27 Feb '20

27 Feb '20

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

2 2

Disable doc generation
by Jaime Arias 27 Feb '20

27 Feb '20

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 --------------------------------------------------------------

2 2

Site is not responding
by Ranjana N 27 Feb '20

27 Feb '20

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

2 1

Python Binding Issue
by Yoonchang Sung 26 Feb '20

26 Feb '20

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

2 1

Bug in version 2.8.6
by Rowe, Reuben 26 Feb '20

26 Feb '20

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

2 1

Random formulas that cannot be converted to automaton
by Carlo Sengers 15 Dec '19

15 Dec '19

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

2 2

Question about the use of ltlcross
by 肖圣平 15 Dec '19

15 Dec '19

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

1 0

Keep all APs when translating LTL?
by Dominick Pastore 21 Nov '19

21 Nov '19

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

2 2

ltl2tgba: diagnostics for stutter-sensitive properties
by Victor Khomenko 21 Nov '19

21 Nov '19

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.

2 1