+class Scheduler;
+class Thread;
+
+/** @brief Shorthand for a list of release sequence heads */
+typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
+
+/**
+ * Model checker parameter structure. Holds run-time configuration options for
+ * the model checker.
+ */
+struct model_params {
+ int maxreads;
+ int maxfuturedelay;
+ unsigned int fairwindow;
+ unsigned int enabledcount;
+ unsigned int bound;
+};
+
+struct PendingFutureValue {
+ ModelAction *writer;
+ 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 */
+ ModelAction *acquire;
+ /** @brief The head of the RMW chain from which 'acquire' reads; may be
+ * equal to 'release' */
+ const ModelAction *rf;
+ /** @brief The head of the potential longest release sequence chain */
+ const ModelAction *release;
+ /** @brief The write(s) that may break the release sequence */
+ std::vector<const ModelAction *> writes;
+};