Some cleanup of Thibaud's patches.
* AUTHORS: Add Thibaud. * NEWS: Mention ltlgrind and ltlcross --grind. * src/ltlvisit/mutation.hh, src/ltlvisit/mutation.cc: Use an enum instead of #define. Rename get_mutations() into mutate(). Other minor cosmetic changes. * src/bin/ltlgrind.cc: Adjust. * src/bin/ltlcross.cc: Slight changes the the output * doc/org/ltlcross.org, doc/org/ltlgrind.org: Minor rewordings and fix for org-mode syntax. * src/ltltest/ltlcrossgrind.test, src/ltltest/ltlgrind.test: Fix copyright year.
This commit is contained in:
Alexandre Duret-Lutz
parent
4e1586dc54
commit
645ecce1c9
10 changed files with 325 additions and 141 deletions
|
|
@ -651,44 +651,190 @@ You can periodically check the contents of =bugs.ltl=, and then run
|
|||
ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N'
|
||||
#+END_SRC
|
||||
|
||||
** =--no-check=
|
||||
|
||||
The =--no-check= option disables all sanity checks, and only use the supplied
|
||||
formulas in their positive form.
|
||||
|
||||
When checks are enabled, the negated formulas are intermixed with the
|
||||
positives ones in the results. Therefore the =--no-check= option can
|
||||
be used to gather statistics about a specific set of formulas.
|
||||
|
||||
# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed
|
||||
# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY
|
||||
# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella
|
||||
# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ
|
||||
# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO
|
||||
# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic
|
||||
# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq
|
||||
# LocalWords: setenv concat getenv
|
||||
** =--grind=FILENAME=
|
||||
This argument tells =ltlcross= that, when an error is detected, it
|
||||
should try to find a smaller formula that still exhibit the
|
||||
bug. This is the procedure used:
|
||||
- Internally list the mutations of the bogus formula and sort
|
||||
them by length (as =ltlgrind --sort= would do)
|
||||
- Process every mutation until one is found that exhibit the bug
|
||||
- Repeat the process with this formula, and again until a formula
|
||||
is found for which no mutation exhibit the bug
|
||||
- Output that last formula in FILENAME
|
||||
Every bogus formula found during the process will be saved if
|
||||
=--save-bogus=FILENAME= is provided.
|
||||
|
||||
Example:
|
||||
#+BEGIN_SRC sh :exports both :results verbatim
|
||||
This option tells =ltlcross= that, when a problem is detected, it
|
||||
should try to find a smaller formula that still exhibits the
|
||||
problem.
|
||||
|
||||
Here is the procedure used:
|
||||
- internally list the mutations of the bogus formula and sort
|
||||
them by length (as [[file:ltlgrind.org][=ltlgrind --sort=]] would do)
|
||||
- process every mutation until one is found that exhibit the bug
|
||||
- repeat the process with this new formula, and again until a formula
|
||||
is found for which no mutation exhibit the bug
|
||||
- output that last formula in =FILENAME=
|
||||
|
||||
If =--save-bogus=OTHERFILENAME= is provided, every bogus formula found
|
||||
during the process will be saved in =OTHERFILENAME=.
|
||||
|
||||
Example:
|
||||
#+BEGIN_SRC sh :exports code :results verbatim
|
||||
ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \
|
||||
--save-bogus=bogus \
|
||||
--grind=bogus-grind
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC sh :exports results :results verbatim
|
||||
ltlcross -f '(G!b & (!c | F!a)) | (c & Ga & Fb)' "modella %L %T" \
|
||||
--save-bogus=bogus --grind=bogus-grind 2>&1
|
||||
true
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
| & G ! p0 | ! p1 F ! p2 & & p1 G p2 F p0
|
||||
Running [P0]: modella 'lcr-i0-YBdcX8' 'lcr-o0-VWBBUF'
|
||||
Running [N0]: modella 'lcr-i0-wteTSc' 'lcr-o0-pqlbRJ'
|
||||
Performing sanity checks and gathering statistics...
|
||||
error: P0*N0 is nonempty; both automata accept the infinite word
|
||||
cycle{!p0 & !p1}
|
||||
|
||||
Trying to find a bogus mutation of "(G!b & (!c | F!a)) | (c & Ga & Fb)"
|
||||
Mutation [1/22]
|
||||
& & p0 G p1 F p2
|
||||
Running [P0]: modella 'lcr-i1-Ursu0g' 'lcr-o0-Lm3N9N'
|
||||
Running [N0]: modella 'lcr-i1-AkNujl' 'lcr-o0-VYRbtS'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [2/22]
|
||||
& G ! p0 | ! p1 F ! p2
|
||||
Running [P0]: modella 'lcr-i2-uuBGGp' 'lcr-o0-eZLbUW'
|
||||
Running [N0]: modella 'lcr-i2-qO717t' 'lcr-o0-evKSl1'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [3/22]
|
||||
| G ! p0 & & p1 G p2 F p0
|
||||
Running [P0]: modella 'lcr-i3-hQAiDy' 'lcr-o0-PoKIU5'
|
||||
Running [N0]: modella 'lcr-i3-Jl5vcD' 'lcr-o0-RtIjua'
|
||||
Performing sanity checks and gathering statistics...
|
||||
error: P0*N0 is nonempty; both automata accept the infinite word
|
||||
cycle{!p0 & !p1}
|
||||
|
||||
Trying to find a bogus mutation of "G!b | (c & Ga & Fb)"
|
||||
Mutation [1/16]
|
||||
t
|
||||
Running [P0]: modella 'lcr-i4-HUTvSH' 'lcr-o0-XXrIgf'
|
||||
Running [N0]: modella 'lcr-i4-MoZ9EM' 'lcr-o0-w2MB3j'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [2/16]
|
||||
G ! p0
|
||||
Running [P0]: modella 'lcr-i5-ZjeLsR' 'lcr-o0-lT2URo'
|
||||
Running [N0]: modella 'lcr-i5-ELzihW' 'lcr-o0-tljGGt'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [3/16]
|
||||
& & p0 G p1 F p2
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [4/16]
|
||||
| G ! p0 & p1 F p0
|
||||
Running [P0]: modella 'lcr-i6-VUy2yy' 'lcr-o0-44be05'
|
||||
Running [N0]: modella 'lcr-i6-SBBHrD' 'lcr-o0-VAcbTa'
|
||||
Performing sanity checks and gathering statistics...
|
||||
error: P0*N0 is nonempty; both automata accept the infinite word
|
||||
cycle{!p0 & !p1}
|
||||
|
||||
Trying to find a bogus mutation of "G!b | (c & Fb)"
|
||||
Mutation [1/10]
|
||||
t
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [2/10]
|
||||
G ! p0
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [3/10]
|
||||
& p0 F p1
|
||||
Running [P0]: modella 'lcr-i7-gBs0mN' 'lcr-o0-bgNCRk'
|
||||
Running [N0]: modella 'lcr-i7-oAYtmS' 'lcr-o0-VvmlRp'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [4/10]
|
||||
| p0 G ! p1
|
||||
Running [P0]: modella 'lcr-i8-wLstoX' 'lcr-o0-jZOBVu'
|
||||
Running [N0]: modella 'lcr-i8-4hBZs2' 'lcr-o0-3Ezn0z'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [5/10]
|
||||
| G ! p0 F p0
|
||||
Running [P0]: modella 'lcr-i9-mqY0z7' 'lcr-o0-hcDE9E'
|
||||
Running [N0]: modella 'lcr-i9-MtDCJc' 'lcr-o0-5fRAjK'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [6/10]
|
||||
| ! p0 & p1 F p0
|
||||
Running [P0]: modella 'lcr-i10-s5ZlUh' 'lcr-o0-fvp7uP'
|
||||
Running [N0]: modella 'lcr-i10-4GWe6m' 'lcr-o0-LKFmHU'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [7/10]
|
||||
| G p1 & p0 F p1
|
||||
Running [P0]: modella 'lcr-i11-wZJKjs' 'lcr-o0-D948VZ'
|
||||
Running [N0]: modella 'lcr-i11-yVpOyx' 'lcr-o0-rjXtb5'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [8/10]
|
||||
| & p0 p1 G ! p0
|
||||
Running [P0]: modella 'lcr-i12-g9bpRC' 'lcr-o0-RhIkxa'
|
||||
Running [N0]: modella 'lcr-i12-rvWBdI' 'lcr-o0-DauTTf'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [9/10]
|
||||
| G ! p0 & p0 F p0
|
||||
Running [P0]: modella 'lcr-i13-sXVtCN' 'lcr-o0-9WE4kl'
|
||||
Running [N0]: modella 'lcr-i13-49803S' 'lcr-o0-BNXXMq'
|
||||
Performing sanity checks and gathering statistics...
|
||||
error: P0*N0 is nonempty; both automata accept the infinite word
|
||||
cycle{!p0}
|
||||
|
||||
Trying to find a bogus mutation of "G!c | (c & Fc)"
|
||||
Mutation [1/7]
|
||||
t
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [2/7]
|
||||
G ! p0
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [3/7]
|
||||
& p0 F p0
|
||||
Running [P0]: modella 'lcr-i14-Ohct43' 'lcr-o0-vKfEPB'
|
||||
Running [N0]: modella 'lcr-i14-aKk2A9' 'lcr-o0-RiFqmH'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [4/7]
|
||||
| p0 G ! p0
|
||||
Running [P0]: modella 'lcr-i15-Oht38e' 'lcr-o0-bhxGVM'
|
||||
Running [N0]: modella 'lcr-i15-iyrAIk' 'lcr-o0-nMFuvS'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [5/7]
|
||||
| G ! p0 F p0
|
||||
warning: This formula or its negation has already been checked.
|
||||
Use --allow-dups if it should not be ignored.
|
||||
|
||||
Mutation [6/7]
|
||||
| ! p0 & p0 F p0
|
||||
Running [P0]: modella 'lcr-i16-nZMD9X' 'lcr-o0-epKIYv'
|
||||
Running [N0]: modella 'lcr-i16-DSW2N3' 'lcr-o0-6ElnDB'
|
||||
Performing sanity checks and gathering statistics...
|
||||
|
||||
Mutation [7/7]
|
||||
| & p0 F p0 G p0
|
||||
Running [P0]: modella 'lcr-i17-Z6avt9' 'lcr-o0-QJhDjH'
|
||||
Running [N0]: modella 'lcr-i17-hEo69e' 'lcr-o0-OBHz0M'
|
||||
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)
|
||||
|
||||
error: some error was detected during the above runs.
|
||||
Check file bogus for problematic formulas.
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC sh :exports both :results verbatim
|
||||
cat bogus
|
||||
|
|
@ -706,3 +852,22 @@ cat bogus-grind
|
|||
|
||||
#+RESULTS:
|
||||
: G!c | (c & Fc)
|
||||
|
||||
** =--no-check=
|
||||
|
||||
The =--no-check= option disables all sanity checks, and only use the supplied
|
||||
formulas in their positive form.
|
||||
|
||||
When checks are enabled, the negated formulas are intermixed with the
|
||||
positives ones in the results. Therefore the =--no-check= option can
|
||||
be used to gather statistics about a specific set of formulas.
|
||||
|
||||
|
||||
# LocalWords: ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed
|
||||
# LocalWords: automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY
|
||||
# LocalWords: ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella
|
||||
# LocalWords: lbtt csv json randltl ltlfilt wm eGEYaZ nYpFBX fGdZQ
|
||||
# LocalWords: CPs kXiZZS ILLzR wU CcMCaQ IOckzW tsT RZ TJXmT jb XRO
|
||||
# LocalWords: nxqfd hS vNItGg acc scc nondetstates nondeterministic
|
||||
# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq
|
||||
# LocalWords: setenv concat getenv
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue