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

Add a WDBA benchmark.

Browse source 
* bench/wdba/: New directory.
* bench/Makefile.am (SUBDIRS): Add wdba.
* NEWS: Mention it.
* configure.ac: Output bench/wdba/defs and bench/wdba/Makefile.
This commit is contained in:
Alexandre Duret-Lutz 2010-12-14 11:13:49 +01:00
parent aadef1fd87
commit edc71b807e
8 changed files with 262 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

85
bench/wdba/README Normal file
View file

@ -0,0 +1,85 @@
This benchmark shows the size of 40 obligation formulae translated by
Spot to degeneralized state-based Büchi automata, before and after
reductions using the WDBA technique introduced in the following paper.
@InProceedings{ dax.07.atva,
author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
title = {Mechanizing the Powerset Construction for Restricted
Classes of {$\omega$}-Automata},
year = 2007,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = 4762,
booktitle = {Proceedings of the 5th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'07)},
editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
and Yoshio Okamura},
month = oct
}
This is meant to complement the experiment 1 at
http://www.daxc.de/eth/atva07/index.html
The formulae used here are the same as the formulae used on the above
page, and are presented in the same order.
Running the `./run' script should produce an output similar to the
following:
# form. nbr., states, trans., states minimized, trans. minimized, formula
1, 2, 3, 2, 3, !(G(!p))
2, 3, 5, 3, 5, !(Fr->(!p U r))
3, 3, 6, 3, 6, !(G(q->G(!p)))
4, 4, 8, 4, 9, !(G((q&!r&Fr)->(!p U r)))
5, 3, 6, 3, 7, !(G(q&!r->((!p U r)|G!p)))
6, 1, 1, 1, 1, !(Fp)
7, 2, 3, 2, 3, !((!r U (p&!r))|(G!r))
8, 2, 3, 2, 3, !(G(!q)|F(q&Fp))
9, 3, 5, 3, 6, !(G(q&!r->((!r U (p&!r))|G!r)))
10, 6, 11, 6, 11, !((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p)
11, 7, 13, 7, 13, !(Fr->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r))))))))))
12, 7, 14, 7, 14, !(Fq->(!q U (q&((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p))))
13, 8, 16, 8, 21, !(G((q&Fr)->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r)))))))))))
14, 7, 14, 7, 19, !(G(q->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|((!p U r)|G!p)|Gp))))))))))
15, 2, 3, 2, 3, !(G(p))
16, 3, 5, 3, 5, !(Fr->(p U r))
17, 3, 6, 3, 6, !(G(q->G(p)))
18, 4, 7, 4, 8, !(G((p&!r&Fr)->(p U r)))
19, 3, 6, 3, 7, !(G(q&!r->((p U r)|Gp)))
20, 4, 7, 4, 7, !((!p U s)|Gp)
21, 3, 5, 3, 5, !(Fr->(!p U (s|r)))
22, 4, 8, 4, 9, !(G((q&!r&Fr)->(!p U (s|r))))
23, 3, 6, 3, 7, !(G(q&!r->((!p U (s|r))|G!p)))
24, 3, 5, 3, 6, !(Fr->(p->(!r U (s&!r))) U r)
25, 4, 8, 4, 10, !(G((q&!r&Fr)->(p->(!r U (s&!r))) U r))
26, 3, 6, 3, 6, !(Fp->(!p U (s&!p&X(!p U t))))
27, 4, 8, 4, 8, !(Fr->(!p U (r|(s&!p&X(!p U t)))))
28, 4, 9, 4, 9, !((G!q)|(!q U (q&Fp->(!p U (s&!p&X(!p U t))))))
29, 5, 12, 5, 15, !(G((q&Fr)->(!p U (r|(s&!p&X(!p U t))))))
30, 4, 10, 4, 13, !(G(q->(Fp->(!p U (r|(s&!p&X(!p U t)))))))
31, 4, 8, 3, 5, !((F(s&XFt))->((!s) U p))
32, 4, 7, 4, 7, !(Fr->((!(s&(!r)&X(!r U (t&!r))))U(r|p)))
33, 5, 12, 4, 8, !((G!q)|((!q)U(q&((F(s&XFt))->((!s) U p)))))
34, 5, 10, 5, 12, !(G((q&Fr)->((!(s&(!r)&X(!r U (t&!r))))U(r|p))))
35, 10, 28, 4, 10, !(G(q->(!(s&(!r)&X(!r U (t&!r)))U(r|p)|G(!(s&XFt)))))
36, 4, 8, 5, 18, !(Fr->(s&X(!r U t)->X(!r U (t&Fp))) U r)
37, 4, 9, 4, 11, !(Fr->(p->(!r U (s&!r&X(!r U t)))) U r)
38, 5, 13, 5, 17, !(G((q&Fr)->(p->(!r U (s&!r&X(!r U t)))) U r))
39, 4, 10, 4, 11, !(Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r)
40, 5, 14, 5, 17, !(G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r))
The first number is the number of the formula, so you can compare with
the number displayed at http://www.daxc.de/eth/atva07/index.html.
The second and third numbers give the number of states and transition
of the automaton produced by Spot (with formula simplifications and SCC
simplifications turned on), while the fourth and fifth number show the
number of states and transitions with an additional WDBA minimization step.
You can observe that some minimized automata have more transitions:
this is because they have become deterministic. There is even one
case where the minimized automaton got one more state (formula 36).
In two cases (formulae 31 and 35) the minimization actually removed
states in addition to making the automata deterministic.