[lbtt] Count deterministic automata and deterministic states.

* src/BuchiAutomaton.h, src/BuchiAutomaton.cc
(BuchiState::isDeterministic, BuchiAutomaton::isDeterministic,
BuchiAutomaton::nondeterminismIndex): New methods.
* src/TestOperations.cc (generateBuchiAutomaton): Collect
nondeterminism indices, and count deterministic automata.
* src/TestStatistics.cc, src/TestStatistics.h: Add storage
for these statistics.
* src/StatDisplay.cc (printBuchiAutomatonStats,
printCollectiveStats): Display these statistics.

lbtt/ChangeLog

@@ -1,3 +1,17 @@
+2012-05-21  Tomáš Babiak  <xbabiak@fi.muni.cz>
+
+	Count deterministic automata and deterministic states.
+
+	* src/BuchiAutomaton.h, src/BuchiAutomaton.cc
+	(BuchiState::isDeterministic, BuchiAutomaton::isDeterministic,
+	BuchiAutomaton::nondeterminismIndex): New methods.
+	* src/TestOperations.cc (generateBuchiAutomaton): Collect
+	nondeterminism indices, and count deterministic automata.
+	* src/TestStatistics.cc, src/TestStatistics.h: Add storage
+	for these statistics.
+	* src/StatDisplay.cc (printBuchiAutomatonStats,
+	printCollectiveStats): Display these statistics.
+
 2012-04-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* doc/gpl.texi: Fix make pdf for newer texinfo.tex.
@@ -336,7 +350,7 @@
 	* src/Product.h, src/SccCollection.h: New files.
 	* src/BuchiProduct.h, src/BuchiProduct.cc, src/StateSpaceProduct.h:
 	New files for providing specializations of the general product
-	computation operation applicable to Büchi automata and state
+	computation operation applicable to Büchi automata and state
 	spaces.
 
 	* src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc,
@@ -381,7 +395,7 @@
 	Product interface for constructing the product and checking
 	it for emptiness.
 	(performBuchiIntersectionCheck): Use the Product interface
-	for constructing the intersection of Büchi automata and
+	for constructing the intersection of Büchi automata and
 	checking it for emptiness.
 
 	* src/UserCommandReader.cc: Do not include the
@@ -412,12 +426,12 @@
 	analyzing a witness for the nonemptiness of a product automaton.
 	(printAutomatonAnalysisResults): Use the Product interface
 	for constructing and analyzing a witness for the nonemptiness
-	of the intersection of two Büchi automata.
+	of the intersection of two Büchi automata.
 	(printPath): Update parameter list and documentation.  Standardize
 	the output to resemble that produced by printAcceptingCycle.
 	(printAcceptingCycle): Update parameter list and documentation.
 	Display all relevant information about an accepting execution
-	of a Büchi automaton.
+	of a Büchi automaton.
 
 2004-05-18  Heikki Tauriainen  <heikki.tauriainen@hut.fi>
 
@@ -1053,7 +1067,7 @@
 2003-07-18  Heikki Tauriainen  <heikki.tauriainen@hut.fi>
 
 	* UserCommands.cc (printAutomatonAnalysisResults): Ensure that
-	the states in a witness for the nonemptiness of two Bûchi
+	the states in a witness for the nonemptiness of two Bûchi
 	automata are distinct to prevent the truth valuation for the
 	atomic propositions from being defined multiple times in any
 	state of the witness.

lbtt/src/BuchiAutomaton.cc

@@ -214,7 +214,7 @@ void BuchiAutomaton::read(istream& input_stream)
 
   clear();
 
-  try 
+  try
   {
     /* Read the number of states in the generalized Büchi automaton. */
 
@@ -271,7 +271,7 @@ void BuchiAutomaton::read(istream& input_stream)
       acceptance_sets_on_states = true;
       acceptance_sets_on_transitions = false;
     }
-      
+
     BitArray acc_sets(number_of_acceptance_sets);
 
     /*
@@ -358,7 +358,7 @@ void BuchiAutomaton::read(istream& input_stream)
         state_mapping.second++;
       }
 
-      /* 
+      /*
        *  Check whether the current state is an initial state. (There must be
        *  exactly one initial state.)
        */
@@ -506,7 +506,7 @@ void BuchiAutomaton::read(istream& input_stream)
 
     if (!initial_state_fixed)
       throw AutomatonParseException("no initial state specified");
-    
+
     if (number_of_processed_states != number_of_states)
       throw AutomatonParseException("incomplete automaton definition");
   }
@@ -535,7 +535,7 @@ void BuchiAutomaton::print
  * Arguments:     stream  --  A reference to an output stream.
  *                indent  --  Number of spaces to leave to the left of output.
  *                fmt     --  Determines the format of the output.
- * 
+ *
  * Returns:       Nothing.
  *
  * ------------------------------------------------------------------------- */
@@ -641,7 +641,85 @@ void BuchiAutomaton::print
   estream.flush();
 }
 
+/* ========================================================================= */
+bool BuchiAutomaton::BuchiState::isDeterministic() const
+/* ----------------------------------------------------------------------------
+ *
+ * Description:   Checks whether there is any nondeterminism
+ *                on the outgoing transitions.
+ *
+ * Arguments:     None.
+ *
+ * Returns:       True iff the state is deterministic.
+ *
+ * ------------------------------------------------------------------------- */
+{
+  size_type size = edges().size();
 
+  if (size <= 1)
+    return true;
+
+  for (int i = 0; i < size - 1; i++)
+  {
+    for (int j = i + 1; j < size; j++)
+    {
+      Ltl::LtlFormula *f =
+	&Ltl::And::construct((static_cast<BuchiTransition*> (edges()[i]))->guard(),
+			     (static_cast<BuchiTransition*> (edges()[j]))->guard());
+      if (f->satisfiable())
+      {
+	Ltl::LtlFormula::destruct(f);
+	return false;
+      }
+      else
+      {
+	Ltl::LtlFormula::destruct(f);
+      }
+    }
+  }
+  return true;
+}
+
+/* ========================================================================= */
+bool BuchiAutomaton::isDeterministic() const
+/* ----------------------------------------------------------------------------
+ *
+ * Description:   Checks whether the automaton is deterministic.
+ *
+ * Arguments:     None.
+ *
+ * Returns:       True iff the automaton is deterministic.
+ *
+ * ------------------------------------------------------------------------- */
+{
+  unsigned long int index = 0;
+  vector<Node*>::const_iterator node;
+  for (node = nodes.begin(); node != nodes.end(); ++node)
+    if (!(static_cast<BuchiState*>(*node))->isDeterministic())
+      return false;
+  return true;
+}
+
+/* ========================================================================= */
+unsigned long int BuchiAutomaton::nondeterminismIndex() const
+/* ----------------------------------------------------------------------------
+ *
+ * Description:   Computes the nondeterminism index for the automaton.
+ *                I.e., the number for nondeterministic states.
+ *
+ * Arguments:     None.
+ *
+ * Returns:       Nondeterminism index.
+ *
+ * ------------------------------------------------------------------------- */
+{
+  unsigned long int index = 0;
+  vector<Node*>::const_iterator node;
+  for (node = nodes.begin(); node != nodes.end(); ++node)
+    if (!(static_cast<BuchiState*>(*node))->isDeterministic())
+      index++;
+  return index;
+}
 
 /******************************************************************************
  *
@@ -753,7 +831,7 @@ void BuchiAutomaton::BuchiState::print
  *                number_of_acceptance_sets  --  Number of acceptance sets in
  *                                               the automaton in which the
  *                                               state belongs.
- * 
+ *
  * Returns:       Nothing.
  *
  * ------------------------------------------------------------------------ */

lbtt/src/BuchiAutomaton.h

@@ -69,10 +69,10 @@ public:
     ~BuchiState();                                  /* Destructor. */
 
     /* `edges' inherited from Graph<GraphEdgeContainer>::Node */
-    
+
     BitArray& acceptanceSets();                     /* Tell the acceptance  */
     const BitArray& acceptanceSets() const;         /* status of the state. */
-    
+
     void print                                      /* Writes information   */
       (ostream& stream,                             /* about the state to a */
        const int indent,                            /* stream.              */
@@ -84,7 +84,12 @@ public:
        const GraphOutputFormat fmt,
        const unsigned long int
          number_of_acceptance_sets)
-      const;     
+      const;
+
+    bool isDeterministic() const;     		    /* Checks wheter there is
+						     * any nondeterminism on
+						     * outgoing transitions.
+						     */
 
   private:
     BuchiState(const BuchiState&);                  /* Prevent copying and */
@@ -182,6 +187,13 @@ public:
                                                      * (determined by the
                                                      * `fmt' argument).
 						     */
+  bool isDeterministic() const;                     /* Checks whether
+                                                     * the automaton
+                                                     * is deterministic.
+						     */
+  unsigned long int nondeterminismIndex() const;    /* Computes the
+                                                     * nondeterminism index.
+						     */
 
   /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
@@ -225,7 +237,7 @@ public:
   ~BuchiTransition();                               /* Destructor. */
 
   /* `targetNode' inherited from Graph<GraphEdgeContainer>::Edge */
-    
+
   bool enabled                                      /* These functions test */
     (const BitArray& truth_assignment,              /* whether the          */
      const unsigned long int assignment_size)       /* transition is        */
@@ -249,7 +261,7 @@ public:
     (ostream& stream,                               /* about the transition */
      const int indent,                              /* (as a plain graph    */
      const GraphOutputFormat fmt) const;            /* edge) to a stream.   */
-    
+
   void print                                        /* Writes information   */
     (ostream& stream,                               /* about the transition */
      const int indent,                              /* to a stream in       */
@@ -534,7 +546,7 @@ inline BuchiAutomaton::BuchiTransition::BuchiTransition
  * Description:   Constructor for class BuchiAutomaton::BuchiTransition.
  *                Initializes a new transition to a BuchiState, guarded by an
  *                LtlFormula (which is actually a propositional formula).
- *                
+ *
  * Arguments:     target    --  Identifier of the target state of the
  *                              automaton.
  *                formula   --  A pointer to a propositional formula guarding
@@ -553,7 +565,7 @@ inline BuchiAutomaton::BuchiTransition::BuchiTransition
 /* ========================================================================= */
 inline BuchiAutomaton::BuchiTransition::~BuchiTransition()
 /* ----------------------------------------------------------------------------
- * 
+ *
  * Description:   Destructor for class BuchiAutomaton::BuchiTransition.
  *
  * Arguments:     None.
@@ -651,7 +663,7 @@ inline bool BuchiAutomaton::BuchiTransition::enabled
  *                the truth assignment.
  *
  * ------------------------------------------------------------------------- */
-{ 
+{
   return guard_formula->evaluate(truth_assignment, assignment_size);
 }
 
@@ -670,7 +682,7 @@ inline bool BuchiAutomaton::BuchiTransition::enabled
  *                the truth assignment.
  *
  * ------------------------------------------------------------------------- */
-{ 
+{
   return enabled(truth_assignment, truth_assignment.capacity());
 }
 
@@ -754,7 +766,7 @@ inline void BuchiAutomaton::BuchiTransition::print
 
 /* ========================================================================= */
 inline BuchiAutomaton::BuchiState::BuchiState
-  (const unsigned long int num_of_acceptance_sets) : 
+  (const unsigned long int num_of_acceptance_sets) :
   Node(), acceptance_sets(num_of_acceptance_sets)
 /* ----------------------------------------------------------------------------
  *
@@ -867,7 +879,7 @@ inline BuchiAutomaton::AutomatonParseException::AutomatonParseException
  *                         error message.
  *
  * Returns:       Nothing.
- * 
+ *
  * ------------------------------------------------------------------------- */
 {
 }

lbtt/src/StatDisplay.cc

@@ -26,6 +26,7 @@
 #include "StatDisplay.h"
 #include "StringUtil.h"
 #include "TestRoundInfo.h"
+#include "Graph.h"
 
 namespace StatDisplay
 {
@@ -101,13 +102,13 @@ void printBuchiAutomatonStats
 {
   Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
 
-  const AutomatonStats& automaton_stats = 
+  const AutomatonStats& automaton_stats =
     test_results[algorithm].automaton_stats[result_id];
 
   if (configuration.global_options.verbosity <= 2)
   {
     if (!automaton_stats.buchiAutomatonComputed())
-      estream << "      N/A       N/A       N/A  N/A";
+      estream << "      N/A       N/A       N/A  N/A       N/A";
     else
     {
       if (automaton_stats.buchi_generation_time >= 0.0)
@@ -130,6 +131,9 @@ void printBuchiAutomatonStats
       changeStreamFormatting(stream, 4, 0, ios::right);
       estream << automaton_stats.number_of_acceptance_sets;
       restoreStreamFormatting(stream);
+      changeStreamFormatting(stream, 9, 0, ios::right);
+      estream << automaton_stats.nondeterminism_index;
+      restoreStreamFormatting(stream);
     }
     estream << ' ';
   }
@@ -148,9 +152,14 @@ void printBuchiAutomatonStats
                  + '\n' + string(indent, ' ') + "acceptance sets:"
                  + string(7, ' ')
                  + toString(automaton_stats.number_of_acceptance_sets)
+                 + '\n' + string(indent, ' ') + "is deterministic:"
+                 + string(6, ' ')
+                 + (automaton_stats.is_deterministic?"Yes":"No")
+                 + '\n' + string(indent, ' ') + "nondeterminism index:  "
+                 + toString(automaton_stats.nondeterminism_index)
                  + '\n' + string(indent, ' ') + "computation time:"
                  + string(6, ' ');
-    
+
       if (automaton_stats.buchi_generation_time != -1.0)
       {
 	changeStreamFormatting(stream, 9, 2, ios::fixed | ios::left);
@@ -595,7 +604,7 @@ void printBuchiIntersectionCheckStats
 	    }
 	    else
 	      estream << "    ";
-	      
+
 	    estream << ' ' + configuration.algorithmString(*alg_1);
 
 	    if (*alg_1 != alg_2)
@@ -621,7 +630,7 @@ void printBuchiIntersectionCheckStats
   estream << "\n";
   estream.flush();
 }
- 
+
 /* ========================================================================= */
 void printAllStats
   (ostream& stream, int indent,
@@ -723,7 +732,7 @@ void printCollectiveCrossComparisonStats
  * Returns:       Nothing.
  *
  * ------------------------------------------------------------------------- */
-{        
+{
   Exceptional_ostream estream(&stream, ios::failbit | ios::badbit);
 
   estream << ' ';
@@ -783,11 +792,11 @@ void printCollectiveCrossComparisonStats
       changeStreamFormatting(stream, 0, 2, ios::fixed);
       estream << percentage;
       restoreStreamFormatting(stream);
-      
+
       estream << "%)";
 
       if (percentage < 100.0)
-	estream << ' ';    
+	estream << ' ';
       if (percentage < 10.0)
 	estream << ' ';
     }
@@ -1015,7 +1024,7 @@ void printCollectiveStats(ostream& stream, int indent)
                    + '\n';
 	symbol_name_string = symbol_number_string = symbol_distribution_string
 	  = "";
-      }	
+      }
       else
       {
 	symbol_name_string += string(12 - name_string.length(), ' ');
@@ -1089,6 +1098,8 @@ void printCollectiveStats(ostream& stream, int indent)
           unsigned long int number_of_successful_instances;
           BIGUINT total_number_of_states;
           BIGUINT total_number_of_transitions;
+          BIGUINT total_nondeterminism_index;
+          int total_deterministic_count;
 
           const TestStatistics& stats = final_statistics[algorithm];
 
@@ -1243,14 +1254,18 @@ void printCollectiveStats(ostream& stream, int indent)
 	      double buchi_generation_time;
 
 	      estream << '\n' + string(22 + indent, ' ')
-                         + "|    Number of    |  Time consumed  |\n"
+                         + "|    Number of    |  Time consumed  |"
+                         + "    Number of    | Nondeterminism |\n"
 		         + string(22 + indent, ' ')
-                         + "| acceptance sets |    (seconds)    |\n"
+                         + "| acceptance sets |    (seconds)    |"
+	                     + "   determ. aut   |     index      |\n"
 		         + string(7 + indent, ' ') + string(15, '-') + '+';
 
-	      for (int j = 0; j < 2; j++)
+	      for (int j = 0; j < 3; j++)
 		estream << string(17, '-') + '+';
 
+		estream << string(16, '-') + '+';
+
 	      for (int j = 0; j < 3; j++)
 	      {
 		estream << '\n' + string(8 + indent, ' ');
@@ -1273,6 +1288,10 @@ void printCollectiveStats(ostream& stream, int indent)
 		  buchi_generation_time = stats.total_buchi_generation_time[j];
 		  total_number_of_acceptance_sets
 		    = stats.total_number_of_acceptance_sets[j];
+		  total_deterministic_count
+		  	= stats.total_deterministic_count[j];
+		  total_nondeterminism_index
+		    = stats.total_nondeterminism_index[j];
 		}
 		else
 		{
@@ -1292,6 +1311,12 @@ void printCollectiveStats(ostream& stream, int indent)
 		  total_number_of_acceptance_sets
 		    = stats.total_number_of_acceptance_sets[0]
 		      + stats.total_number_of_acceptance_sets[1];
+		  total_deterministic_count
+		  	= stats.total_deterministic_count[0]
+		  	  + stats.total_deterministic_count[1];
+		  total_nondeterminism_index
+		    = stats.total_nondeterminism_index[0]
+		      + stats.total_nondeterminism_index[1];
 		}
 
 		number_of_successful_instances =
@@ -1331,6 +1356,40 @@ void printCollectiveStats(ostream& stream, int indent)
 		    restoreStreamFormatting(stream);
 		  }
 
+		  estream << " | ";
+
+		  if (number_of_successful_instances == 0)
+		    estream << string(15, ' ');
+		  else
+		  {
+		    changeStreamFormatting(stream, 15, 2,
+					   ios::fixed | ios::right);
+		    if (z == 0)
+		      estream << total_deterministic_count;
+		    else
+		      estream << total_deterministic_count
+			           / static_cast<double>
+			               (number_of_successful_instances);
+		    restoreStreamFormatting(stream);
+		  }
+
+		  estream << " | ";
+
+		  if (number_of_successful_instances == 0)
+		    estream << string(14, ' ');
+		  else
+		  {
+		    changeStreamFormatting(stream, 14, 2,
+					   ios::fixed | ios::right);
+		    if (z == 0)
+		      estream << total_nondeterminism_index;
+		    else
+		      estream << total_nondeterminism_index
+			           / static_cast<double>
+			               (number_of_successful_instances);
+		    restoreStreamFormatting(stream);
+		  }
+
 		  estream << " |";
 		  if (z == 0)
 		    estream << '\n' + string(indent + 15, ' ') + "(avg.) | ";
@@ -1343,7 +1402,7 @@ void printCollectiveStats(ostream& stream, int indent)
 
 	  if (algorithm + 1 < round_info.number_of_translators)
 	    estream << '\n';
-        
+
           break;
         }
 

lbtt/src/TestOperations.cc

@@ -1336,6 +1336,10 @@ void generateBuchiAutomaton
     automaton_stats.number_of_buchi_transitions = buchi_stats.second;
     automaton_stats.number_of_acceptance_sets
       = automaton_stats.buchi_automaton->numberOfAcceptanceSets();
+	automaton_stats.nondeterminism_index
+	  = automaton_stats.buchi_automaton->nondeterminismIndex();
+	automaton_stats.is_deterministic
+	  = automaton_stats.buchi_automaton->isDeterministic();
 
     /*
      *  Update Büchi automaton statistics for the given algorithm.
@@ -1347,6 +1351,10 @@ void generateBuchiAutomaton
       += automaton_stats.number_of_buchi_transitions;
     final_statistics[algorithm_id].total_number_of_acceptance_sets[f]
       += automaton_stats.number_of_acceptance_sets;
+    final_statistics[algorithm_id].total_nondeterminism_index[f]
+      += automaton_stats.nondeterminism_index;
+    if (automaton_stats.is_deterministic)
+    	final_statistics[algorithm_id].total_deterministic_count[f]++;
 
     if (final_statistics[algorithm_id].total_buchi_generation_time[f] < 0.0
 	|| automaton_stats.buchi_generation_time < 0.0)

lbtt/src/TestStatistics.cc

@@ -84,6 +84,7 @@ void AlgorithmTestResults::fullReset()
     automaton_stats[i].number_of_buchi_transitions = 0;
     automaton_stats[i].number_of_acceptance_sets = 0;
     automaton_stats[i].number_of_msccs = 0;
+    automaton_stats[i].nondeterminism_index = 0;
     automaton_stats[i].buchi_generation_time = 0.0;
     
     for (vector<int>::iterator it

lbtt/src/TestStatistics.h

@@ -102,6 +102,13 @@ struct AutomatonStats
                                                      * automaton.
                                                      */
 
+  unsigned long int nondeterminism_index;           /* Nondeterminism index
+                                                     */
+
+  bool is_deterministic;                            /* True if the automaton
+                                                     * is deterministic
+                                                     */
+
   double buchi_generation_time;                     /* Time used to generate a
                                                      * Büchi automaton.
 						     */
@@ -284,6 +291,14 @@ struct TestStatistics
 						     * automata.
 						     */
 
+  BIGUINT total_nondeterminism_index[2];            /* Total nondetereminism
+                                                     * index for all the
+                                                     * generated Büchi automata.
+                                                     */
+  int total_deterministic_count[2];                 /* Total number of
+                                                     * deterministic automata
+                                                     */
+
   double total_buchi_generation_time[2];            /* Total time used when
                                                      * generating Büchi
                                                      * automata.
@@ -349,10 +364,10 @@ struct TestStatistics
 inline AutomatonStats::AutomatonStats
   (vector<Configuration::AlgorithmInformation>::size_type number_of_algorithms,
    StateSpace::size_type max_statespace_size) :
-  buchi_automaton(0), number_of_buchi_states(0),
+  buchi_automaton(0), number_of_buchi_states(0), nondeterminism_index(0),
   number_of_buchi_transitions(0), number_of_acceptance_sets(0),
   number_of_msccs(0), buchi_generation_time(0.0), number_of_product_states(0),
-  number_of_product_transitions(1),
+  number_of_product_transitions(1), is_deterministic(false),
   emptiness_check_result(max_statespace_size),
   emptiness_check_performed(false),
   cross_comparison_stats(number_of_algorithms, make_pair(false, 0)),
@@ -541,6 +556,8 @@ inline TestStatistics::TestStatistics
     total_number_of_buchi_states[i] = 0;
     total_number_of_buchi_transitions[i] = 0;
     total_number_of_acceptance_sets[i] = 0;
+    total_nondeterminism_index[i] = 0;
+    total_deterministic_count[i] = 0;
     total_number_of_product_states[i] = 0;
     total_number_of_product_transitions[i] = 0;
     total_buchi_generation_time[i] = 0.0;