execution: embed obj_map directly in class

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index 7d84f60112c5ef26b8c54cf9e139f016fc05df7b..89d089d1051aafbcd95ae6cd4961c23f764be739 100644 (file)
--- a/model.h
+++ b/model.h
@@ -52,6 +52,8 @@ public:
 
        const ModelExecution * get_execution() const { return execution; }
 
+       int get_execution_number() const { return execution_number; }
+
        Thread * get_thread(thread_id_t tid) const;
        Thread * get_thread(const ModelAction *act) const;
 
@@ -82,6 +84,8 @@ private:
        NodeStack * const node_stack;
        ModelExecution *execution;
 
+       int execution_number;
+
        void execute_sleep_set();
 
        bool next_execution();