- By default, a state progress counter is displayed on stderr.

src/main.c

@@ -56,9 +56,7 @@ main (int argc, char **argv)
   struct arg_lit *latex = arg_lit0 (NULL, "latex", "output in LaTeX format.");
   struct arg_lit *noreport =
     arg_lit0 ("d", "disable-report", "don't report violations.");
-  struct arg_int *switchS = arg_int0 ("s", "states", NULL,
+  struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "surpress progress bar.");
-				      "report total number of states and claims traversed.");
-  // struct arg_file *outfile = arg_file0("o",NULL,"<output>",            "output file (default is \"-\")");
 #ifdef DEBUG
   struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
   struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
@@ -113,7 +111,6 @@ main (int argc, char **argv)
   maxlength->ival[0] = -1;
   maxruns->ival[0] = INT_MAX;
   prune->ival[0] = 2;
-  switchS->ival[0] = 0;
 
   /* Parse the command line as defined by argtable[] */
   nerrors = arg_parse (argc, argv, argtable);
@@ -185,7 +182,7 @@ main (int argc, char **argv)
       /* try to open */
       if (!freopen (outfile->filename[0], "w", stdout))
         {
-          printf("Error at stdout reopen to '%s'.\n", outfile->filename[0]);
+          printf("Could not create output file '%s'.\n", outfile->filename[0]);
           exit(1);
         }
     }
@@ -197,7 +194,7 @@ main (int argc, char **argv)
 	{
           if (!freopen (infile->filename[0], "r", stdin))
 	    {
-	      printf("Error at stdin reopen from '%s'.\n", infile->filename[0]);
+	      printf("Could not open input file '%s'.\n", infile->filename[0]);
 	      exit(1);
 	    }
 	}
@@ -279,7 +276,12 @@ main (int argc, char **argv)
   sys->traverse = traversal->ival[0];
   sys->match = match->ival[0];
   sys->prune = prune->ival[0];
-  sys->switchS = switchS->ival[0];
+  if (switchS->count > 0)
+      /* disable progress display */
+      sys->switchS = 0;
+  else
+      /* enable progress display */
+      sys->switchS = 10000;
 
   /* TODO for now, warning for -m2 and non-clp */
   if (sys->match == 2 && !sys->clp)

src/modelchecker.c

@@ -167,8 +167,12 @@ executeStep (const System sys, const int run)
     {
       if (sys->statesLow % (long int) sys->switchS == 0)
 	{
-	  indent ();
+	  fprintf (stderr, "States ");
-	  statesPrint (sys);
+	  if (sys->statesHigh == 0 && sys->statesLow < 1000000)
+	      fprintf (stderr, "%u", sys->statesLow);
+	  else
+	      fprintf (stderr, "%8.3e", (double) sys->statesLow + (sys->statesHigh * ULONG_MAX));
+	  fprintf (stderr, " \r");
 	}
     }
   return 1;

src/todo.txt

@@ -1,11 +1,4 @@
-- Remove stupid preamble postamble stuff, or maybe integrate this behaviour
+- Implement run knowledge, and use this in protocol compiler.
-  into some switch, where default would be a standalone latex file, and
-  another option would generate a file that can be included.
-- Variables have to be 'saved' and 'stored' into some structure. However, for
-  this we need a global list of all variables, which is not available at the
-  moment. The compiler and run instantiator should maintain such a list, and
-  then we could save it into a struct with three lists. (from,to,empty)
-  This will need a sys allVariables list.
 - Timer output is broken for values e.g. above an hour. Fix or remove
   altogether.
 - ns3 doesn't even reach a claim in --cl and -t8. Check.
@@ -13,7 +6,6 @@
 - CLP: variables in keys must be branched: maybe even in three situations
   (have key and contents, have inverse key and content, nothing)
 - Implement delayed protocol compiler (on run demand only).
-- Implement run knowledge, and use this in protocol compiler.
 - Remove any remaining global variables, if any.
 - When choosing agents for runs (with an initial read), it does not make
   sense to choose untrusted agents.