- Spot - LRE

Question on LTL to buechi automata
by Zhen Dong 24 Sep '20

24 Sep '20

Dear Spot team, Thanks for developing the nice tool Spot. I am a researcher at National University of Singapore using Spot in my research. I have a question about translating LTL to buechi automata using spot. My LTL properties are constraints over input/output sequences of a program, e.g., output W, output P always responds to input B (false R (! iB | (true U (oW & X (true U oP))))) where iB indicates that input B and oP indicates output P. The buechi automata of the negation of above formula given by Spot is in the following: [image: image.png] Here is a input/output trace to be evaluated: iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH *What I do not understand is that the proposition on the transition from state 0 to state 2 is iB & oW. How can I interpret it?* Given the input/output trace, there is no element that is iB and at the same time is oW. I assume the verification feeds element in the trace to the automata one by one. Do I miss something e.g., wrong configuration on the translation or some basic knowledge about verification? Can you give me some advice on this issue? Thank you very much. Best regards Zhen -- Zhen Dong Senior Research Fellow National University of Singapore https://www.comp.nus.edu.sg/~dongz/

2 2

Spot Polish Notation Parsing
by Niklas Metzger 31 Jul '20

31 Jul '20

Hi Spot Team! First of all, thanks for providing and maintaining such a great tool! I stumbled over a problem with formulas in polish notation: Parsing a formula like “-> a b” returns the “syntax error, unexpected implication operator” (Also tested on the website). It seems like implication and equivalence are not supported by that parser. Is there a technical reason for that and if not, could you give me a hint how to implement it? Thanks in advance Niklas Metzger

2 1

Segfault when postprocessing large automaton
by Reed Oei 20 Apr '20

20 Apr '20

Hello, I am encountering a bug where Spot segfaults when I try to postprocess a relatively large automaton. I have uploaded the file to http://reedoei.com/files/smaller-inner.aut.zip; it has 113930 states and 1537155 edges. I tried to come up with a smaller example but was having trouble doing so. Below is the sequence of commands, using the Python bindings, to reproduce this bug for me: import spot A = spot.automaton('smaller-inner.aut') B = A.postprocess('BA', 'Deterministic', 'Low') # Crashes here B.save('postprocessed.aut') I also tried using various other others for postprocess such as Small and Low, or Any and High (because Any and Low/Medium does nothing). I am using Ubuntu 18.04, Python 3.6.9, and Spot 2.8.7 (but also tried with 2.8.6). Thank you, Reed Oei

2 3

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