From 410a35f4f4675616d56d718f9afac2e9f831c3d8 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 13 Jul 2004 09:36:30 +0000 Subject: [PATCH] - Fixed bug in attack output. - Re-enabled the noreport switch. --- src/modelchecker.c | 1 - src/output.c | 5 ++++- src/runs.c | 1 - src/runs.h | 4 +--- 4 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/modelchecker.c b/src/modelchecker.c index 4fc3760..730e238 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -105,7 +105,6 @@ traverse (const System sys) int executeStep (const System sys, const int run) { - unsigned long int parentBuffer; Roledef runPoint; runPoint = runPointerGet (sys, run); #ifdef DEBUG diff --git a/src/output.c b/src/output.c index 6cfda8e..af513f8 100644 --- a/src/output.c +++ b/src/output.c @@ -481,6 +481,9 @@ attackDisplayAscii (System sys) void attackDisplay (System sys) { + if (!sys->report) + return; + if (sys->latex) { attackDisplayLatex (sys); @@ -575,7 +578,7 @@ void graphPath (const System sys, const char* params) i = 0; while (i < sys->step) { - printf ("\tn%i [%s]\n", sys->traceNode[i], params); + printf ("\tn%li [%s];\n", sys->traceNode[i], params); i++; } } diff --git a/src/runs.c b/src/runs.c index ab27f84..e4a8aa3 100644 --- a/src/runs.c +++ b/src/runs.c @@ -109,7 +109,6 @@ systemReset (const System sys) /* some initial counters */ sys->statesLow = 0; // number of explored states sys->statesHigh = 0; // this is not as ridiculous as it might seem - sys->parentState = 0; sys->explore = 1; // do explore the space sys->claims = 0; // number of claims encountered sys->failed = 0; // number of failed claims diff --git a/src/runs.h b/src/runs.h index 6769eb3..b02b339 100644 --- a/src/runs.h +++ b/src/runs.h @@ -229,8 +229,6 @@ struct system unsigned long int claims; //!< Number of claims encountered. unsigned long int failed; //!< Number of claims failed. - unsigned long int parentState; //!< Parent state number - /* matching */ int match; //!< Matching type. int clp; //!< Do we use clp? @@ -250,7 +248,7 @@ struct system Roledef *traceEvent; //!< Trace roledefs: MaxRuns * maxRoledef int *traceRun; //!< Trace run ids: MaxRuns * maxRoledef Knowledge *traceKnow; //!< Trace intruder knowledge: Maxruns * maxRoledef - unsigned long int *traceNode; //!< Trace node traversal + unsigned long int *traceNode; //!< Trace node traversal: Maxruns * maxRoledef /* POR reduction assistance */ int PORphase; //!< -1: init (all sends), 0...: recurse reads