- Cleanup

src/BUILD.txt

@@ -0,0 +1,12 @@
+Cross-platform building:
+
+On linux:
+
+  ./build-unix-both.sh
+
+On MAC:
+
+  ./build-mac-universal.sh
+
+This copies all files into the gui bin directory, and you're done.
+

src/main.c

@@ -118,13 +118,10 @@ main (int argc, char **argv)
 
   /* compile */
 
-  // Compile no runs for Arachne
+  // Compile no runs for Arachne and preprocess
   compile (spdltac, 0);
   scanner_cleanup ();
 
-  /* preprocess */
-  preprocess (sys);
-
 #ifdef DEBUG
   if (DEBUGL (1))
     {
@@ -254,13 +251,6 @@ modelCheck (const System sys)
   /* modelcheck the system */
   claimcount = arachne ();
 
-  /* clean up any states display */
-  if (switches.reportStates > 0)
-    {
-      //                States: 1.000e+06
-      printfstderr ("                  \r");
-    }
-
   if (claimcount == 0)
     {
       warning ("No claims in system.");

src/switches.c

@@ -62,6 +62,9 @@ switchesInit (int argc, char **argv)
   switches.initUnique = false;	// default allows initiator rho to contain duplicate terms
   switches.respUnique = false;	// default allows responder rho to contain duplicate terms
   switches.intruder = true;	// default allows an intruder
+  switches.agentUnfold = 0;	// default not to unfold agents
+  switches.abstractionMethod = 0;	// default no abstraction used
+  switches.useAttackBuffer = false;	// don't use by default as it does not work properly under windows vista yet
 
   // Misc
   switches.switchP = 0;		// multi-purpose parameter
@@ -81,7 +84,6 @@ switchesInit (int argc, char **argv)
   switches.human = false;	// not human friendly by default
   switches.reportMemory = 0;
   switches.reportTime = 0;
-  switches.reportStates = 0;
   switches.countStates = false;	// default off
   switches.extendNonReads = 0;	// default off
   switches.extendTrivial = 0;	// default off
@@ -450,7 +452,7 @@ switcher (const int process, int index, int commandline)
     {
       if (!process)
 	{
-	  helptext ("-d, --dot-output", "show attack output in dot format");
+	  helptext ("-d, --dot-output", "show patterns in dot format");
 	}
       else
 	{
@@ -464,7 +466,7 @@ switcher (const int process, int index, int commandline)
     {
       if (!process)
 	{
-	  helptext ("-x, --xml-output", "show attack output in XML format");
+	  helptext ("-x, --xml-output", "show patterns in XML format");
 	}
       else
 	{
@@ -570,7 +572,7 @@ switcher (const int process, int index, int commandline)
 	  if (switches.expert)
 	    {
 	      helptext ("-C, --class",
-			"generate full class (show uninstantiated variables in state output)");
+			"show full class (allow uninstantiated variables in pattern output)");
 	    }
 	}
       else
@@ -587,7 +589,7 @@ switcher (const int process, int index, int commandline)
 	  if (switches.expert)
 	    {
 	      helptext ("-s, --state-space",
-			"ignore any existing claims and add 'reachable' claims. Generate full state space classes");
+			"ignore any existing claims and add 'reachable' claims. Gives complete characterization of a roles");
 	    }
 	}
       else
@@ -674,7 +676,7 @@ switcher (const int process, int index, int commandline)
       if (!process)
 	{
 	  helptext ("-r, --max-runs=<int>",
-		    "maximum number of runs in the system [5]");
+		    "maximum number of runs in patterns [5]");
 	}
       else
 	{
@@ -696,7 +698,7 @@ switcher (const int process, int index, int commandline)
       if (!process)
 	{
 	  helptext ("    --unbounded",
-		    "Do not bound the number of runs in the state space");
+		    "Do not bound the number of runs in patterns");
 	}
       else
 	{
@@ -857,6 +859,25 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "abstraction-method", 1))
+    {
+      if (!process)
+	{
+	  if (switches.expert)
+	    {
+	      /* Not working yet
+	         helptext ("    --abstraction-method=<int>",
+	         "Abstraction method used. Default: 0 (disabled)");
+	       */
+	    }
+	}
+      else
+	{
+	  switches.abstractionMethod = integer_argument ();
+	  return index;
+	}
+    }
+
 
   /* ==================
    *  Modelchecker only
@@ -911,6 +932,20 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "agent-unfold", 1))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   */
+	}
+      else
+	{
+	  switches.agentUnfold = integer_argument ();
+	  return index;
+	}
+    }
+
   if (detect (' ', "extend-nonreads", 0))
     {
       if (!process)
@@ -1183,21 +1218,6 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
-  if (detect (' ', "progress-bar", 0))
-    {
-      if (!process)
-	{
-	  /* discourage: do not show in help text 
-	     helptext ("-b,--progress-bar", "show progress bar");
-	   */
-	}
-      else
-	{
-	  switches.reportStates = 50000;
-	  return index;
-	}
-    }
-
   if (detect ('e', "empty", 0))
     {
       if (!process)

src/switches.h

@@ -36,6 +36,9 @@ struct switchdata
   int initUnique;		//!< Default allows duplicate terms in rho (init) 
   int respUnique;		//!< Default allows duplicate terms in rho (resp)
   int intruder;			//!< Enable intruder actions (default)
+  int agentUnfold;		//!< Explicitly unfold for N honest agents and 1 compromised iff > 0
+  int abstractionMethod;	//!< 0 means none, others are specific modes
+  int useAttackBuffer;		//!< Use temporary file for attack storage
 
   // Misc
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
@@ -55,7 +58,6 @@ struct switchdata
   int human;			//!< human readable
   int reportMemory;		//!< Memory display switch.
   int reportTime;		//!< Time display switch.
-  int reportStates;		//!< Progress display switch. (traversed states)
   int countStates;		//!< Count states
   int extendNonReads;		//!< Show further events in arachne xml output.
   int extendTrivial;		//!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)