execution: add const
[model-checker.git] / scanalysis.h
1 #ifndef SCANALYSIS_H
2 #define SCANALYSIS_H
3 #include "traceanalysis.h"
4 #include "hashtable.h"
5
6 class SCAnalysis : public TraceAnalysis {
7  public:
8         SCAnalysis(const ModelExecution *execution);
9         ~SCAnalysis();
10         virtual void analyze(action_list_t *);
11
12         SNAPSHOTALLOC
13  private:
14         void print_list(action_list_t *list);
15         void buildVectors(action_list_t *);
16         bool updateConstraints(ModelAction *act);
17         void computeCV(action_list_t *);
18         action_list_t * generateSC(action_list_t *);
19         bool processRead(ModelAction *read, ClockVector *cv);
20         ModelAction * getNextAction();
21         bool merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2);
22
23         int maxthreads;
24         HashTable<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
25         HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > cycleset;
26         SnapVector<action_list_t> threadlists;
27         const ModelExecution *execution;
28 };
29 #endif