README: more formatting, correct statement about bench.sh
[model-checker.git] / scanalysis.h
1 #ifndef SCANALYSIS_H
2 #define SCANALYSIS_H
3 #include "traceanalysis.h"
4 #include "hashtable.h"
5
6 struct sc_statistics {
7         unsigned long long elapsedtime;
8         unsigned int sccount;
9         unsigned int nonsccount;
10 };
11
12 class SCAnalysis : public TraceAnalysis {
13  public:
14         SCAnalysis();
15         ~SCAnalysis();
16         virtual void setExecution(ModelExecution * execution);
17         virtual void analyze(action_list_t *);
18         virtual const char * name();
19         virtual bool option(char *);
20         virtual void finish();
21
22
23         SNAPSHOTALLOC
24  private:
25         void update_stats();
26         void print_list(action_list_t *list);
27         int buildVectors(action_list_t *);
28         bool updateConstraints(ModelAction *act);
29         void computeCV(action_list_t *);
30         action_list_t * generateSC(action_list_t *);
31         bool processRead(ModelAction *read, ClockVector *cv);
32         int getNextActions(ModelAction **array);
33         bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2);
34         void check_rf(action_list_t *list);
35         void reset(action_list_t *list);
36         ModelAction* pruneArray(ModelAction**, int);
37
38         int maxthreads;
39         HashTable<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
40         bool cyclic;
41         HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset;
42         HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
43         SnapVector<action_list_t> threadlists;
44         ModelExecution *execution;
45         bool print_always;
46         bool print_buggy;
47         bool print_nonsc;
48         bool time;
49         struct sc_statistics *stats;
50 };
51 #endif