-/**
- * Structure for holding small ModelChecker members that should be snapshotted
- */
-struct model_snapshot_members {
- ModelAction *current_action;
- int next_thread_id;
- modelclock_t used_sequence_numbers;
- Thread *nextThread;
- ModelAction *next_backtrack;
-
- /** @see ModelChecker::lazy_sync_size */
- unsigned int lazy_sync_size;
+/** @brief Model checker execution stats */
+struct execution_stats {
+ int num_total; /**< @brief Total number of executions */
+ int num_infeasible; /**< @brief Number of infeasible executions */
+ int num_buggy_executions; /** @brief Number of buggy executions */
+ int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+};
+
+struct PendingFutureValue {
+ ModelAction *writer;
+ ModelAction *act;
+};
+
+/** @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;