From 7ce5736af3b0314a7cb8846f3c164bf8c84cbd85 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 21 Jul 2004 14:26:28 +0000 Subject: [PATCH] - Added attack script. - Worked on ni-synch claims. Todo: weirdness with: ./scyther ../spdl/nsl3-nisynch.spdl -t1 -r2 --- src/claims.c | 33 ++++++++++++++++++++++++--------- src/runs.c | 8 ++++---- src/runs.h | 4 ++-- src/{testl => scytherat} | 6 +++--- src/termmaps.c | 16 ++++++++++++++++ src/termmaps.h | 1 + src/terms.c | 4 ++-- src/terms.h | 4 ++-- 8 files changed, 54 insertions(+), 22 deletions(-) rename src/{testl => scytherat} (87%) diff --git a/src/claims.c b/src/claims.c index 307ef47..e8c8009 100644 --- a/src/claims.c +++ b/src/claims.c @@ -25,10 +25,10 @@ events_match (const System sys, const int i, const int j) rdi = sys->traceEvent[i]; rdj = sys->traceEvent[j]; - if (isTermEqual (rdi->message, rdj->message) && - isTermEqual (rdi->from, rdj->from) && - isTermEqual (rdi->to, rdj->to) && - isTermEqual (rdi->label, rdj->label) && + if ((isTermEqual (rdi->message, rdj->message)) && + (isTermEqual (rdi->from, rdj->from)) && + (isTermEqual (rdi->to, rdj->to)) && + (isTermEqual (rdi->label, rdj->label)) && !(rdi->internal || rdj->internal)) { if (rdi->type == SEND && rdj->type == READ) @@ -61,7 +61,7 @@ int oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) { // Check for completed trace - if (i == -1) + if (i < 0) { // Are all labels well linked? Termmap gscan; @@ -130,7 +130,6 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) int result; int rid2; Term rolename; - Termmap gscan; /* * Two options: it is either involved or not @@ -142,6 +141,7 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) rid2 = termmapGet (f, rolename); if (rid2 == -1 || rid2 == rid) { + Termmap gscan; // Was not involved yet in a registerd way, or was the correct rid gscan = g; while (!result && gscan != NULL) @@ -159,7 +159,7 @@ oki_nisynch (const System sys, const int i, const Termmap f, const Termmap g) fbuf = termmapSet (fbuf, rolename, rid); gbuf = termmapDuplicate (g); gbuf = termmapSet (gbuf, rd->label, -3); - result = oki_nisynch (sys, i-1, fbuf, gbuf) || result; + result = oki_nisynch (sys, i-1, fbuf, gbuf); termmapDelete (gbuf); termmapDelete (fbuf); } @@ -198,7 +198,7 @@ check_claim_nisynch (const System sys, const int i) rid = sys->traceRun[i]; rd = sys->traceEvent[i]; cl = rd->claiminfo; - cl->count++; + cl->count = statesIncrease (cl->count); f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid); // map all labels in prec to LABEL_TODO @@ -217,7 +217,22 @@ check_claim_nisynch (const System sys, const int i) result = oki_nisynch(sys, i, f, g); if (!result) { - cl->failed++; + cl->failed = statesIncrease (cl->failed); + +//#ifdef DEBUG + warning ("Claim has failed!"); + printf ("To be exact, claim label "); + termPrint (cl->label); + printf (" with prec set "); + termlistPrint (cl->prec); + printf ("\n"); + printf ("i: %i\nf: ",i); + termmapPrint (f); + printf ("\ng: "); + termmapPrint (g); + printf ("\n"); +//#endif + } termmapDelete (f); termmapDelete (g); diff --git a/src/runs.c b/src/runs.c index a921727..e73e89f 100644 --- a/src/runs.c +++ b/src/runs.c @@ -113,16 +113,16 @@ systemReset (const System sys) Claimlist cl; /* some initial counters */ - sys->states = STATES0; - sys->interval = STATES0; + sys->states = statesIncrease (STATES0); //!< Initial state is not explored, so start counting at 1 + sys->interval = statesIncrease (STATES0); //!< To keep in line with the states sys->claims = STATES0; sys->failed = STATES0; sys->explore = 1; // do explore the space cl = sys->claimlist; while (cl != NULL) { - cl->count = 0; - cl->failed = 0; + cl->count = STATES0; + cl->failed = STATES0; cl = cl->next; } diff --git a/src/runs.h b/src/runs.h index 2d7193a..4fa3707 100644 --- a/src/runs.h +++ b/src/runs.h @@ -23,9 +23,9 @@ struct claimlist //! The name of the role in which it occurs. Term rolename; //! Number of occurrences in system exploration. - int count; + states_t count; //! Number of occurrences that failed. - int failed; + states_t failed; int r; //!< role number for mapping int ev; //!< event index in role //! Preceding label list diff --git a/src/testl b/src/scytherat similarity index 87% rename from src/testl rename to src/scytherat index ec5544e..fc73d2f 100755 --- a/src/testl +++ b/src/scytherat @@ -5,7 +5,7 @@ # # Usage example: # -# ./testl ns3 +# ./scytherat ns3 # file=../spdl/$1.spdl @@ -19,10 +19,10 @@ then latex $template.tex mv $template.dvi attack.dvi - dvips attack.dvi -o attack.ps + #dvips attack.dvi -o attack.ps # also eps output now - ps2eps -f attack.ps + #ps2eps -f attack.ps xdvi attack.dvi # for Xdvi # kdvi attack.dvi # for KDE environment diff --git a/src/termmaps.c b/src/termmaps.c index 78a7ef0..4d4d8d7 100644 --- a/src/termmaps.c +++ b/src/termmaps.c @@ -105,3 +105,19 @@ termmapDelete (const Termmap f) memFree (f, sizeof (struct termmap)); } } + +//! Print a function +void termmapPrint (Termmap f) +{ + if (f != NULL) + { + printf ("\""); + termPrint (f->term); + printf ("\" -> %i", f->result); + if (f->next != NULL) + { + printf (", "); + termmapPrint (f->next); + } + } +} diff --git a/src/termmaps.h b/src/termmaps.h index 98d32ad..8138abf 100644 --- a/src/termmaps.h +++ b/src/termmaps.h @@ -26,5 +26,6 @@ int termmapGet (Termmap f, const Term x); Termmap termmapSet (const Termmap f, const Term x, const int y); Termmap termmapDuplicate (const Termmap f); void termmapDelete (const Termmap f); +void termmapPrint (Termmap f); #endif diff --git a/src/terms.c b/src/terms.c index b21fc92..8d79e2b 100644 --- a/src/terms.c +++ b/src/terms.c @@ -166,7 +166,8 @@ hasTermVariable (Term term) } } -#ifdef DEBUG +//! Safe wrapper for isTermEqual + int isTermEqualDebug (Term t1, Term t2) { int test1, test2; @@ -187,7 +188,6 @@ int isTermEqualDebug (Term t1, Term t2) } return test1; } -#endif //!Tests whether two terms are completely identical. /** diff --git a/src/terms.h b/src/terms.h index deb97e5..b965785 100644 --- a/src/terms.h +++ b/src/terms.h @@ -102,7 +102,7 @@ int isTermEqualDebug (Term t1, Term t2); ) #define isTermEqual2(t1,t2) ((substVar(t1) || substVar(t2)) \ - ? isTermEqual1(t1,t2) \ + ? isTermEqualFn(t1,t2) \ : ( \ (t1 == t2) \ ? 1 \ @@ -125,7 +125,7 @@ int isTermEqualDebug (Term t1, Term t2); ) #define isTermEqual3(t1,t2) ((substVar(t1) || substVar(t2)) \ - ? isTermEqual2(t1,t2) \ + ? isTermEqualFn(t1,t2) \ : ( \ (t1 == t2) \ ? 1 \