- Rewrote complete switch code. Scyther now no longer depends on

argtable2. Great.

src/main.c

@@ -58,7 +58,7 @@ enum exittypes
 #include "latex.h"
 #include "output.h"
 #include "binding.h"
-#include "version.h"
+#include "switches.h"
 
 #include "argtable2.h"
 
@@ -78,272 +78,13 @@ void MC_incTraces (const System sys);
 void MC_single (const System sys);
 int modelCheck (const System sys);
 
-//! The name of this program.
-const char *progname = "scyther";
-//! Release tag name.
-/**
- * Note that this is only referenced in the help output of the commandline program.
- * \todo Come up with a useful solution for release names.
- */
-const char *releasetag = SVNVERSION;
-
-//! The number of seconds a test is allowed to run
-static int time_limit_seconds;
-
 //! The main body, as called by the environment.
 int
 main (int argc, char **argv)
 {
-  struct arg_file *infile =
-    arg_file0 (NULL, NULL, "FILE", "input file ('-' for stdin)");
-  struct arg_file *outfile = arg_file0 ("o", "output", "FILE",
-					"output file (default is stdout)");
-  struct arg_lit *switch_arachne =
-    arg_lit0 ("a", "arachne", "use Arachne engine");
-  struct arg_lit *switch_proof =
-    arg_lit0 ("P", "proof", "generate proof output");
-  struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM",
-					   "claim type to check (default is all)");
-  struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL,
-					      "select a scenario instance 1-n (-1 to count)");
-  struct arg_int *switch_scenario_size = arg_int0 ("S", "scenario-size", NULL,
-						   "scenario size (fixed trace prefix length)");
-  struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL,
-						      "set traversal method, partial order reduction (default is 12)");
-  struct arg_int *switch_match_method =
-    arg_int0 ("m", "match", NULL, "matching method (default is 0)");
-  struct arg_lit *switch_clp =
-    arg_lit0 ("c", "cl", "use constraint logic, non-associative");
-  struct arg_int *switch_pruning_method = arg_int0 ("p", "prune", NULL,
-						    "pruning method (default is 2)");
-  struct arg_int *switch_prune_trace_length =
-    arg_int0 ("l", "max-length", NULL,
-	      "prune traces longer than <int> events.");
-  struct arg_int *switch_prune_proof_depth = arg_int0 ("d", "max-depth", NULL,
-						       "prune proof deeper than <int> splits.");
-  struct arg_lit *switch_incremental_trace_length =
-    arg_lit0 (NULL, "increment-traces",
-	      "incremental search using the length of the traces.");
-  struct arg_int *switch_maximum_runs =
-    arg_int0 ("r", "max-runs", NULL, "create at most <int> runs");
-  struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs",
-						      "incremental search using the number of runs");
-  struct arg_int *switch_goal_select_method =
-    arg_int0 (NULL, "goal-select", NULL,
-	      "use goal selection method <int> (default 3)");
-  struct arg_lit *switch_latex_output =
-    arg_lit0 (NULL, "latex", "output attacks in LaTeX format");
-  struct arg_lit *switch_empty =
-    arg_lit0 ("e", "empty", "do not generate output");
-  struct arg_lit *switch_progress_bar =
-    arg_lit0 ("b", "progress-bar", "show progress bar");
-  struct arg_lit *switch_state_space_graph =
-    arg_lit0 (NULL, "state-space", "output state space graph");
-  struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose",
-						     "allow implicit choose events (useful for few runs)");
-  struct arg_lit *switch_choose_first =
-    arg_lit0 (NULL, "choose-first", "priority to any choose events");
-  struct arg_lit *switch_enable_read_symmetries =
-    arg_lit0 (NULL, "read-symm", "enable read symmetry reductions");
-  struct arg_lit *switch_disable_agent_symmetries =
-    arg_lit0 (NULL, "no-agent-symm",
-	      "disable agent symmetry reductions");
-  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_disable_claim_symmetry =
-    arg_lit0 (NULL, "no-claimsymmetry-red",
-	      "disable claim symmetry reductions");
-  struct arg_lit *switch_summary = arg_lit0 (NULL, "summary",
-					     "show summary on stdout instead of stderr");
-  struct arg_lit *switch_echo =
-    arg_lit0 ("E", "echo", "echo command line to stdout");
-  struct arg_int *switch_timer =
-    arg_int0 ("T", "timer", NULL, "maximum time in seconds");
-#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",
-						  "indent the debug output using trace length");
-  struct arg_int *switch_debug_level =
-    arg_int0 ("D", "debug", NULL, "set debug level (default is 0)");
-#endif
-  struct arg_lit *help = arg_lit0 (NULL, "help", "print this help and exit");
-  struct arg_lit *version =
-    arg_lit0 (NULL, "version", "print version information and exit");
-  struct arg_end *end = arg_end (30);
-  void *argtable[] = {
-    infile,
-    outfile,
-    switch_empty,
-    switch_proof,
-    switch_state_space_graph,
-    switch_scenario,
-    switch_scenario_size,
-    switch_latex_output,
-    switch_summary,
-    switch_echo,
-    switch_progress_bar,
-
-    switch_arachne,
-    switch_check,
-    switch_traversal_method,
-    switch_match_method,
-    switch_clp,
-    switch_timer,
-    switch_pruning_method,
-    switch_prune_proof_depth,
-    switch_prune_trace_length, switch_incremental_trace_length,
-    switch_maximum_runs, switch_incremental_runs,
-    switch_goal_select_method,
-
-    switch_implicit_choose,
-    switch_choose_first,
-    switch_enable_read_symmetries,
-    switch_enable_symmetry_order,
-    switch_disable_agent_symmetries,
-    switch_disable_noclaims_reductions,
-    switch_disable_endgame_reductions,
-    switch_disable_claim_symmetry,
-#ifdef DEBUG
-    switch_por_parameter,
-    switch_debug_indent,
-    switch_debug_level,
-#endif
-    help, version,
-    end
-  };
   int nerrors;
   int exitcode = EXIT_NOATTACK;
 
-  /* verify the argtable[] entries were allocated sucessfully */
-  if (arg_nullcheck (argtable) != 0)
-    {
-      /* NULL entries were detected, some allocations must have failed */
-      fprintf (stderr, "%s: insufficient memory\n", progname);
-      exitcode = EXIT_ERROR;
-      goto exit;
-    }
-
-  /* defaults
-   * set any command line default values prior to parsing */
-#ifdef DEBUG
-  switch_debug_level->ival[0] = 0;
-  switch_por_parameter->ival[0] = 0;
-#endif
-  switch_scenario->ival[0] = 0;
-  switch_scenario_size->ival[0] = 0;
-  switch_traversal_method->ival[0] = 12;
-  switch_match_method->ival[0] = 0;
-  switch_prune_trace_length->ival[0] = -1;
-  switch_prune_proof_depth->ival[0] = -1;
-  switch_maximum_runs->ival[0] = INT_MAX;
-  switch_pruning_method->ival[0] = 2;
-  switch_goal_select_method->ival[0] = -1;
-  switch_timer->ival[0] = 0;
-
-  /* Parse the command line as defined by argtable[] */
-  nerrors = arg_parse (argc, argv, argtable);
-
-  /* special case: '--help' takes precedence over error reporting */
-  if (help->count > 0)
-    {
-      printf ("Usage: %s ", progname);
-      arg_print_syntax (stdout, argtable, "\n");
-      printf
-	("This program can model check security protocols for various\n");
-      printf ("properties, given a finite scenario.\n\n");
-      arg_print_glossary (stdout, argtable, "  %-25s %s\n");
-      exitcode = 0;
-      goto exit;
-    }
-
-  /* special case: '--version' takes precedence error reporting */
-  if (version->count > 0)
-    {
-      printf ("'%s' model checker for security protocols.\n", progname);
-#ifdef DEBUG
-      printf ("Revision %s, compiled with debugging support.\n", releasetag);
-#else
-      printf ("Revision %s\n", releasetag);
-#endif
-      printf ("December 2003--, Cas Cremers\n");
-      exitcode = 0;
-      goto exit;
-    }
-
-  /* If the parser returned any errors then display them and exit */
-  if (nerrors > 0)
-    {
-      /* Display the error details contained in the arg_end struct. */
-      arg_print_errors (stdout, end, progname);
-      printf ("Try '%s --help' for more information.\n", progname);
-      exitcode = EXIT_ERROR;
-      goto exit;
-    }
-
-  /* special case: uname with no command line options induces brief help */
-  if (argc == 1)
-    {
-      printf ("Try '%s --help' for more information.\n", progname);
-      exitcode = 0;
-      goto exit;
-    }
-
-  /*
-   * Arguments have been parsed by argtable,
-   * continue with main code.
-   */
-
-  /* Lutger-tries-to-test-with-broken-methods detector */
-  if (switch_clp->count > 0)
-    {
-      fprintf (stderr,
-	       "For the time being, this method is not supported, \n");
-      fprintf (stderr, "as too many changes have been made to the normal \n");
-      fprintf (stderr,
-	       "matching logic, and CL simply isn't reliable in \nmany ");
-      fprintf (stderr, "ways. Try again in a few weeks.\n");
-      exit (0);
-    }
-
-  /* redirect in- and output according to supplied filenames */
-  /* output */
-  if (outfile->count > 0)
-    {
-      /* try to open */
-      if (!freopen (outfile->filename[0], "w", stdout))
-	{
-	  fprintf (stderr, "Could not create output file '%s'.\n",
-		   outfile->filename[0]);
-	  exit (1);
-	}
-    }
-  /* input */
-  if (infile->count > 0)
-    {
-      /* check for the single dash */
-      if (strcmp (infile->filename[0], "-"))
-	{
-	  if (!freopen (infile->filename[0], "r", stdin))
-	    {
-	      fprintf (stderr, "Could not open input file '%s'.\n",
-		       infile->filename[0]);
-	      exit (1);
-	    }
-	}
-    }
-
-  /* handle debug level */
-#ifdef DEBUG
-  debugSet (switch_debug_level->ival[0]);
-#else
-  debugSet (0);
-#endif
   /* Initialize memory routines */
   memInit ();
 
@@ -362,113 +103,18 @@ main (int argc, char **argv)
    */
 
   sys = systemInit ();
-  if (switch_arachne->count > 0)
-    {
-      sys->engine = ARACHNE_ENGINE;
-      bindingInit (sys);
-    }
-  /* init compiler for this system */
-  compilerInit (sys);
-
-  /* transfer command line */
   sys->argc = argc;
   sys->argv = argv;
 
-  if (switch_echo->count > 0)
+  process_switches(sys);
-    {
+  // exit (0);	// TODO FIX weghalen [x][cc]
-      /* print command line */
-      fprintf (stdout, "command\t");
-      commandlinePrint (stdout, sys);
-      fprintf (stdout, "\n");
-    }
 
-  /* handle switches */
+  /* init compiler for this system */
+  compilerInit (sys);
 
-  sys->switchRuns = switch_maximum_runs->ival[0];	/* maximum number of runs */
-  if (switch_implicit_choose->count > 0)
-    /* allow implicit chooses */
-    sys->switchForceChoose = 0;
-  if (switch_choose_first->count > 0)
-    sys->switchChooseFirst = 1;	/* priority to chooses */
-  if (switch_enable_read_symmetries->count > 0)
-    {
-      if (switch_enable_symmetry_order->count > 0)
-	error
-	  ("--read-symm and --symm-order cannot be used at the same time.");
-      sys->switchReadSymm = 1;
-    }
-  if (switch_enable_symmetry_order->count > 0)
-    sys->switchSymmOrder = 1;	/* enable symmetry order */
-  if (switch_disable_agent_symmetries->count > 0)
-    sys->switchAgentSymm = 0;	/* disable agent symmetry order */
-  if (switch_disable_noclaims_reductions->count > 0)
-    sys->switchNomoreClaims = 0;	/* disable no more claims cutter */
-  if (switch_disable_endgame_reductions->count > 0)
-    sys->switchReduceEndgame = 0;	/* disable endgame cutter */
-  if (switch_disable_claim_symmetry->count > 0)
-    sys->switchReduceClaims = 0;	/* disable claim symmetry cutter */
-  if (switch_summary->count > 0)
-    sys->output = SUMMARY;	/* report summary on stdout */
-  if (switch_proof->count > 0)
-    sys->output = PROOF;	/* report proof on stdout (for arachne only) */
-
-  /*
-   * The scenario selector has an important side effect; when it is non-null,
-   * any scenario traversing selects chooses first.
-   */
-  sys->switchScenario = switch_scenario->ival[0];	/* scenario selector */
-  sys->switchScenarioSize = switch_scenario_size->ival[0];	/* scenario size */
-  if (sys->switchScenario == 0 && sys->switchScenarioSize > 0)
-    {
-      /* no scenario, but a size is set. so override */
-#ifdef DEBUG
-      warning ("Scanning scenarios.");
-#endif
-      sys->switchScenario = -1;
-    }
-  if (sys->switchScenario < 0)
-    {
-      sys->output = SCENARIOS;
-    }
-  if (sys->switchScenario != 0 && sys->switchScenarioSize == 0)
-    {
-#ifdef DEBUG
-      warning
-	("Scenario selection without trace prefix length implies --choose-first.");
-#endif
-      sys->switchChooseFirst = 1;
-    }
-#ifdef DEBUG
-  sys->porparam = switch_por_parameter->ival[0];
-#endif
-  sys->latex = switch_latex_output->count;
   sys->know = emptyKnowledge ();
 
 
-  /* parse compiler-dependant switches */
-  if (switch_check->count > 0)
-    {
-      Term claim;
-
-#ifdef DEBUG
-      if (lookup (switch_check->sval[0]) == NULL)
-	{
-	  globalError++;
-	  warning ("Could not find this string at all in:");
-	  symbolPrintAll ();
-	  eprintf ("\n");
-	  globalError--;
-	}
-#endif
-      claim = findGlobalConstant (switch_check->sval[0]);
-      if (claim == NULL)
-	error ("Unknown claim type to check.");
-      if (inTermlist (claim->stype, TERM_Claim))
-	sys->switchClaimToCheck = claim;
-      else
-	error ("Claim type to check is not a claim.");
-    }
-
   /* parse input */
 
   yyparse ();
@@ -482,7 +128,7 @@ main (int argc, char **argv)
   if (sys->engine != ARACHNE_ENGINE)
     {
       // Compile as many runs as possible
-      compile (spdltac, switch_maximum_runs->ival[0]);
+      compile (spdltac, sys->switchRuns);
     }
   else
     {
@@ -519,43 +165,6 @@ main (int argc, char **argv)
 
   /* add parameters to system */
 
-  sys->clp = (switch_clp->count > 0 ? 1 : 0);
-
-  sys->traverse = switch_traversal_method->ival[0];
-  sys->match = switch_match_method->ival[0];
-  mgu_match = sys->match;
-  sys->prune = switch_pruning_method->ival[0];
-  time_limit_seconds = switch_timer->ival[0];
-  set_time_limit (switch_timer->ival[0]);
-  if (switch_progress_bar->count > 0)
-    /* enable progress display */
-    sys->switchS = 50000;
-  else
-    /* disable progress display */
-    sys->switchS = 0;
-  if (switch_state_space_graph->count > 0)
-    {
-      /* enable state space graph output */
-      sys->output = STATESPACE;	//!< New method
-    }
-  if (switch_empty->count > 0)
-    sys->output = EMPTY;
-  if (switch_prune_proof_depth->ival[0] >= 0)
-    sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0];
-  if (switch_prune_trace_length->ival[0] >= 0)
-    sys->switch_maxtracelength = switch_prune_trace_length->ival[0];
-  if (switch_goal_select_method->ival[0] >= 0)
-    sys->switchGoalSelectMethod = switch_goal_select_method->ival[0];
-#ifdef DEBUG
-  /* in debugging mode, some extra switches */
-  if (switch_debug_indent->count > 0)
-    indentActivate ();
-  if (DEBUGL (1))
-    printf ("Using traversal method %i.\n", sys->traverse);
-#else
-  /* non-debug defaults */
-  sys->switchM = 0;
-#endif
 
   /*
    * ---------------------------------------
@@ -568,15 +177,6 @@ main (int argc, char **argv)
     {
       error ("Scyther can only generate LaTeX output for attacks.");
     }
-  /* Incremental stuff only works for attack locating */
-  if (switch_incremental_runs->count > 0 ||
-      switch_incremental_trace_length->count > 0)
-    {
-      if (sys->output != ATTACK && sys->output != EMPTY)
-	{
-	  error ("Incremental traversal only for empty or attack output.");
-	}
-    }
 #ifdef DEBUG
   if (DEBUGL (4))
     {
@@ -603,21 +203,7 @@ main (int argc, char **argv)
   if (DEBUGL (1))
     warning ("Start modelchecking system.");
 #endif
-  if (switch_incremental_runs->count > 0)
+  MC_single (sys);
-    {
-      MC_incRuns (sys);
-    }
-  else
-    {
-      if (switch_incremental_trace_length->count > 0)
-	{
-	  MC_incTraces (sys);
-	}
-      else
-	{
-	  MC_single (sys);
-	}
-    }
 
   /*
    * ---------------------------------------
@@ -692,7 +278,6 @@ main (int argc, char **argv)
 
 exit:
   /* deallocate each non-null entry in argtable[] */
-  arg_free (argtable);
 
   return exitcode;
 }
@@ -829,7 +414,7 @@ timersPrint (const System sys)
 		{
 		  eprintf ("bounded_proof");
 		  if (cl_scan->timebound)
-		    eprintf ("\ttime=%i", time_limit_seconds);
+		    eprintf ("\ttime=%i", get_time_limit());
 		}
 	    }
 	}

src/switches.c

@@ -0,0 +1,477 @@
+/**
+ *@file switches.c
+ * \brief Handle command-line options
+ *
+ * Contains the main switch handling.
+ */
+
+#include "string.h"
+#include "system.h"
+#include "debug.h"
+#include "version.h"
+#include "timer.h"
+
+extern System sys;
+
+extern struct tacnode *spdltac;
+extern Term TERM_Claim;
+extern int mgu_match;
+
+const char *progname = "scyther";
+const char *releasetag = SVNVERSION;
+
+//! Process a single switch or generate help text
+/**
+ * When process is false, we just generate the help text.
+ *
+ * Yields new index, or -1 when an error occurred.
+ * When the new index > argc, it should not be called anymore.
+ * By convention, argc = the number of arguments + 1
+ * The index steps through 1..argc-1.
+ */
+int
+switcher (const int process, const System sys, int index)
+{
+  char *this_arg;		// just a shortcut
+  int argc;
+  char **argv;
+
+  char *arg_pointer;
+  int arg_index;
+
+  //! Check whether there are still n options left
+  int enough_arguments_left (const int n, char shortopt, char *longopt)
+  {
+    if (index + n > argc)
+      {
+	error ("Option %c [%s] needs at least %i arguments.", shortopt,
+	       longopt, n);
+      }
+    return 1;
+  }
+
+  // Skip over (processed) argument
+  void arg_next (void)
+  {
+    index++;
+    arg_pointer = argv[index];
+  }
+
+  //! Parse an argument into an integer
+  int integer_argument (void)
+  {
+    int result;
+
+    if (arg_pointer == NULL)
+      {
+	error ("(Integer) argument expected.");
+      }
+    result = 0;
+    if (sscanf (arg_pointer, "%i", &result) != 1)
+      {
+	error ("Could not parse expected integer argument.");
+      }
+    arg_next ();
+    return result;
+  }
+
+  //! Detect whether this confirms to this option.
+  /**
+   * set arg_pointer and index
+   */
+  int detect (char shortopt, char *longopt, int args)
+  {
+    arg_pointer = NULL;
+
+    if (!process)
+      {
+	// If we are not processing, we always yield true.
+	return 1;
+      }
+    // Is it this option anyway?
+    if (strlen (this_arg) < 2 || this_arg[0] != '-')
+      {
+	// No option
+	return 0;
+      }
+    // Compare
+    if (this_arg[1] == '-')
+      {
+	int optlength;
+
+	// Long variant
+	optlength = strlen (longopt);
+	if (strncmp (this_arg + 2, longopt, optlength))
+	  return 0;
+	if ((optlength + 2 < strlen (this_arg)) &&
+	    this_arg[2 + optlength] == '=')
+	  {
+	    // This has an additional thing!
+	    arg_pointer = this_arg + 2 + optlength + 1;
+	  }
+	else
+	  {
+	    // arg = next
+	    index++;
+	    arg_pointer = argv[index];
+	  }
+      }
+    else
+      {
+	// Short variant
+	if (strlen (this_arg) < 2 || this_arg[1] != shortopt)
+	  return 0;
+	if (strlen (this_arg) > 2)
+	  {
+	    // This has an additional thing!
+	    arg_pointer = this_arg + 2;
+	  }
+	else
+	  {
+	    // arg = next
+	    index++;
+	    arg_pointer = argv[index];
+	  }
+      }
+    // Allright, this is the right option
+#ifdef DEBUG
+    // [x] TODO remove
+    printf ("%% Detected switch: [%c] %s\n", shortopt, longopt);
+#endif
+    // Enough arguments left?
+    return enough_arguments_left (args, shortopt, longopt);
+  }
+
+  //! Align columns
+  void helptext (const char *left, const char *right)
+  {
+    printf ("  %-25s %s\n", left, right);
+  }
+
+  if (process)
+    {
+      argc = sys->argc;
+      argv = sys->argv;
+#ifdef DEBUG
+      // Check range for debug; we trust the non-debug version :)
+      if (index < 1 || index >= argc)
+	{
+	  error ("Bad index number %i for argc %i", index, argc);
+	}
+#endif
+      this_arg = argv[index];
+    }
+  else
+    {
+      // Just doing help
+      this_arg = NULL;
+    }
+
+  /*
+   * -------------------------------------------------------------
+   *    Process the options, one by one
+   * -------------------------------------------------------------
+   */
+
+  if (detect ('o', "output", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-o,--output=<int>", "output file [stdout]");
+	}
+      else
+	{
+	  // Set output file name
+	  /* try to open */
+	  if (!freopen (arg_pointer, "w", stdout))
+	    {
+	      fprintf (stderr, "Could not create output file '%s'.\n",
+		       arg_pointer);
+	      exit (1);
+	    }
+	  arg_next ();
+	  return index;
+	}
+    }
+
+  if (detect ('T', "timer", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-T,--timer=<int>",
+		    "maximum time in seconds");
+	}
+      else
+	{
+  	  set_time_limit (integer_argument ());
+	  return index;
+	}
+    }
+
+  if (detect ('r', "max-runs", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-r,--max-runs=<int>",
+		    "Maximum number of runs in the system");
+	}
+      else
+	{
+	  sys->switchRuns = integer_argument ();
+	  return index;
+	}
+    }
+
+  if (detect ('E', "echo", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-E,--echo", "echo command line to stdout");
+	}
+      else
+	{
+	  /* print command line */
+	  fprintf (stdout, "command\t");
+	  commandlinePrint (stdout, sys);
+	  fprintf (stdout, "\n");
+	  return index;
+	}
+    }
+
+  if (detect (' ', "summary", 0))
+    {
+      if (!process)
+	{
+	  helptext ("--summary", "show summary on stdout");
+	}
+      else
+	{
+	  sys->output = SUMMARY;
+	  return index;
+	}
+    }
+
+  if (detect (' ', "state-space", 0))
+    {
+      if (!process)
+	{
+	  helptext ("--state-space", "output state space graph (modelchecker)");
+	}
+      else
+	{
+	  sys->output = STATESPACE;
+	  return index;
+	}
+    }
+
+  if (detect ('b', "progress-bar", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-b,--progress-bar", "show progress bar");
+	}
+      else
+	{
+	  sys->switchS = 50000;
+	  return index;
+	}
+    }
+
+  if (detect ('e', "empty", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-e,--empty", "do not generate output");
+	}
+      else
+	{
+	  sys->output = EMPTY;
+	  return index;
+	}
+    }
+
+  if (detect ('L', "latex", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-L,--latex", "output attacks in LaTeX format");
+	}
+      else
+	{
+	  sys->latex = 1;
+	  return index;
+	}
+    }
+
+  if (detect ('G', "goal-select", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-G,--goal-select=<int>", "use goal selection method <int> (default is 3)");
+	}
+      else
+	{
+	  sys->switchGoalSelectMethod = integer_argument ();
+	  return index;
+	}
+    }
+
+  if (detect ('l', "max-length", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-l,--max-length=<int>", "prune traces longer than <int> events.");
+	}
+      else
+	{
+	  sys->switch_maxtracelength = integer_argument ();
+	  return index;
+	}
+    }
+
+  if (detect ('p', "prune", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-p,--prune", "pruning method");
+	}
+      else
+	{
+	  sys->prune = integer_argument ();
+	  return index;
+	}
+    }
+
+  if (detect ('m', "match", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-m,--match", "matching method");
+	}
+      else
+	{
+	  sys->match = integer_argument ();
+	  return index;
+	}
+    }
+
+  if (detect ('P', "proof", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-P,--proof", "construct explicit proof");
+	}
+      else
+	{
+	  // Proof
+	  sys->output = PROOF;
+	  return index;
+	}
+    }
+
+  if (detect ('a', "arachne", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-a,--arachne", "select Arachne engine");
+	}
+      else
+	{
+	  // Select arachne engine
+	  sys->engine = ARACHNE_ENGINE;
+	  bindingInit (sys);
+	  return index;
+	}
+    }
+
+  if (detect ('v', "version", 0))
+    {
+      if (!process)
+	helptext ("-v,--version", "version information");
+      else
+	{
+	  printf ("'%s' model checker for security protocols.\n", progname);
+#ifdef DEBUG
+	  printf ("Revision %s, compiled with debugging support.\n",
+		  SVNVERSION);
+#else
+	  printf ("Revision %s\n", SVNVERSION);
+#endif
+	  printf ("December 2003--, Cas Cremers\n");
+	  exit (0);
+	}
+    }
+
+  if (detect ('h', "help", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-h,--help", "show this help");
+	}
+      else
+	{
+	  printf ("Usage:\n");
+	  printf ("  %s [switches] [FILE]\nSwitches:\n", progname);
+	  switcher (0, NULL, 0);
+	  exit (0);
+	}
+    }
+
+#ifdef DEBUG
+  if (detect ('D', "debug", 1))
+    {
+      if (!process)
+	{
+	  helptext ("-D,--debug=<int>", "set debug (verbosity) level.");
+	}
+      else
+	{
+	  debugSet (integer_argument ());
+	  return index;
+	}
+    }
+#endif
+
+  // If the option is not recognized, it means a file name.
+  if (!process)
+    {
+      helptext ("FILE", "input file ('-' for stdin)");
+    }
+  else
+    {
+      if (!strcmp (this_arg, "-"))
+	{
+	  // '-' input: Leave input to stdin
+	}
+      else
+	{
+	  // not '-' input: change stdin to come from this file
+	  if (!freopen (this_arg, "r", stdin))
+	    {
+	      fprintf (stderr, "Could not open input file '%s'.\n", this_arg);
+	      exit (1);
+	    }
+	  return index + 1;
+	}
+    }
+  return 0;
+}
+
+//! Process switches
+void
+process_switches (const System sys)
+{
+  int index;
+
+  if (sys->argc == 1)
+    {
+      printf ("Try '%s --help' for more information.\n", progname);
+      exit (0);
+    }
+
+  index = 1;
+  while (index < sys->argc && index > 0)
+    {
+      index = switcher (1, sys, index);
+    }
+}

src/switches.h

@@ -0,0 +1,6 @@
+#ifndef SWITCHES
+#define SWITCHES
+
+void process_switches (const System sys);
+
+#endif

src/system.c

@@ -76,10 +76,8 @@ systemInit ()
   sys->switchClaims = 0;	// default don't report on claims
   sys->switchClaimToCheck = NULL;	// default check all claims
   sys->switchGoalSelectMethod = 3;	// default goal selection method
+  sys->traverse = 12;			// default traversal method
 
-  /* set illegal traversal by default, to make sure it is set
-     later */
-  sys->traverse = 0;
   sys->switch_maxproofdepth = INT_MAX;
   sys->switch_maxtracelength = INT_MAX;
   sys->maxtracelength = INT_MAX;