X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.h;h=047793045e63c954b03b775fd433738aaf8d08d7;hb=473bdc841f3b03b722911a5fa0b4f21ba3a217ed;hp=0cd2d67e704d942c93fdf93404c8d63010e490ed;hpb=49e01b46a51804ca1aef3e4c260d832b38d40bdc;p=model-checker.git diff --git a/scanalysis.h b/scanalysis.h index 0cd2d67..0477930 100644 --- a/scanalysis.h +++ b/scanalysis.h @@ -18,11 +18,16 @@ class SCAnalysis : public TraceAnalysis { action_list_t * generateSC(action_list_t *); bool processRead(ModelAction *read, ClockVector *cv); ModelAction * getNextAction(); - bool merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2); + bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2); + void check_rf(action_list_t *list); + + int maxthreads; - HashTable *cvmap; - HashTable *cycleset; - SnapVector *threadlists; + HashTable cvmap; + bool cyclic; + HashTable badrfset; + HashTable lastwrmap; + SnapVector threadlists; const ModelExecution *execution; }; #endif