3 * @brief Provides structures for queueing ModelChecker actions to be taken
6 #ifndef __WORKQUEUE_H__
7 #define __WORKQUEUE_H__
10 #include "stl-model.h"
15 WORK_NONE = 0, /**< No work to be done */
16 WORK_CHECK_CURR_ACTION, /**< Check the current action; used for the
17 first action of the work loop */
18 WORK_CHECK_RELEASE_SEQ, /**< Check if any pending release sequences
20 WORK_CHECK_MO_EDGES, /**< Check if new mo_graph edges can be added */
25 class WorkQueueEntry {
27 /** @brief Type of work queue entry */
31 * @brief The ModelAction to work on
32 * @see MOEdgeWorkEntry
38 * @brief Work: perform initial promise, mo_graph checks on the current action
40 * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
41 * that is currently being explored. The current ModelAction (@a action) is the
42 * only relevant parameter to this entry.
44 class CheckCurrWorkEntry : public WorkQueueEntry {
47 * @brief Constructor for a "check current action" work entry
48 * @param curr The current action
50 CheckCurrWorkEntry(ModelAction *curr) {
51 type = WORK_CHECK_CURR_ACTION;
57 * @brief Work: check a ModelAction for new mo_graph edges
59 * This WorkQueueEntry checks for new mo_graph edges for a particular
60 * ModelAction (e.g., that was just generated or that updated its
61 * synchronization). The ModelAction @a action is the only relevant parameter
64 class MOEdgeWorkEntry : public WorkQueueEntry {
67 * @brief Constructor for a mo_edge work entry
68 * @param updated The ModelAction which was updated, triggering this work
70 MOEdgeWorkEntry(ModelAction *updated) {
71 type = WORK_CHECK_MO_EDGES;
76 /** @brief typedef for the work queue type */
77 typedef ModelList<WorkQueueEntry> work_queue_t;
79 #endif /* __WORKQUEUE_H__ */