From de1d114f864443807850a936b5b2626357088564 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 21 Jul 2004 10:35:39 +0000 Subject: [PATCH] - Much work on the new states counter abstractions. --- src/main.c | 23 +++++++++++++++-------- src/modelchecker.c | 26 +++++++++----------------- src/output.c | 33 +++++++++++++++++++++++---------- src/runs.c | 38 +++++++++----------------------------- src/runs.h | 11 ++++++----- src/states.c | 40 ++++++++++++++++++++++++++++++++++++++++ src/states.h | 20 ++++++++++++++++++++ 7 files changed, 122 insertions(+), 69 deletions(-) create mode 100644 src/states.c create mode 100644 src/states.h diff --git a/src/main.c b/src/main.c index dd8f65b..816014c 100644 --- a/src/main.c +++ b/src/main.c @@ -422,7 +422,7 @@ main (int argc, char **argv) else { /* check for no claims */ - if (sys->failed == 0) + if (sys->failed == STATES0) { /* mark exit code */ exitcode = 2; @@ -494,13 +494,13 @@ timersPrint (const System sys) * NoClaim no claims */ - if (sys->claims == 0) + if (sys->claims == STATES0) { fprintf (stderr, "NoClaim\t\t"); } else { - if (sys->failed > 0) + if (sys->failed != STATES0) fprintf (stderr, "L:%i\t\t", attackLength(sys->attack)); else fprintf (stderr, "None\t\t"); @@ -513,9 +513,7 @@ timersPrint (const System sys) if (seconds > 0) { - fprintf (stderr, "%.3e\t", - (double) (sys->statesLow + - (sys->statesHigh * ULONG_MAX)) / seconds); + fprintf (stderr, "%.3e\t", statesDouble (sys->states) / seconds); } else { @@ -653,13 +651,22 @@ modelCheck (const System sys) { graphInit (sys); } - traverse (sys); // start model checking + + /* modelcheck the system */ + traverse (sys); + + /* clean up any states display */ + if (sys->switchS > 0) + { + fprintf (stderr, " \r"); + } + timersPrint (sys); if (sys->switchStatespace) { graphDone (sys); } - return (sys->failed); + return (sys->failed != STATES0); } diff --git a/src/modelchecker.c b/src/modelchecker.c index 9de19a7..2e9e5f9 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -171,33 +171,25 @@ executeStep (const System sys, const int run) } /* we will explore this state, so count it. */ - /* ulong was _not_ enough... */ - if (++sys->statesLow == ULONG_MAX) - { - sys->statesLow = 0; - sys->statesHigh++; - /* No test for overflow statesHigh. If stuff gets that fast, then - * I surely hope the max of ulong is set higher in the language def */ - } + sys->states = statesIncrease (sys->states); /* show progression */ if (sys->switchS > 0) { - if (sys->statesLow % (long int) sys->switchS == 0) + sys->interval = statesIncrease (sys->interval); + if (!statesSmallerThan (sys->interval, (unsigned long int) sys->switchS)) { + sys->interval = STATES0; fprintf (stderr, "States "); - if (sys->statesHigh == 0 && sys->statesLow < 1000000) - fprintf (stderr, "%u", sys->statesLow); - else - fprintf (stderr, "%8.3e", (double) sys->statesLow + (sys->statesHigh * ULONG_MAX)); + statesFormat (stderr, sys->states); fprintf (stderr, " \r"); } } /* store new node numbder */ - sys->traceNode[sys->step] = sys->statesLow; + sys->traceNode[sys->step] = sys->states; /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */ - if (sys->switchStatespace && sys->statesHigh == 0 && sys->statesLow < MAX_GRAPH_STATES) + if (sys->switchStatespace && statesSmallerThan (sys->states, MAX_GRAPH_STATES)) { /* display graph */ graphNode (sys); @@ -1443,7 +1435,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt) flag = 1; /* Count the violations */ - sys->failed++; + sys->failed = statesIncrease (sys->failed); /* mark the path in the state graph? */ if (sys->switchStatespace) @@ -1563,7 +1555,7 @@ executeTry (const System sys, int run) /* * update claim counters */ - sys->claims++; + sys->claims = statesIncrease (sys->claims); /* * distinguish claim types diff --git a/src/output.c b/src/output.c index 3764343..d7c2175 100644 --- a/src/output.c +++ b/src/output.c @@ -513,7 +513,9 @@ void graphInit (const System sys) printf ("\torientation=landscape;\n"); /* start with initial node 0 */ - printf ("\tn0 [shape=box,label=\"M0: "); + printf ("\tn"); + statesFormat (stdout, STATES0); + printf (" [shape=box,label=\"M0: "); tl = knowledgeSet (sys->know); termlistPrint (tl); termlistDelete (tl); @@ -529,18 +531,20 @@ void graphDone (const System sys) void graphNode (const System sys) { Termlist newtl; - unsigned long int thisNode, parentNode; + states_t thisNode, parentNode; int index; Roledef rd; /* determine node numbers */ index = sys->step - 1; parentNode = sys->traceNode[index]; - thisNode = sys->statesLow; + thisNode = sys->states; rd = sys->traceEvent[index]; /* add node */ - printf ("\tn%li [shape=", thisNode); + printf ("\tn"); + statesFormat (stdout, thisNode); + printf (" [shape="); newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]); if (newtl != NULL) @@ -559,9 +563,12 @@ void graphNode (const System sys) printf ("];\n"); /* add edge */ - printf ("\tn%li -> n%li ", parentNode, thisNode); + printf ("\tn"); + statesFormat (stdout, parentNode); + printf (" -> n"); + statesFormat (stdout, thisNode); /* add label */ - printf ("[label=\""); + printf (" [label=\""); if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[sys->traceRun[index]].agents)) { printf ("Skip claim in #%i\"", sys->traceRun[index]); @@ -588,7 +595,7 @@ void graphNode (const System sys) void graphNodePath (const System sys, const int length, const char* nodepar) { int i; - unsigned long int thisNode; + states_t thisNode; i = 0; while (i < length) @@ -597,7 +604,9 @@ void graphNodePath (const System sys, const int length, const char* nodepar) thisNode = sys->traceNode[i]; /* color node */ - printf ("\tn%li [%s];\n", thisNode, nodepar); + printf ("\tn"); + statesFormat (stdout, thisNode); + printf (" [%s];\n", nodepar); i++; } } @@ -605,7 +614,7 @@ void graphNodePath (const System sys, const int length, const char* nodepar) void graphEdgePath (const System sys, const int length, const char* edgepar) { int i; - unsigned long int thisNode, prevNode; + states_t thisNode, prevNode; i = 0; prevNode = sys->traceNode[i]; @@ -615,7 +624,11 @@ void graphEdgePath (const System sys, const int length, const char* edgepar) thisNode = sys->traceNode[i+1]; /* color edge */ - printf ("\tn%li -> n%li [%s];\n", prevNode, thisNode, edgepar); + printf ("\tn"); + statesFormat (stdout, prevNode); + printf (" -> "); + statesFormat (stdout, thisNode); + printf (" [%s];\n", edgepar); prevNode = thisNode; i++; } diff --git a/src/runs.c b/src/runs.c index f0b520d..a921727 100644 --- a/src/runs.c +++ b/src/runs.c @@ -113,11 +113,11 @@ systemReset (const System sys) Claimlist cl; /* some initial counters */ - sys->statesLow = 0; // number of explored states - sys->statesHigh = 0; // this is not as ridiculous as it might seem + sys->states = STATES0; + sys->interval = STATES0; + sys->claims = STATES0; + sys->failed = STATES0; sys->explore = 1; // do explore the space - sys->claims = 0; // number of claims encountered - sys->failed = 0; // number of failed claims cl = sys->claimlist; while (cl != NULL) { @@ -161,7 +161,7 @@ systemDone (const System sys) memFree (sys->traceEvent, s * sizeof (Roledef)); memFree (sys->traceRun, s * sizeof (int)); memFree (sys->traceKnow, s * sizeof (Knowledge)); - memFree (sys->traceNode, s * sizeof (unsigned long int)); + memFree (sys->traceNode, s * sizeof (states_t)); /* clear roledefs */ for (run = 0; run < sys->maxruns; run++) @@ -174,38 +174,18 @@ systemDone (const System sys) systemDestroy (sys); } -//! Approximate the number of states traversed using a double type. -double -statesApproximation (const System sys) -{ - if (sys->statesHigh == 0) - return (double) sys->statesLow; - else - return (double) (sys->statesLow + (sys->statesHigh * ULONG_MAX)); -} - //! Print a short version of the number of states. void statesPrintShort (const System sys) { - fprintf (stderr,"%.3e", statesApproximation (sys)); + fprintf (stderr,"%.3e", statesDouble (sys->states)); } //! Print the number of states. void statesPrint (const System sys) { - if (sys->statesHigh == 0) - { - printf ("%g", (double) sys->statesLow); - } - else - { - double dstates; - - dstates = sys->statesLow + (sys->statesHigh * ULONG_MAX); - printf ("%.3e (...)", dstates); - } + statesFormat (stdout, sys->states); printf (" states traversed.\n"); if (globalLatex) printf("\n"); @@ -777,7 +757,7 @@ systemStart (const System sys) sys->traceEvent = memAlloc (s * sizeof (Roledef)); sys->traceRun = memAlloc (s * sizeof (int)); sys->traceKnow = memAlloc (s * sizeof (Knowledge)); - sys->traceNode = memAlloc (s * sizeof (unsigned long int)); + sys->traceNode = memAlloc (s * sizeof (states_t)); /* clear, for niceties */ for (i = 0; i < s; i++) @@ -785,7 +765,7 @@ systemStart (const System sys) sys->traceEvent[i] = NULL; sys->traceRun[i] = 0; sys->traceKnow[i] = NULL; - sys->traceNode[i] = 0; + sys->traceNode[i] = STATES0; } } diff --git a/src/runs.h b/src/runs.h index 9c18c0e..2d7193a 100644 --- a/src/runs.h +++ b/src/runs.h @@ -6,6 +6,7 @@ #include "termlists.h" #include "knowledge.h" #include "constraints.h" +#include "states.h" #define READ 1 #define SEND 2 @@ -228,10 +229,10 @@ struct system int explore; //!< Boolean: explore states after actions or not. /* counters */ - unsigned long int statesLow; //!< State number (low) - unsigned long int statesHigh; //!< State number (high) - unsigned long int claims; //!< Number of claims encountered. - unsigned long int failed; //!< Number of claims failed. + states_t states; + 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. /* matching */ int match; //!< Matching type. @@ -252,7 +253,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: Maxruns * maxRoledef + states_t *traceNode; //!< Trace node traversal: Maxruns * maxRoledef /* POR reduction assistance */ int PORphase; //!< -1: init (all sends), 0...: recurse reads diff --git a/src/states.c b/src/states.c new file mode 100644 index 0000000..75900ac --- /dev/null +++ b/src/states.c @@ -0,0 +1,40 @@ +#include "states.h" + +/* States counter operations + * + * Note that these are also used for encountered claims and such. + */ + +__inline__ states_t +statesIncrease (const states_t states) +{ + return states+1; +} + +__inline__ double +statesDouble (const states_t states) +{ + return (double) states; +} + +__inline__ int +statesSmallerThan (const states_t states, unsigned long int reflint) +{ + if (states < (states_t) reflint) + return 1; + else + return 0; +} + +//! Sensible output for number of states/claims +/** + * Acts like a modified form of %g + */ +__inline__ void +statesFormat (FILE* out, const states_t states) +{ + if (states < 1000000) + fprintf (out, "%lu", states); + else + fprintf (out, "%.3e", statesDouble (states)); +} diff --git a/src/states.h b/src/states.h new file mode 100644 index 0000000..2b33a26 --- /dev/null +++ b/src/states.h @@ -0,0 +1,20 @@ +#ifndef STATES +#define STATES +/** + * Header file for the states counter datatype. + * + * Previously, the states number was just a unsigned int, but that + * turned out to be insufficient. + */ + +#include + +typedef unsigned long int states_t; +#define STATES0 0 + +__inline__ states_t statesIncrease (const states_t states); +__inline__ double statesDouble (const states_t states); +__inline__ int statesSmallerThan (const states_t states, unsigned long int reflint); +__inline__ void statesFormat (FILE* out, const states_t states); + +#endif