3 * @brief Provides structures for queueing ModelChecker actions to be taken
6 #ifndef __WORKQUEUE_H__
7 #define __WORKQUEUE_H__
11 #include "stl-model.h"
16 WORK_NONE = 0, /**< No work to be done */
17 WORK_CHECK_CURR_ACTION, /**< Check the current action; used for the
18 first action of the work loop */
19 WORK_CHECK_RELEASE_SEQ, /**< Check if any pending release sequences
21 WORK_CHECK_MO_EDGES, /**< Check if new mo_graph edges can be added */
26 class WorkQueueEntry {
28 /** @brief Type of work queue entry */
32 * @brief Object affected
33 * @see CheckRelSeqWorkEntry
38 * @brief The ModelAction to work on
39 * @see MOEdgeWorkEntry
45 * @brief Work: perform initial promise, mo_graph checks on the current action
47 * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
48 * that is currently being explored. The current ModelAction (@a action) is the
49 * only relevant parameter to this entry.
51 class CheckCurrWorkEntry : public WorkQueueEntry {
54 * @brief Constructor for a "check current action" work entry
55 * @param curr The current action
57 CheckCurrWorkEntry(ModelAction *curr) {
58 type = WORK_CHECK_CURR_ACTION;
65 * @brief Work: check an object location for resolved release sequences
67 * This WorkQueueEntry checks synchronization and the mo_graph for resolution
68 * of any release sequences. The object @a location is the only relevant
69 * parameter to this entry.
71 class CheckRelSeqWorkEntry : public WorkQueueEntry {
74 * @brief Constructor for a "check release sequences" work entry
75 * @param l The location which must be checked for release sequences
77 CheckRelSeqWorkEntry(void *l) {
78 type = WORK_CHECK_RELEASE_SEQ;
85 * @brief Work: check a ModelAction for new mo_graph edges
87 * This WorkQueueEntry checks for new mo_graph edges for a particular
88 * ModelAction (e.g., that was just generated or that updated its
89 * synchronization). The ModelAction @a action is the only relevant parameter
92 class MOEdgeWorkEntry : public WorkQueueEntry {
95 * @brief Constructor for a mo_edge work entry
96 * @param updated The ModelAction which was updated, triggering this work
98 MOEdgeWorkEntry(ModelAction *updated) {
99 type = WORK_CHECK_MO_EDGES;
105 /** @brief typedef for the work queue type */
106 typedef ModelList<WorkQueueEntry> work_queue_t;
108 #endif /* __WORKQUEUE_H__ */