X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.h;h=988c8f75c13ad58f0fdfc44ebd3e936bb59601e1;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hp=3ad69e57023b074993083c4268c74aac0ec341c9;hpb=a4d3f2ae3f3a9e2a30cc36c92cee9f83bb09e9b1;p=model-checker.git diff --git a/scanalysis.h b/scanalysis.h index 3ad69e5..988c8f7 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -3,6 +3,12 @@ #include "traceanalysis.h" #include "hashtable.h" +struct sc_statistics { + unsigned long long elapsedtime; + unsigned int sccount; + unsigned int nonsccount; +}; + class SCAnalysis : public TraceAnalysis { public: SCAnalysis(); @@ -11,9 +17,12 @@ class SCAnalysis : public TraceAnalysis { virtual void analyze(action_list_t *); virtual const char * name(); virtual bool option(char *); + virtual void finish(); + SNAPSHOTALLOC private: + void update_stats(); void print_list(action_list_t *list); int buildVectors(action_list_t *); bool updateConstraints(ModelAction *act); @@ -35,5 +44,8 @@ class SCAnalysis : public TraceAnalysis { ModelExecution *execution; bool print_always; bool print_buggy; + bool print_nonsc; + bool time; + struct sc_statistics *stats; }; #endif