From 7b6626d176153b1ee5146694e94fa487cc11660d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 25 May 2015 17:41:02 +0200
Subject: [PATCH] ltlcross: add a complete column

* src/bin/ltlcross.cc: Add the column.
* NEWS: Update.
---
 NEWS                | 22 +++++++++++++---------
 src/bin/ltlcross.cc | 10 +++++++---
 2 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/NEWS b/NEWS
index fbf894e08..036537e57 100644
--- a/NEWS
+++ b/NEWS
@@ -91,17 +91,21 @@ New in spot 1.99b (not yet released)
       So it can effectively be used to validate tools producing Rabin
       or Streett automata.
 
-    - ltlcross has a new option --grind, that attempts to reduce the
-      size of any bogus formula it discovers, while still exhibiting
-      the bug.
+    - ltlcross has several new options:
 
-    - ltlcross has a new option --ignore-execution-failures that
-      ignore translator returning non-zero exist status instead of
-      returning an error.
+        --grind attempts to reduce the size of any bogus formula it
+        discovers, while still exhibiting the bug.
 
-    - ltlcross has a new option --automata to save the produced
-      automata into the CSV or JSON file.  Those automata are saved
-      into the HOA format.
+        --ignore-execution-failures that ignores translators returning
+        non-zero exist status instead of returning an error.
+
+	--automata save the produced automata into the CSV or JSON
+        file.  Those automata are saved into the HOA format.
+
+      ltlcross will also output two extra columns in its CSV/JSON
+      output: "ambiguous_aut" and "complete_aut" are Boolean
+      that respectively tells whether the automaton is
+      ambiguous and complete.
 
     - "ltlfilt --stutter-invariant" will now work with PSL formulas.
       The implementation is actually much more efficient
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 69cb3abb0..b8049e813 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -300,6 +300,7 @@ struct statistics
   std::vector<double> product_transitions;
   std::vector<double> product_scc;
   bool ambiguous;
+  bool complete;
   std::string hoa_str;
 
   static void
@@ -325,7 +326,8 @@ struct statistics
 	   "\"terminal_aut\","
 	   "\"weak_aut\","
 	   "\"strong_aut\","
-	   "\"ambiguous_aut\"");
+	   "\"ambiguous_aut\","
+	   "\"complete_aut\"");
     size_t m = products_avg ? 1U : products;
     for (size_t i = 0; i < m; ++i)
       os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
@@ -366,7 +368,8 @@ struct statistics
 	   << terminal_aut << ','
 	   << weak_aut << ','
 	   << strong_aut << ','
-	   << ambiguous;
+	   << ambiguous << ','
+	   << complete;
 	if (!products_avg)
 	  {
 	    for (size_t i = 0; i < products; ++i)
@@ -394,7 +397,7 @@ struct statistics
       {
 	size_t m = products_avg ? 1U : products;
 	m *= 3;
-	m += 14 + show_sr * 6;
+	m += 15 + show_sr * 6;
 	os << na;
 	for (size_t i = 0; i < m; ++i)
 	  os << ',' << na;
@@ -715,6 +718,7 @@ namespace
 	      else
 		st->terminal_aut = true;
 	      st->ambiguous = !spot::is_unambiguous(res);
+	      st->complete = spot::is_complete(res);
 
 	      if (opt_automata)
 		{