From 15fcbf80909b5b70e04db71e324bbe441d3036b8 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 30 Jul 2004 12:04:38 +0000 Subject: [PATCH] - Added scen_st to the output, which lists the number of states in the specific scenario. --- src/main.c | 13 +++++++++++-- src/modelchecker.c | 15 ++++++++++++--- src/output.c | 14 +++++++------- src/states.c | 6 +++--- src/states.h | 2 +- src/system.c | 14 ++++++-------- src/system.h | 3 ++- 7 files changed, 42 insertions(+), 25 deletions(-) diff --git a/src/main.c b/src/main.c index e84de81..a2aff51 100644 --- a/src/main.c +++ b/src/main.c @@ -593,6 +593,15 @@ timersPrint (const System sys) statesPrintShort (sys); eprintf ("\n"); + /* scenario info */ + + if (sys->switchScenario > 0) + { + eprintf ("scen_st\t"); + statesFormat (sys->statesScenario); + eprintf ("\n"); + } + /* flag * * L n Attack of length @@ -651,13 +660,13 @@ timersPrint (const System sys) eprintf (":"); termPrint (cl_scan->label); eprintf ("\t"); - statesFormat (stderr, cl_scan->count); + statesFormat (cl_scan->count); if (cl_scan->count > 0) { eprintf ("\t"); if (cl_scan->failed > 0) { - statesFormat (stderr, cl_scan->failed); + statesFormat (cl_scan->failed); eprintf (" failed"); } } diff --git a/src/modelchecker.c b/src/modelchecker.c index 0d17101..025213a 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -202,16 +202,25 @@ executeStep (const System sys, const int run) /* we will explore this state, so count it. */ sys->states = statesIncrease (sys->states); + /* what about scenario exploration? */ + if (sys->switchScenario && sys->step+1 > sys->switchScenarioSize) + { + /* count states within scenario */ + sys->statesScenario = statesIncrease (sys->statesScenario); + } + /* show progression */ if (sys->switchS > 0) { sys->interval = statesIncrease (sys->interval); if (!statesSmallerThan (sys->interval, (unsigned long int) sys->switchS)) { + globalError++; sys->interval = STATES0; - fprintf (stderr, "States "); - statesFormat (stderr, sys->states); - fprintf (stderr, " \r"); + eprintf ("States "); + statesFormat (sys->states); + eprintf (" \r"); + globalError--; } } diff --git a/src/output.c b/src/output.c index cbc8743..9dc95bb 100644 --- a/src/output.c +++ b/src/output.c @@ -529,7 +529,7 @@ void graphInit (const System sys) /* start with initial node 0 */ printf ("\tn"); - statesFormat (stdout, STATES0); + statesFormat (STATES0); printf (" [shape=box,height=0.2,label=\"M0: "); tl = knowledgeSet (sys->know); termlistPrint (tl); @@ -560,7 +560,7 @@ void graphNode (const System sys) /* add node */ printf ("\tn"); - statesFormat (stdout, thisNode); + statesFormat (thisNode); printf (" ["); newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]); @@ -595,9 +595,9 @@ void graphNode (const System sys) /* add edge */ printf ("\tn"); - statesFormat (stdout, parentNode); + statesFormat (parentNode); printf (" -> n"); - statesFormat (stdout, thisNode); + statesFormat (thisNode); /* add label */ printf (" [label=\""); @@ -641,7 +641,7 @@ void graphNodePath (const System sys, const int length, const char* nodepar) /* color node */ printf ("\tn"); - statesFormat (stdout, thisNode); + statesFormat (thisNode); printf (" [%s];\n", nodepar); i++; } @@ -661,9 +661,9 @@ void graphEdgePath (const System sys, const int length, const char* edgepar) /* color edge */ printf ("\tn"); - statesFormat (stdout, prevNode); + statesFormat (prevNode); printf (" -> n"); - statesFormat (stdout, thisNode); + statesFormat (thisNode); printf (" [%s];\n", edgepar); prevNode = thisNode; i++; diff --git a/src/states.c b/src/states.c index 75900ac..a5400d9 100644 --- a/src/states.c +++ b/src/states.c @@ -31,10 +31,10 @@ statesSmallerThan (const states_t states, unsigned long int reflint) * Acts like a modified form of %g */ __inline__ void -statesFormat (FILE* out, const states_t states) +statesFormat (const states_t states) { if (states < 1000000) - fprintf (out, "%lu", states); + eprintf ("%lu", states); else - fprintf (out, "%.3e", statesDouble (states)); + eprintf ("%.3e", statesDouble (states)); } diff --git a/src/states.h b/src/states.h index 2b33a26..1e79cd1 100644 --- a/src/states.h +++ b/src/states.h @@ -15,6 +15,6 @@ typedef unsigned long int states_t; __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); +__inline__ void statesFormat (const states_t states); #endif diff --git a/src/system.c b/src/system.c index 353b026..c87e212 100644 --- a/src/system.c +++ b/src/system.c @@ -111,7 +111,8 @@ systemReset (const System sys) /* some initial counters */ 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->statesScenario = STATES0; + sys->interval = sys->states; //!< To keep in line with the states sys->claims = STATES0; sys->failed = STATES0; sys->countScenario = 0; @@ -205,20 +206,17 @@ systemDone (const System sys) void statesPrintShort (const System sys) { - if (globalError == 0) - statesFormat (stdout, sys->states); - else - statesFormat (stderr, sys->states); + statesFormat (sys->states); } //! Print the number of states. void statesPrint (const System sys) { - statesFormat (stdout, sys->states); - printf (" states traversed.\n"); + statesFormat (sys->states); + eprintf (" states traversed.\n"); if (globalLatex) - printf("\n"); + eprintf("\n"); } //! Destroy a system memory block and system::runs diff --git a/src/system.h b/src/system.h index cc9bccc..cd39c24 100644 --- a/src/system.h +++ b/src/system.h @@ -143,7 +143,8 @@ struct system int explore; //!< Boolean: explore states after actions or not. /* counters */ - states_t states; + states_t states; //!< States traversed + states_t statesScenario; //!< States traversed that are within the scenario, not the prefix 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.