- Much work on the new states counter abstractions.

src/main.c

@@ -422,7 +422,7 @@ main (int argc, char **argv)
   else
     {
       /* check for no claims */
-      if (sys->failed == 0)
+      if (sys->failed == STATES0)
 	{
           /* mark exit code */
 	  exitcode = 2;
@@ -494,13 +494,13 @@ timersPrint (const System sys)
    * NoClaim      no claims
    */
 
-  if (sys->claims == 0)
+  if (sys->claims == STATES0)
     {
       fprintf (stderr, "NoClaim\t\t");
     }
   else
     {
-      if (sys->failed > 0)
+      if (sys->failed != STATES0)
 	fprintf (stderr, "L:%i\t\t", attackLength(sys->attack));
       else
 	fprintf (stderr, "None\t\t");
@@ -513,9 +513,7 @@ timersPrint (const System sys)
 
   if (seconds > 0)
     {
-      fprintf (stderr, "%.3e\t",
+      fprintf (stderr, "%.3e\t", statesDouble (sys->states) / seconds);
-	      (double) (sys->statesLow +
-			(sys->statesHigh * ULONG_MAX)) / seconds);
     }
   else
     {
@@ -653,13 +651,22 @@ modelCheck (const System sys)
     {
       graphInit (sys);
     }
-  traverse (sys);		// start model checking
+
+  /* modelcheck the system */
+  traverse (sys);
+
+  /* clean up any states display */
+  if (sys->switchS > 0)
+    {
+      fprintf (stderr, "                 \r");
+    }
+
   timersPrint (sys);
   if (sys->switchStatespace)
     {
       graphDone (sys);
     }
-  return (sys->failed);
+  return (sys->failed != STATES0);
 }
 
 

src/modelchecker.c

@@ -171,33 +171,25 @@ executeStep (const System sys, const int run)
     }
 
   /* we will explore this state, so count it. */
-  /* ulong was _not_ enough... */
+  sys->states = statesIncrease (sys->states);
-  if (++sys->statesLow == ULONG_MAX)
-    {
-      sys->statesLow = 0;
-      sys->statesHigh++;
-      /* No test for overflow statesHigh. If stuff gets that fast, then 
-       * I surely hope the max of ulong is set higher in the language def */
-    }
 
   /* show progression */
   if (sys->switchS > 0)
     {
-      if (sys->statesLow % (long int) sys->switchS == 0)
+      sys->interval = statesIncrease (sys->interval);
+      if (!statesSmallerThan (sys->interval, (unsigned long int) sys->switchS))
 	{
+	  sys->interval = STATES0;
 	  fprintf (stderr, "States ");
-	  if (sys->statesHigh == 0 && sys->statesLow < 1000000)
+	  statesFormat (stderr, sys->states);
-	      fprintf (stderr, "%u", sys->statesLow);
-	  else
-	      fprintf (stderr, "%8.3e", (double) sys->statesLow + (sys->statesHigh * ULONG_MAX));
 	  fprintf (stderr, " \r");
 	}
     }
 
   /* store new node numbder */
-  sys->traceNode[sys->step] = sys->statesLow;
+  sys->traceNode[sys->step] = sys->states;
   /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */
-  if (sys->switchStatespace && sys->statesHigh == 0 && sys->statesLow < MAX_GRAPH_STATES)
+  if (sys->switchStatespace && statesSmallerThan (sys->states, MAX_GRAPH_STATES))
     {
       /* display graph */
       graphNode (sys);
@@ -1443,7 +1435,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   flag = 1;
 
   /* Count the violations */
-  sys->failed++;
+  sys->failed = statesIncrease (sys->failed);
 
   /* mark the path in the state graph? */
   if (sys->switchStatespace)
@@ -1563,7 +1555,7 @@ executeTry (const System sys, int run)
 	  /*
 	   * update claim counters
 	   */
-	  sys->claims++;
+	  sys->claims = statesIncrease (sys->claims);
 
 	  /*
 	   * distinguish claim types

src/output.c

@@ -513,7 +513,9 @@ void graphInit (const System sys)
   printf ("\torientation=landscape;\n");
 
   /* start with initial node 0 */
-  printf ("\tn0 [shape=box,label=\"M0: ");
+  printf ("\tn");
+  statesFormat (stdout, STATES0);
+  printf (" [shape=box,label=\"M0: ");
   tl = knowledgeSet (sys->know);
   termlistPrint (tl);
   termlistDelete (tl);
@@ -529,18 +531,20 @@ void graphDone (const System sys)
 void graphNode (const System sys)
 {
   Termlist newtl;
-  unsigned long int thisNode, parentNode;
+  states_t thisNode, parentNode;
   int index;
   Roledef rd;
 
   /* determine node numbers */
   index = sys->step - 1;
   parentNode = sys->traceNode[index];
-  thisNode = sys->statesLow;
+  thisNode = sys->states;
   rd = sys->traceEvent[index];
 
   /* add node */
-  printf ("\tn%li [shape=", thisNode);
+  printf ("\tn");
+  statesFormat (stdout, thisNode);
+  printf (" [shape=");
   
   newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]);
   if (newtl != NULL)
@@ -559,9 +563,12 @@ void graphNode (const System sys)
   printf ("];\n");
 
   /* add edge */
-  printf ("\tn%li -> n%li ", parentNode, thisNode);
+  printf ("\tn");
+  statesFormat (stdout, parentNode);
+  printf (" -> n");
+  statesFormat (stdout, thisNode);
   /* add label */
-  printf ("[label=\"");
+  printf (" [label=\"");
   if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[sys->traceRun[index]].agents))
     {
       printf ("Skip claim in #%i\"", sys->traceRun[index]);
@@ -588,7 +595,7 @@ void graphNode (const System sys)
 void graphNodePath (const System sys, const int length, const char* nodepar)
 {
   int i;
-  unsigned long int thisNode;
+  states_t thisNode;
 
   i = 0;
   while (i < length)
@@ -597,7 +604,9 @@ void graphNodePath (const System sys, const int length, const char* nodepar)
       thisNode = sys->traceNode[i];
 
       /* color node */
-      printf ("\tn%li [%s];\n", thisNode, nodepar);
+      printf ("\tn");
+      statesFormat (stdout, thisNode);
+      printf (" [%s];\n", nodepar);
       i++;
     }
 }
@@ -605,7 +614,7 @@ void graphNodePath (const System sys, const int length, const char* nodepar)
 void graphEdgePath (const System sys, const int length, const char* edgepar)
 {
   int i;
-  unsigned long int thisNode, prevNode;
+  states_t thisNode, prevNode;
 
   i = 0;
   prevNode = sys->traceNode[i];
@@ -615,7 +624,11 @@ void graphEdgePath (const System sys, const int length, const char* edgepar)
       thisNode = sys->traceNode[i+1];
 
       /* color edge */
-      printf ("\tn%li -> n%li [%s];\n", prevNode, thisNode, edgepar);
+      printf ("\tn");
+      statesFormat (stdout, prevNode);
+      printf (" -> ");
+      statesFormat (stdout, thisNode);
+      printf (" [%s];\n", edgepar);
       prevNode = thisNode;
       i++;
     }

src/runs.c

@@ -113,11 +113,11 @@ systemReset (const System sys)
   Claimlist cl;
 
   /* some initial counters */
-  sys->statesLow = 0;		// number of explored states
+  sys->states = STATES0;
-  sys->statesHigh = 0;		// this is not as ridiculous as it might seem
+  sys->interval = STATES0;
+  sys->claims = STATES0;
+  sys->failed = STATES0;
   sys->explore = 1;		// do explore the space
-  sys->claims = 0;		// number of claims encountered
-  sys->failed = 0;		// number of failed claims
   cl = sys->claimlist;
   while (cl != NULL)
     {
@@ -161,7 +161,7 @@ systemDone (const System sys)
   memFree (sys->traceEvent, s * sizeof (Roledef));
   memFree (sys->traceRun, s * sizeof (int));
   memFree (sys->traceKnow, s * sizeof (Knowledge));
-  memFree (sys->traceNode, s * sizeof (unsigned long int));
+  memFree (sys->traceNode, s * sizeof (states_t));
 
   /* clear roledefs */
   for (run = 0; run < sys->maxruns; run++)
@@ -174,38 +174,18 @@ systemDone (const System sys)
   systemDestroy (sys);
 }
 
-//! Approximate the number of states traversed using a double type.
-double
-statesApproximation (const System sys)
-{
-  if (sys->statesHigh == 0)
-    return (double) sys->statesLow;
-  else
-    return (double) (sys->statesLow + (sys->statesHigh * ULONG_MAX));
-}
-
 //! Print a short version of the number of states.
 void
 statesPrintShort (const System sys)
 {
-  fprintf (stderr,"%.3e", statesApproximation (sys));
+  fprintf (stderr,"%.3e", statesDouble (sys->states));
 }
 
 //! Print the number of states.
 void
 statesPrint (const System sys)
 {
-  if (sys->statesHigh == 0)
+  statesFormat (stdout, sys->states);
-    {
-      printf ("%g", (double) sys->statesLow);
-    }
-  else
-    {
-      double dstates;
-
-      dstates = sys->statesLow + (sys->statesHigh * ULONG_MAX);
-      printf ("%.3e (...)", dstates);
-    }
   printf (" states traversed.\n");
   if (globalLatex)
       printf("\n");
@@ -777,7 +757,7 @@ systemStart (const System sys)
   sys->traceEvent = memAlloc (s * sizeof (Roledef));
   sys->traceRun = memAlloc (s * sizeof (int));
   sys->traceKnow = memAlloc (s * sizeof (Knowledge));
-  sys->traceNode = memAlloc (s * sizeof (unsigned long int));
+  sys->traceNode = memAlloc (s * sizeof (states_t));
 
   /* clear, for niceties */
   for (i = 0; i < s; i++)
@@ -785,7 +765,7 @@ systemStart (const System sys)
       sys->traceEvent[i] = NULL;
       sys->traceRun[i] = 0;
       sys->traceKnow[i] = NULL;
-      sys->traceNode[i] = 0;
+      sys->traceNode[i] = STATES0;
     }
 }
 

src/runs.h

@@ -6,6 +6,7 @@
 #include "termlists.h"
 #include "knowledge.h"
 #include "constraints.h"
+#include "states.h"
 
 #define	READ	1
 #define SEND	2
@@ -228,10 +229,10 @@ struct system
   int explore;			//!< Boolean: explore states after actions or not.
 
   /* counters */
-  unsigned long int statesLow;	//!< State number (low)
+  states_t states;
-  unsigned long int statesHigh; //!< State number (high)
+  states_t interval;		//!< Used to update state printing at certain intervals
-  unsigned long int claims;	//!< Number of claims encountered.
+  states_t claims;		//!< Number of claims encountered.
-  unsigned long int failed;	//!< Number of claims failed.
+  states_t failed;		//!< Number of claims failed.
 
   /* matching */
   int match;			//!< Matching type.
@@ -252,7 +253,7 @@ struct system
   Roledef *traceEvent;		//!< Trace roledefs: MaxRuns * maxRoledef
   int *traceRun;		//!< Trace run ids: MaxRuns * maxRoledef
   Knowledge *traceKnow;		//!< Trace intruder knowledge: Maxruns * maxRoledef
-  unsigned long int *traceNode;	//!< Trace node traversal: Maxruns * maxRoledef
+  states_t *traceNode;		//!< Trace node traversal: Maxruns * maxRoledef
 
   /* POR reduction assistance */
   int PORphase;			//!< -1: init (all sends), 0...: recurse reads

src/states.c

@@ -0,0 +1,40 @@
+#include "states.h"
+
+/* States counter operations
+ *
+ * Note that these are also used for encountered claims and such.
+ */
+
+__inline__ states_t
+statesIncrease (const states_t states)
+{
+  return states+1;
+}
+
+__inline__ double
+statesDouble (const states_t states)
+{
+  return (double) states;
+}
+
+__inline__ int
+statesSmallerThan (const states_t states, unsigned long int reflint)
+{
+  if (states < (states_t) reflint)
+      return 1;
+  else
+      return 0;
+}
+
+//! Sensible output for number of states/claims
+/**
+ * Acts like a modified form of %g
+ */
+__inline__ void
+statesFormat (FILE* out, const states_t states)
+{
+  if (states < 1000000)
+      fprintf (out, "%lu", states);
+  else
+      fprintf (out, "%.3e", statesDouble (states));
+}

src/states.h

@@ -0,0 +1,20 @@
+#ifndef STATES
+#define STATES
+/**
+ * Header file for the states counter datatype.
+ *
+ * Previously, the states number was just a unsigned int, but that
+ * turned out to be insufficient.
+ */
+
+#include <stdio.h>
+
+typedef unsigned long int states_t;
+#define STATES0 0
+
+__inline__ states_t statesIncrease (const states_t states);
+__inline__ double statesDouble (const states_t states);
+__inline__ int statesSmallerThan (const states_t states, unsigned long int reflint);
+__inline__ void statesFormat (FILE* out, const states_t states);
+
+#endif