#define VALUE_NONE -1
+/** @brief Represents an action type, identifying one of several types of
+ * ModelAction */
typedef enum action_type {
- THREAD_CREATE,
- THREAD_YIELD,
- THREAD_JOIN,
- ATOMIC_READ,
- ATOMIC_WRITE,
- ATOMIC_RMW,
- ATOMIC_INIT
+ THREAD_CREATE, /**< A thread creation action */
+ THREAD_YIELD, /**< A thread yield action */
+ THREAD_JOIN, /**< A thread join action */
+ ATOMIC_READ, /**< An atomic read action */
+ ATOMIC_WRITE, /**< An atomic write action */
+ ATOMIC_RMW, /**< An atomic read-modify-write action */
+ ATOMIC_INIT /**< Initialization of an atomic object (e.g.,
+ * atomic_init()) */
} action_type_t;
/* Forward declaration */
#define THREAD_ID_T_NONE -1
+/** @brief Represents the state of a user Thread */
typedef enum thread_state {
+ /** Thread was just created and hasn't run yet */
THREAD_CREATED,
+ /** Thread is running */
THREAD_RUNNING,
+ /**
+ * Thread has yielded to the model-checker but is ready to run. Used
+ * during an action that caused a context switch to the model-checking
+ * context.
+ */
THREAD_READY,
+ /** Thread has completed its execution */
THREAD_COMPLETED
} thread_state;