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 ("attackid); printf (">\n"); xmlindent++;