diff --git a/src/arachne.c b/src/arachne.c index 412686d..3ea7d1f 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1329,7 +1329,7 @@ prune_claim_specifics () { if (current_claim->type == CLAIM_Niagree) { - if (arachne_claim_niagree (sys, current_claim->r, current_claim->ev)) + if (arachne_claim_niagree (sys, 0, current_claim->ev)) { current_claim->count = statesIncrease (current_claim->count); if (sys->output == PROOF) @@ -1342,7 +1342,7 @@ prune_claim_specifics () } if (current_claim->type == CLAIM_Nisynch) { - if (arachne_claim_nisynch (sys, current_claim->r, current_claim->ev)) + if (arachne_claim_nisynch (sys, 0, current_claim->ev)) { current_claim->count = statesIncrease (current_claim->count); if (sys->output == PROOF) @@ -1402,16 +1402,14 @@ 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 (); - if (sys->output == ATTACK) - printSemiState (); - } + + /** + * By the way the claim is handled, this automatically means a flaw. + */ + count_false (); + if (sys->output == ATTACK) + printSemiState (); + return flag; } diff --git a/src/claim.c b/src/claim.c index b509553..dfa3dcc 100644 --- a/src/claim.c +++ b/src/claim.c @@ -3,6 +3,7 @@ #include "system.h" #include "label.h" #include "error.h" +#include "debug.h" #define MATCH_NONE 0 #define MATCH_ORDER 1 @@ -12,6 +13,8 @@ #define LABEL_GOOD -3 #define LABEL_TODO -2 +extern int globalError; + // Debugging the NI-SYNCH checks //#define OKIDEBUG @@ -477,6 +480,15 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs Termlist labels; int flag; +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Checking runs agreement for Arachne.\n"); + termmapPrint (runs); + eprintf ("\n"); + } +#endif + flag = 1; labels = cl->prec; while (flag && labels != NULL) @@ -492,7 +504,25 @@ int arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs int i; int run; - run = termmapGet (runs, label); + run = termmapGet (runs, role); +#ifdef DEBUG + if (run < 0 || run >= sys->maxruns ) + { + globalError++; + eprintf ("Run mapping %i out of bounds for role ", run); + termPrint (role); + eprintf (" and label "); + termPrint (label); + eprintf ("\n"); + eprintf ("This label has sendrole "); + termPrint (linfo->sendrole); + eprintf (" and readrole "); + termPrint (linfo->readrole); + eprintf ("\n"); + globalError--; + error ("Run mapping is out of bounds."); + } +#endif rd = sys->runs[run].start; rd_res = NULL; i = 0; @@ -559,11 +589,12 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai else { // Choose a run for this role, if possible + // Note that any will do int run, flag; run = 0; - flag = 1; - while (flag && run < sys->maxruns) + flag = 0; + while (run < sys->maxruns) { // Has to be from the right protocol if (sys->runs[run].protocol == cl->protocol) @@ -573,7 +604,7 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai { // Choose, iterate runs_involved = termmapSet (runs_involved, roles_tofill->term, run); - flag = flag && fill_roles (roles_tofill->next); + flag = flag || fill_roles (roles_tofill->next); } } run++; @@ -582,6 +613,13 @@ int arachne_claim_niagree (const System sys, const int claim_run, const int clai } } +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Testing for Niagree claim with any sort of runs.\n"); + } +#endif + rd = roledef_shift (sys->runs[claim_run].start, claim_index); #ifdef DEBUG if (rd == NULL)