- Added --claims flag for some detailed output on claim violations.

src/main.c

@@ -113,6 +113,7 @@ main (int argc, char **argv)
   struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions");
   struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions");
   struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
+  struct arg_lit *switch_claims = arg_lit0 (NULL, "claims", "show claims report");
 #ifdef DEBUG
   struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter");
   struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent",
@@ -132,6 +133,7 @@ main (int argc, char **argv)
     switch_scenario,
     switch_latex_output,
     switch_progress_bar, 
+    switch_claims,
 
     switch_traversal_method, 
     switch_match_method, 
@@ -323,6 +325,8 @@ main (int argc, char **argv)
       sys->switchNomoreClaims = 0;	/* disable no more claims cutter */
   if (switch_disable_endgame_reductions->count > 0)
       sys->switchReduceEndgame = 0;	/* disable endgame cutter */
+  if (switch_claims->count > 0)
+      sys->switchClaims = 1;		/* claims report */
 
   /*
    * The scenario selector has an important side effect; when it is non-null,
@@ -613,7 +617,13 @@ timersPrint (const System sys)
   fprintf (stderr, "\n");
 #endif
 
-  /* print also individual claims */
+  if (sys->switchClaims)
+    {
+      /* Print also individual claims */
+      /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing)
+       */
+      if (sys->output != EMPTY)
+          globalError++;
       cl_scan = sys->claimlist;
       anyclaims = 0;
       while (cl_scan != NULL)
@@ -624,20 +634,34 @@ timersPrint (const System sys)
 	   */
 	  if (!anyclaims)
 	    {
-	  fprintf (stderr, "Claim\tCount\tFailed\n");
+	      eprintf ("Claim\tOccurrences\n");
 	      anyclaims = 1;
 	    }
-      fprintf (stderr, "-\t");
+
+	  termPrint (cl_scan->rolename);
+	  eprintf (":");
+	  termPrint (cl_scan->label);
+	  eprintf ("\t");
 	  statesFormat (stderr, cl_scan->count);
-      fprintf (stderr, "\t");
+	  if (cl_scan->count > 0)
+	    {
+	      eprintf ("\t");
+	      if (cl_scan->failed > 0)
+		{
 		  statesFormat (stderr, cl_scan->failed);
-      fprintf (stderr, "\n");
+		  eprintf (" failed");
+		}
+	    }
+	  eprintf ("\n");
 	  cl_scan = cl_scan->next;
 	}
       if (!anyclaims)
 	{
 	  warning ("No claims in system.");
 	}
+      if (sys->output != EMPTY)
+          globalError--;
+    }
 }
 
 //! Analyse the model by incremental runs.

src/symbol.c

@@ -1,5 +1,6 @@
 #include <stdio.h>
 #include <stdlib.h>
+#include <stdarg.h>
 
 #include "symbol.h"
 #include "memory.h"
@@ -12,6 +13,12 @@
    symbols.h.
 */
 
+/* accessible for externals */
+
+int globalError;		//!< If >0, stdout output goes to stderr (for e.g. terms)
+
+/* external declarations */
+
 extern int yylineno;
 
 /* global declarations */
@@ -35,6 +42,7 @@ symbolsInit (void)
     symbtab[i] = NULL;
   symb_list = NULL;
   symb_alloc = NULL;
+  globalError = 0;
 }
 
 //! Close symbols code.
@@ -145,7 +153,7 @@ symbolPrint (Symbol s)
     return;
 
   /* TODO maybe action depending on type? */
-  printf ("%s", s->text);
+  eprintf ("%s", s->text);
 }
 
 //! Insert a string into the symbol table, if it wasn't there yet.
@@ -168,3 +176,21 @@ symbolSysConst (char *str)
     }
   return symb;
 }
+
+//! Print out according to globalError
+/**
+ * Input is comparable to printf, only depends on globalError. This should be used by any function trying to do output.
+ *\sa globalError
+ */
+void
+eprintf (char *fmt, ... )
+{
+  va_list args;
+
+  va_start (args, fmt);
+  if (globalError == 0)
+  	vfprintf (stdout, fmt, args);
+  else
+  	vfprintf (stderr, fmt, args);
+  va_end (args);
+}

src/symbol.h

@@ -40,4 +40,8 @@ Symbol lookup (char *s);
 void symbolPrint (Symbol s);
 Symbol symbolSysConst (char *str);
 
+void eprintf (char *fmt, ... );
+
+extern int globalError;
+
 #endif

src/system.c

@@ -65,6 +65,7 @@ systemInit ()
   sys->switchSymmOrder = 0;	// don't force symmetry order reduction by default
   sys->switchNomoreClaims = 1;	// default cutter when there are no more claims
   sys->switchReduceEndgame = 1;	// default cutter of last events in a trace
+  sys->switchClaims = 0;	// default don't report on claims
 
   /* set illegal traversal by default, to make sure it is set
      later */

src/system.h

@@ -128,6 +128,7 @@ struct system
   int switchSymmOrder;		//!< Enable symmetry order reduction
   int switchNomoreClaims;	//!< Enable no more claims cutter
   int switchReduceEndgame;	//!< Enable endgame cutter
+  int switchClaims;		//!< Enable clails report
 
   //! Latex output switch.
   /**

src/term.c

@@ -19,7 +19,6 @@
 #include "memory.h"
 #include "ctype.h"
 
-
 /* external definitions */
 
 extern Term TERM_Function;
@@ -285,7 +284,7 @@ termPrint (Term term)
 {
   if (term == NULL)
     {
-      printf ("Empty term");
+      eprintf ("Empty term");
       return;
     }
 #ifdef DEBUG
@@ -300,28 +299,28 @@ termPrint (Term term)
     {
       symbolPrint (term->left.symb);
       if (realTermVariable (term))
-	printf ("V");
+	eprintf ("V");
       if (term->right.runid >= 0)
 	{
-	  if (globalLatex)
+	  if (globalLatex && globalError == 0)
-	    printf ("\\sharp%i", term->right.runid);
+	    eprintf ("\\sharp%i", term->right.runid);
 	  else
-	    printf ("#%i", term->right.runid);
+	    eprintf ("#%i", term->right.runid);
 	}
       if (term->subst != NULL)
 	{
 	  if (globalLatex)
-	    printf ("\\rightarrow");
+	    eprintf ("\\rightarrow");
 	  else
-	    printf ("->");
+	    eprintf ("->");
 	  termPrint (term->subst);
 	}
     }
   if (realTermTuple (term))
     {
-      printf ("(");
+      eprintf ("(");
       termTuplePrint(term);
-      printf (")");
+      eprintf (")");
       return;
     }
   if (realTermEncrypt (term))
@@ -331,26 +330,26 @@ termPrint (Term term)
 	{
 	  /* function application */
 	  termPrint (term->right.key);
-	  printf ("(");
+	  eprintf ("(");
 	  termTuplePrint (term->left.op);
-	  printf (")");
+	  eprintf (")");
 	}
       else
 	{
 	  /* normal encryption */
 	  if (globalLatex)
 	    {
-	      printf ("\\{");
+	      eprintf ("\\{");
 	      termTuplePrint (term->left.op);
-	      printf ("\\}_{");
+	      eprintf ("\\}_{");
 	      termPrint (term->right.key);
-	      printf ("}");
+	      eprintf ("}");
 	    }
 	  else
 	    {
-	      printf ("{");
+	      eprintf ("{");
 	      termTuplePrint (term->left.op);
-	      printf ("}");
+	      eprintf ("}");
 	      termPrint (term->right.key);
 	    }
 	}
@@ -368,7 +367,7 @@ termTuplePrint (Term term)
 {
   if (term == NULL)
     {
-      printf ("Empty term");
+      eprintf ("Empty term");
       return;
     }
   term = deVar(term);
@@ -376,7 +375,7 @@ termTuplePrint (Term term)
     {
       // To remove any brackets, change this into termTuplePrint.
       termPrint (term->left.op1);
-      printf (",");
+      eprintf (",");
       term = deVar(term->right.op2);
     }
   termPrint(term);

src/termlist.c

@@ -352,18 +352,18 @@ termlistPrint (Termlist tl)
 {
   if (tl == NULL)
     {
-      printf ("[Empty]");
+      eprintf ("[Empty]");
       return;
     }
-  printf ("[");
+  eprintf ("[");
   while (tl != NULL)
     {
       termPrint (tl->term);
       tl = tl->next;
       if (tl != NULL)
-	  printf(", ");
+	  eprintf(", ");
     }
-  printf ("]");
+  eprintf ("]");
 }
 
 //! Append all open variables in a term to a list.