- Spot - LRE

Online translator: RuntimeError for LTL3BA
by Ayrat 07 Jul '16

07 Jul '16

hi there, smth is wrong with online translator for LTL3BA -- see message below. Thanks for amazing web-page! regards, ayrat *RuntimeError* Python 3.4.2: /usr/bin/python3 Thu Jul 7 11:57:15 2016 A problem occurred in a Python script. Here is the sequence of function calls leading up to the error, in the order they occurred. /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in **() 747 dont_run_dot = print_stats(degen, True) 748 automaton.set_name(str(f)) => 749 render_automaton(degen, dont_run_dot) 750 degen = 0 751 automaton = 0 *render_automaton* = <function render_automaton>, *degen* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, *dont_run_dot* = False /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *render_automaton*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, dont_run_dot=False) 314 else: # TGBA 315 if not dont_run_dot: => 316 hoaname = save_hoa(automaton) 317 spot.print_dot(dotsrc, automaton, '.t' if buchi_type == 't' else '.') 318 render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) *hoaname* = None, /global/ *save_hoa* = <function save_hoa>, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> > /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *save_hoa*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >) 259 def save_hoa(automaton): 260 hoasrc = spot.ostringstream() => 261 spot.print_hoa(hoasrc, automaton, 't' if buchi_type == 't' else '') 262 hoasrc = hoasrc.str() 263 hoasrc += '\n' /global/ *spot* = <module 'spot' from '/usr/lib/python3/dist-packages/spot/__init__.py'>, spot.*print_hoa* = <built-in function print_hoa>, *hoasrc* = <spot.impl.ostringstream; proxy of <Swig Object of type 'std::ostringstream *' at 0x7f2ae4164d20> >, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, /global/ *buchi_type* = 't' *RuntimeError*: print_hoa(): automaton uses unregistered atomic propositions args = ('print_hoa(): automaton uses unregistered atomic propositions',) with_traceback = <built-in method with_traceback of RuntimeError object>

3 2

Java Implementation
by Виктор Фридман 11 Jun '16

11 Jun '16

Hello! Do You have any Java implementations of Spot? Regards. Отправлено из Почты для Windows 10

2 1

Completing automata using efficiente bdd operations
by Sergio Hernández 23 May '16

23 May '16

Hi, i would like to ask you about the most efficient way of completing an automaton using bdd operations. we are working with huge automata and we want to improve the automaton creation process. For that, one of the bottlenecks is generating the logical formulas corresponding to the automaton transitions as bdds. For example, let us consider we have the following automaton: State 0 | | a & b | v State 1 | | a & c | v State 2 Then, the alphabet is {a,b,c,d,e}. Thus, we need to add (!c & !d & !e) to the first transition and (!b & !d & !e) to the second one in order to make queries such as "F(e)". Currently, we are implementing this manually using a loop where for each transition we add the negation of every condition that is not present in the transition. But it is not fast enough. Is there any bdd operation to implement this in an efficient way? Thanks in advance, Sergio Hernández

2 1

Acceptance check in Spot
by Matthias Heizmann 14 Mar '16

14 Mar '16

Hi Spot developers, I just extended our automata library https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_in… with support to write Büchi automata in the HOA format. Now, I just wanted to check a few results without implementing support to read HOA files. Syntactically my files seem to be correct, (example attached, file is read by Spot), but I also wanted to do some semantic check, e.g., test if a certain word is accepted. Spot provides quite a number of sophisticated operations but I did not find something "simple" like an acceptance check. Have I overlooked it or is it not documented? For my purpose it is sufficient if it works on the "usual" Büchi automata. Best, Matthias

2 3

Creating bdds
by Miriam Blank 10 Jan '16

10 Jan '16

Hi, Can you please explain the api for creating a bdd? How can I create a bdd? How do I define it? How do I give parameter names so that I can later use it to model check a formula? What is the meaning of bdd_ithvar and bdd_nithvar and the int parameter they receive? I would be very happy if you can supply a simple example. Thank you very much and happy new year, Miriam

2 5

Parsing HOA using Python
by Marcel Walter 10 Jan '16

10 Jan '16

Hi all, I am a masters student of computer science at University of Bremen, Germany. I am working with Büchi-Automata for a study at the moment. Therefore I want to parse an HOA file representing a Büchi-Automaton using Python. It would be great to get an object in Python representing the automaton. So that I can iterate over the states and their edges, read the labels, etc. Can this be done using Spot? If so, how? It would be nice to have a code example. Thank you so much for your help! Best regards from Germany, Marcel Walter

2 2

Python documentation for spot
by Miriam Blank 17 Nov '15

17 Nov '15

Hello, Is there a full documentation of the python api for spot? All I found are the examples in wrap/python/tests. Thank you, Miriam

2 1

Unambiguous test on empty automata
by Ming-Hsien Tsai 20 Oct '15

20 Oct '15

Dear Spot developers, Attached is an automaton accepting an empty language. I think it is supposed to be unambiguous. But when I ran the following command, I got 0. autfilt --count --is-unambiguous empty.hoa After tracing the code, I found that the problem might be caused by get_init_state_number (called in the product function), which creates a new state if the input automaton has no state. -- Ming-Hsien

2 1

SPOT error in make check
by Christopher Ziegler 24 Aug '15

24 Aug '15

Hello Ladies and Gentlemen, I used your program (SPOT) on Ubuntu 12.4. 32bit, configured it with the two parameters --disable-python and --prefix=/home/my_username (for which I don't need any sudo priviliges to read/write. Then I did make check and the program reported the following: See src/tests/test-suite.log Please report to spot(a)lrde.epita.fr However, I ran make install afterwards, and tried the program and it seems to work. But when I tried to do the same (last week or so), I didn't use the --prefix parameter and I got an error, when I tried to start the program: it said: "error while loading shared libraries: libspot.so.0: cannot open shared object file: No such file or directory" I also include the src/tests/test-suite.log in the attachment. I hope this helps you finding a bug or something. Since the program works for me now, I just wrote you because it said "Please report to spot@..." . If you need more information (for example, which compiler I used etc.) you can write me back. Regards, Christopher Ziegler

2 2

Bug Report
by Oscar Chang 05 Aug '15

05 Aug '15

If you enter (FGa)||(FGb) and tick the option for the degeneralized buchi automaton, it still gives a generalised one.

2 1