Introduce -ks to print only the size of the automaton (without

SCC information).

* src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option.
* src/tgbatest/ltl2tgba.test, bench/ltlclasses/run,
bench/ltlcounter/run: Use -ks instead of -k to speed things up.

ChangeLog

+2010-12-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Introduce -ks to print only the size of the automaton (without
+	SCC information).
+
+	* src/tgbatest/ltl2tgba.cc (syntax, main): Add a -ks option.
+	* src/tgbatest/ltl2tgba.test, bench/ltlclasses/run,
+	bench/ltlcounter/run: Use -ks instead of -k to speed things up.
+
 2010-12-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Use a cache to speed up tgba_tba_proxy.

bench/ltlclasses/run

@@ -32,7 +32,7 @@ for F in 1 2 3 4 5; do
   echo "# time2 = exploration time"
   echo "# n, states, transitions, user time1, system time1, wall time2, user time1, system time2, wall time2"
   for n in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do
-    $LTL2TGBA -T -r1 -DS -k -f "`"$gen" $F $n`" >out 2>&1
+    $LTL2TGBA -T -r1 -DS -ks -f "`"$gen" $F $n`" >out 2>&1
     states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
     transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
     time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`

bench/ltlcounter/run

 #!/bin/sh
 
-# Copyright (C) 2009 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
 # l'EPITA (LRDE)
 #
 # This file is part of Spot, a model checking library.
@@ -30,7 +30,7 @@ echo "# time1 = translation time"
 echo "# time2 = exploration time"
 echo "# n, states, transitions, user time1, system time1, wall time2, user time1, system time2, wall time2"
 for n in 1 2 3 4 5 6 7 8 9 10 11 12 13; do
-  $LTL2TGBA -T -k -f "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
+  $LTL2TGBA -T -ks -f "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
   states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
   transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
   time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
@@ -44,7 +44,7 @@ echo "# time1 = translation time"
 echo "# time2 = exploration time"
 echo "# n, states, transitions, user time1, system time1, wall time2, user time1, system time2, wall time2"
 for n in 1 2 3 4 5 6 7; do
-  $LTL2TGBA -T -k "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
+  $LTL2TGBA -T -ks "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
   states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
   transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
   time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`

src/tgbatest/ltl2tgba.cc

@@ -243,7 +243,9 @@ syntax(char* prog)
             << std::endl
             << "  -FC   dump the automaton showing future conditions on states"
 	    << std::endl
-	    << "  -k    display statistics on the automaton of dumping it"
+	    << "  -k    display statistics on the automaton (size and SCCs)"
+	    << std::endl
+	    << "  -ks   display statistics on the automaton (size only)"
 	    << std::endl
 	    << "  -K    dump the graph of SCCs in dot format" << std::endl
 	    << "  -KV   verbosely dump the graph of SCCs in dot format"
@@ -467,6 +469,10 @@ main(int argc, char** argv)
 	{
 	  output = 9;
 	}
+      else if (!strcmp(argv[formula_index], "-ks"))
+	{
+	  output = 12;
+	}
       else if (!strcmp(argv[formula_index], "-K"))
 	{
 	  output = 10;
@@ -1067,6 +1073,9 @@ main(int argc, char** argv)
 	    case 11:
 	      dump_scc_dot(a, std::cout, true);
 	      break;
+	    case 12:
+	      stats_reachable(a).dump(std::cout);
+	      break;
 	    default:
 	      assert(!"unknown output option");
 	    }

src/tgbatest/ltl2tgba.test

@@ -55,7 +55,7 @@ check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
 # Make sure 'a U (b U c)' has 3 states and 6 transitions,
 # before and after degeneralization.
 for opt in '' -D -DS; do
-  ../ltl2tgba -k -f -R3 $opt 'a U (b U c)' > stdout
+  ../ltl2tgba -ks -f -R3 $opt 'a U (b U c)' > stdout
   grep 'transitions: 6$' stdout
   grep 'states: 3$' stdout
 done
@@ -63,7 +63,7 @@ done
 # Make sure '!(Ga U b)' has 3 states and 6 transitions,
 # before and after degeneralization.
 for opt in '' -D -DS; do
-  ../ltl2tgba -k -f -R3 $opt '!(Ga U b)' > stdout
+  ../ltl2tgba -ks -f -R3 $opt '!(Ga U b)' > stdout
   grep 'transitions: 6$' stdout
   grep 'states: 3$' stdout
 done
@@ -71,7 +71,7 @@ done
 # Make sure 'Ga U b' has 4 states and 6 transitions,
 # before and after degeneralization.
 for opt in '' -D -DS; do
-  ../ltl2tgba -k -f -R3 $opt 'Ga U b' > stdout
+  ../ltl2tgba -ks -f -R3 $opt 'Ga U b' > stdout
   grep 'transitions: 6$' stdout
   grep 'states: 4$' stdout
 done
@@ -80,12 +80,12 @@ done
 # has 6 states and 15 transitions, before and after degeneralization.
 f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
 for opt in '' -D -DS; do
-  ../ltl2tgba -k -f -R3 $opt "$f" > stdout
+  ../ltl2tgba -ks -f -R3 $opt "$f" > stdout
   grep 'transitions: 15$' stdout
   grep 'states: 6$' stdout
 done
 
 # Note: this is worse with -R3f.
-../ltl2tgba -k -f -R3f -DS "$f" > stdout
+../ltl2tgba -ks -f -R3f -DS "$f" > stdout
 grep 'transitions: 17$' stdout
 grep 'states: 7$' stdout