From 9cf3bf3da32f214c05ec36dc79d0e84e32e13cae Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 11 Aug 2004 09:51:17 +0000
Subject: [PATCH] - Setup main arachne infrastructure.

---
 src/arachne.c | 16 ++++++++++++++++
 src/arachne.h |  8 ++++++++
 src/main.c    | 21 ++++++++++++++++++---
 src/system.c  |  1 +
 4 files changed, 43 insertions(+), 3 deletions(-)
 create mode 100644 src/arachne.c
 create mode 100644 src/arachne.h

diff --git a/src/arachne.c b/src/arachne.c
new file mode 100644
index 0000000..2aa6316
--- /dev/null
+++ b/src/arachne.c
@@ -0,0 +1,16 @@
+/**
+ *@file arachne.c
+ *
+ * Introduces a method for proofs akin to the Athena modelchecker
+ * http://www.ece.cmu.edu/~dawnsong/athena/
+ *
+ */
+
+#include "system.h"
+#include "arachne.h"
+
+//! Main recursive procedure for Arachne
+int
+arachne (const System sys)
+{
+}
diff --git a/src/arachne.h b/src/arachne.h
new file mode 100644
index 0000000..410f3f5
--- /dev/null
+++ b/src/arachne.h
@@ -0,0 +1,8 @@
+#ifndef ARACHNE
+#define ARACHNE
+
+#include "system.h"
+
+int arachne (const System sys);
+
+#endif
diff --git a/src/main.c b/src/main.c
index 522f1ec..cb6932f 100644
--- a/src/main.c
+++ b/src/main.c
@@ -87,6 +87,8 @@ main (int argc, char **argv)
     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_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,
@@ -166,6 +168,7 @@ main (int argc, char **argv)
     switch_echo,
     switch_progress_bar,
 
+    switch_arachne,
     switch_check,
     switch_traversal_method,
     switch_match_method,
@@ -333,8 +336,10 @@ main (int argc, char **argv)
    */
 
   sys = systemInit ();
-  /* select default engine */
-  sys->engine = POR_ENGINE;
+  if (switch_arachne->count > 0)
+    {
+      sys->engine = ARACHNE_ENGINE;
+    }
   /* init compiler for this system */
   compilerInit (sys);
 
@@ -892,7 +897,17 @@ modelCheck (const System sys)
     }
 
   /* modelcheck the system */
-  traverse (sys);
+  switch (sys->engine)
+    {
+    case POR_ENGINE:
+      traverse (sys);
+      break;
+    case ARACHNE_ENGINE:
+      arachne (sys);
+      break;
+    default:
+      error ("Unknown engine type %i.", sys->engine);
+    }
 
   /* clean up any states display */
   if (sys->switchS > 0)
diff --git a/src/system.c b/src/system.c
index 714c2d0..5e5f431 100644
--- a/src/system.c
+++ b/src/system.c
@@ -54,6 +54,7 @@ systemInit ()
   sys->attack = tracebufInit ();
 
   /* switches */
+  sys->engine = POR_ENGINE;	// default is partial ordering engine
   sys->output = ATTACK;		// default is to show the attacks
   sys->porparam = 0;		// multi-purpose parameter
   sys->latex = 0;		// latex output?