From 85ac32fbd1b6767e2349d1649a2e137643c43d97 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 18 Aug 2004 20:22:33 +0000
Subject: [PATCH] - Claim counting now works.

---
 src/arachne.c | 42 ++++++++++++++++++++++++++++++++++--------
 1 file changed, 34 insertions(+), 8 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 0972221..e51b5fc 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -28,6 +28,8 @@ extern Term TERM_Agent;
 extern Term TERM_Hidden;
 
 static System sys;
+static Claimlist current_claim;
+
 Protocol INTRUDER;		// Pointers, to be set by the Init
 Role I_M;			// Same here.
 Role I_F;
@@ -953,10 +955,39 @@ add_claim_specifics (const Claimlist cl, const Roledef rd)
     }
 }
 
+//! Count a false claim
+void
+count_false ()
+{
+  current_claim->failed = statesIncrease (current_claim->failed);
+}
+
 //------------------------------------------------------------------------
 // Main logic core
 //------------------------------------------------------------------------
 
+//! Check properties
+int
+property_check ()
+{
+  int flag;
+
+  flag = 1;
+  if (current_claim->type == CLAIM_Secret)
+    {
+      // Secrecy claim
+      /**
+       * By the way the claim is handled, this automatically means a flaw.
+       */
+      count_false ();
+#ifdef DEBUG
+      if (DEBUGL (3))
+	  printSemiState();
+#endif
+    }
+  return flag;
+}
+
 //! Main recursive procedure for Arachne
 int
 iterate ()
@@ -1014,13 +1045,8 @@ iterate ()
 	   * all goals bound, check for property
 	   */
 	  sys->claims = statesIncrease (sys->claims);
-#ifdef DEBUG
-	  if (DEBUGL (3))
-	    {
-	      printSemiState ();
-	    }
-#endif
-	  //!@todo Property check in Arachne.
+	  current_claim->count = statesIncrease (current_claim->count);
+	  flag = flag && property_check ();
 	}
       else
 	{
@@ -1129,7 +1155,7 @@ arachne ()
 	  e_term2 = NULL;
 	  e_term3 = NULL;
 #endif
-
+          current_claim = cl;
 	  p = (Protocol) cl->protocol;
 	  r = (Role) cl->role;
 #ifdef DEBUG