From 964c2bed431b33e2eca3d630690c865b483b741a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Feb 2011 12:21:36 +0100 Subject: [PATCH] Adjust the WDBA test to count for sub-transitions. * bench/wdba/run: Use -kt to count sub-transitions. * bench/wdba/README: Adjust comments. --- ChangeLog | 7 ++++ bench/wdba/README | 93 ++++++++++++++++++++++++++--------------------- bench/wdba/run | 12 +++--- 3 files changed, 64 insertions(+), 48 deletions(-) diff --git a/ChangeLog b/ChangeLog index 27552aa14..386bb8d4a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-02-08 Alexandre Duret-Lutz + + Adjust the WDBA test to count for sub-transitions. + + * bench/wdba/run: Use -kt to count sub-transitions. + * bench/wdba/README: Adjust comments. + 2011-02-08 Alexandre Duret-Lutz Fix a spurious g++ warning observed on Darwin builds. diff --git a/bench/wdba/README b/bench/wdba/README index bc5cef20f..6bbc54df5 100644 --- a/bench/wdba/README +++ b/bench/wdba/README @@ -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. diff --git a/bench/wdba/run b/bench/wdba/run index c3aa24fee..b41cf36a7 100755 --- a/bench/wdba/run +++ b/bench/wdba/run @@ -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