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