Adjust the WDBA test to count for sub-transitions.
* bench/wdba/run: Use -kt to count sub-transitions. * bench/wdba/README: Adjust comments.
This commit is contained in:
Alexandre Duret-Lutz
parent
baf1288dc6
commit
964c2bed43
3 changed files with 64 additions and 48 deletions
|
|
@ -28,58 +28,67 @@ 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)))
|
||||
1, 2, 4, 2, 4, !(G(!p))
|
||||
2, 3, 10, 3, 10, !(Fr->(!p U r))
|
||||
3, 3, 13, 3, 12, !(G(q->G(!p)))
|
||||
4, 4, 30, 4, 32, !(G((q&!r&Fr)->(!p U r)))
|
||||
5, 3, 21, 3, 24, !(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))
|
||||
7, 2, 7, 2, 7, !((!r U (p&!r))|(G!r))
|
||||
8, 2, 5, 2, 5, !(G(!q)|F(q&Fp))
|
||||
9, 3, 23, 3, 24, !(G(q&!r->((!r U (p&!r))|G!r)))
|
||||
10, 6, 12, 6, 12, !((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p)
|
||||
11, 7, 18, 7, 18, !(Fr->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r))))))))))
|
||||
12, 7, 28, 7, 28, !(Fq->(!q U (q&((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p))))
|
||||
13, 8, 46, 8, 64, !(G((q&Fr)->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r)))))))))))
|
||||
14, 7, 38, 7, 56, !(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, 4, 2, 4, !(G(p))
|
||||
16, 3, 10, 3, 10, !(Fr->(p U r))
|
||||
17, 3, 13, 3, 12, !(G(q->G(p)))
|
||||
18, 4, 15, 4, 16, !(G((p&!r&Fr)->(p U r)))
|
||||
19, 3, 21, 3, 24, !(G(q&!r->((p U r)|Gp)))
|
||||
20, 4, 12, 4, 12, !((!p U s)|Gp)
|
||||
21, 3, 18, 3, 18, !(Fr->(!p U (s|r)))
|
||||
22, 4, 54, 4, 64, !(G((q&!r&Fr)->(!p U (s|r))))
|
||||
23, 3, 37, 3, 48, !(G(q&!r->((!p U (s|r))|G!p)))
|
||||
24, 3, 19, 3, 20, !(Fr->(p->(!r U (s&!r))) U r)
|
||||
25, 4, 59, 4, 64, !(G((q&!r&Fr)->(p->(!r U (s&!r))) U r))
|
||||
26, 3, 20, 3, 20, !(Fp->(!p U (s&!p&X(!p U t))))
|
||||
27, 4, 44, 4, 44, !(Fr->(!p U (r|(s&!p&X(!p U t)))))
|
||||
28, 4, 48, 4, 48, !((G!q)|(!q U (q&Fp->(!p U (s&!p&X(!p U t))))))
|
||||
29, 5, 128, 5, 160, !(G((q&Fr)->(!p U (r|(s&!p&X(!p U t))))))
|
||||
30, 4, 92, 4, 128, !(G(q->(Fp->(!p U (r|(s&!p&X(!p U t)))))))
|
||||
31, 4, 34, 3, 20, !((F(s&XFt))->((!s) U p))
|
||||
32, 4, 46, 4, 44, !(Fr->((!(s&(!r)&X(!r U (t&!r))))U(r|p)))
|
||||
33, 5, 82, 4, 52, !((G!q)|((!q)U(q&((F(s&XFt))->((!s) U p)))))
|
||||
34, 5, 130, 5, 160, !(G((q&Fr)->((!(s&(!r)&X(!r U (t&!r))))U(r|p))))
|
||||
35, 10, 254, 4, 128, !(G(q->(!(s&(!r)&X(!r U (t&!r)))U(r|p)|G(!(s&XFt)))))
|
||||
36, 4, 36, 5, 50, !(Fr->(s&X(!r U t)->X(!r U (t&Fp))) U r)
|
||||
37, 4, 52, 4, 52, !(Fr->(p->(!r U (s&!r&X(!r U t)))) U r)
|
||||
38, 5, 148, 5, 160, !(G((q&Fr)->(p->(!r U (s&!r&X(!r U t)))) U r))
|
||||
39, 4, 104, 4, 104, !(Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r)
|
||||
40, 5, 296, 5, 320, !(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
|
||||
The second and third numbers give the number of states and transitions
|
||||
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.
|
||||
|
||||
When counting transitions, we are actually counting the number of
|
||||
"sub-transitions". That is, on an automaton defined over two atomic
|
||||
properties "p" and "q", a transition labelled by "p" actually stands
|
||||
for two sub-transitions labelled by "p&q" and "p&!q". So we are
|
||||
counting it as two transitions.
|
||||
|
||||
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).
|
||||
this is because their structure changed when they where determinized.
|
||||
Even though they have the same number of states as the non-minimized
|
||||
automaton, the states do not accept the same language. There is even
|
||||
one case (formula 36) where the minimized automaton got one more
|
||||
state.
|
||||
|
||||
In two cases (formulae 31 and 35) the minimization actually removed
|
||||
states in addition to making the automata deterministic.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2010 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -68,15 +68,15 @@ EOF
|
|||
line=0
|
||||
echo "# form. nbr., states, trans., states minimized, trans. minimized, formula"
|
||||
while read f; do
|
||||
"$LTL2TGBA" -f -r7 -R3 -DS -k "!($f)" >out
|
||||
"$LTL2TGBA" -f -r7 -x -R3 -DS -kt "!($f)" >out
|
||||
states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
|
||||
transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
|
||||
transitions=`sed -n 's/^sub trans.: \([0-9]*\)$/\1/p' out`
|
||||
|
||||
"$LTL2TGBA" -f -r1 -R3 -Rm -k "!($f)" >out
|
||||
"$LTL2TGBA" -f -r1 -R3 -Rm -kt "!($f)" >out
|
||||
states2=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
|
||||
transitions2=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
|
||||
transitions2=`sed -n 's/^sub trans.: \([0-9]*\)$/\1/p' out`
|
||||
|
||||
line=`expr $line + 1`
|
||||
line=`expr $line + 1`
|
||||
echo "$line, $states, $transitions, $states2, $transitions2, !($f)"
|
||||
done < obligations.txt
|
||||
) | tee results.txt
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue