- Spot - LRE

Generate Words for verification
by hashim ali 27 Mar '19

27 Mar '19

Hi, I am using spot.from_ltlf().translate() to translate LTL rules into a finite automata (with alive property). Now I want to verify certain words that whether they are accepted by the automata or not. These words will be generated from a powerset of the set of atomic propositions. Lets suppose I have AP = {a,b,c,d}. How do I generate words from the powerset of AP and verify it on the automata. Should the word always contain a cycle and a prefix part. If yes, what should be the cycle part and what should be the prefix part. I will be waiting for your response. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 4

Weighted Automata
by hashim ali 25 Mar '19

25 Mar '19

Hi, Is there any support for weighted Automata in spot. Here is a thing I want to implement. I want to test certain words on a certain automata, if a word is rejected by the automata I want to add a new transition (weighted transition) to this automata and later on if that same word comes for verification, I want this automata to return this weight corresponding to this transition. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 1

C interface for Spot?
by Stephen Siegel 25 Mar '19

25 Mar '19

Is there a C (not C++) interface for Spot? I want to call Spot from my C program. Thanks.

2 1

Re: [Spot] Questions regarding handling of Kripke structures in Spot
by Alexandre Duret-Lutz 05 Mar '19

05 Mar '19

Dear Patrick, (Please keep the mailing list in copy so that these explanations get archived and then indexed by search engines.) On Tue, Mar 5, 2019 at 8:58 AM Halder, Patrick <patrick.halder(a)tum.de> wrote: > When I have the twa_product automaton with its respective acceptance states, > how can I find out, to which states of my original Kripke structure they correspond to. > I read somewhere in the spot examples that the labeling of the twa_product states > (of the form <*,*>) has just cosmetic reasons and does therefor not give any help. Let's say you have built the product between two automata autx and auty: prod = spot.product(autx, auty) then pairs = prod.get_product_states() will return an array of pairs of the form [(x0,y0),(x1,y1),....]. State i in the product corresponds to states pairs[i][0] in autx, and pairs[i][1] in auty. See https://spot.lrde.epita.fr/ipynb/product.html around cell 10 for a concrete example, and a tip about using show("1") in this context. > Is it even possible to do this, meaning getting directly from the acc states of the product automaton to the acc states/runs of the Kripke structure? You should probably look for the accepting SCCs of the product, not only its accepting states. You could list all states that belong to acceptings SCCs of the product with something like si = spot.scc_info(prod) n = si.scc_count() for i in range(n): if si.is_accepting_scc(i): for s in si.states_of(i): print(s) Unfortunately, we do not yet have any online example of use of scc_info in Python. You can find some in the test suite, or simply look at the C++ documentation for this class https://spot.lrde.epita.fr/doxygen/classspot_1_1scc__info.html > Or do I have to get the accepting runs of the product automaton, e.g., with the x.intersecting_run(y) method and reason with it about the accepting runs in the Kripke structure? This will only return one accepting run. -- Alexandre Duret-Lutz

1 0

SPOT
by Alina Florina Popa /Student 01 Mar '19

01 Mar '19

Hello, I am trying to convert a LTL formula to Buchi automata in MATLAB. I want to know if you have any script or library that can help me do this? Thank you and best regards, Alina Popa -- Fourth-year Student | Automatic Control and Applied Informatics | Systems Engineering Faculty of Automatic Control and Computer Engineering “Gheorghe Asachi” Technical University of Iasi, Romania www.ac.tuiasi.ro <http://www.ac.tuiasi.ro/> | www.tuiasi.ro <http://www.tuiasi.ro/>

2 1

Questions regarding handling of Kripke structures in Spot
by Halder, Patrick 21 Feb '19

21 Feb '19

Dear Spot Team, I'm a master's student at Technical University of Munich and I'm currently writing my Master's Thesis in the research field of path planning for autonomous cars. I came across Spot on the internet and I think it's a very nice tool that fits exactly my needs: I've got a discrete finite automaton (with certain attributes/APs per node) and I want to check, if this automaton satisfies a certain LTL specification. Especially, my intention is to find all path in my automaton, that satisfy a LTL specification. I've already installed Spot on my computer and tried to implement this with Python. Now I've got the following two questions: 1. What is the most simple and fastest way of defining a spot kripke graph, based on my own automaton (which is basically just a dictionary with nodes, that hold certain attributes and parent/child relations) ? Is there a possibility of including my nodes and transitions step by step into a spot kripke graph or do I have to convert my automaton at first into e.g. the HOA format and afterwards import this HOA-string as a kripke graph? 2. Building the product of a LTL formula (resp. the Büchi automaton) with the kripke graph leads to a object of the class twa_product. Is there a possibility of transforming this product back into a kripke structure or exporting it as a simple dictionary, so that I can make further computations on this "reduced" graph? I hope you can help me with my questions and maybe provide some simple code examples. Thank you very much in advance! Yours sincerely, Patrick Halder

2 1

UBA-generation of ltl2tgba
by Simon Jantsch 12 Feb '19

12 Feb '19

Hello, I have noticed two types of errors that seem to occur when telling ltl2tgba to output unambiguous Büchi automata (UBA). One seems to be some kind of assertion triggering and happens only in combination with the flag „—low“. That is, on running: ltl2tgba —low -U -B -f $FRML the tool occasionally exits with exit code 2 and: „ltl2tgba: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true“ This happens for example for the formula: (G(!(G("2")))) & (("1") | (F("2"))) In some cases the UBA generated by ltl2tgba seem to be incorrect as well, and I don’t think this has to do with the „—low“ flag. An example formula is (("2") W (G("1"))) -> (G("1")) To reproduce these behaviors you can run ltlcross on the attached file „error“, as follows: cat error | ltlcross —-lbt-input ‚ltl2tgba -U -B —-low -f %f >%O' 'ltl2tgba -f %f >%O' Best regards, Simon

2 1

_impl issue with install
by Lonnie Parker 06 Jan '19

06 Jan '19

Hello, I'm new to spot and a bit of a novice with coding in general but I've been running into an issue related to one of the modules that comes with spot when attempting to run python code using the spot python bindings: File "/usr/lib/python3.6/importlib/__init__.py", line 126, in import_module return _bootstrap._gcd_import(name[level:], package, level) ModuleNotFoundError: No module named '_impl' I understand if it is too difficult to diagnose with the limited output, but I didn't want to bombard anyone with lengthy output. I am running Ubuntu 18.04 (Bionic Beaver) and have successfully installed spot using ./configure, make, make install. Prior to installing spot, I also installed the latest version of swig. I've also verified that the relevant .so files are located within my .local/lib/python3.6/site-packages/spot directory. If this issue with using import_module to locate the _impl package looks familiar, any information would be much appreciated. Thank you! Best, Lonnie -- "But as for you, promote the kind of living that promotes right teaching." --Titus 2:1

2 1

partial order reduction and stuttering
by Stephen Siegel 11 Dec '18

11 Dec '18

The web page https://spot.lrde.epita.fr/ipynb/stutter-inv.html shows how to use Spot to highlight the states in a Büchi automaton which have a stutter invariant language. It says "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton.” Does anyone know a reference for this technique? I mean specifically the idea that POR is something that can be turned on or off depending on the current state of the property automaton. I feel I’ve seen that somewhere, but don’t remember where. Thanks! -Steve

2 1

spot's website is down
by 刘天池 07 Dec '18

07 Dec '18

Hello: I want know why all website about spot is down. website list: https://spot.lrde.epita.fr/ https://www.lrde.epita.fr/mailman/listinfo/spot-announce best regards! Tianchi Liu from ECNU

2 1