model: move snapshot members out of header

This struct is only used within model.cc

diff --git a/model.cc b/model.cc
index 94620ea9d0400fcee239973705361210542040f5..bfdae30d407dc0b8a41b7815427b3380c7b65ffc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -18,6 +18,17 @@
 
 ModelChecker *model;
 
+/**
+ * Structure for holding small ModelChecker members that should be snapshotted
+ */
+struct model_snapshot_members {
+       ModelAction *current_action;
+       unsigned int next_thread_id;
+       modelclock_t used_sequence_numbers;
+       Thread *nextThread;
+       ModelAction *next_backtrack;
+};
+
 /** @brief Constructor */
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
@@ -863,6 +874,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
        return true;
 }
 
+/**
+ * Stores the ModelAction for the current thread action.  Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
+void ModelChecker::set_current_action(ModelAction *act) {
+       priv->current_action = act;
+}
+
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it

diff --git a/model.h b/model.h
index 6d702b0d94604d281a0cdea8331eb669e15a3704..7065960b882bc8fc71eb3da2f8565fb1adc9eb9d 100644 (file)
--- a/model.h
+++ b/model.h
@@ -23,6 +23,7 @@ class CycleGraph;
 class Promise;
 class Scheduler;
 class Thread;
+struct model_snapshot_members;
 
 /** @brief Shorthand for a list of release sequence heads */
 typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
@@ -53,17 +54,6 @@ struct PendingFutureValue {
        ModelAction * act;
 };
 
-/**
- * Structure for holding small ModelChecker members that should be snapshotted
- */
-struct model_snapshot_members {
-       ModelAction *current_action;
-       unsigned int next_thread_id;
-       modelclock_t used_sequence_numbers;
-       Thread *nextThread;
-       ModelAction *next_backtrack;
-};
-
 /** @brief Records information regarding a single pending release sequence */
 struct release_seq {
        /** @brief The acquire operation */
@@ -142,13 +132,7 @@ private:
        void wake_up_sleeping_actions(ModelAction * curr);
        modelclock_t get_next_seq_num();
 
-       /**
-        * Stores the ModelAction for the current thread action.  Call this
-        * immediately before switching from user- to system-context to pass
-        * data between them.
-        * @param act The ModelAction created by the user-thread action
-        */
-       void set_current_action(ModelAction *act) { priv->current_action = act; }
+       void set_current_action(ModelAction *act);
        Thread * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);