X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.h;h=988c8f75c13ad58f0fdfc44ebd3e936bb59601e1;hb=130a35155171503883aaf18e57f8957ce63d06e8;hp=ffa933ad5e2b872769199ca81fbcec9d7afd8333;hpb=b090a4abc4915a9aa2a29787f76a6add79f838e2;p=model-checker.git diff --git a/scanalysis.h b/scanalysis.h index ffa933a..988c8f7 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -3,17 +3,26 @@ #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(); ~SCAnalysis(); virtual void setExecution(ModelExecution * execution); virtual void analyze(action_list_t *); - virtual char * name(); + 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); @@ -33,5 +42,10 @@ class SCAnalysis : public TraceAnalysis { HashTable lastwrmap; SnapVector threadlists; ModelExecution *execution; + bool print_always; + bool print_buggy; + bool print_nonsc; + bool time; + struct sc_statistics *stats; }; #endif