From 1331f5e7a3b5fd5ed88cf64661b79db64a7b939b Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 7 Jun 2005 13:40:56 +0000
Subject: [PATCH] - Added a global attack id, starting at one. Currently only
 shown in   XML and Dot output. For Dot, it is included in the label. For XML,
 it   is an added attribute of the 'attack' tag.

---
 src/arachne.c      | 6 +++++-
 src/modelchecker.c | 1 +
 src/system.c       | 1 +
 src/system.h       | 1 +
 src/xmlout.c       | 2 ++
 5 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/arachne.c b/src/arachne.c
index f8b3508..8fc058a 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1427,7 +1427,7 @@ dotSemiState ()
   // Open graph
   attack_number++;
   eprintf ("digraph semiState%i {\n", attack_number);
-  eprintf ("\tlabel = \"Protocol ");
+  eprintf ("\tlabel = \"[Id %i] Protocol ", sys->attackid);
   p = (Protocol) sys->current_claim->protocol;
   termPrint (p->nameterm);
   eprintf (", role ");
@@ -3066,9 +3066,13 @@ add_claim_specifics (const Claimlist cl, const Roledef rd)
 }
 
 //! Count a false claim
+/**
+ * Counts global attacks as well as claim instances.
+ */
 void
 count_false ()
 {
+  sys->attackid++;
   sys->current_claim->failed = statesIncrease (sys->current_claim->failed);
 }
 
diff --git a/src/modelchecker.c b/src/modelchecker.c
index a467393..5c21d58 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -1239,6 +1239,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   flag = 1;
 
   /* Count the violations */
+  sys->attackid++;
   sys->failed = statesIncrease (sys->failed);
   clinfo = sys->traceEvent[claimev]->claiminfo;
   clinfo->failed = statesIncrease (clinfo->failed);	// note: for modelchecking secrecy, this can lead to more fails (at further events in branches of the tree) than claim encounters
diff --git a/src/system.c b/src/system.c
index 3b21451..40f8c7e 100644
--- a/src/system.c
+++ b/src/system.c
@@ -104,6 +104,7 @@ systemInit ()
   sys->claimlist = NULL;
   sys->labellist = NULL;
   sys->match = 0;		// default matching
+  sys->attackid = 0;		// First attack will have id 1, because the counter is increased before any attacks are displayed.
 
   /* matching CLP */
   sys->constraints = NULL;	// no initial constraints
diff --git a/src/system.h b/src/system.h
index 91552e6..ea01969 100644
--- a/src/system.h
+++ b/src/system.h
@@ -163,6 +163,7 @@ struct system
   states_t interval;		//!< Used to update state printing at certain intervals
   states_t claims;		//!< Number of claims encountered.
   states_t failed;		//!< Number of claims failed.
+  int attackid;			//!< Global counter of attacks (used for assigning identifiers) within this Scyther call.
   int countScenario;		//!< Number of scenarios skipped.
 
   /* matching */
diff --git a/src/xmlout.c b/src/xmlout.c
index fbecbae..87fee45 100644
--- a/src/xmlout.c
+++ b/src/xmlout.c
@@ -752,6 +752,8 @@ xmlOutSemitrace (const System sys)
   printf ("<attack");
   /* add trace length attribute */
   printf (" tracelength=\"%i\"", get_semitrace_length ());
+  /* add attack id attribute (within this scyther call) */
+  printf (" id=\"%i\"", sys->attackid);
   printf (">\n");
   xmlindent++;