From 97f178aee55168667ccc6a537d6219db9de33300 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 23 Apr 2004 15:02:24 +0000
Subject: [PATCH] - By default, a state progress counter is displayed on
 stderr.

---
 src/main.c         | 16 +++++++++-------
 src/modelchecker.c |  8 ++++++--
 src/todo.txt       | 10 +---------
 3 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/src/main.c b/src/main.c
index d4bd1c8..4b4a045 100644
--- a/src/main.c
+++ b/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,
-				      "report total number of states and claims traversed.");
-  // struct arg_file *outfile = arg_file0("o",NULL,"<output>",            "output file (default is \"-\")");
+  struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "surpress progress bar.");
 #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)
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 4f8c5e1..37b2225 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -167,8 +167,12 @@ executeStep (const System sys, const int run)
     {
       if (sys->statesLow % (long int) sys->switchS == 0)
 	{
-	  indent ();
-	  statesPrint (sys);
+	  fprintf (stderr, "States ");
+	  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;
diff --git a/src/todo.txt b/src/todo.txt
index 6349d5b..7cc5a16 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -1,11 +1,4 @@
-- Remove stupid preamble postamble stuff, or maybe integrate this behaviour
-  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.
+- Implement run knowledge, and use this in protocol compiler.
 - 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.