From 46f4c5bd8f9fc91c7778a996f2a39577ece75a3f Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Fri, 18 Oct 2024 15:37:36 -0700
Subject: [PATCH 01/13] change: Rough pass on converting the argument parsing
 over to the argp format

---
 Src/main.c | 552 ++++++++++++++++++++++++++++++-----------------------
 1 file changed, 308 insertions(+), 244 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index e307ad0..9cfbbc0 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -1,3 +1,4 @@
+// clang-format off
 /***** spin: main.c *****/
 
 /*
@@ -21,6 +22,8 @@
 #endif
 #include "y.tab.h"
 
+#include <argp.h>
+
 extern int	DstepStart, lineno, tl_terse;
 extern FILE	*yyin, *yyout, *tl_out;
 extern Symbol	*context;
@@ -38,6 +41,10 @@ static void	add_runtime(char *);
 
 Symbol	*Fname, *oFname;
 
+static char doc[] = "Spin Version 6.5.2 -- 15 February 2024";
+// The arguments that get printed after the program, ex: `spin [OPTIONS...] ARGUMENTS`
+static char args_doc[] = "FILE";
+
 int	Etimeouts;	/* nr timeouts in program */
 int	Ntimeouts;	/* nr timeouts in never claim */
 int	analyze, columns, dumptab, has_remote, has_remvar;
@@ -613,99 +620,120 @@ preprocess(char *a, char *b, int a_tmp)
 	if (a_tmp) (void) unlink((const char *) a);
 }
 
-void
-usage(void)
-{
-	printf("use: spin [-option] ... [-option] file\n");
-	printf("\tNote: file must always be the last argument\n");
-	printf("\t-A apply slicing algorithm\n");
-	printf("\t-a generate a verifier in pan.c\n");
-	printf("\t-B no final state details in simulations\n");
-	printf("\t-b don't execute printfs in simulation\n");
-	printf("\t-C print channel access info (combine with -g etc.)\n");
-	printf("\t-c columnated -s -r simulation output\n");
-	printf("\t-d produce symbol-table information\n");
-	printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
-	printf("\t-Eyyy pass yyy to the preprocessor\n");
-	printf("\t-e compute synchronous product of multiple never claims (modified by -L)\n");
-	printf("\t-f \"..formula..\"  translate LTL ");
-	printf("into never claim\n");
-	printf("\t-F file  like -f, but with the LTL formula stored in a 1-line file\n");
-	printf("\t-g print all global variables\n");
-	printf("\t-h at end of run, print value of seed for random nr generator used\n");
-	printf("\t-i interactive (random simulation)\n");
-	printf("\t-I show result of inlining and preprocessing\n");
-	printf("\t-J reverse eval order of nested unlesses\n");
-	printf("\t-jN skip the first N steps ");
-	printf("in simulation trail\n");
-	printf("\t-k fname use the trailfile stored in file fname, see also -t\n");
-	printf("\t-L when using -e, use strict language intersection\n");
-	printf("\t-l print all local variables\n");
-	printf("\t-M generate msc-flow in tcl/tk format\n");
-	printf("\t-m lose msgs sent to full queues\n");
-	printf("\t-N fname use never claim stored in file fname\n");
-	printf("\t-nN seed for random nr generator\n");
-	printf("\t-O use old scope rules (pre 5.3.0)\n");
-	printf("\t-o1 turn off dataflow-optimizations in verifier\n");
-	printf("\t-o2 don't hide write-only variables in verifier\n");
-	printf("\t-o3 turn off statement merging in verifier\n");
-	printf("\t-o4 turn on rendezvous optiomizations in verifier\n");
-	printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\n");
-	printf("\t-o6 revert to the old rules for interpreting priority tags (pre version 6.2)\n");
-	printf("\t-o7 revert to the old rules for semi-colon usage (pre version 6.3)\n");
-	printf("\t-Pxxx use xxx for preprocessing\n");
-	printf("\t-p print all statements\n");
-	printf("\t-pp pretty-print (reformat) stdin, write stdout\n");
-	printf("\t-qN suppress io for queue N in printouts\n");
-	printf("\t-r print receive events\n");
-	printf("\t-replay  replay an error trail-file found earlier\n");
-	printf("\t	if the model contains embedded c-code, the ./pan executable is used\n");
-	printf("\t	otherwise spin itself is used to replay the trailfile\n");
-	printf("\t	note that pan recognizes different runtime options than spin itself\n");
-	printf("\t-run  (or -search) generate a verifier, and compile and run it\n");
-	printf("\t      options before -search are interpreted by spin to parse the input\n");
-	printf("\t      options following a -search are used to compile and run the verifier pan\n");
-	printf("\t	    valid options that can follow a -search argument include:\n");
-	printf("\t	    -bfs	perform a breadth-first search\n");
-	printf("\t	    -bfspar	perform a parallel breadth-first search\n");
-	printf("\t	    -dfspar	perform a parallel depth-first search, same as -DNCORE=4\n");
-	printf("\t	    -bcs	use the bounded-context-switching algorithm\n");
-	printf("\t	    -bitstate	or -bit, use bitstate storage\n");
-	printf("\t	    -biterateN,M use bitstate with iterative search refinement (-w18..-w35)\n");
-	printf("\t			perform N randomized runs and increment -w every M runs\n");
-	printf("\t			default value for N is 10, default for M is 1\n");
-	printf("\t			(use N,N to keep -w fixed for all runs)\n");
-	printf("\t			(add -w to see which commands will be executed)\n");
-	printf("\t			(add -W if ./pan exists and need not be recompiled)\n");
-	printf("\t	    -swarmN,M like -biterate, but running all iterations in parallel\n");
-	printf("\t	    -link file.c  link executable pan to file.c\n");
-	printf("\t	    -collapse	use collapse state compression\n");
-	printf("\t	    -noreduce	do not use partial order reduction\n");
-	printf("\t	    -hc  	use hash-compact storage\n");
-	printf("\t	    -noclaim	ignore all ltl and never claims\n");
-	printf("\t	    -p_permute	use process scheduling order random permutation\n");
-	printf("\t	    -p_rotateN	use process scheduling order rotation by N\n");
-	printf("\t	    -p_reverse	use process scheduling order reversal\n");
-	printf("\t	    -rhash      randomly pick one of the -p_... options\n");
-	printf("\t	    -ltl p	verify the ltl property named p\n");
-	printf("\t	    -safety	compile for safety properties only\n");
-	printf("\t	    -i	    	use the dfs iterative shortening algorithm\n");
-	printf("\t	    -a	    	search for acceptance cycles\n");
-	printf("\t	    -l	    	search for non-progress cycles\n");
-	printf("\t	similarly, a -D... parameter can be specified to modify the compilation\n");
-	printf("\t	and any valid runtime pan argument can be specified for the verification\n");
-	printf("\t-S1 and -S2 separate pan source for claim and model\n");
-	printf("\t-s print send events\n");
-	printf("\t-T do not indent printf output\n");
-	printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
-	printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
-	printf("\t-uN stop a simulation run after N steps\n");
-	printf("\t-v verbose, more warnings\n");
-	printf("\t-w very verbose (when combined with -l or -g)\n");
-	printf("\t-[XYZ] reserved for use by xspin interface\n");
-	printf("\t-V print version number and exit\n");
-	alldone(1);
-}
+
+// The format for each `argp_option` struct is as follows:
+// 1. The name of the option's long option
+// 2. The option's key when passed into the parser, or the short option
+// 3. The name printed for the argument, for cases such as -output <FILE>
+// 4. Flags for the argument
+// 5. A documentation string for the option
+static struct argp_option options[] = {
+  {0, 'A', 0, 0, "apply slicing algorithm"},
+  {0, 'a', 0, 0, "generate a verifier in pan.c"},
+  {0, 'B', 0, 0, "no final state details in simulations"},
+  {0, 'b', 0, 0, "don't execute printfs in simulation"},
+  {0, 'C', 0, 0, "print channel access info (combine with -g etc."},
+	{0, 'c', 0, 0, "columnated -s -r simulation output"},
+	{0, 'd', 0, 0, "produce symbol-table information"},
+	{0, 'D', 0, 0, "pass -Dyyy to the preprocessor"},
+	{0, 'E', 0, 0, "pass yyy to the preprocessor"},
+	{0, 'e', 0, 0, "compute synchronous product of multiple never claims (modified by -L)"},
+	{0, 'f', 0, 0, "\"..formula..\"  translate LTL "},
+
+  {0, 0, 0, OPTION_DOC, "into never claim"},
+	{0, 'F', 0, 0, "file  like -f, but with the LTL formula stored in a 1-line file"},
+	{0, 'g', 0, 0, "print all global variables"},
+	{0, 'h', 0, 0, "at end of run, print value of seed for random nr generator used"},
+	{0, 'i', 0, 0, "interactive (random simulation)"},
+	{0, 'I', 0, 0, "show result of inlining and preprocessing"},
+	{0, 'J', 0, 0, "reverse eval order of nested unlesses"},
+	{"jN", 0, 0, 0, "skip the first N steps "},
+
+  {0, 0, 0, OPTION_DOC, "in simulation trail"},
+	{0, 'k', 0, 0, "fname use the trailfile stored in file fname, see also -t"},
+	{0, 'L', 0, 0, "when using -e, use strict language intersection\n"},
+	{0, 'l', 0, 0, "print all local variables\n"},
+	{0, 'M', 0, 0, "generate msc-flow in tcl/tk format\n"},
+	{0, 'm', 0, 0, "lose msgs sent to full queues\n"},
+	{0, 'N', 0, 0, "fname use never claim stored in file fname\n"},
+	{"nN", 0, 0, 0, "seed for random nr generator\n"},
+	{0, 'O', 0, 0, "use old scope rules (pre 5.3.0)\n"},
+	{"o1", 0, 0, 0, "turn off dataflow-optimizations in verifier\n"},
+	{"o2", 0, 0, 0, "don't hide write-only variables in verifier\n"},
+	{"o3", 0, 0, 0, "turn off statement merging in verifier\n"},
+	{"o4", 0, 0, 0, "turn on rendezvous optiomizations in verifier\n"},
+	{"o5", 0, 0, 0, "turn on case caching (reduces size of pan.m, but affects reachability reports)\n"},
+	{"o6", 0, 0, 0, "revert to the old rules for interpreting priority tags (pre version 6.2)\n"},
+	{"o7", 0, 0, 0, "revert to the old rules for semi-colon usage (pre version 6.3)\n"},
+
+	{0, 'P', 0, 0, "use xxx for preprocessing\n"},
+	{0, 'p', 0, 0, "print all statements\n"},
+	{"pp", OPT_PRETTY_PRINT, 0, 0, "pretty-print (reformat) stdin, write stdout\n"},
+	{0, 'q', 0, 0, "suppress io for queue N in printouts\n"},
+	{0, 'r', 0, 0, "print receive events\n"},
+
+	// printf("\t-replay  replay an error trail-file found earlier\n");
+	// printf("\t	if the model contains embedded c-code, the ./pan executable is used\n");
+	// printf("\t	otherwise spin itself is used to replay the trailfile\n");
+	// printf("\t	note that pan recognizes different runtime options than spin itself\n");
+
+	// printf("\t-run  (or -search) generate a verifier, and compile and run it\n");
+	// printf("\t      options before -search are interpreted by spin to parse the input\n");
+	// printf("\t      options following a -search are used to compile and run the verifier pan\n");
+	// printf("\t	    valid options that can follow a -search argument include:\n");
+	// printf("\t	    -bfs	perform a breadth-first search\n");
+	// printf("\t	    -bfspar	perform a parallel breadth-first search\n");
+	// printf("\t	    -dfspar	perform a parallel depth-first search, same as -DNCORE=4\n");
+	// printf("\t	    -bcs	use the bounded-context-switching algorithm\n");
+	// printf("\t	    -bitstate	or -bit, use bitstate storage\n");
+	// printf("\t	    -biterateN,M use bitstate with iterative search refinement (-w18..-w35)\n");
+	// printf("\t			perform N randomized runs and increment -w every M runs\n");
+	// printf("\t			default value for N is 10, default for M is 1\n");
+	// printf("\t			(use N,N to keep -w fixed for all runs)\n");
+	// printf("\t			(add -w to see which commands will be executed)\n");
+	// printf("\t			(add -W if ./pan exists and need not be recompiled)\n");
+	// printf("\t	    -swarmN,M like -biterate, but running all iterations in parallel\n");
+	// printf("\t	    -link file.c  link executable pan to file.c\n");
+	// printf("\t	    -collapse	use collapse state compression\n");
+	// printf("\t	    -noreduce	do not use partial order reduction\n");
+	// printf("\t	    -hc  	use hash-compact storage\n");
+	// printf("\t	    -noclaim	ignore all ltl and never claims\n");
+	// printf("\t	    -p_permute	use process scheduling order random permutation\n");
+	// printf("\t	    -p_rotateN	use process scheduling order rotation by N\n");
+	// printf("\t	    -p_reverse	use process scheduling order reversal\n");
+	// printf("\t	    -rhash      randomly pick one of the -p_... options\n");
+	// printf("\t	    -ltl p	verify the ltl property named p\n");
+	// printf("\t	    -safety	compile for safety properties only\n");
+	// printf("\t	    -i	    	use the dfs iterative shortening algorithm\n");
+	// printf("\t	    -a	    	search for acceptance cycles\n");
+	// printf("\t	    -l	    	search for non-progress cycles\n");
+	// printf("\t	similarly, a -D... parameter can be specified to modify the compilation\n");
+	// printf("\t	and any valid runtime pan argument can be specified for the verification\n");
+
+	// printf("\t-S1 and -S2 separate pan source for claim and model\n");
+	// printf("\t-s print send events\n");
+	// printf("\t-T do not indent printf output\n");
+	// printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
+	// printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
+	// printf("\t-uN stop a simulation run after N steps\n");
+	// printf("\t-v verbose, more warnings\n");
+	// printf("\t-w very verbose (when combined with -l or -g)\n");
+	// printf("\t-[XYZ] reserved for use by xspin interface\n");
+	// printf("\t-V print version number and exit\n");
+
+  // argp: An options vector should be terminated by an option with all fields zero
+  {0},
+};
+
+enum opt_level {
+  OPT_LEVEL_DATAFLOW,
+  OPT_LEVEL_DEAD_VARIABLE_ELIM,
+  OPT_LEVEL_STATEMENT_MERGING,
+  OPT_LEVEL_RV_MERGING,
+  OPT_LEVEL_CASE_CACHING,
+  OPT_OLD_PRIO_RULES,
+  OPT_NO_IMPLIES_SEMIS,
+};
 
 int
 optimizations(int nr)
@@ -758,7 +786,7 @@ optimizations(int nr)
 		return 0; /* no break */
 	default:
 		printf("spin: bad or missing parameter on -o\n");
-		usage();
+		// usage();
 		break;
 	}
 	return 1;
@@ -882,6 +910,190 @@ getline(char **lineptr, size_t *n, FILE *stream)
 }
 #endif
 
+#define OPT_KEY_RUN 1
+#define OPT_KEY_PRETTY_PRINT 2
+#define OPT_KEY_LTL 3
+#define OPT_KEY_LINK 4
+#define OPT_KEY_REPLAY 5
+#define OPT_KEY_SIMULATE 6
+#define OPT_KEY_SEARCH 7
+
+struct cli_args {
+  int export_ast;
+  int analyze;
+  int no_wrapup;
+  int no_print;
+  int Caccess;
+  int columns;
+  int dumptab;
+  int product;
+  char* ltl_file;
+  char* add_ltl;
+  int verbose;
+  int seedy;
+  int interactive;
+  int inlineonly;
+  int like_java;
+  // TODO: Validate the types of these variables
+  int jumpsteps;
+  int s_trail;
+  char* trailfilename;
+  int Strict;
+  int m_loss;
+  int T;
+  char* nvr_file;
+  int old_scope_rules;
+  int tl_terse;
+  int usedopts;
+  int buzzed;
+  int norecompile;
+  int replay;
+  int separate;
+  int notabs;
+  int ntrail;
+  int cutoff;
+  char* pan_runtime;
+  int xspin;
+  int limited_vis;
+  int preprocessonly;
+};
+
+static error_t parse_opt(int key, char *arg, struct argp_state *state) {
+  struct cli_args *args = state->input;
+
+  switch (key) {
+		case 'A': args->export_ast = 1; break;
+		case 'a': args->analyze = 1; break;
+		case 'B': args->no_wrapup = 1; break;
+		case 'b': args->no_print = 1; break;
+		case 'C': args->Caccess = 1; break;
+		case 'c': args->columns = 1; break;
+    case 'D': PreArg[++PreCnt] = arg; break;
+		case 'd': args->dumptab = 1; break;
+    case 'E': PreArg[++PreCnt] = arg; break;
+		case 'e': args->product++; break; /* see also 'L' */
+		case 'F': args->ltl_file = arg; break;
+		case 'f': args->add_ltl = arg; break;
+		case 'g': args->verbose +=  1; break;
+		case 'h': args->seedy = 1; break;
+		case 'i': args->interactive = 1; break;
+		case 'I': args->inlineonly = 1; break;
+		case 'J': args->like_java = 1; break;
+		case 'j': jumpsteps = atoi(arg); break;
+    case 'k': args->s_trail = 1; args->trailfilename = arg; break;
+    case 'L': args->Strict++; break; /* modified -e */
+    case 'l': args->verbose += 2; break;
+    case 'M': args->columns = 2; break;
+    case 'm': args->m_loss = 1; break;
+    case 'N': args->nvr_file = arg; break;
+    case 'n': args->T = atoi(arg); args->tl_terse = 1; break;
+    case 'O': args->old_scope_rules = 1; break;
+    case 'o': args->usedopts += optimizations(atoi(arg));
+    case 'P': {
+      assert(strlen(arg) < sizeof(PreProc));
+      strcpy(PreProc, arg);
+      break;
+    }
+    case 'p': args->verbose += 4; break;
+    case OPT_KEY_PRETTY_PRINT: pretty_print(); break;
+    case 'q': {
+      if (isdigit(arg[0])) {
+        qhide(atoi(arg));
+      }
+    }
+    case OPT_KEY_RUN: {
+      Srand((unsigned int) args->T);
+      if (args->buzzed != 0) {
+        fatal("cannot combine -x with -run -replay or -search", (char *)0);
+      }
+
+      buzzed = 2;
+      analyze = 1;
+
+      // TODO: Parse run args here
+      break;
+    }
+    case OPT_KEY_REPLAY: {
+      args->replay = 1;
+      break;
+    }
+    case 'r': args->verbose += 8; break;
+    case 'S': args->separate = atoi(arg); args->analyze = 1; break;
+    case OPT_KEY_SIMULATE: break; // ignore
+    case OPT_KEY_SEARCH: break; // samecase
+    case 's': args->verbose += 16; break;
+    case 'T': args->notabs = 1; break;
+    case 't': {
+      args->s_trail = 1;
+      if (isdigit(arg[0])) {
+        args->ntrail = atoi(arg);
+      }
+      break;
+    }
+    case 'U': PreArg[++PreCnt] = arg; break;
+    case 'u': args->cutoff = atoi(arg); break;
+    case 'v': args->verbose += 32; break;
+    case 'V': printf("%s\n", SpinVersion); break;
+    case 'w': args->verbose += 64; break;
+    case 'W': args->norecompile = 1; break; /* 6.4.7: for swarm/biterate */
+    case 'x': { /* internal - reserved use */
+      if (buzzed != 0) {
+        fatal("cannot combine -x with -run -search or -replay", (char *)0);
+      }
+      args->buzzed = 1; /* implies also -a -o3 */
+      args->pan_runtime = "-d";
+      args->analyze = 1;
+      args->usedopts += optimizations('3');
+      break;
+    }
+    case 'X': {
+      args->xspin = args->notabs = 1;
+#ifndef PC
+    signal(SIGPIPE, alldone); /* not posix */
+#endif
+      break;
+    }
+    case 'Y': args->limited_vis = 1; break; /* used by xspin */
+    case 'Z': args->preprocessonly = 1; break; /* used by xspin */
+    default:
+      return ARGP_ERR_UNKNOWN;
+  }
+
+  return 0;
+}
+
+static error_t parse_run_opt(int key, char *arg, struct argp_state *state) {
+  struct cli_args *args = state->input;
+
+  switch (key) {
+    case 'D':
+    case 'O':
+    case 'U': add_comptime(arg); break;
+    case 'W': args->norecompile = 1; break;
+    case OPT_KEY_LTL: add_runtime("-N"); add_runtime("ltl"); break;
+    case OPT_KEY_LINK: add_comptime("link"); break;
+    default: add_runtime(arg);
+  }
+
+  return 0;
+}
+
+static int validate_args(const struct cli_args *args) {
+  return 1;
+};
+
+static struct argp_child arg_children[] = {
+  { 0 },
+};
+
+static struct argp argp = { 
+  .options = options, 
+  .parser = parse_opt,
+  .args_doc = args_doc, 
+  .doc = doc,
+  .children = arg_children,
+};
+
 int
 main(int argc, char *argv[])
 {	Symbol *s;
@@ -896,155 +1108,9 @@ main(int argc, char *argv[])
 	assert(strlen(CPP) < sizeof(PreProc));
 	strcpy(PreProc, CPP);
 
-	/* unused flags: y, z, G, L, Q, R, W */
-	while (argc > 1 && argv[1][0] == '-')
-	{	switch (argv[1][1]) {
-		case 'A': export_ast = 1; break;
-		case 'a': analyze = 1; break;
-		case 'B': no_wrapup = 1; break;
-		case 'b': no_print = 1; break;
-		case 'C': Caccess = 1; break;
-		case 'c': columns = 1; break;
-		case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
-			  break;	/* define */
-		case 'd': dumptab =  1; break;
-		case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
-			  break;
-		case 'e': product++; break; /* see also 'L' */
-		case 'F': ltl_file = (char **) (argv+2);
-			  argc--; argv++; break;
-		case 'f': add_ltl = (char **) argv;
-			  argc--; argv++; break;
-		case 'g': verbose +=  1; break;
-		case 'h': seedy = 1; break;
-		case 'i': interactive = 1; break;
-		case 'I': inlineonly = 1; break;
-		case 'J': like_java = 1; break;
-		case 'j': jumpsteps = atoi(&argv[1][2]); break;
-		case 'k': s_trail = 1;
-			  trailfilename = (char **) (argv+2);
-			  argc--; argv++; break;
-		case 'L': Strict++; break; /* modified -e */
-		case 'l': verbose +=  2; break;
-		case 'M': columns = 2; break;
-		case 'm': m_loss   =  1; break;
-		case 'N': nvr_file = (char **) (argv+2);
-			  argc--; argv++; break;
-		case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
-		case 'O': old_scope_rules = 1; break;
-		case 'o': usedopts += optimizations(argv[1][2]); break;
-		case 'P': assert(strlen((const char *) &argv[1][2]) < sizeof(PreProc));
-			  strcpy(PreProc, (const char *) &argv[1][2]);
-			  break;
-		case 'p': if (argv[1][2] == 'p')
-			  {	pretty_print();
-				alldone(0);
-			  }
-			  verbose +=  4; break;
-		case 'q': if (isdigit((int) argv[1][2]))
-				qhide(atoi(&argv[1][2]));
-			  break;
-		case 'r':
-			  if (strcmp(&argv[1][1], "run") == 0)
-			  {	Srand((unsigned int) T);
-samecase:			if (buzzed != 0)
-				{ fatal("cannot combine -x with -run -replay or -search", (char *)0);
-				}
-				buzzed  = 2;
-				analyze = 1;
-				argc--; argv++;
-				/* process all remaining arguments, except -w/-W, as relating to pan: */
-				while (argc > 1 && argv[1][0] == '-')
-				{ switch (argv[1][1]) {
-				  case 'D': /* eg -DNP */
-			/*	  case 'E': conflicts with runtime arg */
-				  case 'O': /* eg -O2 */
-				  case 'U': /* to undefine a macro */
-					add_comptime(argv[1]);
-					break;
-#if 0
-				  case 'w': /* conflicts with bitstate runtime arg */
-					verbose += 64; 
-					break;
-#endif
-				  case 'W':
-					norecompile = 1;
-					break;
-				  case 'l':
-					if (strcmp(&argv[1][1], "ltl") == 0)
-					{	add_runtime("-N");
-						argc--; argv++;
-						add_runtime(argv[1]); /* prop name */
-						break;
-					}
-					if (strcmp(&argv[1][1], "link") == 0)
-					{	argc--; argv++;
-						add_comptime(argv[1]);
-						break;
-					}
-					/* else fall through */
-				  default:
-					add_runtime(argv[1]); /* -bfs etc. */
-					break;
-				  }
-				  argc--; argv++;
-				}
-				argc++; argv--;
-			  } else if (strcmp(&argv[1][1], "replay") == 0)
-			  {	replay = 1;
-				add_runtime("-r");
-				goto samecase;
-			  } else
-			  {	verbose +=  8;
-			  }
-			  break;
-		case 'S': separate = atoi(&argv[1][2]); /* S1 or S2 */
-			  /* generate code for separate compilation */
-			  analyze = 1; break;
-		case 's': 
-			  if (strcmp(&argv[1][1], "simulate") == 0)
-			  {	break; /* ignore */
-			  }
-			  if (strcmp(&argv[1][1], "search") == 0)
-			  {	goto samecase;
-			  }
-			  verbose += 16; break;
-		case 'T': notabs = 1; break;
-		case 't': s_trail  =  1;
-			  if (isdigit((int)argv[1][2]))
-			  {	ntrail = atoi(&argv[1][2]);
-			  }
-			  break;
-		case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
-			  break;	/* undefine */
-		case 'u': cutoff = atoi(&argv[1][2]); break;
-		case 'v': verbose += 32; break;
-		case 'V': printf("%s\n", SpinVersion);
-			  alldone(0);
-			  break;
-		case 'w': verbose += 64; break;
-		case 'W': norecompile = 1; break;	/* 6.4.7: for swarm/biterate */
-		case 'x': /* internal - reserved use */
-			  if (buzzed != 0)
-			  {	fatal("cannot combine -x with -run -search or -replay", (char *)0);
-			  }
-			  buzzed = 1;	/* implies also -a -o3 */
-			  pan_runtime = "-d";
-			  analyze = 1; 
-			  usedopts += optimizations('3');
-			  break;
-		case 'X': xspin = notabs = 1;
-#ifndef PC
-			  signal(SIGPIPE, alldone); /* not posix... */
-#endif
-			  break;
-		case 'Y': limited_vis = 1; break;	/* used by xspin */
-		case 'Z': preprocessonly = 1; break;	/* used by xspin */
+  struct cli_args arguments = { 0 };
 
-		default : usage(); break;
-		}
-		argc--; argv++;
-	}
+  argp_parse(&argp, argc, argv, 0, 0, &arguments);
 
 	if (columns == 2 && !cutoff)
 	{	cutoff = 1024;
@@ -1575,5 +1641,3 @@ explain(int n)
 	case UNLESS:	fprintf(fd, "%sunless",	Keyword); break;
 	}
 }
-
-

From 4d6fdf2b516217ac6a822c366ec3182a6849b4ca Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sat, 19 Oct 2024 02:04:31 -0700
Subject: [PATCH 02/13] feat: Added support for all the flags, and fixed some
 missing break statements

---
 Src/main.c | 194 ++++++++++++++++++++++++-----------------------------
 1 file changed, 87 insertions(+), 107 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 9cfbbc0..28e6eee 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -41,7 +41,7 @@ static void	add_runtime(char *);
 
 Symbol	*Fname, *oFname;
 
-static char doc[] = "Spin Version 6.5.2 -- 15 February 2024";
+static char doc[] = SpinVersion;
 // The arguments that get printed after the program, ex: `spin [OPTIONS...] ARGUMENTS`
 static char args_doc[] = "FILE";
 
@@ -620,6 +620,13 @@ preprocess(char *a, char *b, int a_tmp)
 	if (a_tmp) (void) unlink((const char *) a);
 }
 
+#define OPT_KEY_RUN 1
+#define OPT_KEY_PRETTY_PRINT 2
+#define OPT_KEY_LTL 3
+#define OPT_KEY_LINK 4
+#define OPT_KEY_REPLAY 5
+#define OPT_KEY_SIMULATE 6
+#define OPT_KEY_SEARCH 7
 
 // The format for each `argp_option` struct is as follows:
 // 1. The name of the option's long option
@@ -635,93 +642,97 @@ static struct argp_option options[] = {
   {0, 'C', 0, 0, "print channel access info (combine with -g etc."},
 	{0, 'c', 0, 0, "columnated -s -r simulation output"},
 	{0, 'd', 0, 0, "produce symbol-table information"},
-	{0, 'D', 0, 0, "pass -Dyyy to the preprocessor"},
-	{0, 'E', 0, 0, "pass yyy to the preprocessor"},
+	{0, 'D', "yyy", 0, "pass -Dyyy to the preprocessor"},
+	{0, 'E', "yyy", 0, "pass yyy to the preprocessor"},
 	{0, 'e', 0, 0, "compute synchronous product of multiple never claims (modified by -L)"},
 	{0, 'f', 0, 0, "\"..formula..\"  translate LTL "},
 
-  {0, 0, 0, OPTION_DOC, "into never claim"},
+  {0, 0, 0, OPTION_DOC, "Into never claim:"},
 	{0, 'F', 0, 0, "file  like -f, but with the LTL formula stored in a 1-line file"},
 	{0, 'g', 0, 0, "print all global variables"},
 	{0, 'h', 0, 0, "at end of run, print value of seed for random nr generator used"},
 	{0, 'i', 0, 0, "interactive (random simulation)"},
 	{0, 'I', 0, 0, "show result of inlining and preprocessing"},
 	{0, 'J', 0, 0, "reverse eval order of nested unlesses"},
-	{"jN", 0, 0, 0, "skip the first N steps "},
+	{0, 'j', "N", 0, "skip the first N steps "},
 
-  {0, 0, 0, OPTION_DOC, "in simulation trail"},
+  {0, 0, 0, OPTION_DOC, "In simulation trail:"},
 	{0, 'k', 0, 0, "fname use the trailfile stored in file fname, see also -t"},
-	{0, 'L', 0, 0, "when using -e, use strict language intersection\n"},
-	{0, 'l', 0, 0, "print all local variables\n"},
-	{0, 'M', 0, 0, "generate msc-flow in tcl/tk format\n"},
-	{0, 'm', 0, 0, "lose msgs sent to full queues\n"},
-	{0, 'N', 0, 0, "fname use never claim stored in file fname\n"},
-	{"nN", 0, 0, 0, "seed for random nr generator\n"},
-	{0, 'O', 0, 0, "use old scope rules (pre 5.3.0)\n"},
-	{"o1", 0, 0, 0, "turn off dataflow-optimizations in verifier\n"},
-	{"o2", 0, 0, 0, "don't hide write-only variables in verifier\n"},
-	{"o3", 0, 0, 0, "turn off statement merging in verifier\n"},
-	{"o4", 0, 0, 0, "turn on rendezvous optiomizations in verifier\n"},
-	{"o5", 0, 0, 0, "turn on case caching (reduces size of pan.m, but affects reachability reports)\n"},
-	{"o6", 0, 0, 0, "revert to the old rules for interpreting priority tags (pre version 6.2)\n"},
-	{"o7", 0, 0, 0, "revert to the old rules for semi-colon usage (pre version 6.3)\n"},
-
-	{0, 'P', 0, 0, "use xxx for preprocessing\n"},
-	{0, 'p', 0, 0, "print all statements\n"},
-	{"pp", OPT_PRETTY_PRINT, 0, 0, "pretty-print (reformat) stdin, write stdout\n"},
-	{0, 'q', 0, 0, "suppress io for queue N in printouts\n"},
-	{0, 'r', 0, 0, "print receive events\n"},
-
-	// printf("\t-replay  replay an error trail-file found earlier\n");
-	// printf("\t	if the model contains embedded c-code, the ./pan executable is used\n");
-	// printf("\t	otherwise spin itself is used to replay the trailfile\n");
-	// printf("\t	note that pan recognizes different runtime options than spin itself\n");
-
-	// printf("\t-run  (or -search) generate a verifier, and compile and run it\n");
-	// printf("\t      options before -search are interpreted by spin to parse the input\n");
-	// printf("\t      options following a -search are used to compile and run the verifier pan\n");
-	// printf("\t	    valid options that can follow a -search argument include:\n");
-	// printf("\t	    -bfs	perform a breadth-first search\n");
-	// printf("\t	    -bfspar	perform a parallel breadth-first search\n");
-	// printf("\t	    -dfspar	perform a parallel depth-first search, same as -DNCORE=4\n");
-	// printf("\t	    -bcs	use the bounded-context-switching algorithm\n");
-	// printf("\t	    -bitstate	or -bit, use bitstate storage\n");
-	// printf("\t	    -biterateN,M use bitstate with iterative search refinement (-w18..-w35)\n");
-	// printf("\t			perform N randomized runs and increment -w every M runs\n");
-	// printf("\t			default value for N is 10, default for M is 1\n");
-	// printf("\t			(use N,N to keep -w fixed for all runs)\n");
-	// printf("\t			(add -w to see which commands will be executed)\n");
-	// printf("\t			(add -W if ./pan exists and need not be recompiled)\n");
-	// printf("\t	    -swarmN,M like -biterate, but running all iterations in parallel\n");
-	// printf("\t	    -link file.c  link executable pan to file.c\n");
-	// printf("\t	    -collapse	use collapse state compression\n");
-	// printf("\t	    -noreduce	do not use partial order reduction\n");
-	// printf("\t	    -hc  	use hash-compact storage\n");
-	// printf("\t	    -noclaim	ignore all ltl and never claims\n");
-	// printf("\t	    -p_permute	use process scheduling order random permutation\n");
-	// printf("\t	    -p_rotateN	use process scheduling order rotation by N\n");
-	// printf("\t	    -p_reverse	use process scheduling order reversal\n");
-	// printf("\t	    -rhash      randomly pick one of the -p_... options\n");
-	// printf("\t	    -ltl p	verify the ltl property named p\n");
-	// printf("\t	    -safety	compile for safety properties only\n");
-	// printf("\t	    -i	    	use the dfs iterative shortening algorithm\n");
-	// printf("\t	    -a	    	search for acceptance cycles\n");
-	// printf("\t	    -l	    	search for non-progress cycles\n");
-	// printf("\t	similarly, a -D... parameter can be specified to modify the compilation\n");
-	// printf("\t	and any valid runtime pan argument can be specified for the verification\n");
+	{0, 'L', 0, 0, "when using -e, use strict language intersection"},
+	{0, 'l', 0, 0, "print all local variables"},
+	{0, 'M', 0, 0, "generate msc-flow in tcl/tk format"},
+	{0, 'm', 0, 0, "lose msgs sent to full queues"},
+	{0, 'N', 0, 0, "fname use never claim stored in file fname"},
+	{0, 'n', "N", 0, "seed for random nr generator"},
+	{0, 'O', 0, 0, "use old scope rules (pre 5.3.0)"},
+  {0, 'o', "NUM", 0, "\nSet optimization level for the program:\n\
+1. Turn off dataflow-optimizations in verifier\n\
+2. Don't hide write-only variables in verifier\n\
+3. Turn off statement merging in verifier\n\
+4. Turn on rendezvous optiomizations in verifier\n\
+5. Turn on case caching (reduces size of pan.m, but affects reachability reports)\n\
+6. Revert to the old rules for interpreting priority tags (pre version 6.2)\n\
+7. Revert to the old rules for semi-colon usage (pre version 6.3)\n"},
+	{0, 'P', "xxx", 0, "use xxx for preprocessing"},
+	{0, 'p', 0, 0, "print all statements"},
+	{"pp", OPT_KEY_PRETTY_PRINT, 0, 0, "pretty-print (reformat) stdin, write stdout"},
+	{0, 'q', 0, 0, "suppress io for queue N in printouts"},
+	{0, 'r', 0, 0, "print receive events"},
+
+  {"replay", OPT_KEY_REPLAY, 0, 0, "replay an error trail-file found earlier\n\
+if the model contains embedded c-code, the ./pan executable is used\n\
+otherwise spin itself is used to replay the trailfile\n\
+note that pan recognizes different runtime options than spin itself"},
+
+  {"run", OPT_KEY_RUN, 0, 0, "(or -search) generate a verifier, and compile and run it\n\
+options before -search are interpreted by spin to parse the input\n\
+options following a -search are used to compile and run the verifier pan\n\
+valid options that can follow a -search argument are in the following section.\n\
+Similarly, a -D... parameter can be specified to modify the compilation\n\
+and any valid runtime pan argument can be specified for the verification"},
+  {"search", OPT_KEY_SEARCH, 0, OPTION_ALIAS, 0},
+
+  {0, 0, 0, OPTION_DOC, "Following a -search or -run argument:"},
+  {"bfs", 0, 0, 0, "perform a breadth-first search"},
+  {"bfspar", 0, 0, 0, "perform a parallel breadth-first search"},
+  {"dfspar", 0, 0, 0, "perform a parallel depth-first search, same as -DNCORE=4"},
+  {"bcs", 0, 0, 0, "use the bounded-context-switching algorithm"},
+  {"bitstate", 0, 0, 0, "or -bit, use bitstate storage"},
+  {"biterate", 0, "N,M", 0, "use bitstate with iterative search refinement (-w18..-w35)\n\
+perform N randomized runs and increment -w every M runs\n\
+default value for N is 10, default for M is 1\n\
+(use N,N to keep -w fixed for all runs)\n\
+(add -w to see which commands will be executed)\n\
+(add -W if ./pan exists and need not be recompiled)"},
+  {"swarm", 0, "N,M", 0, "like -biterate, but running all iterations in parallel"},
+  {"link", 0, 0, 0, "file.c link executable pan to file.c"},
+  {"collapse", 0, 0, 0, "use collapse state compression"},
+  {"noreduce", 0, 0, 0, "do not use partial order reduction"},
+  {"hc", 0, 0, 0, "use hash-compact storage"},
+  {"noclaim", 0, 0, 0, "ignore all ltl and never claims"},
+  {"p_permute", 0, 0, 0, "use process scheduling order random permutation"},
+  {"p_rotateN", 0, 0, 0, "use process scheduling order rotation by N"},
+  {"p_reverse", 0, 0, 0, "use process scheduling order reversal"},
+  {"rhash", 0, 0, 0, "randomly pick one of the -p_... options"},
+  {"ltl", 0, 0, 0, "p	verify the ltl property named p"},
+  {"safety", 0, 0, 0, "compile for safety properties only"},
+  {"i", 0, 0, 0, "use the dfs iterative shortening algorithm"},
+  {"a", 0, 0, 0, "search for acceptance cycles"},
+  {"l", 0, 0, 0, "search for non-progress cycles"},
 
 	// printf("\t-S1 and -S2 separate pan source for claim and model\n");
 	// printf("\t-s print send events\n");
-	// printf("\t-T do not indent printf output\n");
-	// printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
-	// printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
-	// printf("\t-uN stop a simulation run after N steps\n");
-	// printf("\t-v verbose, more warnings\n");
-	// printf("\t-w very verbose (when combined with -l or -g)\n");
-	// printf("\t-[XYZ] reserved for use by xspin interface\n");
-	// printf("\t-V print version number and exit\n");
-
-  // argp: An options vector should be terminated by an option with all fields zero
+  {0, 'T', 0, 0, "do not indent printf output"},
+  {0, 't', "[N]", 0, "follow [Nth] simulation trail, see also -k"},
+  {0, 'U', "yyy", 0, "pass -Uyyy to the preprocessor"},
+  {0, 'u', "N", 0, "stop a simulation run after N steps"},
+  {0, 'v', 0, 0, "verbose, more warnings"},
+  {0, 'w', 0, 0, "very verbose (when combined with -l or -g)"},
+  {0, 'X', 0, 0, "reserved for use by xspin interface"},
+  {0, 'Y', 0, OPTION_ALIAS, 0},
+  {0, 'Z', 0, OPTION_ALIAS, 0},
+  {0, 'V', 0, 0, "print version number and exit"},
+
   {0},
 };
 
@@ -910,13 +921,6 @@ getline(char **lineptr, size_t *n, FILE *stream)
 }
 #endif
 
-#define OPT_KEY_RUN 1
-#define OPT_KEY_PRETTY_PRINT 2
-#define OPT_KEY_LTL 3
-#define OPT_KEY_LINK 4
-#define OPT_KEY_REPLAY 5
-#define OPT_KEY_SIMULATE 6
-#define OPT_KEY_SEARCH 7
 
 struct cli_args {
   int export_ast;
@@ -988,7 +992,7 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
     case 'N': args->nvr_file = arg; break;
     case 'n': args->T = atoi(arg); args->tl_terse = 1; break;
     case 'O': args->old_scope_rules = 1; break;
-    case 'o': args->usedopts += optimizations(atoi(arg));
+    case 'o': args->usedopts += optimizations(atoi(arg)); break;
     case 'P': {
       assert(strlen(arg) < sizeof(PreProc));
       strcpy(PreProc, arg);
@@ -1000,6 +1004,7 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
       if (isdigit(arg[0])) {
         qhide(atoi(arg));
       }
+      break;
     }
     case OPT_KEY_RUN: {
       Srand((unsigned int) args->T);
@@ -1062,36 +1067,11 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
   return 0;
 }
 
-static error_t parse_run_opt(int key, char *arg, struct argp_state *state) {
-  struct cli_args *args = state->input;
-
-  switch (key) {
-    case 'D':
-    case 'O':
-    case 'U': add_comptime(arg); break;
-    case 'W': args->norecompile = 1; break;
-    case OPT_KEY_LTL: add_runtime("-N"); add_runtime("ltl"); break;
-    case OPT_KEY_LINK: add_comptime("link"); break;
-    default: add_runtime(arg);
-  }
-
-  return 0;
-}
-
-static int validate_args(const struct cli_args *args) {
-  return 1;
-};
-
-static struct argp_child arg_children[] = {
-  { 0 },
-};
-
 static struct argp argp = { 
   .options = options, 
   .parser = parse_opt,
   .args_doc = args_doc, 
   .doc = doc,
-  .children = arg_children,
 };
 
 int

From 05d2480cfe79a20da4b6ef1c103aa944bf425743 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sat, 19 Oct 2024 16:37:54 -0700
Subject: [PATCH 03/13] feat: Added all the supported flags to the argp options

---
 Src/main.c | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 28e6eee..65cb062 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -627,6 +627,8 @@ preprocess(char *a, char *b, int a_tmp)
 #define OPT_KEY_REPLAY 5
 #define OPT_KEY_SIMULATE 6
 #define OPT_KEY_SEARCH 7
+#define OPT_KEY_S1 8
+#define OPT_KEY_S2 9
 
 // The format for each `argp_option` struct is as follows:
 // 1. The name of the option's long option
@@ -720,8 +722,9 @@ default value for N is 10, default for M is 1\n\
   {"a", 0, 0, 0, "search for acceptance cycles"},
   {"l", 0, 0, 0, "search for non-progress cycles"},
 
-	// printf("\t-S1 and -S2 separate pan source for claim and model\n");
-	// printf("\t-s print send events\n");
+  {"S1", OPT_KEY_S1, 0, 0, "separate pan source for claim and model"},
+  {"S2", OPT_KEY_S2, 0, OPTION_ALIAS, 0},
+  {0, 's', 0, 0, "print send events"},
   {0, 'T', 0, 0, "do not indent printf output"},
   {0, 't', "[N]", 0, "follow [Nth] simulation trail, see also -k"},
   {0, 'U', "yyy", 0, "pass -Uyyy to the preprocessor"},
@@ -983,7 +986,7 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
 		case 'i': args->interactive = 1; break;
 		case 'I': args->inlineonly = 1; break;
 		case 'J': args->like_java = 1; break;
-		case 'j': jumpsteps = atoi(arg); break;
+		case 'j': args->jumpsteps = atoi(arg); break;
     case 'k': args->s_trail = 1; args->trailfilename = arg; break;
     case 'L': args->Strict++; break; /* modified -e */
     case 'l': args->verbose += 2; break;

From 66f1605171f49a603995b302adb91426c05ee194 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 15:09:06 -0700
Subject: [PATCH 04/13] feat: Added support for the last couple of flags, and
 fixed some duplicate argument support

---
 Src/main.c | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 65cb062..b5f8463 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -1009,7 +1009,14 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
       }
       break;
     }
+    case OPT_KEY_SEARCH:
+    case OPT_KEY_REPLAY:
     case OPT_KEY_RUN: {
+      if (key == OPT_KEY_REPLAY) {
+        args->replay = 1;
+        add_runtime("-r");
+      }
+
       Srand((unsigned int) args->T);
       if (args->buzzed != 0) {
         fatal("cannot combine -x with -run -replay or -search", (char *)0);
@@ -1021,14 +1028,10 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
       // TODO: Parse run args here
       break;
     }
-    case OPT_KEY_REPLAY: {
-      args->replay = 1;
-      break;
-    }
     case 'r': args->verbose += 8; break;
-    case 'S': args->separate = atoi(arg); args->analyze = 1; break;
+    case OPT_KEY_S1:
+    case OPT_KEY_S2: args->separate = atoi(arg); args->analyze = 1; break; /* S1 or S2 */
     case OPT_KEY_SIMULATE: break; // ignore
-    case OPT_KEY_SEARCH: break; // samecase
     case 's': args->verbose += 16; break;
     case 'T': args->notabs = 1; break;
     case 't': {

From 1b984c5f75de483aab5a89536ff32607a0947a10 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 15:10:05 -0700
Subject: [PATCH 05/13] feat: Enabled support for long options to be specified
 with a single dash

This is to support backwards-compatibility with the initial programs'
parsing logic
---
 Src/main.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Src/main.c b/Src/main.c
index b5f8463..ba1ed97 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -1096,7 +1096,7 @@ main(int argc, char *argv[])
 
   struct cli_args arguments = { 0 };
 
-  argp_parse(&argp, argc, argv, 0, 0, &arguments);
+  argp_parse(&argp, argc, argv, ARGP_LONG_ONLY, 0, &arguments);
 
 	if (columns == 2 && !cutoff)
 	{	cutoff = 1024;

From 545dea65ba250d5dbfc31b7b125651fa828f9eb7 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 17:04:14 -0700
Subject: [PATCH 06/13] change: Added a helper function for PreArg and improved
 safety

This implements an assertion on a fixed-size buffer, and also replaces
the usage at every other implementation point
---
 Src/main.c | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index ba1ed97..4c9da22 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -93,6 +93,11 @@ static char	*PreArg[64];
 static int	PreCnt = 0;
 static char	out1[64];
 
+void pre_arg_append(char* arg) {
+  assert(PreCnt < sizeof(PreArg));
+  PreArg[PreCnt++] = arg;
+}
+
 char	**trailfilename;	/* new option 'k' */
 
 void	explain(int);
@@ -310,7 +315,7 @@ alldone(int estatus)
 		if (cutoff)
 		{	sprintf(&pan_runtime[strlen(pan_runtime)], "-u%d ", cutoff);
 		}
-		for (i = 1; i <= PreCnt; i++)
+		for (i = 0; i < PreCnt; i++)
 		{	strcat(pan_runtime, PreArg[i]);
 			strcat(pan_runtime, " ");
 		}
@@ -602,7 +607,7 @@ preprocess(char *a, char *b, int a_tmp)
 
 	assert(strlen(PreProc) < sizeof(precmd));
 	strcpy(precmd, PreProc);
-	for (i = 1; i <= PreCnt; i++)
+	for (i = 0; i < PreCnt; i++)
 	{	strcat(precmd, " ");
 		strcat(precmd, PreArg[i]);
 	}
@@ -975,9 +980,10 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
 		case 'b': args->no_print = 1; break;
 		case 'C': args->Caccess = 1; break;
 		case 'c': args->columns = 1; break;
-    case 'D': PreArg[++PreCnt] = arg; break;
+    case 'D':
+    case 'E':
+    case 'U': pre_arg_append(arg); break;
 		case 'd': args->dumptab = 1; break;
-    case 'E': PreArg[++PreCnt] = arg; break;
 		case 'e': args->product++; break; /* see also 'L' */
 		case 'F': args->ltl_file = arg; break;
 		case 'f': args->add_ltl = arg; break;
@@ -1041,7 +1047,6 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
       }
       break;
     }
-    case 'U': PreArg[++PreCnt] = arg; break;
     case 'u': args->cutoff = atoi(arg); break;
     case 'v': args->verbose += 32; break;
     case 'V': printf("%s\n", SpinVersion); break;

From bb0def33d5fa319128460c1c8b3058239899aeb3 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 17:26:41 -0700
Subject: [PATCH 07/13] fix: Correctly pass in the argument names to the
 preprocess arguments

---
 Src/main.c | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 4c9da22..2e4d121 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -11,6 +11,7 @@
 #include <assert.h>
 #include "spin.h"
 #include "version.h"
+#include <string.h>
 #include <sys/types.h>
 #include <sys/stat.h>
 #include <signal.h>
@@ -981,8 +982,17 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
 		case 'C': args->Caccess = 1; break;
 		case 'c': args->columns = 1; break;
     case 'D':
-    case 'E':
-    case 'U': pre_arg_append(arg); break;
+    case 'U': {
+      unsigned long arg_len = strlen(arg);
+      // Allocate enough space for the dash and character, e.g. '-D'
+      char* cli_arg = emalloc(arg_len + 2 + 1);
+      cli_arg[0] = '-';
+      cli_arg[1] = key; // Append a '-D' or '-U'
+      strcpy(cli_arg + 2, arg);
+      pre_arg_append(cli_arg);
+      break;
+    }
+    case 'E': pre_arg_append(arg); break;
 		case 'd': args->dumptab = 1; break;
 		case 'e': args->product++; break; /* see also 'L' */
 		case 'F': args->ltl_file = arg; break;

From 466af98052cd0c7d3ee012f9913cdca9022a42d0 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 22:37:02 -0700
Subject: [PATCH 08/13] fix: Parse the args to -run separately, and convert
 some of the errors

---
 Src/main.c | 58 ++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 48 insertions(+), 10 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 2e4d121..fa2c464 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -737,6 +737,7 @@ default value for N is 10, default for M is 1\n\
   {0, 'u', "N", 0, "stop a simulation run after N steps"},
   {0, 'v', 0, 0, "verbose, more warnings"},
   {0, 'w', 0, 0, "very verbose (when combined with -l or -g)"},
+  {0, 'x', 0, 0, "internal - reserved use"},
   {0, 'X', 0, 0, "reserved for use by xspin interface"},
   {0, 'Y', 0, OPTION_ALIAS, 0},
   {0, 'Z', 0, OPTION_ALIAS, 0},
@@ -969,11 +970,41 @@ struct cli_args {
   int xspin;
   int limited_vis;
   int preprocessonly;
+
+  int parse_run; // Set when parsing the options to -run
 };
 
+static char* prepend_arg(const char c, const char* arg) {
+  char* tmp = emalloc(strlen(arg) + 2 + 1);
+  sprintf(tmp, "-%c%s", c, arg);
+  return tmp;
+}
+
 static error_t parse_opt(int key, char *arg, struct argp_state *state) {
   struct cli_args *args = state->input;
 
+  // Handle the run args separately
+  if (args->parse_run) {
+    switch (key) {
+      case 'D': /* eg -DNP */
+      /*	  case 'E': conflicts with runtime arg */
+      case 'O': /* eg -O2 */
+      case 'U': /* to undefine a macro */
+        add_comptime(prepend_arg(key, arg)); break;
+#if 0
+      case 'w': /* conflicts with bitstate runtime arg */
+      verbose += 64; 
+      break;
+#endif
+      case 'W': args->norecompile = 1; break;
+      case OPT_KEY_LTL: add_runtime("-N"); add_runtime("-ltl"); break; /* prop name */
+      case OPT_KEY_LINK: add_comptime("-link");
+      default: add_runtime(prepend_arg(key, arg)); break; /* -bfs etc. */
+    }
+
+    return 0;
+  }
+
   switch (key) {
 		case 'A': args->export_ast = 1; break;
 		case 'a': args->analyze = 1; break;
@@ -1028,20 +1059,26 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
     case OPT_KEY_SEARCH:
     case OPT_KEY_REPLAY:
     case OPT_KEY_RUN: {
-      if (key == OPT_KEY_REPLAY) {
-        args->replay = 1;
-        add_runtime("-r");
+      switch (key) {
+        case OPT_KEY_RUN: {
+          Srand((unsigned int) args->T);
+        }
+        case OPT_KEY_REPLAY: {
+          args->replay = 1;
+          add_runtime("-r");
+        }
       }
 
-      Srand((unsigned int) args->T);
       if (args->buzzed != 0) {
-        fatal("cannot combine -x with -run -replay or -search", (char *)0);
+        argp_failure(state, 1, 0, "cannot combine -x with -run -replay or -search");
+        return EINVAL;
       }
 
-      buzzed = 2;
-      analyze = 1;
+      args->buzzed = 2;
+      args->analyze = 1;
 
-      // TODO: Parse run args here
+      // Handle future args as passed into the run command
+      args->parse_run = 1;
       break;
     }
     case 'r': args->verbose += 8; break;
@@ -1063,8 +1100,9 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
     case 'w': args->verbose += 64; break;
     case 'W': args->norecompile = 1; break; /* 6.4.7: for swarm/biterate */
     case 'x': { /* internal - reserved use */
-      if (buzzed != 0) {
-        fatal("cannot combine -x with -run -search or -replay", (char *)0);
+      if (args->buzzed != 0) {
+        argp_failure(state, 1, 0, "cannot combine -x with -run -search or -replay");
+        return EINVAL;
       }
       args->buzzed = 1; /* implies also -a -o3 */
       args->pan_runtime = "-d";

From a79f91d08e4c76c9f83ae6505fe3d5f25af25aff Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 22:40:52 -0700
Subject: [PATCH 09/13] change: Replaced manual code with helper function to
 prepend args

---
 Src/main.c | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index fa2c464..d29919c 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -1013,16 +1013,7 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
 		case 'C': args->Caccess = 1; break;
 		case 'c': args->columns = 1; break;
     case 'D':
-    case 'U': {
-      unsigned long arg_len = strlen(arg);
-      // Allocate enough space for the dash and character, e.g. '-D'
-      char* cli_arg = emalloc(arg_len + 2 + 1);
-      cli_arg[0] = '-';
-      cli_arg[1] = key; // Append a '-D' or '-U'
-      strcpy(cli_arg + 2, arg);
-      pre_arg_append(cli_arg);
-      break;
-    }
+    case 'U': pre_arg_append(prepend_arg(key, arg)); break;
     case 'E': pre_arg_append(arg); break;
 		case 'd': args->dumptab = 1; break;
 		case 'e': args->product++; break; /* see also 'L' */

From d8585ad32a7be52935fc4680a7f7f1771481aab7 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 22:50:54 -0700
Subject: [PATCH 10/13] change: Changed all args to use the global versions of
 themselves

---
 Src/main.c | 149 +++++++++++++++++++++++------------------------------
 1 file changed, 65 insertions(+), 84 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index d29919c..51c2142 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -933,44 +933,8 @@ getline(char **lineptr, size_t *n, FILE *stream)
 
 
 struct cli_args {
-  int export_ast;
-  int analyze;
-  int no_wrapup;
-  int no_print;
-  int Caccess;
-  int columns;
-  int dumptab;
-  int product;
-  char* ltl_file;
-  char* add_ltl;
-  int verbose;
-  int seedy;
-  int interactive;
-  int inlineonly;
-  int like_java;
-  // TODO: Validate the types of these variables
-  int jumpsteps;
-  int s_trail;
-  char* trailfilename;
-  int Strict;
-  int m_loss;
   int T;
-  char* nvr_file;
-  int old_scope_rules;
-  int tl_terse;
   int usedopts;
-  int buzzed;
-  int norecompile;
-  int replay;
-  int separate;
-  int notabs;
-  int ntrail;
-  int cutoff;
-  char* pan_runtime;
-  int xspin;
-  int limited_vis;
-  int preprocessonly;
-
   int parse_run; // Set when parsing the options to -run
 };
 
@@ -996,7 +960,7 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
       verbose += 64; 
       break;
 #endif
-      case 'W': args->norecompile = 1; break;
+      case 'W': norecompile = 1; break;
       case OPT_KEY_LTL: add_runtime("-N"); add_runtime("-ltl"); break; /* prop name */
       case OPT_KEY_LINK: add_comptime("-link");
       default: add_runtime(prepend_arg(key, arg)); break; /* -bfs etc. */
@@ -1006,40 +970,57 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
   }
 
   switch (key) {
-		case 'A': args->export_ast = 1; break;
-		case 'a': args->analyze = 1; break;
-		case 'B': args->no_wrapup = 1; break;
-		case 'b': args->no_print = 1; break;
-		case 'C': args->Caccess = 1; break;
-		case 'c': args->columns = 1; break;
+		case 'A': export_ast = 1; break;
+		case 'a': analyze = 1; break;
+		case 'B': no_wrapup = 1; break;
+		case 'b': no_print = 1; break;
+		case 'C': Caccess = 1; break;
+		case 'c': columns = 1; break;
     case 'D':
     case 'U': pre_arg_append(prepend_arg(key, arg)); break;
     case 'E': pre_arg_append(arg); break;
-		case 'd': args->dumptab = 1; break;
-		case 'e': args->product++; break; /* see also 'L' */
-		case 'F': args->ltl_file = arg; break;
-		case 'f': args->add_ltl = arg; break;
-		case 'g': args->verbose +=  1; break;
-		case 'h': args->seedy = 1; break;
-		case 'i': args->interactive = 1; break;
-		case 'I': args->inlineonly = 1; break;
-		case 'J': args->like_java = 1; break;
-		case 'j': args->jumpsteps = atoi(arg); break;
-    case 'k': args->s_trail = 1; args->trailfilename = arg; break;
-    case 'L': args->Strict++; break; /* modified -e */
-    case 'l': args->verbose += 2; break;
-    case 'M': args->columns = 2; break;
-    case 'm': args->m_loss = 1; break;
-    case 'N': args->nvr_file = arg; break;
-    case 'n': args->T = atoi(arg); args->tl_terse = 1; break;
-    case 'O': args->old_scope_rules = 1; break;
+    case 'd': dumptab = 1; break;
+    case 'e': product++; break; /* see also 'L' */
+    case 'F': {
+      ltl_file = &state->argv[state->next];
+      state->next = state->argc;
+      break;
+    }
+		case 'f': {
+      add_ltl = &state->argv[state->next];
+      state->next = state->argc;
+      break;
+    }
+    case 'g': verbose +=  1; break;
+    case 'h': seedy = 1; break;
+    case 'i': interactive = 1; break;
+    case 'I': inlineonly = 1; break;
+    case 'J': like_java = 1; break;
+    case 'j': jumpsteps = atoi(arg); break;
+    case 'k': {
+      s_trail = 1;
+      trailfilename = &state->argv[state->next];
+      state->next = state->argc;
+      break;
+    }
+    case 'L': Strict++; break; /* modified -e */
+    case 'l': verbose += 2; break;
+    case 'M': columns = 2; break;
+    case 'm': m_loss = 1; break;
+    case 'N': {
+      nvr_file = &state->argv[state->next];
+      state->next = state->argc;
+      break;
+    }
+    case 'n': args->T = atoi(arg); tl_terse = 1; break;
+    case 'O': old_scope_rules = 1; break;
     case 'o': args->usedopts += optimizations(atoi(arg)); break;
     case 'P': {
       assert(strlen(arg) < sizeof(PreProc));
       strcpy(PreProc, arg);
       break;
     }
-    case 'p': args->verbose += 4; break;
+    case 'p': verbose += 4; break;
     case OPT_KEY_PRETTY_PRINT: pretty_print(); break;
     case 'q': {
       if (isdigit(arg[0])) {
@@ -1055,61 +1036,61 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
           Srand((unsigned int) args->T);
         }
         case OPT_KEY_REPLAY: {
-          args->replay = 1;
+          replay = 1;
           add_runtime("-r");
         }
       }
 
-      if (args->buzzed != 0) {
+      if (buzzed != 0) {
         argp_failure(state, 1, 0, "cannot combine -x with -run -replay or -search");
         return EINVAL;
       }
 
-      args->buzzed = 2;
-      args->analyze = 1;
+      buzzed = 2;
+      analyze = 1;
 
       // Handle future args as passed into the run command
       args->parse_run = 1;
       break;
     }
-    case 'r': args->verbose += 8; break;
+    case 'r': verbose += 8; break;
     case OPT_KEY_S1:
-    case OPT_KEY_S2: args->separate = atoi(arg); args->analyze = 1; break; /* S1 or S2 */
+    case OPT_KEY_S2: separate = atoi(arg); analyze = 1; break; /* S1 or S2 */
     case OPT_KEY_SIMULATE: break; // ignore
-    case 's': args->verbose += 16; break;
-    case 'T': args->notabs = 1; break;
+    case 's': verbose += 16; break;
+    case 'T': notabs = 1; break;
     case 't': {
-      args->s_trail = 1;
+      s_trail = 1;
       if (isdigit(arg[0])) {
-        args->ntrail = atoi(arg);
+        ntrail = atoi(arg);
       }
       break;
     }
-    case 'u': args->cutoff = atoi(arg); break;
-    case 'v': args->verbose += 32; break;
-    case 'V': printf("%s\n", SpinVersion); break;
-    case 'w': args->verbose += 64; break;
-    case 'W': args->norecompile = 1; break; /* 6.4.7: for swarm/biterate */
+    case 'u': cutoff = atoi(arg); break;
+    case 'v': verbose += 32; break;
+    case 'V': printf("%s\n", SpinVersion); alldone(0); break;
+    case 'w': verbose += 64; break;
+    case 'W': norecompile = 1; break; /* 6.4.7: for swarm/biterate */
     case 'x': { /* internal - reserved use */
-      if (args->buzzed != 0) {
+      if (buzzed != 0) {
         argp_failure(state, 1, 0, "cannot combine -x with -run -search or -replay");
         return EINVAL;
       }
-      args->buzzed = 1; /* implies also -a -o3 */
-      args->pan_runtime = "-d";
-      args->analyze = 1;
+      buzzed = 1; /* implies also -a -o3 */
+      pan_runtime = "-d";
+      analyze = 1;
       args->usedopts += optimizations('3');
       break;
     }
     case 'X': {
-      args->xspin = args->notabs = 1;
+      xspin = notabs = 1;
 #ifndef PC
     signal(SIGPIPE, alldone); /* not posix */
 #endif
       break;
     }
-    case 'Y': args->limited_vis = 1; break; /* used by xspin */
-    case 'Z': args->preprocessonly = 1; break; /* used by xspin */
+    case 'Y': limited_vis = 1; break; /* used by xspin */
+    case 'Z': preprocessonly = 1; break; /* used by xspin */
     default:
       return ARGP_ERR_UNKNOWN;
   }

From 3b65a101be16ddfc8be9b358bb23259ad1e3d8d2 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Sun, 20 Oct 2024 22:54:09 -0700
Subject: [PATCH 11/13] fix: Pass correct arguments into cli parsing

---
 Src/main.c | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 51c2142..40010cd 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -1108,8 +1108,6 @@ static struct argp argp = {
 int
 main(int argc, char *argv[])
 {	Symbol *s;
-	int T = (int) time((time_t *)0);
-	int usedopts = 0;
 
 	yyin  = stdin;
 	yyout = stdout;
@@ -1119,10 +1117,17 @@ main(int argc, char *argv[])
 	assert(strlen(CPP) < sizeof(PreProc));
 	strcpy(PreProc, CPP);
 
-  struct cli_args arguments = { 0 };
+  struct cli_args arguments = {
+    .parse_run = 0,
+    .T = (int) time((time_t *)0),
+    .usedopts = 0,
+  };
 
   argp_parse(&argp, argc, argv, ARGP_LONG_ONLY, 0, &arguments);
 
+  int T = arguments.T;
+  int usedopts = arguments.usedopts;
+
 	if (columns == 2 && !cutoff)
 	{	cutoff = 1024;
 	}

From 952a45938c1a922a15aeaa155bbc88e31db1d825 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Mon, 21 Oct 2024 00:55:59 -0700
Subject: [PATCH 12/13] fix: Removed experimental enum for verbosity level

---
 Src/main.c | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 40010cd..8897ffd 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -746,16 +746,6 @@ default value for N is 10, default for M is 1\n\
   {0},
 };
 
-enum opt_level {
-  OPT_LEVEL_DATAFLOW,
-  OPT_LEVEL_DEAD_VARIABLE_ELIM,
-  OPT_LEVEL_STATEMENT_MERGING,
-  OPT_LEVEL_RV_MERGING,
-  OPT_LEVEL_CASE_CACHING,
-  OPT_OLD_PRIO_RULES,
-  OPT_NO_IMPLIES_SEMIS,
-};
-
 int
 optimizations(int nr)
 {

From b9f756ccf1fcb367ce286703ae834b23560d8ff1 Mon Sep 17 00:00:00 2001
From: Nicholas Novak <34256932+NickyBoy89@users.noreply.github.com>
Date: Mon, 21 Oct 2024 01:19:12 -0700
Subject: [PATCH 13/13] fix: Fixed a minor issue in parsing the optimizations,
 and improved error handling

---
 Src/main.c | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Src/main.c b/Src/main.c
index 8897ffd..2416c07 100644
--- a/Src/main.c
+++ b/Src/main.c
@@ -796,9 +796,7 @@ optimizations(int nr)
 		printf("spin: no implied semi-colons (pre version 6.3)\n");
 		return 0; /* no break */
 	default:
-		printf("spin: bad or missing parameter on -o\n");
-		// usage();
-		break;
+    return -1;
 	}
 	return 1;
 }
@@ -1004,7 +1002,13 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state) {
     }
     case 'n': args->T = atoi(arg); tl_terse = 1; break;
     case 'O': old_scope_rules = 1; break;
-    case 'o': args->usedopts += optimizations(atoi(arg)); break;
+    case 'o': {
+      args->usedopts += optimizations(arg[0]);
+      if (args->usedopts == -1) {
+        argp_failure(state, 0, 1, "bad or missing parameter on -o: %c", arg[0]);
+        return EINVAL;
+      }
+      break;
     case 'P': {
       assert(strlen(arg) < sizeof(PreProc));
       strcpy(PreProc, arg);