- Spot - LRE

Re: [Spot] c++ help stepping through automaton
by Alexandre Duret-Lutz 06 Dec '16

06 Dec '16

Hi Marvin, > Hello dear spot devs, > > I have a question concerning stepping through an automaton based on the boolean formula assigned to the edge between two states, using c++. > What I want to achieve is the following: > I'm translating an LTL formula into a deterministic monitor automaton, so I have a spot::const_twa_graph_ptr. > Now I simply want to "run" the DFA, i.e., I have a trace and want to perform a state change based on the transition matching the current letter in my trace. > I don't get that step just from the examples or the doxygen documentation. maybe something like unsigned step(const const_twa_graph_ptr& aut, unsigned src, bdd label) { for (auto& edge: aut->out(src)) if (bdd_implies(label, edge.cond)) return edge.dst; throw std::runtime_error("unmatched label"); } > Furthermore it would also be great, if you could tell me how to output the bdd on the edge in an human readable way (boolean formula), as it is done in the online tool of yours (https://spot.lrde.epita.fr/trans.html) I believe this is shown in https://spot.lrde.epita.fr/tut21.html -- Alexandre Duret-Lutz

2 1

Re: [Spot] SPOT installation error
by Alexandre Duret-Lutz 10 Nov '16

10 Nov '16

On Thu, Nov 10, 2016 at 8:44 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: > 2016-11-10 13:01 GMT-06:00 Alexandre Duret-Lutz <adl(a)lrde.epita.fr>: >> On Thu, Nov 10, 2016 at 6:33 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: >> > can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or >> > directory >> > libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a >> > valid libtool archive >> >> Could you show the entire output you get when you type "make" ? > > Please see attached for the entire output. OK, so this error is due to the fact that the source code is in a directory called /home/saffie/LTLf synthesis/spot-2.1.2 with "LTLf synthesis" containing a space. Directory or file names with spaces cannot be supported in Makefiles. Just rename that directory to LTLf_synthesis (or something else), and be sure to run './configure && make clean' (to forget about the old path) before rebuilding with 'make'. -- Alexandre Duret-Lutz

1 0

SPOT installation error
by ShufangZhu 10 Nov '16

10 Nov '16

Hi, I am trying to install SPOT. But after I entered the command "make", there is an error as following, can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or directory libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a valid libtool archive My system is Ubuntu 14.04, 64-bit. And it's a virtual machine. Thanks! Best Regards, Shufang

2 1

Possible Bug (Spot 2.1)
by Reuben Rowe 01 Nov '16

01 Nov '16

Dear Spot Team, I am a postdoc at UCL working on the Cyclist theorem-proving framework, which makes use of Spot. We have recently upgraded Cyclist to use Spot 2.1 from Spot 1.2.4, and one of our benchmark tests has thrown up a possible bug in the Spot library. Cyclist searches for cyclic proofs, and validates them by building two Buchi automata out of a proof and checking language inclusion (ℒ(A) ⊆ ℒ(B)), which we do by first complementing B and then checking emptiness of the product with A. With version 1.2.4, we did this using with the following code: spot::twa a = ...; spot::twa b = ...; spot::tgba_safra_complement complement(&b); spot::tgba_product product(&a, &b); spot::couvreur99_check ec(&product); spot::emptiness_check_result * res = ec.check(); Since version 2.1 does not provide the tgba_safra_complement class, we now use the following code: spot::twa_graph_ptr a = ...; spot::twa_graph_ptr b = ...; spot::twa_graph_ptr det = tgba_determinize(b); spot::twa_graph_ptr complement = to_generalized_buchi(dtwa_complement(det)); spot::const_twa_ptr product = std::make_shared<spot::twa_product>(proof, complement); spot::couvreur99_check ec(product); std::shared_ptr<spot::emptiness_check_result> res = ec.check(); Our benchmark test generates the following automata (given in dot format) for a and b, respectively: digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label="p_0 & !p_1 & !p_2 & !p_3\n{0}"] 1 [label="S1 t_53"] 1 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 2 [label="S2 t_53,t_49,t_50,t_51,t_52"] 2 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 2 -> 3 [label="p_0 & p_1 & !p_2 & !p_3\n{0}"] 3 [label="S3 t_53,t_52"] 3 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 3 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 4 [label="S5 t_53"] 4 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 5 [label="S4 t_53"] 5 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] } digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="init"] 0 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3"] 0 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"] 0 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"] 0 -> 4 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 5 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 7 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 9 [label="p_0 & !p_1 & p_2 & !p_3"] 0 -> 10 [label="p_0 & !p_1 & !p_2 & !p_3"] 0 -> 0 [label="1"] 1 [label="S4,t53"] 1 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 2 [label="S3,t52"] 2 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 3 [label="S3,t53"] 3 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 4 [label="S2,t52"] 5 [label="S2,t51"] 5 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"] 6 [label="S2,t50"] 7 [label="S2,t49"] 7 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"] 8 [label="S2,t53"] 8 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 8 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 9 [label="S5,t53"] 9 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 10 [label="S1,t53"] 10 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 10 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"] } The code I gave above returns a non-null (i.e. non-empty) result, however we expect that this should actually return an empty result. What I have discovered is that the code above does indeed return an empty result when the use_simulation flag to the tgba_determinize function is set to false (the values of the other two flags do not make a difference). Thus, it seems to me that this is a bug, no? I am happy to provide any more information which is necessary for diagnosis. Best wishes, Reuben Rowe.

2 2

[SPOT Question] Little Question about LTL/PSL Fragment
by Willy Chang 05 Sep '16

05 Sep '16

Hello, I'm a graduate student at National Taiwan University (Taiwan), doing automatic verification related researches. Currently I'm working on integration of PSL translation with other types of Büchi automata and formats with our own tool (based on Java), which the linear fragment part is implemented by Spot (and ltl2tgba). I appreciate this fantastic tool and all of your respectable work on this. Upon using ltl2tgba, I'd like to ask some basic question regarding F formula and SERE sequences. Take the following formula as example: G ( {a;b} -> F q ) where a, b, q are all atomic Boolean expressions. ltl2tgba would give me the result like the following: https://spot.lrde.epita.fr/spotimg/af005ecb477ea78d3b55f538089ac0fce1fa99f7… (This is captured from online Spot converter, but is the same as one output by command-line tools.) As we can see, there are multiple transitions marked as "a & !q", meaning this automaton is a non-deterministic one. Is this intended to be so? If yes, how could I specify Spot to get a deterministic output? If no, would this be a bug or something ambiguous? Also, I have been curious about the algorithm that Spot parses PSL fragment. It seems like Spot first extracts PSL symbols to LTL compatible ones and then apply LTL translation method to automata, Is this right? Or did I miss some parts? I'm new to PSL translations and reading related papers now (thanks for the SPOT citation page). Please feel free to correct me or recommend me some must-read publications. Currently I"m working on the IEEE Standard (2010) and the book Practical Introduction to PSL. Thank you very much. Sincerely, Willy Chang Dept. of Information Management National Taiwan University

2 1

ltl2dstar
by armin mojoodi 13 Jul '16

13 Jul '16

Hello I want to use ltl2dstar.exe for a project, but I have a problem with v.0.5.3. when I run it with cmd it returns an error... Exception in file common/RunProgram.win32.cpp at line 85: CreateProcess failed... I would be appreciate if you tell me how should I fix it. Best, Armin

2 1

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