alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: replace %H,%T,%N by %O

Browse source 
Also get rid of the lbt_parser, and fix the LBT support of the HOA
parser.

* doc/org/ltlcross.org, doc/org/ltldo.org: Update.
* src/bin/common_trans.cc, src/bin/common_trans.hh: Add support for
%O, and keep %T,%N,%H as hidden aliases without disabling them.
* src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tgbatest/ltl2tgba.cc:
Call hoa_parse instead of lbt_parse.
* src/hoaparse/hoaparse.yy: Improve error reporting from LBT.
* src/hoaparse/hoascan.ll: Fix typos preventing parsing of
LBT files with more than 10 states.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: Delete the lbt
parser.
* src/tgbatest/lbttparse.test: Adjust the expected error message.
* NEWS: Update.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-01 01:54:39 +01:00
parent dbd824c539
commit 847270b480
13 changed files with 264 additions and 540 deletions
Download patch file Download diff file Expand all files Collapse all files

11
NEWS
View file

@ -62,11 +62,12 @@ New in spot 1.99a (not yet released)
used in a stream. The parser currently ignore all optional used in a stream. The parser currently ignore all optional
headers (starting with a lowercase letter). headers (starting with a lowercase letter).
- The above HOA parser can also parse neverclaims, so the - The above HOA parser can also parse never claims, and LBTT
neverclaim parser has been removed. This implies that automata, so the never claim parser and the LBTT parser have
autfilt can input a mix of HOA and neverclaims, and that been removed. This implies that autfilt can input a mix of HOA,
ltlcross' %N and %H specifiers (used to indicate whether never claims, and LBTT automata. ltlcross also use the same
a tool produces neverclaims or HOA) are now synonyms. parser for all these output, and the old %T and %N specifiers
have been deprecated and replaced by %O (for output).
- randomize() is a new algorithm that reorder the states - randomize() is a new algorithm that reorder the states
and transition of an automaton at random. It can be and transition of an automaton at random. It can be

388
doc/org/ltlcross.org
View file

@ -60,54 +60,57 @@ ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
: LBT, or Wring's syntax : LBT, or Wring's syntax
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or : %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
: Wring's syntax : Wring's syntax
: %N,%T,%D the output automaton as a Never claim, in LBTT's : %O,%D the automaton is output as either (%O) HOA/never
: or in LTL2DSTAR's format : claim/LBTT, or (%D) in LTL2DSTAR's format
For instance here is how we could cross-compare the never claims For instance here is how we could cross-compare the never claims
output by =spin= and =ltl2tgba= for the formulas =GFa= and =X(a U b)=. output by =spin= and =ltl2tgba= for the formulas =GFa= and =X(a U b)=.
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N' ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%O' 'spin -f %s >%O'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
When =ltlcross= executes these commands, =%s= will be replaced When =ltlcross= executes these commands, =%s= will be replaced
by the formula in Spin's syntax, and =%N= will be replaced by a by the formula in Spin's syntax, and =%O= will be replaced by a
temporary file into which the output of the translator is redirected temporary file into which the output of the translator is redirected
before it is read back by =ltlcross=. before it is read back by =ltlcross=.
#+BEGIN_SRC sh :results verbatim :exports results #+BEGIN_SRC sh :results verbatim :exports results
ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%N' 'spin -f %s >%N' 2>&1 ltlcross -f 'GFa' -f 'X(a U b)' 'ltl2tgba -s %s >%O' 'spin -f %s >%O' 2>&1
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
([](<>(a))) ([](<>(a)))
Running [P0]: ltl2tgba -s '([](<>(a)))' >'lck-o0-iDGV6y' Running [P0]: ltl2tgba -s '([](<>(a)))' >'lcr-o0-hvzgTC'
Running [P1]: spin -f '([](<>(a)))' >'lck-o1-sA3FYp' Running [P1]: spin -f '([](<>(a)))' >'lcr-o1-iYh45L'
Running [N0]: ltl2tgba -s '(!([](<>(a))))' >'lck-o0-1ClVQg' Running [N0]: ltl2tgba -s '(!([](<>(a))))' >'lcr-o0-z6nzjV'
Running [N1]: spin -f '(!([](<>(a))))' >'lck-o1-wyErP7' Running [N1]: spin -f '(!([](<>(a))))' >'lcr-o1-8JB5F4'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
(X((a) U (b))) (X((a) U (b)))
Running [P0]: ltl2tgba -s '(X((a) U (b)))' >'lck-o0-ex1BYY' Running [P0]: ltl2tgba -s '(X((a) U (b)))' >'lcr-o0-rqfB6d'
Running [P1]: spin -f '(X((a) U (b)))' >'lck-o1-UNE8dQ' Running [P1]: spin -f '(X((a) U (b)))' >'lcr-o1-OUNHEn'
Running [N0]: ltl2tgba -s '(!(X((a) U (b))))' >'lck-o0-coM8tH' Running [N0]: ltl2tgba -s '(!(X((a) U (b))))' >'lcr-o0-qzVvdx'
Running [N1]: spin -f '(!(X((a) U (b))))' >'lck-o1-eHPoQy' Running [N1]: spin -f '(!(X((a) U (b))))' >'lcr-o1-eUfHTG'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
no problem detected No problem detected.
#+end_example #+end_example
=ltlcross= can only read three kinds of output: =ltlcross= can only read four kinds of output:
- Never claims (only if they are restricted to representing an - Never claims (only if they are restricted to representing an
automaton using =if=, =goto=, and =skip= statements) such as those automaton using =if=, =goto=, and =skip= statements) such as those
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. These output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. These
should be indicated using =%N=. The newer syntax introduced by should be indicated using =%O=. The newer syntax introduced by
Spin 6.24, using =do= instead of =if=, is also supported. Spin 6.24, using =do= instead of =if=, is also supported.
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with - [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with
either state-based acceptance or transition-based acceptance. either state-based acceptance or transition-based acceptance.
This output is used for instance by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][=lbt=]], [[http://web.archive.org/web/20080607170403/http://www.science.unitn.it/~stonetta/modella.html][=modella=]], or =ltl2tgba This output is used for instance by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][=lbt=]], [[http://web.archive.org/web/20080607170403/http://www.science.unitn.it/~stonetta/modella.html][=modella=]], or =ltl2tgba
--lbtt=. These should be indicated using =%T=. --lbtt=. These should also be indicated using =%O=.
- Non-alaternating automata in [[file:http://adl.github.io/hoaf/][the HOA format]] with an acceptance
condition that is is generalized-Büchi or inferior. These
should also be indicated using =%O=.
- [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]], which support deterministic Rabin or Streett - [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]], which support deterministic Rabin or Streett
automata. After =ltlcross= reads such input, it immediately automata. After =ltlcross= reads such input, it immediately
convert it into a Büchi automaton. Rabin automata are converted convert it into a Büchi automaton. Rabin automata are converted
@ -124,24 +127,24 @@ Of course all configured tools need not use the same =%= sequences.
The following list shows some typical configurations for some existing The following list shows some typical configurations for some existing
tools: tools:
- '=spin -f %s >%N=' - '=spin -f %s >%O='
- '=ltl2ba -f %s >%N=' - '=ltl2ba -f %s >%O='
- '=ltl3ba -M0 -f %s >%N=' (less deterministic output, can be smaller) - '=ltl3ba -M0 -f %s >%O=' (less deterministic output, can be smaller)
- '=ltl3ba -M1 -f %s >%N=' (more deterministic output) - '=ltl3ba -M1 -f %s >%O=' (more deterministic output)
- '=modella -r12 -g -e %L %T=' - '=modella -r12 -g -e %L %O='
- '=/path/to/script4lbtt.py %L %T=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for - '=/path/to/script4lbtt.py %L %O=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for
its interface with LBTT) its interface with LBTT)
- '=ltl2tgba -s %s >%N=' (smaller output, Büchi automaton) - '=ltl2tgba -s %s >%O=' (smaller output, Büchi automaton)
- '=ltl2tgba -s -D %s >%N=' (more deterministic output, Büchi automaton) - '=ltl2tgba -s -D %s >%O=' (more deterministic output, Büchi automaton)
- '=ltl2tgba --lbtt %s >%T=' (smaller output, TGBA) - '=ltl2tgba --lbtt %s >%O=' (smaller output, TGBA)
- '=ltl2tgba --lbtt -D %s >%T=' (more deterministic output, TGBA) - '=ltl2tgba --lbtt -D %s >%O=' (more deterministic output, TGBA)
- '=lbt <%L >%T=' - '=lbt <%L >%O='
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D=' - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D='
(deterministic Rabin output) (deterministic Rabin output)
- '=ltl2dstar --automata=streett --ltl2nba=spin:path/to/ltl2tgba@-sD - '=ltl2dstar --automata=streett --ltl2nba=spin:path/to/ltl2tgba@-sD
%L %D=' (deterministic Streett output) %L %D=' (deterministic Streett output)
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba
-s >%N=' (external conversion from Rabin to Büchi done by -s >%O=' (external conversion from Rabin to Büchi done by
=dstar2tgba= for more reduction of the Büchi automaton than =dstar2tgba= for more reduction of the Büchi automaton than
what =ltlcross= would provide) what =ltlcross= would provide)
- '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer - '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer
@ -161,22 +164,22 @@ ltlcross --list-shorthands
If a COMMANDFMT does not use any %-sequence, and starts with one of If a COMMANDFMT does not use any %-sequence, and starts with one of
the following words, then the string on the right is appended. the following words, then the string on the right is appended.
lbt <%L>%T lbt <%L>%O
ltl2ba -f %s>%N ltl2ba -f %s>%O
ltl2dstar %L %D ltl2dstar %L %D
ltl2tgba -H %f>%H ltl2tgba -H %f>%O
ltl3ba -f %s>%N ltl3ba -f %s>%O
ltl3dra -f %f>%D ltl3dra -f %f>%D
modella %L %T modella %L %O
spin -f %s>%N spin -f %s>%O
#+end_example #+end_example
What this implies is that running =ltlcross ltl2ba ltl3ba ...= is What this implies is that running =ltlcross ltl2ba ltl3ba ...= is
the same as running =ltlcross 'ltl2ba -f %s>%N' 'ltl3ba -f %s>%N' ...= the same as running =ltlcross 'ltl2ba -f %s>%O' 'ltl3ba -f %s>%O' ...=
Because only the prefix of the actual command is checked, you can Because only the prefix of the actual command is checked, you can
still specify some options. For instance =ltlcross 'ltl2tgba -D' ...= still specify some options. For instance =ltlcross 'ltl2tgba -D' ...=
is short for =ltlcross 'ltl2tgba -D -H %F>%H' ...= is short for =ltlcross 'ltl2tgba -D -H %F>%O' ...=
* Getting statistics * Getting statistics
@ -194,37 +197,37 @@ they are not supported by =spin= and =lbt=).
randltl -n 2 a b | randltl -n 2 a b |
ltlfilt --remove-wm | ltlfilt --remove-wm |
ltlcross --csv=results.csv \ ltlcross --csv=results.csv \
'ltl2tgba -s %f >%N' \ 'ltl2tgba -s %f >%O' \
'spin -f %s >%N' \ 'spin -f %s >%O' \
'lbt < %L >%T' 'lbt < %L >%O'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+BEGIN_SRC sh :results verbatim :exports results #+BEGIN_SRC sh :results verbatim :exports results
randltl -n 2 a b c | ltlfilt --remove-wm | randltl -n 2 a b c | ltlfilt --remove-wm |
ltlcross --csv=results.csv --json=results.json \ ltlcross --csv=results.csv --json=results.json \
'ltl2tgba -s %f >%N' \ 'ltl2tgba -s %f >%O' \
'spin -f %s >%N' \ 'spin -f %s >%O' \
'lbt < %L >%T' --csv=results.csv 2>&1 'lbt < %L >%O' --csv=results.csv 2>&1
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
-:1: (G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))) -:1: (1)
Running [P0]: ltl2tgba -s '(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))' >'lcr-o0-I7yemj' Running [P0]: ltl2tgba -s '(1)' >'lcr-o0-zO7jLB'
Running [P1]: spin -f '([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1)))))))' >'lcr-o1-VFo8q2' Running [P1]: spin -f '(true)' >'lcr-o1-r7P86U'
Running [P2]: lbt < 'lcr-i0-SYp5lA' >'lcr-o2-GIQcxL' Running [P2]: lbt < 'lcr-i0-idYSPi' >'lcr-o2-l220te'
Running [N0]: ltl2tgba -s '(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))' >'lcr-o0-jppaKd' Running [N0]: ltl2tgba -s '(0)' >'lcr-o0-ylbgfR'
Running [N1]: spin -f '(!([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1))))))))' >'lcr-o1-7v46UW' Running [N1]: spin -f '(false)' >'lcr-o1-HwVbKa'
Running [N2]: lbt < 'lcr-i0-8AoGDu' >'lcr-o2-PzOH6F' Running [N2]: lbt < 'lcr-i0-uVICRx' >'lcr-o2-MSsIfu'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
-:2: (!((G(F(p0))) -> (F(p1)))) -:2: (!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))
Running [P0]: ltl2tgba -s '(!((G(F(p0))) -> (F(p1))))' >'lcr-o0-J9i0Ac' Running [P0]: ltl2tgba -s '(!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))' >'lcr-o0-sPvik7'
Running [P1]: spin -f '(!((<>(p1)) || (!([](<>(p0))))))' >'lcr-o1-N2NUTX' Running [P1]: spin -f '(!((!(((p0) U ([](p1))) U (p1))) U ([](<>(p0)))))' >'lcr-o1-yQ8BZq'
Running [P2]: lbt < 'lcr-i1-T8OQlr' >'lcr-o2-xaj9cJ' Running [P2]: lbt < 'lcr-i1-uob0MN' >'lcr-o2-0IrdjL'
Running [N0]: ltl2tgba -s '(G(F(p0))) -> (F(p1))' >'lcr-o0-YfWgQf' Running [N0]: ltl2tgba -s '(!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))' >'lcr-o0-tSN3Xp'
Running [N1]: spin -f '(<>(p1)) || (!([](<>(p0))))' >'lcr-o1-cpcHd1' Running [N1]: spin -f '(!(((p0) U ([](p1))) U (p1))) U ([](<>(p0)))' >'lcr-o1-DsLkqK'
Running [N2]: lbt < 'lcr-i1-vqYHwu' >'lcr-o2-WCqqBM' Running [N2]: lbt < 'lcr-i1-WmkDD5' >'lcr-o2-D77Ai7'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
No problem detected. No problem detected.
@ -238,18 +241,18 @@ cat results.csv
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
"formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc"
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))","ltl2tgba -s %f >%N","ok",0,0.0315577,3,5,9,1,3,2,0,1,0,2,1,0,1,0,401,5168,3 "(1)","ltl2tgba -s %f >%O","ok",0,0.137237,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4142,1
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))","spin -f %s >%N","ok",0,0.00750061,6,13,18,1,3,2,0,0,1,6,1,0,0,1,999,14414,5 "(1)","spin -f %s >%O","ok",0,0.00531029,2,2,2,1,2,1,1,0,0,0,0,1,0,0,201,4161,2
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))","lbt < %L >%T","ok",0,0.0022915,8,41,51,1,3,2,0,0,1,8,1,0,0,1,1397,43175,5 "(1)","lbt < %L >%O","ok",0,0.00358417,3,3,3,0,3,2,1,0,0,0,0,1,0,0,220,4550,21
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))","ltl2tgba -s %f >%N","ok",0,0.0296025,4,10,16,1,3,1,1,0,1,0,0,0,0,1,797,16411,3 "(0)","ltl2tgba -s %f >%O","ok",0,0.0377477,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))","spin -f %s >%N","ok",0,0.00388934,7,24,63,1,4,2,1,0,1,6,1,0,0,1,1400,64822,4 "(0)","spin -f %s >%O","ok",0,0.00286865,2,2,1,1,2,1,1,0,0,0,0,1,0,0,1,0,1
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))","lbt < %L >%T","ok",0,0.00268385,39,286,614,3,28,26,1,0,1,33,1,0,0,1,7583,600472,4394 "(0)","lbt < %L >%O","ok",0,0.00280551,1,0,0,0,1,1,0,0,0,0,0,1,0,0,1,0,1
"(!((G(F(p0))) -> (F(p1))))","ltl2tgba -s %f >%N","ok",0,0.0248804,2,4,4,1,1,0,0,0,1,0,0,0,0,1,399,4130,1 "(!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))","ltl2tgba -s %f >%O","ok",0,0.0415092,2,3,4,1,2,1,0,1,0,1,1,0,1,0,400,8567,2
"(!((G(F(p0))) -> (F(p1))))","spin -f %s >%N","ok",0,0.0019908,2,3,5,1,1,0,0,0,1,1,1,0,0,1,399,5174,1 "(!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))","spin -f %s >%O","ok",0,0.209455,23,86,127,1,17,10,0,2,5,21,1,0,0,1,4392,116876,24
"(!((G(F(p0))) -> (F(p1))))","lbt < %L >%T","ok",0,0.00197792,5,10,15,1,4,3,0,0,1,5,1,0,0,1,407,6333,9 "(!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))","lbt < %L >%O","ok",0,0.00363823,37,109,164,3,35,28,0,7,0,28,1,0,1,0,7182,155216,4006
"(G(F(p0))) -> (F(p1))","ltl2tgba -s %f >%N","ok",0,0.0256492,3,5,11,1,3,1,1,1,0,1,1,0,1,0,600,11305,3 "(!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))","ltl2tgba -s %f >%O","ok",0,0.0406385,2,4,4,1,1,0,0,0,1,0,0,0,0,1,400,8522,1
"(G(F(p0))) -> (F(p1))","spin -f %s >%N","ok",0,0.00185036,3,5,14,1,3,1,1,1,0,1,1,0,1,0,600,14397,3 "(!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))","spin -f %s >%O","ok",0,0.781573,22,152,257,1,9,4,0,0,5,21,1,0,0,1,4400,282361,208
"(G(F(p0))) -> (F(p1))","lbt < %L >%T","ok",0,0.00209399,11,18,54,2,11,9,1,1,0,5,1,0,1,0,1245,25838,449 "(!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))","lbt < %L >%O","ok",0,0.00471071,72,551,914,3,52,47,0,0,5,72,1,0,0,1,14201,983174,8808
#+end_example #+end_example
This file can be loaded in any spreadsheet or statistical application. This file can be loaded in any spreadsheet or statistical application.
@ -269,33 +272,33 @@ cat results.json
#+begin_example #+begin_example
{ {
"tool": [ "tool": [
"ltl2tgba -s %f >%N", "ltl2tgba -s %f >%O",
"spin -f %s >%N", "spin -f %s >%O",
"lbt < %L >%T" "lbt < %L >%O"
], ],
"formula": [ "formula": [
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "(1)",
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "(0)",
"(!((G(F(p0))) -> (F(p1))))", "(!((!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))))",
"(G(F(p0))) -> (F(p1))" "(!(((p0) U (G(p1))) U (p1))) U (G(F(p0)))"
], ],
"fields": [ "fields": [
"formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc"
], ],
"inputs": [ 0, 1 ], "inputs": [ 0, 1 ],
"results": [ "results": [
[ 0,0,"ok",0,0.0315577,3,5,9,1,3,2,0,1,0,2,1,0,1,0,401,5168,3 ], [ 0,0,"ok",0,0.137237,1,1,1,1,1,0,1,0,0,0,0,1,0,0,200,4142,1 ],
[ 0,1,"ok",0,0.00750061,6,13,18,1,3,2,0,0,1,6,1,0,0,1,999,14414,5 ], [ 0,1,"ok",0,0.00531029,2,2,2,1,2,1,1,0,0,0,0,1,0,0,201,4161,2 ],
[ 0,2,"ok",0,0.0022915,8,41,51,1,3,2,0,0,1,8,1,0,0,1,1397,43175,5 ], [ 0,2,"ok",0,0.00358417,3,3,3,0,3,2,1,0,0,0,0,1,0,0,220,4550,21 ],
[ 1,0,"ok",0,0.0296025,4,10,16,1,3,1,1,0,1,0,0,0,0,1,797,16411,3 ], [ 1,0,"ok",0,0.0377477,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,1 ],
[ 1,1,"ok",0,0.00388934,7,24,63,1,4,2,1,0,1,6,1,0,0,1,1400,64822,4 ], [ 1,1,"ok",0,0.00286865,2,2,1,1,2,1,1,0,0,0,0,1,0,0,1,0,1 ],
[ 1,2,"ok",0,0.00268385,39,286,614,3,28,26,1,0,1,33,1,0,0,1,7583,600472,4394 ], [ 1,2,"ok",0,0.00280551,1,0,0,0,1,1,0,0,0,0,0,1,0,0,1,0,1 ],
[ 2,0,"ok",0,0.0248804,2,4,4,1,1,0,0,0,1,0,0,0,0,1,399,4130,1 ], [ 2,0,"ok",0,0.0415092,2,3,4,1,2,1,0,1,0,1,1,0,1,0,400,8567,2 ],
[ 2,1,"ok",0,0.0019908,2,3,5,1,1,0,0,0,1,1,1,0,0,1,399,5174,1 ], [ 2,1,"ok",0,0.209455,23,86,127,1,17,10,0,2,5,21,1,0,0,1,4392,116876,24 ],
[ 2,2,"ok",0,0.00197792,5,10,15,1,4,3,0,0,1,5,1,0,0,1,407,6333,9 ], [ 2,2,"ok",0,0.00363823,37,109,164,3,35,28,0,7,0,28,1,0,1,0,7182,155216,4006 ],
[ 3,0,"ok",0,0.0256492,3,5,11,1,3,1,1,1,0,1,1,0,1,0,600,11305,3 ], [ 3,0,"ok",0,0.0406385,2,4,4,1,1,0,0,0,1,0,0,0,0,1,400,8522,1 ],
[ 3,1,"ok",0,0.00185036,3,5,14,1,3,1,1,1,0,1,1,0,1,0,600,14397,3 ], [ 3,1,"ok",0,0.781573,22,152,257,1,9,4,0,0,5,21,1,0,0,1,4400,282361,208 ],
[ 3,2,"ok",0,0.00209399,11,18,54,2,11,9,1,1,0,5,1,0,1,0,1245,25838,449 ] [ 3,2,"ok",0,0.00471071,72,551,914,3,52,47,0,0,5,72,1,0,0,1,14201,983174,8808 ]
] ]
} }
#+end_example #+end_example
@ -335,9 +338,9 @@ for i in range(0, len(data["tool"])):
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: tool & count & time & states & edges & transitions & acc & scc & nonacc_scc & terminal_scc & weak_scc & strong_scc & nondet_states & nondet_aut & terminal_aut & weak_aut & strong_aut & product_states & product_transitions & product_scc \\ : tool & count & time & states & edges & transitions & acc & scc & nonacc_scc & terminal_scc & weak_scc & strong_scc & nondet_states & nondet_aut & terminal_aut & weak_aut & strong_aut & product_states & product_transitions & product_scc \\
: ltl2tgba -s %f >%N & 4 & 0.0 & 3.0 & 6.0 & 10.0 & 1.0 & 2.5 & 1.0 & 0.5 & 0.5 & 0.5 & 0.8 & 0.5 & 0.0 & 0.5 & 0.5 & 549.2 & 9253.5 & 2.5 \\ : ltl2tgba -s %f >%O & 4 & 0.1 & 1.5 & 2.2 & 2.2 & 1.0 & 1.2 & 0.5 & 0.2 & 0.2 & 0.2 & 0.2 & 0.2 & 0.5 & 0.2 & 0.2 & 250.2 & 5307.8 & 1.2 \\
: spin -f %s >%N & 4 & 0.0 & 4.5 & 11.2 & 25.0 & 1.0 & 2.8 & 1.2 & 0.5 & 0.2 & 0.8 & 3.5 & 1.0 & 0.0 & 0.2 & 0.8 & 849.5 & 24701.8 & 3.2 \\ : spin -f %s >%O & 4 & 0.2 & 12.2 & 60.5 & 96.8 & 1.0 & 7.5 & 4.0 & 0.5 & 0.5 & 2.5 & 10.5 & 0.5 & 0.5 & 0.0 & 0.5 & 2248.5 & 100849.5 & 58.8 \\
: lbt < %L >%T & 4 & 0.0 & 15.8 & 88.8 & 183.5 & 1.8 & 11.5 & 10.0 & 0.5 & 0.2 & 0.8 & 12.8 & 1.0 & 0.0 & 0.2 & 0.8 & 2658.0 & 168954.5 & 1214.2 \\ : lbt < %L >%O & 4 & 0.0 & 28.2 & 165.8 & 270.2 & 1.5 & 22.8 & 19.5 & 0.2 & 1.8 & 1.2 & 25.0 & 0.5 & 0.5 & 0.2 & 0.2 & 5401.0 & 285735.0 & 3209.0 \\
The script =bench/ltl2tgba/sum.py= is a more evolved version of the The script =bench/ltl2tgba/sum.py= is a more evolved version of the
above script that generates two kinds of LaTeX tables. above script that generates two kinds of LaTeX tables.
@ -499,22 +502,22 @@ By default, the names used in the CSV and JSON output to designate the
translators are the command specified on the command line. translators are the command specified on the command line.
For instance in the following, =ltl2tgba= is run in two For instance in the following, =ltl2tgba= is run in two
configurations, and the strings =ltl2tgba -s --small %f >%N= and configurations, and the strings =ltl2tgba -s --small %f >%O= and
=ltl2tgba -s --deter %f >%N= appear verbatim in the output: =ltl2tgba -s --deter %f >%O= appear verbatim in the output:
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltlcross -f a -f Ga 'ltl2tgba -s --small %f >%N' 'ltl2tgba -s --deter %f >%N' --csv ltlcross -f a -f Ga 'ltl2tgba -s --small %f >%O' 'ltl2tgba -s --deter %f >%O' --csv
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" : "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc"
: "(a)","ltl2tgba -s --small %f >%N","ok",0,0.0274533,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4092,2 : "(a)","ltl2tgba -s --small %f >%O","ok",0,0.043876,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2
: "(a)","ltl2tgba -s --deter %f >%N","ok",0,0.0274613,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4092,2 : "(a)","ltl2tgba -s --deter %f >%O","ok",0,0.0432137,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2
: "(!(a))","ltl2tgba -s --small %f >%N","ok",0,0.0271082,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4098,2 : "(!(a))","ltl2tgba -s --small %f >%O","ok",0,0.0400653,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2
: "(!(a))","ltl2tgba -s --deter %f >%N","ok",0,0.0263196,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4098,2 : "(!(a))","ltl2tgba -s --deter %f >%O","ok",0,0.0450417,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2
: "(G(a))","ltl2tgba -s --small %f >%N","ok",0,0.0232094,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2023,1 : "(G(a))","ltl2tgba -s --small %f >%O","ok",0,0.0429628,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1
: "(G(a))","ltl2tgba -s --deter %f >%N","ok",0,0.0253393,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2023,1 : "(G(a))","ltl2tgba -s --deter %f >%O","ok",0,0.0478663,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1
: "(!(G(a)))","ltl2tgba -s --small %f >%N","ok",0,0.023919,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8166,2 : "(!(G(a)))","ltl2tgba -s --small %f >%O","ok",0,0.0436822,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2
: "(!(G(a)))","ltl2tgba -s --deter %f >%N","ok",0,0.0235093,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8166,2 : "(!(G(a)))","ltl2tgba -s --deter %f >%O","ok",0,0.039919,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2
To present these results graphically, or even when analyzing these To present these results graphically, or even when analyzing these
data, it might be convenient to give each configured tool a shorter data, it might be convenient to give each configured tool a shorter
@ -524,18 +527,18 @@ form "={short name}actual command=".
For instance: For instance:
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltlcross -f a -f Ga '{small} ltl2tgba -s --small %f >%N' '{deter} ltl2tgba -s --deter %f >%N' --csv ltlcross -f a -f Ga '{small} ltl2tgba -s --small %f >%O' '{deter} ltl2tgba -s --deter %f >%O' --csv
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" : "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc"
: "(a)","small","ok",0,0.0310046,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4092,2 : "(a)","small","ok",0,0.0433468,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2
: "(a)","deter","ok",0,0.0292434,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4092,2 : "(a)","deter","ok",0,0.0429179,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2
: "(!(a))","small","ok",0,0.027431,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4098,2 : "(!(a))","small","ok",0,0.0400513,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2
: "(!(a))","deter","ok",0,0.0259028,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4098,2 : "(!(a))","deter","ok",0,0.040167,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2
: "(G(a))","small","ok",0,0.0245275,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2023,1 : "(G(a))","small","ok",0,0.0447826,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1
: "(G(a))","deter","ok",0,0.0245139,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2023,1 : "(G(a))","deter","ok",0,0.0439892,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1
: "(!(G(a)))","small","ok",0,0.0241781,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8166,2 : "(!(G(a)))","small","ok",0,0.0444007,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2
: "(!(G(a)))","deter","ok",0,0.0235059,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8166,2 : "(!(G(a)))","deter","ok",0,0.0396312,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2
* Detecting problems * Detecting problems
@ -591,7 +594,7 @@ positive and negative formulas by the ith translator).
complementation is cheap is that case. When validating a complementation is cheap is that case. When validating a
translator with =ltlcross=, we highly recommend to include a translator with =ltlcross=, we highly recommend to include a
translator with good deterministic output to augment test translator with good deterministic output to augment test
coverage. Using '=ltl2tgba -lD %f >%T=' will produce coverage. Using '=ltl2tgba -lD %f >%O=' will produce
deterministic automata for all obligation properties and many deterministic automata for all obligation properties and many
recurrence properties. Using '=ltl2dstar recurrence properties. Using '=ltl2dstar
--ltl2nba=spin:pathto/ltl2tgba@-sD %L %D=' is more expansive, but --ltl2nba=spin:pathto/ltl2tgba@-sD %L %D=' is more expansive, but
@ -653,7 +656,7 @@ runs out of memory (the hash tables used by =randltl= and =ltlcross=
to remove duplicate formulas will keep growing). to remove duplicate formulas will keep growing).
#+BEGIN_SRC sh :export code :eval no #+BEGIN_SRC sh :export code :eval no
randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC #+END_SRC
** =--save-bogus=FILENAME= ** =--save-bogus=FILENAME=
@ -670,14 +673,14 @@ will run the translators on an infinite number of formulas, saving
any problematic formula in =bugs.ltl=. any problematic formula in =bugs.ltl=.
#+BEGIN_SRC sh :export code :eval no #+BEGIN_SRC sh :export code :eval no
randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC #+END_SRC
You can periodically check the contents of =bugs.ltl=, and then run You can periodically check the contents of =bugs.ltl=, and then run
=ltlcross= only on those formulas to look at the problems: =ltlcross= only on those formulas to look at the problems:
#+BEGIN_SRC sh :export code :eval no #+BEGIN_SRC sh :export code :eval no
ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC #+END_SRC
** =--grind=FILENAME= ** =--grind=FILENAME=
@ -699,167 +702,144 @@ during the process will be saved in =OTHERFILENAME=.
Example: Example:
#+BEGIN_SRC sh :exports code :results verbatim #+BEGIN_SRC sh :exports code :results verbatim
ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \ ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %O" \
--save-bogus=bogus \ --save-bogus=bogus \
--grind=bogus-grind --grind=bogus-grind
#+END_SRC #+END_SRC
#+BEGIN_SRC sh :exports results :results verbatim #+BEGIN_SRC sh :exports results :results verbatim
ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \ ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %O" \
--save-bogus=bogus --grind=bogus-grind 2>&1 --save-bogus=bogus --grind=bogus-grind 2>&1
true true
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
| & G ! p0 | ! p1 F ! p2 & & p1 G p2 F p0 | & G ! p0 | ! p1 F ! p2 & & p1 G p2 F p0
Running [P0]: modella 'lcr-i0-YBdcX8' 'lcr-o0-VWBBUF' Running [P0]: modella 'lcr-i0-1XJw2X' 'lcr-o0-p2nbUW'
Running [N0]: modella 'lcr-i0-wteTSc' 'lcr-o0-pqlbRJ' Running [N0]: modella 'lcr-i0-lSPMMV' 'lcr-o0-3xEoFU'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
error: P0*N0 is nonempty; both automata accept the infinite word error: P0*N0 is nonempty; both automata accept the infinite word
cycle{!p0 & !p1} cycle{!p0 & !p1}
Trying to find a bogus mutation of "(G!b & (!c | F!a)) | (c & Ga & Fb)" Trying to find a bogus mutation of (G!b & (!c | F!a)) | (c & Ga & Fb)...
Mutation [1/22] Mutation 1/22: & & p0 G p1 F p2
& & p0 G p1 F p2 Running [P0]: modella 'lcr-i1-3PI0CT' 'lcr-o0-GxBDAS'
Running [P0]: modella 'lcr-i1-Ursu0g' 'lcr-o0-Lm3N9N' Running [N0]: modella 'lcr-i1-eOijzR' 'lcr-o0-wkIZxQ'
Running [N0]: modella 'lcr-i1-AkNujl' 'lcr-o0-VYRbtS'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [2/22] Mutation 2/22: & G ! p0 | ! p1 F ! p2
& G ! p0 | ! p1 F ! p2 Running [P0]: modella 'lcr-i2-6cYUzP' 'lcr-o0-3ihRBO'
Running [P0]: modella 'lcr-i2-uuBGGp' 'lcr-o0-eZLbUW' Running [N0]: modella 'lcr-i2-6u8pEN' 'lcr-o0-phxZGM'
Running [N0]: modella 'lcr-i2-qO717t' 'lcr-o0-evKSl1'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [3/22] Mutation 3/22: | G ! p0 & & p1 G p2 F p0
| G ! p0 & & p1 G p2 F p0 Running [P0]: modella 'lcr-i3-iwZZML' 'lcr-o0-LMB2SK'
Running [P0]: modella 'lcr-i3-hQAiDy' 'lcr-o0-PoKIU5' Running [N0]: modella 'lcr-i3-r2g9ZJ' 'lcr-o0-HEfh7I'
Running [N0]: modella 'lcr-i3-Jl5vcD' 'lcr-o0-RtIjua'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
error: P0*N0 is nonempty; both automata accept the infinite word error: P0*N0 is nonempty; both automata accept the infinite word
cycle{!p0 & !p1} cycle{!p0 & !p1}
Trying to find a bogus mutation of "G!b | (c & Ga & Fb)" Trying to find a bogus mutation of G!b | (c & Ga & Fb)...
Mutation [1/16] Mutation 1/16: t
t Running [P0]: modella 'lcr-i4-R8PbkI' 'lcr-o0-6ts7wH'
Running [P0]: modella 'lcr-i4-HUTvSH' 'lcr-o0-XXrIgf' Running [N0]: modella 'lcr-i4-cv7EKG' 'lcr-o0-vVmdYF'
Running [N0]: modella 'lcr-i4-MoZ9EM' 'lcr-o0-w2MB3j'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [2/16] Mutation 2/16: G ! p0
G ! p0 Running [P0]: modella 'lcr-i5-ZO3HcF' 'lcr-o0-UiydrE'
Running [P0]: modella 'lcr-i5-ZjeLsR' 'lcr-o0-lT2URo' Running [N0]: modella 'lcr-i5-gOseGD' 'lcr-o0-CL4fVC'
Running [N0]: modella 'lcr-i5-ELzihW' 'lcr-o0-tljGGt'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [3/16] Mutation 3/16: & & p0 G p1 F p2
& & p0 G p1 F p2
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [4/16] Mutation 4/16: | G ! p0 & p1 F p0
| G ! p0 & p1 F p0 Running [P0]: modella 'lcr-i6-QTDjtB' 'lcr-o0-tFpmKA'
Running [P0]: modella 'lcr-i6-VUy2yy' 'lcr-o0-44be05' Running [N0]: modella 'lcr-i6-1lnX1z' 'lcr-o0-TWWyjz'
Running [N0]: modella 'lcr-i6-SBBHrD' 'lcr-o0-VAcbTa'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
error: P0*N0 is nonempty; both automata accept the infinite word error: P0*N0 is nonempty; both automata accept the infinite word
cycle{!p0 & !p1} cycle{!p0 & !p1}
Trying to find a bogus mutation of "G!b | (c & Fb)" Trying to find a bogus mutation of G!b | (c & Fb)...
Mutation [1/10] Mutation 1/10: t
t
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [2/10] Mutation 2/10: G ! p0
G ! p0
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [3/10] Mutation 3/10: & p0 F p1
& p0 F p1 Running [P0]: modella 'lcr-i7-CJTWjx' 'lcr-o0-DKbNEw'
Running [P0]: modella 'lcr-i7-gBs0mN' 'lcr-o0-bgNCRk' Running [N0]: modella 'lcr-i7-tSts1v' 'lcr-o0-CGbWov'
Running [N0]: modella 'lcr-i7-oAYtmS' 'lcr-o0-VvmlRp'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [4/10] Mutation 4/10: | p0 G ! p1
| p0 G ! p1 Running [P0]: modella 'lcr-i8-6dtbPu' 'lcr-o0-gLnsfu'
Running [P0]: modella 'lcr-i8-wLstoX' 'lcr-o0-jZOBVu' Running [N0]: modella 'lcr-i8-Xn6gGt' 'lcr-o0-U7966s'
Running [N0]: modella 'lcr-i8-4hBZs2' 'lcr-o0-3Ezn0z'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [5/10] Mutation 5/10: | G ! p0 F p0
| G ! p0 F p0 Running [P0]: modella 'lcr-i9-Vh7hAs' 'lcr-o0-eYZt3r'
Running [P0]: modella 'lcr-i9-mqY0z7' 'lcr-o0-hcDE9E' Running [N0]: modella 'lcr-i9-I6dfxr' 'lcr-o0-DoY00q'
Running [N0]: modella 'lcr-i9-MtDCJc' 'lcr-o0-5fRAjK'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [6/10] Mutation 6/10: | ! p0 & p1 F p0
| ! p0 & p1 F p0 Running [P0]: modella 'lcr-i10-j7fVvq' 'lcr-o0-aChQ0p'
Running [P0]: modella 'lcr-i10-s5ZlUh' 'lcr-o0-fvp7uP' Running [N0]: modella 'lcr-i10-bnpgwp' 'lcr-o0-KV3G1o'
Running [N0]: modella 'lcr-i10-4GWe6m' 'lcr-o0-LKFmHU'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [7/10] Mutation 7/10: | G p1 & p0 F p1
| G p1 & p0 F p1 Running [P0]: modella 'lcr-i11-uUhFyo' 'lcr-o0-OlrF5n'
Running [P0]: modella 'lcr-i11-wZJKjs' 'lcr-o0-D948VZ' Running [N0]: modella 'lcr-i11-XHjeDn' 'lcr-o0-0CINan'
Running [N0]: modella 'lcr-i11-yVpOyx' 'lcr-o0-rjXtb5'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [8/10] Mutation 8/10: | & p0 p1 G ! p0
| & p0 p1 G ! p0 Running [P0]: modella 'lcr-i12-a7eJLm' 'lcr-o0-RUZFmm'
Running [P0]: modella 'lcr-i12-g9bpRC' 'lcr-o0-RhIkxa' Running [N0]: modella 'lcr-i12-dobiYl' 'lcr-o0-LuVUzl'
Running [N0]: modella 'lcr-i12-rvWBdI' 'lcr-o0-DauTTf'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [9/10] Mutation 9/10: | G ! p0 & p0 F p0
| G ! p0 & p0 F p0 Running [P0]: modella 'lcr-i13-nFQYdl' 'lcr-o0-Mq84Rk'
Running [P0]: modella 'lcr-i13-sXVtCN' 'lcr-o0-9WE4kl' Running [N0]: modella 'lcr-i13-CnPRwk' 'lcr-o0-7f4Fbk'
Running [N0]: modella 'lcr-i13-49803S' 'lcr-o0-BNXXMq'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
error: P0*N0 is nonempty; both automata accept the infinite word error: P0*N0 is nonempty; both automata accept the infinite word
cycle{!p0} cycle{!p0}
Trying to find a bogus mutation of "G!c | (c & Fc)" Trying to find a bogus mutation of G!c | (c & Fc)...
Mutation [1/7] Mutation 1/7: t
t
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [2/7] Mutation 2/7: G ! p0
G ! p0
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [3/7] Mutation 3/7: & p0 F p0
& p0 F p0 Running [P0]: modella 'lcr-i14-KsKPgj' 'lcr-o0-Qo3UXi'
Running [P0]: modella 'lcr-i14-Ohct43' 'lcr-o0-vKfEPB' Running [N0]: modella 'lcr-i14-FVPvFi' 'lcr-o0-Zh06mi'
Running [N0]: modella 'lcr-i14-aKk2A9' 'lcr-o0-RiFqmH'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [4/7] Mutation 4/7: | p0 G ! p0
| p0 G ! p0 Running [P0]: modella 'lcr-i15-JB045h' 'lcr-o0-EIL4Oh'
Running [P0]: modella 'lcr-i15-Oht38e' 'lcr-o0-bhxGVM' Running [N0]: modella 'lcr-i15-sYY8yh' 'lcr-o0-KVOdjh'
Running [N0]: modella 'lcr-i15-iyrAIk' 'lcr-o0-nMFuvS'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [5/7] Mutation 5/7: | G ! p0 F p0
| G ! p0 F p0
warning: This formula or its negation has already been checked. warning: This formula or its negation has already been checked.
Use --allow-dups if it should not be ignored. Use --allow-dups if it should not be ignored.
Mutation [6/7] Mutation 6/7: | ! p0 & p0 F p0
| ! p0 & p0 F p0 Running [P0]: modella 'lcr-i16-hoqdSg' 'lcr-o0-xghJEg'
Running [P0]: modella 'lcr-i16-nZMD9X' 'lcr-o0-epKIYv' Running [N0]: modella 'lcr-i16-5JvOrg' 'lcr-o0-SUdVeg'
Running [N0]: modella 'lcr-i16-DSW2N3' 'lcr-o0-6ElnDB'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
Mutation [7/7] Mutation 7/7: | & p0 F p0 G p0
| & p0 F p0 G p0 Running [P0]: modella 'lcr-i17-BNo92f' 'lcr-o0-0T8nRf'
Running [P0]: modella 'lcr-i17-Z6avt9' 'lcr-o0-QJhDjH' Running [N0]: modella 'lcr-i17-J5v5Ff' 'lcr-o0-MOyNuf'
Running [N0]: modella 'lcr-i17-hEo69e' 'lcr-o0-OBHz0M'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
The smallest bogus mutation found for (G!b & (!c | F!a)) | (c & Ga & Fb) was G!c | (c & Fc) Smallest bogus mutation found for (G!b & (!c | F!a)) | (c & Ga & Fb) is G!c | (c & Fc).
error: some error was detected during the above runs. error: some error was detected during the above runs.
Check file bogus for problematic formulas. Check file bogus for problematic formulas.

68
doc/org/ltldo.org
View file

@ -81,7 +81,7 @@ X[]!<>((a && ![]b) || (!a && []b)),4,10
Using =ltldo= the above command can be reduced to this: Using =ltldo= the above command can be reduced to this:
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltldo 'ltl3ba -f %s>%N' -F sample.ltl --stats='%f,%s,%t' ltldo 'ltl3ba -f %s>%O' -F sample.ltl --stats='%f,%s,%t'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
@ -129,7 +129,7 @@ the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, bu
converts the never claim produced by =spin= into this format. converts the never claim produced by =spin= into this format.
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltldo -f a -f GFa 'spin -f %s>%N' -H ltldo -f a -f GFa 'spin -f %s>%O' -H
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
@ -184,8 +184,8 @@ ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
: LBT, or Wring's syntax : LBT, or Wring's syntax
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or : %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
: Wring's syntax : Wring's syntax
: %N,%T,%D,%H the automaton is output as a Never claim, or in : %O,%D the automaton is output as either (%O) HOA/never
: LBTT's, in LTL2DSTAR's, or in the HOA format : claim/LBTT, or (%D) in LTL2DSTAR's format
Contrarily to =ltlcross=, it this not mandatory to specify an output Contrarily to =ltlcross=, it this not mandatory to specify an output
filename using one of the sequence for that last line. For instance filename using one of the sequence for that last line. For instance
@ -209,31 +209,31 @@ executed on each formula in the same order.
A typical use-case is to compare statistics of different tools: A typical use-case is to compare statistics of different tools:
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltldo -F sample.ltl 'spin -f %s>%N' 'ltl3ba -f %s>%N' --stats=%T,%f,%s,%e ltldo -F sample.ltl 'spin -f %s>%O' 'ltl3ba -f %s>%O' --stats=%T,%f,%s,%e
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
spin -f %s>%N,1,2,2 spin -f %s>%O,1,2,2
ltl3ba -f %s>%N,1,1,1 ltl3ba -f %s>%O,1,1,1
spin -f %s>%N,1 U a,2,3 spin -f %s>%O,1 U a,2,3
ltl3ba -f %s>%N,1 U a,2,3 ltl3ba -f %s>%O,1 U a,2,3
spin -f %s>%N,!(!((a U Gb) U b) U GFa),23,86 spin -f %s>%O,!(!((a U Gb) U b) U GFa),23,86
ltl3ba -f %s>%N,!(!((a U Gb) U b) U GFa),2,3 ltl3ba -f %s>%O,!(!((a U Gb) U b) U GFa),2,3
spin -f %s>%N,(b <-> Xc) xor Fb,12,23 spin -f %s>%O,(b <-> Xc) xor Fb,12,23
ltl3ba -f %s>%N,(b <-> Xc) xor Fb,7,11 ltl3ba -f %s>%O,(b <-> Xc) xor Fb,7,11
spin -f %s>%N,FXb R (a R (1 U b)),28,176 spin -f %s>%O,FXb R (a R (1 U b)),28,176
ltl3ba -f %s>%N,FXb R (a R (1 U b)),6,20 ltl3ba -f %s>%O,FXb R (a R (1 U b)),6,20
spin -f %s>%N,Ga,1,1 spin -f %s>%O,Ga,1,1
ltl3ba -f %s>%N,Ga,1,1 ltl3ba -f %s>%O,Ga,1,1
spin -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),15,51 spin -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),15,51
ltl3ba -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),1,0 ltl3ba -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),1,0
spin -f %s>%N,GF((b R !a) U (Xc M 1)),12,60 spin -f %s>%O,GF((b R !a) U (Xc M 1)),12,60
ltl3ba -f %s>%N,GF((b R !a) U (Xc M 1)),2,4 ltl3ba -f %s>%O,GF((b R !a) U (Xc M 1)),2,4
spin -f %s>%N,G(Xb | Gc),4,8 spin -f %s>%O,G(Xb | Gc),4,8
ltl3ba -f %s>%N,G(Xb | Gc),3,5 ltl3ba -f %s>%O,G(Xb | Gc),3,5
spin -f %s>%N,XG!F(a xor Gb),8,21 spin -f %s>%O,XG!F(a xor Gb),8,21
ltl3ba -f %s>%N,XG!F(a xor Gb),4,7 ltl3ba -f %s>%O,XG!F(a xor Gb),4,7
#+end_example #+end_example
Here we used =%T= to output the name of the tool used to translate the Here we used =%T= to output the name of the tool used to translate the
@ -247,7 +247,7 @@ using the trick that the command =echo %f= will not be subject to
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
ltldo -F sample.ltl --stats=%T,%s,%e \ ltldo -F sample.ltl --stats=%T,%s,%e \
'echo "#" %f' '{spin}spin -f %s>%N' '{ltl3ba}ltl3ba -f %s>%N' 'echo "#" %f' '{spin}spin -f %s>%O' '{ltl3ba}ltl3ba -f %s>%O'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
@ -300,14 +300,14 @@ ltldo --list-shorthands
If a COMMANDFMT does not use any %-sequence, and starts with one of If a COMMANDFMT does not use any %-sequence, and starts with one of
the following words, then the string on the right is appended. the following words, then the string on the right is appended.
lbt <%L>%T lbt <%L>%O
ltl2ba -f %s>%N ltl2ba -f %s>%O
ltl2dstar %L %D ltl2dstar %L %D
ltl2tgba -H %f>%H ltl2tgba -H %f>%O
ltl3ba -f %s>%N ltl3ba -f %s>%O
ltl3dra -f %f>%D ltl3dra -f %f>%D
modella %L %T modella %L %O
spin -f %s>%N spin -f %s>%O
#+end_example #+end_example
So for instance you can type just So for instance you can type just
@ -331,7 +331,7 @@ for the neverclaim produced by =ltl2ba -f a=.
: } : }
The =ltl2ba= argument passed to =ltldo= was interpreted as if you had The =ltl2ba= argument passed to =ltldo= was interpreted as if you had
typed ={ltl2ba}ltl2ba -f %s>%N=. typed ={ltl2ba}ltl2ba -f %s>%O=.
The shorthand is only used if it is the first word of an command The shorthand is only used if it is the first word of an command
string that does not use any =%= character. This makes it possible to string that does not use any =%= character. This makes it possible to
@ -390,7 +390,7 @@ claim was then relabeled by =ltldo= to use =Error= instead of =p0=.
This renaming occurs any time some command uses =%s= or =%S= and the This renaming occurs any time some command uses =%s= or =%S= and the
formula has atomic propositions incompatible with Spin's conventions; formula has atomic propositions incompatible with Spin's conventions;
or when some command uses =%l=, =%L=, or =%T=, and the formula has or when some command uses =%l= or =%L=, and the formula has
atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]]. atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]].

36
src/bin/common_trans.cc
View file

@ -39,14 +39,14 @@ static struct shorthands_t
const char* suffix; const char* suffix;
} }
shorthands[] = { shorthands[] = {
{ "lbt", " <%L>%T" }, { "lbt", " <%L>%O" },
{ "ltl2ba", " -f %s>%N" }, { "ltl2ba", " -f %s>%O" },
{ "ltl2dstar", " %L %D"}, { "ltl2dstar", " %L %D"},
{ "ltl2tgba", " -H %f>%H" }, { "ltl2tgba", " -H %f>%O" },
{ "ltl3ba", " -f %s>%N" }, { "ltl3ba", " -f %s>%O" },
{ "ltl3dra", " -f %f>%D" }, { "ltl3dra", " -f %f>%D" },
{ "modella", " %L %T" }, { "modella", " %L %O" },
{ "spin", " -f %s>%N" }, { "spin", " -f %s>%O" },
}; };
void show_shorthands() void show_shorthands()
@ -162,14 +162,11 @@ void
printable_result_filename::print(std::ostream& os, const char* pos) const printable_result_filename::print(std::ostream& os, const char* pos) const
{ {
output_format old_format = format; output_format old_format = format;
if (*pos == 'N') // The HOA parser can read LBTT, neverclaims, and HOA.
format = Hoa; // The HOA parse also reads neverclaims if (*pos == 'N' || *pos == 'T' || *pos == 'H' || *pos == 'O')
else if (*pos == 'T') format = Hoa;
format = Lbtt;
else if (*pos == 'D') else if (*pos == 'D')
format = Dstar; format = Dstar;
else if (*pos == 'H')
format = Hoa;
else else
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();
@ -179,7 +176,7 @@ printable_result_filename::print(std::ostream& os, const char* pos) const
// to mix the formats. // to mix the formats.
if (format != old_format) if (format != old_format)
error(2, 0, error(2, 0,
"you may not mix %%D, %%H, %%N, and %%T specifiers: %s", "you may not mix different output specifiers: %s",
translators[translator_num].spec); translators[translator_num].spec);
} }
else else
@ -209,6 +206,7 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict,
declare('H', &output); declare('H', &output);
declare('N', &output); declare('N', &output);
declare('T', &output); declare('T', &output);
declare('O', &output);
size_t s = translators.size(); size_t s = translators.size();
assert(s); assert(s);
@ -225,9 +223,11 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict,
"one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how "
"to pass the formula.", t.spec); "to pass the formula.", t.spec);
if (!no_output_allowed if (!no_output_allowed
&& !(has['D'] || has['N'] || has['T'] || has['H'])) && !(has['O'] || has['D'] ||
// backward-compatibility
has['N'] || has['T'] || has['H']))
error(2, 0, "no output %%-sequence in '%s'.\n Use one of " error(2, 0, "no output %%-sequence in '%s'.\n Use one of "
"%%D,%%H,%%N,%%T to indicate where the automaton is saved.", "%%O or %%D to indicate where and how the automaton is saved.",
t.spec); t.spec);
// Remember the %-sequences used by all translators. // Remember the %-sequences used by all translators.
prime(t.cmd); prime(t.cmd);
@ -402,9 +402,9 @@ static const argp_option options[] =
0 }, 0 },
{ "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
{ "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%O,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's," "the automaton is output as either (%O) HOA/never claim/LBTT, or (%D) "
" or in the HOA format", 0 }, "in LTL2DSTAR's format", 0 },
{ 0, 0, 0, 0, { 0, 0, 0, 0,
"If either %l, %L, or %T are used, any input formula that does " "If either %l, %L, or %T are used, any input formula that does "
"not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "

2
src/bin/common_trans.hh
View file

@ -61,7 +61,7 @@ struct printable_result_filename final:
public spot::printable_value<spot::temporary_file*> public spot::printable_value<spot::temporary_file*>
{ {
unsigned translator_num; unsigned translator_num;
enum output_format { None, Lbtt, Dstar, Hoa }; enum output_format { None, Dstar, Hoa };
mutable output_format format; mutable output_format format;
printable_result_filename(); printable_result_filename();

29
src/bin/ltlcross.cc
View file

@ -529,35 +529,6 @@ namespace
es = 0; es = 0;
switch (output.format) switch (output.format)
{ {
case printable_result_filename::Lbtt:
{
std::string error;
std::ifstream f(output.val()->name());
if (!f)
{
status_str = "no output";
problem = true;
es = -1;
global_error() << "Cannot open " << output.val()
<< std::endl;
end_error();
}
else
{
res = spot::lbtt_parse(f, error, dict);
if (!res)
{
status_str = "parse error";
problem = true;
es = -1;
global_error() << ("error: failed to parse output in "
"LBTT format: ")
<< error << std::endl;
end_error();
}
}
break;
}
case printable_result_filename::Dstar: case printable_result_filename::Dstar:
{ {
spot::dstar_parse_error_list pel; spot::dstar_parse_error_list pel;

26
src/bin/ltldo.cc
View file

@ -171,29 +171,6 @@ namespace
problem = false; problem = false;
switch (output.format) switch (output.format)
{ {
case printable_result_filename::Lbtt:
{
std::string error;
std::ifstream f(output.val()->name());
if (!f)
{
problem = true;
std::cerr << "error: could not open " << output.val()
<< " after running \"" << cmd << "\".\n";
}
else
{
res = spot::lbtt_parse(f, error, dict);
if (!res)
{
problem = true;
std::cerr << "error: failed to parse output of \""
<< cmd << "\" in LBTT format:\n"
<< "error: " << error << '\n';
}
}
break;
}
case printable_result_filename::Dstar: case printable_result_filename::Dstar:
{ {
spot::dstar_parse_error_list pel; spot::dstar_parse_error_list pel;
@ -213,8 +190,9 @@ namespace
} }
break; break;
} }
case printable_result_filename::Hoa: // Will also read neverclaims case printable_result_filename::Hoa:
{ {
// Will also read neverclaims/LBTT
spot::hoa_parse_error_list pel; spot::hoa_parse_error_list pel;
std::string filename = output.val()->name(); std::string filename = output.val()->name();
auto aut = spot::hoa_parse(filename, pel, dict); auto aut = spot::hoa_parse(filename, pel, dict);

6
src/hoaparse/hoaparse.yy
View file

@ -1259,7 +1259,11 @@ lbtt-guard: STRING
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env); auto* f = spot::ltl::parse_lbt(*$1, pel, *res.env);
if (!f || !pel.empty()) if (!f || !pel.empty())
error(@$, "failed to parse guard"); {
std::string s = "failed to parse guard: ";
s += *$1;
error(@$, s);
}
if (!pel.empty()) if (!pel.empty())
for (auto& j: pel) for (auto& j: pel)
{ {

4
src/hoaparse/hoascan.ll
View file

@ -213,7 +213,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
"-1" BEGIN(in_LBTT_TRANS); yylloc->step(); "-1" BEGIN(in_LBTT_TRANS); yylloc->step();
} }
<in_LBTT_TRANS>{ <in_LBTT_TRANS>{
[0-9+] { [0-9]+ {
parse_int(); parse_int();
if (lbtt_t) if (lbtt_t)
BEGIN(in_LBTT_T_ACC); BEGIN(in_LBTT_T_ACC);
@ -235,7 +235,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
} }
} }
<in_LBTT_T_ACC>{ <in_LBTT_T_ACC>{
[0-9+] parse_int(); return token::ACC; [0-9]+ parse_int(); return token::ACC;
"-1" BEGIN(in_LBTT_GUARD); yylloc->step(); "-1" BEGIN(in_LBTT_GUARD); yylloc->step();
} }
<in_LBTT_GUARD>{ <in_LBTT_GUARD>{

173
src/tgbaalgos/lbtt.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -130,139 +130,7 @@ namespace spot
bool sba_format_; bool sba_format_;
const_tgba_digraph_ptr sba_; const_tgba_digraph_ptr sba_;
}; };
static
tgba_digraph_ptr
lbtt_read_tgba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
const bdd_dict_ptr& dict, ltl::environment& env)
{
auto aut = make_tgba_digraph(dict);
acc_mapper_int acc_b(aut, num_acc);
aut->new_states(num_states);
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
// Read the acceptance conditions.
acc_cond::mark_t acc = 0U;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
auto p = acc_b.lookup(acc_n);
if (p.first)
{
acc |= p.second;
} }
else
{
error += "more acceptance sets used than declared";
return nullptr;
}
}
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
return nullptr;
}
bdd cond = formula_to_bdd(f, dict, aut.get());
f->destroy();
aut->new_transition(src_state, dst_state, cond, acc);
}
}
return aut;
}
tgba_digraph_ptr
lbtt_read_gba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
const bdd_dict_ptr& dict, ltl::environment& env)
{
auto aut = make_tgba_digraph(dict);
acc_mapper_int acc_b(aut, num_acc);
aut->new_states(num_states);
aut->prop_state_based_acc();
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the acceptance conditions.
acc_cond::mark_t acc = 0U;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
auto p = acc_b.lookup(acc_n);
if (p.first)
{
acc |= p.second;
}
else
{
error += "more acceptance sets used than declared";
return nullptr;
}
}
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
return nullptr;
}
bdd cond = formula_to_bdd(f, dict, aut.get());
f->destroy();
aut->new_transition(src_state, dst_state, cond, acc);
}
}
return aut;
}
} // anonymous
std::ostream& std::ostream&
lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba) lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba)
@ -271,41 +139,4 @@ namespace spot
b.run(); b.run();
return os; return os;
} }
tgba_digraph_ptr
lbtt_parse(std::istream& is, std::string& error, const bdd_dict_ptr& dict,
ltl::environment& env)
{
is >> std::skipws;
unsigned num_states = 0;
is >> num_states;
if (!is)
{
error += "failed to read the number of states";
return 0;
}
// No states? Read the rest of the line and return an empty automaton.
if (num_states == 0)
{
std::string header;
std::getline(is, header);
return make_tgba_digraph(dict);
}
unsigned num_acc = 0;
is >> num_acc;
int type;
type = is.peek();
if (type == 't' || type == 'T' || type == 's' || type == 'S')
type = is.get();
if (type == 't' || type == 'T')
return lbtt_read_tgba(num_states, num_acc, is, error, dict, env);
else
return lbtt_read_gba(num_states, num_acc, is, error, dict, env);
}
} }

18
src/tgbaalgos/lbtt.hh
View file

@ -23,9 +23,8 @@
#ifndef SPOT_TGBAALGOS_LBTT_HH #ifndef SPOT_TGBAALGOS_LBTT_HH
# define SPOT_TGBAALGOS_LBTT_HH # define SPOT_TGBAALGOS_LBTT_HH
#include "tgba/tgbagraph.hh" #include "tgba/tgba.hh"
#include <iosfwd> #include <iosfwd>
#include "ltlenv/defaultenv.hh"
namespace spot namespace spot
{ {
@ -38,21 +37,6 @@ namespace spot
/// acceptance format (similar to LBT's format). /// acceptance format (similar to LBT's format).
SPOT_API std::ostream& SPOT_API std::ostream&
lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba = false); lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba = false);
/// \ingroup tgba_io
/// \brief Read an automaton in LBTT's format
///
/// \param is The stream on which the automaton should be input.
/// \param error A string in which to write any error message.
/// \param dict The dictionary that should register the BDD variables
/// used by the automaton built.
/// \param env The environment of atomic proposition into which parsing
/// should take place.
/// \return the read tgba or 0 on error.
SPOT_API tgba_digraph_ptr
lbtt_parse(std::istream& is, std::string& error,
const bdd_dict_ptr& dict,
ltl::environment& env = ltl::default_environment::instance());
} }
#endif // SPOT_TGBAALGOS_LBTT_HH #endif // SPOT_TGBAALGOS_LBTT_HH

6
src/tgbatest/lbttparse.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement # Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -122,7 +122,7 @@ cat > input <<EOF
-1 -1
EOF EOF
cat >expected <<EOF cat >expected <<EOF
input:3.5-20: failed to parse guard input:3.5-20: failed to parse guard: & ! "a" ! "b" !
input:3.20: syntax error, unexpected '!', expecting end of formula input:3.20: syntax error, unexpected '!', expecting end of formula
input:3.20: ignoring trailing garbage input:3.20: ignoring trailing garbage
EOF EOF

29
src/tgbatest/ltl2tgba.cc
View file

@ -343,7 +343,7 @@ checked_main(int argc, char** argv)
bool accepting_run = false; bool accepting_run = false;
bool accepting_run_replay = false; bool accepting_run_replay = false;
bool from_file = false; bool from_file = false;
enum { ReadLbtt, ReadDstar, ReadHoa } readformat = ReadHoa; enum { ReadDstar, ReadHoa } readformat = ReadHoa;
bool nra2nba = false; bool nra2nba = false;
bool dra2dba = false; bool dra2dba = false;
bool scc_filter = false; bool scc_filter = false;
@ -883,7 +883,7 @@ checked_main(int argc, char** argv)
else if (!strcmp(argv[formula_index], "-XL")) else if (!strcmp(argv[formula_index], "-XL"))
{ {
from_file = true; from_file = true;
readformat = ReadLbtt; readformat = ReadHoa;
} }
else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH
{ {
@ -967,31 +967,6 @@ checked_main(int argc, char** argv)
{ {
switch (readformat) switch (readformat)
{ {
case ReadLbtt:
{
std::string error;
std::istream* in = &std::cin;
std::fstream* f = 0;
if (input != "-")
{
in = f = new std::fstream(input.c_str());
if (!*f)
{
std::cerr << "cannot open " << input << std::endl;
return 2;
}
}
tm.start("parsing lbtt");
a = spot::lbtt_parse(*in, error, dict, env);
tm.stop("parsing lbtt");
delete f;
if (!a)
{
std::cerr << error << std::endl;
return 2;
}
}
break;
case ReadDstar: case ReadDstar:
{ {
spot::dstar_parse_error_list pel; spot::dstar_parse_error_list pel;